PlayGo Feature List
Contents
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].
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.
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 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 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 [7] 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 play-in is described in [8].
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 [9].
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 [10]. TraceVis is described in [11].
Figure 2: A trace of a pacman game in the Tracer tool.
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.
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:
- 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.
- 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 [12].
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 [13].
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 [14].
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("MemoryGameMove");
LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
("User", "Env", LifelineType.USER, Binding.STATIC);
LSCLifeline mc1Lifeline = memoryGameMoveLSC.createLSCLifeline
("memoryCard1", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
LSCLifeline mc2Lifeline = memoryGameMoveLSC.createLSCLifeline
("memoryCard2", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
("memoryPanel", "MemoryPanel", LifelineType.SYSTEM, Binding.STATIC);
memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "flipUp", 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("!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);
model.save(new File("memoryGame.lsc"));
}
This code represents the LSC shown in the figure below:
References
- ↑ 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.
- ↑ 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
- ↑ 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
- ↑ N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of Reactive(1) Designs,” in VMCAI, ser. LNCS, vol. 3855. Springer,2006, pp. 364–380.
- ↑ S. Maoz and Y. Sa’ar, “Counter Play-Out: Executing Unrealizable Scenario-Based Specifications,” to appear in ICSE'13 (2013)
- ↑ 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.
- ↑ Princeton University "About WordNet." WordNet. Princeton University. 2010. wordnet
- ↑ 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.
- ↑ 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.
- ↑ S. Maoz and D. Harel, "On Tracing Reactive Systems", Software and System Modeling (SoSyM), 10(4): 447-468 (2011)
- ↑ 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.
- ↑ D. Harel and I. Segall, "Visualizing Inter-Dependencies Between Scenarios", Proc. ACM Symp. on Software Visualization (SOFTVIS'08), 2008, pp. 145-153.
- ↑ Y. Atir, D. Harel, A. Kleinbort, and S. Maoz, "Object Composition in Scenario-Based Programming", FASE 2008, pp. 301-316.
- ↑ S. Maoz, Polymorphic Scenario-Based Specification Models: Semantics and Applications Software and Systems Modeling (SoSyM), 11 (3), 2012, pp. 327-345.
