PlayGo Feature List - Revision history

Smadar: /* Natural language play-in */

2014-11-09T06:56:33Z

‎Natural language play-in

Smadar: /* Java API for LSC Creation */

2014-05-01T08:45:24Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T08:44:54Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T08:31:32Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T08:20:36Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T08:14:48Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T08:14:01Z

‎Java API for LSC Creation

Smadar: /* Java API for LSC Creation */

2014-05-01T07:09:59Z

‎Java API for LSC Creation

Yaaritn: /* Java API for LSC Creation */

2014-04-30T15:45:22Z

‎Java API for LSC Creation

Smadar: /* Play-out strategies */

2014-04-29T06:23:40Z

‎Play-out strategies

@@ Line 75: / Line 75: @@
 [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 &amp; tell.
+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:
+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:
-#''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 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''
+#''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 <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.
+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>
-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>.
+Natural language requirements may be played in using one of the two following execution modes:
-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].
+#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>.
 == Show &amp; tell play-in  ==

@@ Line 174: / Line 174: @@
    LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);<br>
    memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);<br>
-   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition<br>("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");<br>
+   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition
    memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
    memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);<br>

@@ Line 174: / Line 174: @@
    LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);<br>
    memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);<br>
-   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");<br>
+   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition<br>("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");<br>
    memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
    memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);<br>

@@ Line 157: / Line 157: @@
    LSCModel model = (LSCModel) Utils.createModel("memoryGame");
    LSCCollaboration memoryGameCollaboration = model.createLSCCollaboration();<br>
-   LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("MemoryGameMove");<br>
+   LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("matchCards");<br>
    LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
                         ("User", "Env", LifelineType.USER, Binding.STATIC);
    LSCLifeline mc1Lifeline = memoryGameMoveLSC.createLSCLifeline
-                        ("memoryCard1", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
+                        ("card", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
    LSCLifeline mc2Lifeline = memoryGameMoveLSC.createLSCLifeline
-                        ("memoryCard2", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
+                        ("anotherCard", "Card", LifelineType.SYSTEM, Binding.DYNAMIC);
    LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
-                        ("memoryPanel", "MemoryPanel", LifelineType.SYSTEM, Binding.STATIC);<br>
+                        ("panel", "Panel", LifelineType.SYSTEM, Binding.STATIC);<br>
-   memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
+   memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);
-   memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);<br>
+   memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "click", Temperature.Cold, ExecutionKind.MONITORED);<br>
    ArrayList<LSCLifeline> conditionLifelines = new ArrayList<LSCLifeline>();
    conditionLifelines.add(mc1Lifeline);
@@ Line 174: / Line 174: @@
    LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);<br>
    memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);<br>
-   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition("!memoryCard1.match(memoryCard2)", conditionLifelines, "!memoryCard1.match(memoryCard2)");<br>
+   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition("!card.getValue().equals(anotherCard.getValue())", conditionLifelines, "!card.getValue().equals(anotherCard.getValue())");<br>
    memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
    memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);<br>

@@ Line 152: / Line 152: @@
 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;">
+  {
    LSCModel model = (LSCModel) Utils.createModel("memoryGame");
-   LSCCollaboration memoryGameCollaboration = model.createLSCCollaboration();
+   LSCCollaboration memoryGameCollaboration = model.createLSCCollaboration();<br>
-<br>
+   LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("MemoryGameMove");<br>
    LSCInteraction memoryGameMoveLSC = memoryGameCollaboration.createLSC("MemoryGameMove");
 <br>
    LSCLifeline user = memoryGameMoveLSC.createLSCLifeline
                         ("User", "Env", LifelineType.USER, Binding.STATIC);
@@ Line 167: / Line 165: @@
                         ("memoryCard2", "MemoryCard", LifelineType.SYSTEM, Binding.DYNAMIC);
    LSCLifeline memoryPanelLifeline = memoryGameMoveLSC.createLSCLifeline
-                        ("memoryPanel", "MemoryPanel", LifelineType.SYSTEM, Binding.STATIC);
+                        ("memoryPanel", "MemoryPanel", LifelineType.SYSTEM, Binding.STATIC);<br>
 <br>
    memoryGameMoveLSC.createLSCMessage(user, mc1Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
-   memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);
+   memoryGameMoveLSC.createLSCMessage(user, mc2Lifeline, "flipUp", Temperature.Cold, ExecutionKind.MONITORED);<br>
 <br>
    ArrayList<LSCLifeline> conditionLifelines = new ArrayList<LSCLifeline>();
    conditionLifelines.add(mc1Lifeline);
    conditionLifelines.add(mc2Lifeline);
-   conditionLifelines.add(memoryPanelLifeline);
+   conditionLifelines.add(memoryPanelLifeline);<br>
-<br>
+   LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);<br>
-   LSCStateInvariant sync = memoryGameMoveLSC.createLSCSyncConstraint(conditionLifelines);
+   memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);<br>
-   memoryGameMoveLSC.createLSCMessage(memoryPanelLifeline, memoryPanelLifeline, "beep", Temperature.Hot, ExecutionKind.EXECUTE);
+   LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition("!memoryCard1.match(memoryCard2)", conditionLifelines, "!memoryCard1.match(memoryCard2)");<br>
 <br>
    LSCStateInvariant condition = memoryGameMoveLSC.createLSCOpaqueCondition
-		              ("!memoryCard1.match(memoryCard2)", conditionLifelines, "!memoryCard1.match(memoryCard2)");
 <br>
    memoryGameMoveLSC.createLSCMessage(mc1Lifeline, mc1Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
-   memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);
+   memoryGameMoveLSC.createLSCMessage(mc2Lifeline, mc2Lifeline, "flipDown", Temperature.Hot, ExecutionKind.EXECUTE);<br>
 <br>
    model.save(new File("memoryGame.lsc"));
   } </span></big></code>

← Older revision		Revision as of 06:23, 29 April 2014
Line 36:		Line 36:

	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>.		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 ==