Difference between revisions of "PlayGo Feature List"

From WeizmannWiki
Jump to: navigation, search
(→‎Natural language play-in)
 
(11 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 
== Play-out strategies  ==
 
== Play-out strategies  ==
  
−
LSC specifications or `programs' may be underspecified, since the language allows various kinds of non-determinism. Thus, a special mechanism is needed in order to execute LSC programs. This execution mechanism is generically termed [[Language & Concepts#Play-Out|''play-out'']]. The core of the [[Language & Concepts#Play-Out|play-out]] process is a strategy mechanism that is responsible for choosing the next method to execute. The choice is based on the specification and the current state of the system.  
+
LSC specifications or `programs' may be underspecified, since the language allows various kinds of non-determinism. Thus, a special mechanism is needed in order to execute LSC programs. This execution mechanism is generically termed [[Language & Concepts#Play-Out|''play-out'']]. The core of the [[Language & Concepts#Play-Out|play-out]] process is a strategy mechanism that is responsible for choosing the next method to execute. The choice is based on the specification and the current state of the system.
  
−
Different kinds of play-out mechanisms may be defined. Each may be viewed as a different operational semantics for LSC.  
+
Different kinds of play-out mechanisms may be defined. Each may be viewed as a different operational semantics for LSC.
  
−
PlayGo uses a [http://en.wikipedia.org/wiki/Strategy_pattern strategy pattern] to allow the definition, implementation, and use of new, user-defined play-out strategies. It also includes several built-in, pre-defined play-out strategies, which we now describe.  
+
PlayGo uses a [http://en.wikipedia.org/wiki/Strategy_pattern strategy pattern] to allow the definition, implementation, and use of new, user-defined play-out strategies. It also includes several built-in, pre-defined play-out strategies, which we now describe.
  
 
=== Naïve play-out  ===
 
=== Naïve play-out  ===
  
−
The ''naïve play-out'' strategy is the simplest one. It arbitrarily chooses a non-violating method from among the current set of methods that are enabled for execution in at least one chart, but which are not violating in any chart.  
+
The ''naïve play-out'' strategy is the simplest one. It arbitrarily chooses a non-violating method from among the current set of methods that are enabled for execution in at least one chart, but which are not violating in any chart.
  
 
=== Random play-out  ===
 
=== Random play-out  ===
  
−
The ''random play-out'' strategy is similar to the naïve play-out strategy. However, it chooses the next method to execute randomly, using a 'seed' number. The user can either choose a constant seed, in which case the same method will be selected in repeated runs, or ask PlayGo to use random seed, thus causing different, random method selection in each run.  
+
The ''random play-out'' strategy is similar to the naïve play-out strategy. However, it chooses the next method to execute randomly, using a 'seed' number. The user can either choose a constant seed, in which case the same method will be selected in repeated runs, or ask PlayGo to use random seed, thus causing different, random method selection in each run.
  
 
=== Interactive play-out  ===
 
=== Interactive play-out  ===
  
−
The ''interactive play-out'' strategy allows the user to choose the next method to execute. The user is presented with a dialog that lists all the currently enabled non-violating methods and is expected to select one of them. The selected method is returned to the play-out mechanism for execution.  
+
The ''interactive play-out'' strategy allows the user to choose the next method to execute. The user is presented with a dialog that lists all the currently enabled non-violating methods and is expected to select one of them. The selected method is returned to the play-out mechanism for execution.
  
 
=== Smart play-out  ===
 
=== Smart play-out  ===
  
−
''Smart play-out'' is a smarter, safer way of choosing the next method to execute. It considers not only the current set of enabled non-violating methods, but also looks ahead and picks up a finite sequence of methods that will lead to a successful (non-violating) [[LSC Reference#Step_and_Superstep|superstep]], if any such sequence exists.  
+
''Smart play-out'' is a smarter, safer way of choosing the next method to execute. It considers not only the current set of enabled non-violating methods, but also looks ahead and picks up a finite sequence of methods that will lead to a successful (non-violating) [[LSC Reference#Step_and_Superstep|superstep]], if any such sequence exists.
  
−
To compute a safe superstep, PlayGo uses model-checking techniques. This is done by challenging the model checker to prove that there is no superstep that can take place without violating the LSC specification. If no such superstep exists, there is no way to proceed. But if there is such a superstep, the model checker provides it as a counter-example. PlayGo uses the counter-example to guide the execution.  
+
To compute a safe superstep, PlayGo uses model-checking techniques. This is done by challenging the model checker to prove that there is no superstep that can take place without violating the LSC specification. If no such superstep exists, there is no way to proceed. But if there is such a superstep, the model checker provides it as a counter-example. PlayGo uses the counter-example to guide the execution.
  
−
Smart play-out is implemented in PlayGo using [http://jtlv.ysaar.net/ JTLV].  
+
Smart play-out is implemented in PlayGo using [http://jtlv.ysaar.net/ JTLV].
  
−
Smart play-out was first described in <ref> D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2002), November 2002, pp. 378-398.</ref>.  
+
Smart play-out was first described in <ref> D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2002), November 2002, pp. 378-398.</ref>.
  
 
=== Synthesis  ===
 
=== Synthesis  ===
  
−
Looking one superstep forward, as is done in the smart play-out strategy, may not be enough, because a safe superstep does not guarantee future execution free of dead locks. An adverse environment may be able to cause the system to fail in satisfying the requirements. Thus, PlayGo offers another strategy, based on the technology of ''controller synthesis''. Controller synthesis takes the LSC specification and attempts to compute a controller whose behavior is guaranteed to satisfy the requirements set by the specification. The computed controller is then used to guide the play-out mechanism. For the case where the LSC specification is unrealizable and a controller cannot be synthesized, PlayGo offers a debugging mode termed [[PlayGo Feature List#Counter_play-out|counter play-out]].  
+
Looking one superstep forward, as is done in the smart play-out strategy, may not be enough, because a safe superstep does not guarantee future execution free of dead locks. An adverse environment may be able to cause the system to fail in satisfying the requirements. Thus, PlayGo offers another strategy, based on the technology of ''controller synthesis''. Controller synthesis takes the LSC specification and attempts to compute a controller whose behavior is guaranteed to satisfy the requirements set by the specification. The computed controller is then used to guide the play-out mechanism. For the case where the LSC specification is unrealizable and a controller cannot be synthesized, PlayGo offers a debugging mode termed [[PlayGo Feature List#Counter_play-out|counter play-out]].
  
−
Synthesis for LSC was first described in <ref>D. Harel and H. Kugler,fckLR“Synthesizing state-based object systems from LSC specifications,”fckLRInt. J. Found. Comput. Sci.,vol. 13, no. 1, pp. 5–51, 2002</ref>.  
+
Synthesis for LSC was first described in <ref>D. Harel and H. Kugler, “Synthesizing state-based object systems from LSC specifications,” Int. J. Found. Comput. Sci.,vol. 13, no. 1, pp. 5–51, 2002</ref>.
  
−
The variant of LSC synthesis used in PlayGo is described in <ref>S.fckLRMaoz and Y. Sa’ar, “Assume-Guarantee Scenarios: Semantics andfckLRSynthesis,” Proc. 15th Int. Conf. on Model Driven Engineering Languages and Systems (MoDELS), LNCS 7590, pp. 335-351, Springer, 2012</ref>. This variant is stronger than previous variants of LSC synthesis, as it supports environment assumptions. It is implemented using [http://jtlv.ysaar.net/ JTLV], following the symbolic fixpoint algorithm described in <ref>N.fckLRPiterman, A. Pnueli, and Y. Sa’ar, “Synthesis of Reactive(1) Designs,”fckLRin VMCAI, ser. LNCS, vol. 3855. Springer,2006, pp. 364–380.</ref>.  
+
The variant of LSC synthesis used in PlayGo is described in <ref>S. Maoz and Y. Sa’ar, “Assume-Guarantee Scenarios: Semantics and Synthesis,” Proc. 15th Int. Conf. on Model Driven Engineering Languages and Systems (MoDELS), LNCS 7590, pp. 335-351, Springer, 2012</ref>. This variant is stronger than previous variants of LSC synthesis, as it supports environment assumptions. It is implemented using [http://jtlv.ysaar.net/ JTLV], following the symbolic fixpoint algorithm described in <ref>N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of Reactive(1) Designs,” in VMCAI, ser. LNCS, vol. 3855. Springer,2006, pp. 364–380.</ref>.
 +
 
 +
=== S2A-BPJ play-out ===
 +
 
 +
The ''S2A-BPJ play-out'' strategy considers not only the LSC specification but also scenarios written in BPJ. It does that by enclosing the BPJ decision mechanism
 +
inside an S2A strategy and delegating the decision from S2A
 +
to BPJ. This way, BPJ b-threads may become aware of S2A
 +
events. In the other direction, S2A is aware of the BPJ events
 +
by having a lifeline representing the BPJ environment
 +
and monitoring relevant events that are carried out by BPJ.
  
 
== Counter play-out  ==
 
== Counter play-out  ==
  
−
An LSC specification may be unrealizable. That is, if an adverse environment can force any possible execution to violate the guarantees that the system needs to satisfy, a controller cannot be synthesized.  
+
An LSC specification may be unrealizable. That is, if an adverse environment can force any possible execution to violate the guarantees that the system needs to satisfy, a controller cannot be synthesized.
  
−
Counter play-out is an interactive debugging method for unrealizable LSC specifications. When such a specification is identified, PlayGo generates a controller that plays the role of the environment and lets the engineer play the role of the system. During execution, the former chooses environment moves such that the latter is forced to eventually fail in satisfying the system's requirements. This results in an interactive, guided execution, which can lead to the root causes of unrealizability. The generated controller constitutes a proof that the specification is conflicting and cannot be realized.  
+
Counter play-out is an interactive debugging method for unrealizable LSC specifications. When such a specification is identified, PlayGo generates a controller that plays the role of the environment and lets the engineer play the role of the system. During execution, the former chooses environment moves such that the latter is forced to eventually fail in satisfying the system's requirements. This results in an interactive, guided execution, which can lead to the root causes of unrealizability. The generated controller constitutes a proof that the specification is conflicting and cannot be realized.
  
−
Counter play-out is based on a counter strategy, which is computed in PlayGo by solving a Rabin game using a symbolic, fixpoint algorithm. Counter play-out is described in <ref>S. Maoz and Y. Sa’ar, “CounterfckLRPlay-Out: Executing Unrealizable Scenario-Based Specifications,”fckLRto appear in ICSE'13 (2013)</ref>.  
+
Counter play-out is based on a counter strategy, which is computed in PlayGo by solving a Rabin game using a symbolic, fixpoint algorithm. Counter play-out is described in <ref>S. Maoz and Y. Sa’ar, “Counter Play-Out: Executing Unrealizable Scenario-Based Specifications,” to appear in ICSE'13 (2013)</ref>.
  
 
== Semantic Zoom  ==
 
== Semantic Zoom  ==
  
−
Large LSCs are difficult to view and navigate. To address this, PlayGo offers a ''semantic zoom'' feature. It allows one to zoom-in and zoom-out of the chart, based on custom weights on the chart's elements (messages, conditions, etc.).  
+
Large LSCs are difficult to view and navigate. To address this, PlayGo offers a ''semantic zoom'' feature. It allows one to zoom-in and zoom-out of the chart, based on custom weights on the chart's elements (messages, conditions, etc.).
  
−
Zooming in and out reveals and hides chart elements. Hidden elements are replaced with a placeholder, to allows the user to understand the context of the remaining elements. Consecutive placeholders are merged into a single, darker-colored placeholder. Effectively, the user can view the most important elements that fit on the screen, while the placeholders hint at the missing information.  
+
Zooming in and out reveals and hides chart elements. Hidden elements are replaced with a placeholder, to allows the user to understand the context of the remaining elements. Consecutive placeholders are merged into a single, darker-colored placeholder. Effectively, the user can view the most important elements that fit on the screen, while the placeholders hint at the missing information.
  
−
In different contexts, different chart elements may be considered more important than others. Thus, the custom weights of the elements are calculated according to the task at hand (debugging, understanding inter-dependencies, etc.). The user can choose a strategy to use for calculating the weights.  
+
In different contexts, different chart elements may be considered more important than others. Thus, the custom weights of the elements are calculated according to the task at hand (debugging, understanding inter-dependencies, etc.). The user can choose a strategy to use for calculating the weights.
  
−
Semantic zoom in PlayGo is described in <ref>M. Gordon and D. Harel, "Semantic Navigation Strategies for Scenario-Based Programming", Proc. IEEE Symp. on Visual Languages and Human-Centric Computing (VL/HCC 2010), 2010, pp.219-226.</ref>.  
+
Semantic zoom in PlayGo is described in <ref>M. Gordon and D. Harel, "Semantic Navigation Strategies for Scenario-Based Programming", Proc. IEEE Symp. on Visual Languages and Human-Centric Computing (VL/HCC 2010), 2010, pp.219-226.</ref>.
  
−
[[Image:ATM.ZoomOut.png|500px]] [[Image:ATM.png]]  
+
[[Image:ATM.ZoomOut.png|500px]] [[Image:ATM.png]]
  
 
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 1: On the right, the full LSC. On the left, a zoomed-out view. Note the gray scale placeholders, which hide LSC elements. The darker it is, the more elements it hides.
 
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 1: On the right, the full LSC. On the left, a zoomed-out view. Note the gray scale placeholders, which hide LSC elements. The darker it is, the more elements it hides.
Line 61: Line 70:
  
 
  The green dotted ellipse marks the most recent placeholder that was added or changed during zoom-out.
 
  The green dotted ellipse marks the most recent placeholder that was added or changed during zoom-out.
−
  When zooming in, the last added element is marked with this green dotted ellipse.<span style="color: rgb(0, 128, 128);"> </span>  
+
  When zooming in, the last added element is marked with this green dotted ellipse.<span style="color: rgb(0, 128, 128);"> </span>
−
+
 
 +
 
 +
[http://www.youtube.com/watch?v=dDSszMjanXs Watch a Semantic Zoom demo]
  
−
[http://www.youtube.com/watch?v=dDSszMjanXs Watch a Semantic Zoom demo]
+
== Natural language play-in ==
  
−
== Natural language play-in ==
+
PlayGo supports a number of ways to define LSCs: manual editing, play-in, natural language play-in and show & tell.
  
−
PlayGo supports a number of ways to define LSCs: manual editing, play-in, natural language play-in and show &amp; tell.  
+
Natural language play-in allows the user to create LSCs through a natural language textual interface rather than by drawing the elements or interacting with the system.
  
−
Natural language play-in allows the user to create LSCs through a natural language textual interface rather than by drawing the elements or interacting with the system.
+
The allowed input language is a controlled and structured fragment of English tailored specifically to capture LSCs. This language is generated by a context free grammar. It makes it possible to write requirements, each one phrased as a single sentence which the system will parse and transform into an LSC. The resulting LSCs can then be executed.<br> Here are two examples of natural language requirements that can be dealt with by the system:
  
−
The language is controlled and structured English fragment accepted by a CFG parser especially developed for the semantics of LSCs. It allows writing requirements in separate sentences and parsing them into LSCs that can be later executed. Here are two examples of requirements:
+
#''when the user presses the d_button, if the display mode is time, the display mode changes to date, otherwise if the display mode is date, the display mode changes to time''.
 +
#''when the mobile_unit state changes to on, as long as the mobile_unit state is on, if two seconds have elapsed and the baby_unit does not connect to the mobile_unit, the connection_light color changes to red''.
  
−
#''when the user presses the d button, if the display mode is time, the display mode changes to date, otherwise if the display mode is date, the display mode changes to time''
+
The language is domain-general, and uses the wordnet dictionary <ref> Princeton University "About WordNet." WordNet. Princeton University. 2010. [http://wordnet.princeton.edu wordnet] </ref> to decide which part of speech tags can be used  (e.g., noun, verb, adjective, etc.) and what element in the model is assigned to each word. <br>
−
#''when the user presses the a button, if the display mode is time, the display mode changes to alarm, otherwise if the display mode is alarm, the display mode changes to chime, otherwise if the display mode is chime, the display mode changes to stopwatch, otherwise if the display mode is stopwatch, the display mode changes to time''
+
  
−
The language is domain-general, and uses the wordnet dictionary <ref> Princeton University "About WordNet." WordNet. Princeton University. 2010. [http://wordnet.princeton.edu wordnet] </ref> to decide which part of speech is to be used (e.g., noun, verb, adjective, etc.) and what element in the model matches each word. The user can disambiguate terms where necessary, and the selections are persistent for the model, assuming the writer refers to the same objects / actions using the same words.
+
Natural language requirements may be played in using one of the two following execution modes:
  
−
Natural language play-in is described in <ref> M. Gordon and D. Harel, "Generating Executable Scenarios from Natural Language", Proc. 10th Int. Conf. on Comput. Linguistics and Intelligent Text Processing (CICLing'09), Lecture Notes In Computer Science, vol. 5449. Springer-Verlag, Berlin, Heidelberg, 2009, pp. 456-467.</ref>.  
+
#Interactive natural language play-in - The text is parsed using a symbolic parser. When the system cannot assign a single role in the model to a term in the text, it prompts the user with the problem and offers possible fixes.  The user can then disambiguate these terms. We assume the user always refers to the same objects / actions using the same words. Based on the fix chosen by the user, the LSC is constructed.<br/>Interactive natural language play-in is described in <ref> M. Gordon and D. Harel, "Generating Executable Scenarios from Natural Language", Proc. 10th Int. Conf. on Comput. Linguistics and Intelligent Text Processing (CICLing'09), Lecture Notes In Computer Science, vol. 5449. Springer-Verlag, Berlin, Heidelberg, 2009, pp. 456-467.</ref>.
 +
#Statistical natural language play-in - The text is parsed using a statistical parser trained on a large set of pre-annotated example requirements. When the system cannot assign a single role in the model to a term in the text, it relies on the trained statistical model to select a role from among several previously attested alternatives. Based on the decisions made by the statistical model, the LSC is constructed.<br/>Automatic Natural language play-in is described in <ref> R. Tsarfaty, E. Pogrebezky, G. Weiss, Y. Natan, S. Szekely and D. Harel, "Semantic Parsing Using Content and Context: A Case Study from Requirements Elicitation", Proc. Int. Conf. on Empirical Methods in Natural Language Processing (EMNLP), to appear, 2014.</ref>
  
−
More about [http://www.weizmann.ac.il/mediawiki/playgo/index.php/How_to_Play-In#Natural_language_play-in How to Play-In with NL].  
+
More about [http://www.weizmann.ac.il/mediawiki/playgo/index.php/How_to_Play-In How to Play-In with NL].
  
 
== Show &amp; tell play-in  ==
 
== Show &amp; tell play-in  ==
  
−
Show &amp; Tell is a play-in feature that allows the user to create LSCs through a natural language textual interface combined with the classical play-in technique of interacting with the GUI of the system.  
+
Show &amp; Tell is a play-in feature that allows the user to create LSCs through a natural language textual interface combined with the classical play-in technique of interacting with the GUI of the system.
  
−
The 'TELL' part is based on natural language play-in; see above.  
+
The 'TELL' part is based on natural language play-in; see above.
  
−
The 'SHOW' part allows the user to point at or manipulate objects in the GUI or the [[Language & Concepts#System_Model|System Model]] in order to create parts of the LSC. A description of the recorded interaction is first added to the requirements text, and when the user approves it the LSC is created.  
+
The 'SHOW' part allows the user to point at or manipulate objects in the GUI or the [[Language & Concepts#System_Model|System Model]] in order to create parts of the LSC. A description of the recorded interaction is first added to the requirements text, and when the user approves it the LSC is created.
  
−
The interaction is interpreted according to the action performed by the user and the current parsing state for the entered text at the time of interaction. The user can click on a button and refer to its name, or drag a slider and refer to the drag operation.  
+
The interaction is interpreted according to the action performed by the user and the current parsing state for the entered text at the time of interaction. The user can click on a button and refer to its name, or drag a slider and refer to the drag operation.
  
−
For example, if the state of the textual part is "when the user clicks..." and the user clicks the cancel button, the suggested addition to the text will be "the cancel-button". However, if the state of the text is "when ...", with the same interaction, the suggested addition to the text will be "the user clicks the cancel-button".  
+
For example, if the state of the textual part is "when the user clicks..." and the user clicks the cancel button, the suggested addition to the text will be "the cancel-button". However, if the state of the text is "when ...", with the same interaction, the suggested addition to the text will be "the user clicks the cancel-button".
  
−
The parsing is performed online using an active chart parser, and the show &amp; tell algorithm tests possible completions for the incompleted parse and finds the best fit and longest possible addition. If more than one possible addition exists, the user is prompted to choose from a list of the possibilities.  
+
The parsing is performed online using an active chart parser, and the show &amp; tell algorithm tests possible completions for the incompleted parse and finds the best fit and longest possible addition. If more than one possible addition exists, the user is prompted to choose from a list of the possibilities.
  
−
Show &amp; tell is described in <ref>M. Gordon, D. Harel, "Show-and-Tell Play-In: Combining Natural Language with User Interaction for Specifying Behavior", Proc. IADIS Interfaces and Human Computer Interaction 2011 (IHCI 2011), pp. 360-364.</ref>.  
+
Show &amp; tell is described in <ref>M. Gordon, D. Harel, "Show-and-Tell Play-In: Combining Natural Language with User Interaction for Specifying Behavior", Proc. IADIS Interfaces and Human Computer Interaction 2011 (IHCI 2011), pp. 360-364.</ref>.
  
−
[http://www.wisdom.weizmann.ac.il/~michalk/Projects/SaT/ More about show &amp; tell]  
+
[http://www.wisdom.weizmann.ac.il/~michalk/Projects/SaT/ More about show &amp; tell]
  
 
== Trace exploration and visualization  ==
 
== Trace exploration and visualization  ==
  
−
PlayGo provides ways to explore and visualize traces of LSC executions. A trace log may be generated during play-out and it can then be visually explored using the [http://www.weizmann.ac.il/mediawiki/playgo/index.php/The_Tracer Tracer] and the [http://www.cs.bgu.ac.il/~geraw/SupWebSite/ TraceVis] tools.  
+
PlayGo provides ways to explore and visualize traces of LSC executions. A trace log may be generated during play-out and it can then be visually explored using the [http://www.weizmann.ac.il/mediawiki/playgo/index.php/The_Tracer Tracer] and the [http://www.cs.bgu.ac.il/~geraw/SupWebSite/ TraceVis] tools.
  
−
The Tracer is described in <ref> S. Maoz and D. Harel, "On Tracing Reactive Systems", Software and System Modeling (SoSyM), 10(4): 447-468 (2011)</ref>. TraceVis is described in <ref>N. Eitan, M. Gordon, D. Harel, A. Marron and G. Weiss, "On Visualization and Comprehension of Scenario-Based Programs", Proc. 19th Int. Conf. on Program Comprehension (ICPC), 2011, pp. 189-192.</ref>.  
+
The Tracer is described in <ref> S. Maoz and D. Harel, "On Tracing Reactive Systems", Software and System Modeling (SoSyM), 10(4): 447-468 (2011)</ref>. TraceVis is described in <ref>N. Eitan, M. Gordon, D. Harel, A. Marron and G. Weiss, "On Visualization and Comprehension of Scenario-Based Programs", Proc. 19th Int. Conf. on Program Comprehension (ICPC), 2011, pp. 189-192.</ref>.
  
−
<br> [[Image:Tracer.png|800px|A trace of a pacman game in the Tracer tool]]  
+
<br> [[Image:Tracer.png|800px|A trace of a pacman game in the Tracer tool]]
  
−
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 2: A trace of a pacman game in the Tracer tool.</span></span></span><span style="color: rgb(0, 128, 128);"> </span> <br><br>  
+
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 2: A trace of a pacman game in the Tracer tool.</span></span></span><span style="color: rgb(0, 128, 128);"> </span> <br><br>
  
−
[[Image:TraceVis.png|800px|A trace of a pacman game in the TraceVis]]  
+
[[Image:TraceVis.png|800px|A trace of a pacman game in the TraceVis]]
  
−
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 3: A trace of a pacman game in the TraceVis.</span></span></span><span style="color: rgb(0, 128, 128);"> </span>  
+
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 3: A trace of a pacman game in the TraceVis.</span></span></span><span style="color: rgb(0, 128, 128);"> </span>
  
 
== Scenario inter-dependency visualization  ==
 
== Scenario inter-dependency visualization  ==
  
−
PlayGo provides a graph-based visualization of inter-dependencies between LSCs.  
+
PlayGo provides a graph-based visualization of inter-dependencies between LSCs.
  
−
[[Image:SIVExample.png|800px|Scenario inter-dependency visualization]]  
+
[[Image:SIVExample.png|800px|Scenario inter-dependency visualization]]
  
−
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 4: Scenario inter-dependency visualization of an ATM model. Dependencies of three types are shown.</span></span></span><span style="color: rgb(0, 128, 128);"> </span>  
+
<span style="font-size: smaller;"><span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;">Figure 4: Scenario inter-dependency visualization of an ATM model. Dependencies of three types are shown.</span></span></span><span style="color: rgb(0, 128, 128);"> </span>
  
−
Each LSC is represented by a node. Edges represent various kinds of inter-dependencies between the LSCs. There are three kinds of inter-dependencies that the graph visualizes:  
+
Each LSC is represented by a node. Edges represent various kinds of inter-dependencies between the LSCs. There are three kinds of inter-dependencies that the graph visualizes:
  
−
#Causal edge: A directed edge that represents a message in execution mode in the source LSC being potentially unifiable with a message in monitor mode in the target LSC. This edge type represents the possibility that, during runtime, the source LSC might trigger the target LSC. Causal edges are denoted by brown directed arrows.  
+
#Causal edge: A directed edge that represents a message in execution mode in the source LSC being potentially unifiable with a message in monitor mode in the target LSC. This edge type represents the possibility that, during runtime, the source LSC might trigger the target LSC. Causal edges are denoted by brown directed arrows.
−
#Sync edge: An undirected edge that represents a message in execution mode in one LSC being potentially unifiable with a message in execution mode in the other. This edge type represents the possibility that two LSCs might have to synchronize their execution. Sync edges are undirected and are denoted by green lines.  
+
#Sync edge: An undirected edge that represents a message in execution mode in one LSC being potentially unifiable with a message in execution mode in the other. This edge type represents the possibility that two LSCs might have to synchronize their execution. Sync edges are undirected and are denoted by green lines.
 
#Shared object edge: An undirected edge that represents that the two LSCs containing lifelines of the same object. Shared object edges are undirected and are denoted by purple lines.
 
#Shared object edge: An undirected edge that represents that the two LSCs containing lifelines of the same object. Shared object edges are undirected and are denoted by purple lines.
  
−
The graph-based visualization of inter-dependencies was presented in <ref>D. Harel and I. Segall, "Visualizing Inter-Dependencies Between Scenarios", Proc. ACM Symp. on Software Visualization (SOFTVIS'08), 2008, pp. 145-153.</ref>.  
+
The graph-based visualization of inter-dependencies was presented in <ref>D. Harel and I. Segall, "Visualizing Inter-Dependencies Between Scenarios", Proc. ACM Symp. on Software Visualization (SOFTVIS'08), 2008, pp. 145-153.</ref>.
  
 
== Composition  ==
 
== Composition  ==
  
−
PlayGo supports the notion of object composition in scenario-based specifications. Roughly, in order to deal with object composition, the LSC language is extended with appropriate syntax and semantics that allow the specification and interpretation of scenario hierarchies – trees of scenarios – based on the object composition hierarchy in the underlying model. Object composition for LSC is described in <ref>Y. Atir, D. Harel, A. Kleinbort, and S. Maoz, "Object Composition in Scenario-Based Programming", FASE 2008, pp. 301-316.</ref>.  
+
PlayGo supports the notion of object composition in scenario-based specifications. Roughly, in order to deal with object composition, the LSC language is extended with appropriate syntax and semantics that allow the specification and interpretation of scenario hierarchies – trees of scenarios – based on the object composition hierarchy in the underlying model. Object composition for LSC is described in <ref>Y. Atir, D. Harel, A. Kleinbort, and S. Maoz, "Object Composition in Scenario-Based Programming", FASE 2008, pp. 301-316.</ref>.
  
 
== Polymorphism  ==
 
== Polymorphism  ==
  
−
PlayGo supports an extended, polymorphic variant of scenario-based specification. Roughly, lifelines may be marked as symbolic and are labeled with class names rather than specific object names. In this case, the lifeline is not statically bound to a concrete object. Instead, it may dynamically bind, at execution time, to any object of the class or any of its sub classes. This results in a scenario-based behavioral subtyping mechanism.<br> Polymorphism is described in <ref>S. Maoz,  Polymorphic Scenario-Based SpecificationfckLRModels: Semantics and Applications Software and Systems Modeling (SoSyM), 11 (3), 2012, pp. 327-345.</ref>.  
+
PlayGo supports an extended, polymorphic variant of scenario-based specification. Roughly, lifelines may be marked as symbolic and are labeled with class names rather than specific object names. In this case, the lifeline is not statically bound to a concrete object. Instead, it may dynamically bind, at execution time, to any object of the class or any of its sub classes. This results in a scenario-based behavioral subtyping mechanism.<br> Polymorphism is described in <ref>S. Maoz,  Polymorphic Scenario-Based Specification Models: Semantics and Applications Software and Systems Modeling (SoSyM), 11 (3), 2012, pp. 327-345.</ref>.
  
 
== Java API for LSC Creation  ==
 
== Java API for LSC Creation  ==
  
−
PlayGo provides a Java API for the purpose of directly coding a non-graphic version of an LSC. Below is a code sample for creating an LSC that describes the basic move of a memory game.  
+
PlayGo provides a Java API for the purpose of directly coding a non-graphic version of an LSC. Below is a code sample for creating an LSC that describes the basic move of a memory game.
  
−
<code><big><span style="font-size: larger;">void createMemoryGameMoveLSC()
+
<code><big><span style="font-size: larger;">
 +
void createMemoryGameMoveLSC()
 
  {
 
  {
−
+
  LSCModel model = (LSCModel) Utils.createModel("memoryGame");
−
+
  LSCCollaboration memoryGameCollaboration = model.createLSCCollaboration();<br>
−
LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("MemoryGameMove");
+
  LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("matchCards");<br>
−
+
  LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
−
+
                      ("User", "Env", LifelineType.USER, Binding.STATIC);
−
LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
+
  LSCLifeline mc1Lifeline = memoryGameMoveLSC.createLSCLifeline
−
                        ("User", "User", LifelineType.USER, Binding.STATIC);
+
                      ("card", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
−
LSCLifeline mc1Lifeline = memoryGameMoveLSC.createLSCLifeline
+
  LSCLifeline mc2Lifeline = memoryGameMoveLSC.createLSCLifeline
−
                        ("memoryCard1", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
+
                      ("anotherCard", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
−
LSCLifeline mc2Lifeline = memoryGameMoveLSC.createLSCLifeline
+
  LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
−
                        ("memoryCard2", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
+
                      ("panel", "Panel", LifelineType.SYSTEM, Binding.STATIC);<br>
−
LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
+
  memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);
−
                        ("memoryPanel", "MemoryPanel", LifelineType.SYSTEM, Binding.STATIC);
+
  memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);<br>
−
+
  ArrayList<LSCLifeline> conditionLifelines = new ArrayList<LSCLifeline>();
−
+
  conditionLifelines.add(mc1Lifeline);
−
memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
+
  conditionLifelines.add(mc2Lifeline);
−
memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
+
  conditionLifelines.add(memoryPanelLifeline);<br>
−
+
  LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);<br>
−
+
  memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);<br>
−
ArrayList&lt;LSCLifeline&gt; conditionLifelines = new ArrayList&lt;LSCLifeline&gt;();
+
  LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition
−
conditionLifelines.add(mc1Lifeline);
+
                                ("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");<br>
−
conditionLifelines.add(mc2Lifeline);
+
  memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
−
conditionLifelines.add(memoryPanelLifeline);
+
  memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);<br>
−
+
  model.save(new File("memoryGame.lsc"));
−
+
−
LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);
+
−
+
−
+
−
memoryGameMoveLSC.createLSCMessage
+
−
                (memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);
+
−
+
−
+
−
LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition
+
−
                ("!memoryCard1.match(memoryCard2)", conditionLifelines, "!memoryCard1.match(memoryCard2)");
+
−
+
−
+
−
memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
+
−
memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
+
−
+
−
+
 
  } </span></big></code>
 
  } </span></big></code>
  
−
<br>  
+
<br>
  
−
This code represents the LSC shown in the figure below:<br>  
+
This code represents the LSC shown in the figure below:<br>
  
−
[[Image:LSCExample.png|frame|left|An LSC describing the basic rule of a memory game]]<br>  
+
[[Image:LSCExample.png|frame|left|An LSC describing the basic rule of a memory game]]<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br> <br> <br> <br>  
+
<br> <br> <br> <br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
−
<br>  
+
<br>
  
 +
<br>
  
 +
<br>
  
  
  
−
[[Java API|More about Java API]]  
+
[[Java API|More about Java API]]
  
 
== References  ==
 
== References  ==
  
 
<references />
 
<references />

Latest revision as of 06:56, 9 November 2014

Play-out strategies

LSC specifications or `programs' may be underspecified, since the language allows various kinds of non-determinism. Thus, a special mechanism is needed in order to execute LSC programs. This execution mechanism is generically termed play-out. The core of the play-out process is a strategy mechanism that is responsible for choosing the next method to execute. The choice is based on the specification and the current state of the system.

Different kinds of play-out mechanisms may be defined. Each may be viewed as a different operational semantics for LSC.

PlayGo uses a strategy pattern to allow the definition, implementation, and use of new, user-defined play-out strategies. It also includes several built-in, pre-defined play-out strategies, which we now describe.

Naïve play-out

The naïve play-out strategy is the simplest one. It arbitrarily chooses a non-violating method from among the current set of methods that are enabled for execution in at least one chart, but which are not violating in any chart.

Random play-out

The random play-out strategy is similar to the naïve play-out strategy. However, it chooses the next method to execute randomly, using a 'seed' number. The user can either choose a constant seed, in which case the same method will be selected in repeated runs, or ask PlayGo to use random seed, thus causing different, random method selection in each run.

Interactive play-out

The interactive play-out strategy allows the user to choose the next method to execute. The user is presented with a dialog that lists all the currently enabled non-violating methods and is expected to select one of them. The selected method is returned to the play-out mechanism for execution.

Smart play-out

Smart play-out is a smarter, safer way of choosing the next method to execute. It considers not only the current set of enabled non-violating methods, but also looks ahead and picks up a finite sequence of methods that will lead to a successful (non-violating) superstep, if any such sequence exists.

To compute a safe superstep, PlayGo uses model-checking techniques. This is done by challenging the model checker to prove that there is no superstep that can take place without violating the LSC specification. If no such superstep exists, there is no way to proceed. But if there is such a superstep, the model checker provides it as a counter-example. PlayGo uses the counter-example to guide the execution.

Smart play-out is implemented in PlayGo using JTLV.

Smart play-out was first described in [1].

Synthesis

Looking one superstep forward, as is done in the smart play-out strategy, may not be enough, because a safe superstep does not guarantee future execution free of dead locks. An adverse environment may be able to cause the system to fail in satisfying the requirements. Thus, PlayGo offers another strategy, based on the technology of controller synthesis. Controller synthesis takes the LSC specification and attempts to compute a controller whose behavior is guaranteed to satisfy the requirements set by the specification. The computed controller is then used to guide the play-out mechanism. For the case where the LSC specification is unrealizable and a controller cannot be synthesized, PlayGo offers a debugging mode termed counter play-out.

Synthesis for LSC was first described in [2].

The variant of LSC synthesis used in PlayGo is described in [3]. This variant is stronger than previous variants of LSC synthesis, as it supports environment assumptions. It is implemented using JTLV, following the symbolic fixpoint algorithm described in [4].

S2A-BPJ play-out

The S2A-BPJ play-out strategy considers not only the LSC specification but also scenarios written in BPJ. It does that by enclosing the BPJ decision mechanism inside an S2A strategy and delegating the decision from S2A to BPJ. This way, BPJ b-threads may become aware of S2A events. In the other direction, S2A is aware of the BPJ events by having a lifeline representing the BPJ environment and monitoring relevant events that are carried out by BPJ.

Counter play-out

An LSC specification may be unrealizable. That is, if an adverse environment can force any possible execution to violate the guarantees that the system needs to satisfy, a controller cannot be synthesized.

Counter play-out is an interactive debugging method for unrealizable LSC specifications. When such a specification is identified, PlayGo generates a controller that plays the role of the environment and lets the engineer play the role of the system. During execution, the former chooses environment moves such that the latter is forced to eventually fail in satisfying the system's requirements. This results in an interactive, guided execution, which can lead to the root causes of unrealizability. The generated controller constitutes a proof that the specification is conflicting and cannot be realized.

Counter play-out is based on a counter strategy, which is computed in PlayGo by solving a Rabin game using a symbolic, fixpoint algorithm. Counter play-out is described in [5].

Semantic Zoom

Large LSCs are difficult to view and navigate. To address this, PlayGo offers a semantic zoom feature. It allows one to zoom-in and zoom-out of the chart, based on custom weights on the chart's elements (messages, conditions, etc.).

Zooming in and out reveals and hides chart elements. Hidden elements are replaced with a placeholder, to allows the user to understand the context of the remaining elements. Consecutive placeholders are merged into a single, darker-colored placeholder. Effectively, the user can view the most important elements that fit on the screen, while the placeholders hint at the missing information.

In different contexts, different chart elements may be considered more important than others. Thus, the custom weights of the elements are calculated according to the task at hand (debugging, understanding inter-dependencies, etc.). The user can choose a strategy to use for calculating the weights.

Semantic zoom in PlayGo is described in [6].

ATM.ZoomOut.png ATM.png

Figure 1: On the right, the full LSC. On the left, a zoomed-out view. Note the gray scale placeholders, which hide LSC elements. The darker it is, the more elements it hides. 

The green dotted ellipse marks the most recent placeholder that was added or changed during zoom-out.
When zooming in, the last added element is marked with this green dotted ellipse.


Watch a Semantic Zoom demo

Natural language play-in

PlayGo supports a number of ways to define LSCs: manual editing, play-in, natural language play-in and show & tell.

Natural language play-in allows the user to create LSCs through a natural language textual interface rather than by drawing the elements or interacting with the system.

The allowed input language is a controlled and structured fragment of English tailored specifically to capture LSCs. This language is generated by a context free grammar. It makes it possible to write requirements, each one phrased as a single sentence which the system will parse and transform into an LSC. The resulting LSCs can then be executed.
Here are two examples of natural language requirements that can be dealt with by the system:

  1. when the user presses the d_button, if the display mode is time, the display mode changes to date, otherwise if the display mode is date, the display mode changes to time.
  2. when the mobile_unit state changes to on, as long as the mobile_unit state is on, if two seconds have elapsed and the baby_unit does not connect to the mobile_unit, the connection_light color changes to red.

The language is domain-general, and uses the wordnet dictionary [7] to decide which part of speech tags can be used (e.g., noun, verb, adjective, etc.) and what element in the model is assigned to each word.

Natural language requirements may be played in using one of the two following execution modes:

  1. Interactive natural language play-in - The text is parsed using a symbolic parser. When the system cannot assign a single role in the model to a term in the text, it prompts the user with the problem and offers possible fixes. The user can then disambiguate these terms. We assume the user always refers to the same objects / actions using the same words. Based on the fix chosen by the user, the LSC is constructed.
    Interactive natural language play-in is described in [8].
  2. Statistical natural language play-in - The text is parsed using a statistical parser trained on a large set of pre-annotated example requirements. When the system cannot assign a single role in the model to a term in the text, it relies on the trained statistical model to select a role from among several previously attested alternatives. Based on the decisions made by the statistical model, the LSC is constructed.
    Automatic Natural language play-in is described in [9]

More about How to Play-In with NL.

Show & tell play-in

Show & Tell is a play-in feature that allows the user to create LSCs through a natural language textual interface combined with the classical play-in technique of interacting with the GUI of the system.

The 'TELL' part is based on natural language play-in; see above.

The 'SHOW' part allows the user to point at or manipulate objects in the GUI or the System Model in order to create parts of the LSC. A description of the recorded interaction is first added to the requirements text, and when the user approves it the LSC is created.

The interaction is interpreted according to the action performed by the user and the current parsing state for the entered text at the time of interaction. The user can click on a button and refer to its name, or drag a slider and refer to the drag operation.

For example, if the state of the textual part is "when the user clicks..." and the user clicks the cancel button, the suggested addition to the text will be "the cancel-button". However, if the state of the text is "when ...", with the same interaction, the suggested addition to the text will be "the user clicks the cancel-button".

The parsing is performed online using an active chart parser, and the show & tell algorithm tests possible completions for the incompleted parse and finds the best fit and longest possible addition. If more than one possible addition exists, the user is prompted to choose from a list of the possibilities.

Show & tell is described in [10].

More about show & tell

Trace exploration and visualization

PlayGo provides ways to explore and visualize traces of LSC executions. A trace log may be generated during play-out and it can then be visually explored using the Tracer and the TraceVis tools.

The Tracer is described in [11]. TraceVis is described in [12].


A trace of a pacman game in the Tracer tool

Figure 2: A trace of a pacman game in the Tracer tool.

A trace of a pacman game in the TraceVis

Figure 3: A trace of a pacman game in the TraceVis.

Scenario inter-dependency visualization

PlayGo provides a graph-based visualization of inter-dependencies between LSCs.

Scenario inter-dependency visualization

Figure 4: Scenario inter-dependency visualization of an ATM model. Dependencies of three types are shown.

Each LSC is represented by a node. Edges represent various kinds of inter-dependencies between the LSCs. There are three kinds of inter-dependencies that the graph visualizes:

  1. Causal edge: A directed edge that represents a message in execution mode in the source LSC being potentially unifiable with a message in monitor mode in the target LSC. This edge type represents the possibility that, during runtime, the source LSC might trigger the target LSC. Causal edges are denoted by brown directed arrows.
  2. Sync edge: An undirected edge that represents a message in execution mode in one LSC being potentially unifiable with a message in execution mode in the other. This edge type represents the possibility that two LSCs might have to synchronize their execution. Sync edges are undirected and are denoted by green lines.
  3. Shared object edge: An undirected edge that represents that the two LSCs containing lifelines of the same object. Shared object edges are undirected and are denoted by purple lines.

The graph-based visualization of inter-dependencies was presented in [13].

Composition

PlayGo supports the notion of object composition in scenario-based specifications. Roughly, in order to deal with object composition, the LSC language is extended with appropriate syntax and semantics that allow the specification and interpretation of scenario hierarchies – trees of scenarios – based on the object composition hierarchy in the underlying model. Object composition for LSC is described in [14].

Polymorphism

PlayGo supports an extended, polymorphic variant of scenario-based specification. Roughly, lifelines may be marked as symbolic and are labeled with class names rather than specific object names. In this case, the lifeline is not statically bound to a concrete object. Instead, it may dynamically bind, at execution time, to any object of the class or any of its sub classes. This results in a scenario-based behavioral subtyping mechanism.
Polymorphism is described in [15].

Java API for LSC Creation

PlayGo provides a Java API for the purpose of directly coding a non-graphic version of an LSC. Below is a code sample for creating an LSC that describes the basic move of a memory game. 

void createMemoryGameMoveLSC()
{
 LSCModel model = (LSCModel) Utils.createModel("memoryGame");
 LSCCollaboration memoryGameCollaboration = model.createLSCCollaboration();

 LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("matchCards");

 LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
                      ("User", "Env", LifelineType.USER, Binding.STATIC);
 LSCLifeline mc1Lifeline = memoryGameMoveLSC.createLSCLifeline
                      ("card", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
 LSCLifeline mc2Lifeline = memoryGameMoveLSC.createLSCLifeline
                      ("anotherCard", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
 LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
                      ("panel", "Panel", LifelineType.SYSTEM, Binding.STATIC);

 memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);
 memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);

 ArrayList<LSCLifeline> conditionLifelines = new ArrayList<LSCLifeline>();
 conditionLifelines.add(mc1Lifeline);
 conditionLifelines.add(mc2Lifeline);
 conditionLifelines.add(memoryPanelLifeline);

 LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);

 memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);

 LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition
                                ("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");

 memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
 memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);

 model.save(new File("memoryGame.lsc"));
}


This code represents the LSC shown in the figure below:

An LSC describing the basic rule of a memory game
































More about Java API

References

  1. ↑ D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2002), November 2002, pp. 378-398.
  2. ↑ D. Harel and H. Kugler, “Synthesizing state-based object systems from LSC specifications,” Int. J. Found. Comput. Sci.,vol. 13, no. 1, pp. 5–51, 2002
  3. ↑ S. Maoz and Y. Sa’ar, “Assume-Guarantee Scenarios: Semantics and Synthesis,” Proc. 15th Int. Conf. on Model Driven Engineering Languages and Systems (MoDELS), LNCS 7590, pp. 335-351, Springer, 2012
  4. ↑ N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of Reactive(1) Designs,” in VMCAI, ser. LNCS, vol. 3855. Springer,2006, pp. 364–380.
  5. ↑ S. Maoz and Y. Sa’ar, “Counter Play-Out: Executing Unrealizable Scenario-Based Specifications,” to appear in ICSE'13 (2013)
  6. ↑ M. Gordon and D. Harel, "Semantic Navigation Strategies for Scenario-Based Programming", Proc. IEEE Symp. on Visual Languages and Human-Centric Computing (VL/HCC 2010), 2010, pp.219-226.
  7. ↑ Princeton University "About WordNet." WordNet. Princeton University. 2010. wordnet
  8. ↑ M. Gordon and D. Harel, "Generating Executable Scenarios from Natural Language", Proc. 10th Int. Conf. on Comput. Linguistics and Intelligent Text Processing (CICLing'09), Lecture Notes In Computer Science, vol. 5449. Springer-Verlag, Berlin, Heidelberg, 2009, pp. 456-467.
  9. ↑ R. Tsarfaty, E. Pogrebezky, G. Weiss, Y. Natan, S. Szekely and D. Harel, "Semantic Parsing Using Content and Context: A Case Study from Requirements Elicitation", Proc. Int. Conf. on Empirical Methods in Natural Language Processing (EMNLP), to appear, 2014.
  10. ↑ M. Gordon, D. Harel, "Show-and-Tell Play-In: Combining Natural Language with User Interaction for Specifying Behavior", Proc. IADIS Interfaces and Human Computer Interaction 2011 (IHCI 2011), pp. 360-364.
  11. ↑ S. Maoz and D. Harel, "On Tracing Reactive Systems", Software and System Modeling (SoSyM), 10(4): 447-468 (2011)
  12. ↑ N. Eitan, M. Gordon, D. Harel, A. Marron and G. Weiss, "On Visualization and Comprehension of Scenario-Based Programs", Proc. 19th Int. Conf. on Program Comprehension (ICPC), 2011, pp. 189-192.
  13. ↑ D. Harel and I. Segall, "Visualizing Inter-Dependencies Between Scenarios", Proc. ACM Symp. on Software Visualization (SOFTVIS'08), 2008, pp. 145-153.
  14. ↑ Y. Atir, D. Harel, A. Kleinbort, and S. Maoz, "Object Composition in Scenario-Based Programming", FASE 2008, pp. 301-316.
  15. ↑ S. Maoz, Polymorphic Scenario-Based Specification Models: Semantics and Applications Software and Systems Modeling (SoSyM), 11 (3), 2012, pp. 327-345.
Retrieved from "https://wiki.weizmann.ac.il/playgo/index.php?title=PlayGo_Feature_List&oldid=1369"