Difference between revisions of "PlayGo Examples"

From WeizmannWiki
Jump to: navigation, search
(Wrist Watch)
(Memory Game LSC project)
 
(33 intermediate revisions by 3 users not shown)
Line 1: Line 1:
==Applications==
+
== Applications ==
===Memory Game===
+
 
[[Image:LSCExample.png |frame|left]][[Image:MemoryGameUI.png]]<br><br><br><br><br>
+
=== Memory Game ===
 +
 
 +
[[Image:LSCExample.png|420px]][[Image:MemoryGameUI.png|400px]]<br><br>
 +
 
 +
The memory game is a simple application containing a single LSC that specifies the behavior of a memory game. The memory game UI is written in Java Swing.<br> The memory game application demonstrates the following features:<br>
 +
 
 +
*Symbolic Instances: '''card''' and '''anotherCard''' lifelines are symbolic: their lifeline head is dashed to visualize just that. The memory game contains 16 cards. During play-out, the clicked cards will dynamically be bound to specific card lifelines. The memory panel is represented by a static lifeline (there is a single panel in the game). This panel will be statically bound to the panel lifeline during play-out.
 +
*Live copy: A second '''click''' (the second time a user clicks on a card) opens another live copy of the LSC.
 +
*Enable Events: After a second '''click''', the '''beep''' event is enabled in the first live copy but is not enabled in the second live copy. The second live copy expects another '''click''', and when this event does not occur (instead a '''beep''' event occurs) the live copy is violated and is closed.
  
The memory game is a simple application containing a single LSC that specifies the behavior of a memory game.
 
The memory game UI is based on [http://code.google.com/webtoolkit/ GWT].<br>
 
The memory game application demonstrates the following features:<br>
 
*Symbolic Instances: memoryCard1 and memoryCard2 lifelines are symbolic: their lifeline head is dashed to visualize just that. The memory game contains 12 cards. During play-out, the clicked cards will dynamically be bound to specific card lifelines. The memory panel is represented by a static lifeline (there is a single panel in the game). This panel will be statically bound to the panel lifeline during play-out.
 
*Live copy: A second '''flipUp''' (the second time a user clicks on a card) opens another live copy of the LSC.
 
*Enable Events: After a second '''flipUp''', the '''beep''' event is enabled in the first live copy but is not enabled in the second live copy. The second live copy expects another '''flipUp''', and when this event does not occur (instead a '''beep''' event occurs) the live copy is violated and is closed.
 
 
<br>
 
<br>
The memory game application is included in the workspace provided with the PlayGo download.
 
*[[Getting Started with PlayGo]]
 
*[[PlayGo_HowTo | PlayGo HowTo]]
 
  
===Baby Monitor===
+
==== Download the Memory Game Example ====
[[Image:BabyMonitor.Lsc12.jpg |frame|left]][[Image:BabyMonitor.png|235px]]<br><br>
+
The baby monitor application includes 14 LSCs, each of which includes 3-4 lifelines. The specification demonstrates various features of PlayGo and the underlying language.
+
<br>Most of the LSCs were created by [[PlayGo_Feature_List#Natural_language_play-in | natural language play-in]], and others by [[Language & Concepts#Play-In |basic play-in]].
+
<br><br> To see the system's requirements in controlled English click [[Baby Monitor Specification | here]].
+
<br><br>
+
The Baby Monitor application is included in the workspace provided with the PlayGo download.
+
  
*[[Getting Started with PlayGo]]
+
Below is a download of the memory game final application, as well as instructions for creating the memory game example in PlayGo.
*[[PlayGo_HowTo | PlayGo HowTo]]
+
  
===Water Tap===
+
===== Memory game final application (runnable jar) =====
[[Image:WaterTap.png | 420px]][[Image:WaterTapUI.jpg |400px]]<br><br>
+
  
The water tap is a simple application containing three LSCs that describe a specific water tap behavior by which a sink is filled with lukewarm water.
+
[https://weizmann.box.com/s/dina60yqs7dgd6oljzv1 Runnable Memory Game with Swing GUI]
The water tap application demonstrates the following concepts:<br>
+
* Modularity - each LSC is self standing and is responsible for a certain aspect of the application's behavior.
+
* Incremental development - due to modularity, a system can be developed incrementally. Adding a new behavior affects the complete system behavior but does not require changes to existing LSCs or existing code.
+
* Enabled Events: The Interleave LSC shows how after the 'addHot' event occurs, only the 'addCold' event is enabled; Until 'addCold' occurs, 'addHot' is not allowed to occur, thus will wait for its turn.
+
* Loops are demonstrated here, bounded by a fixed limit (e.g., 5 times in the addHotFiveTimes LSC) or unbounded (in the Interleave LSC).
+
  
[[Media:WaterTap.zip | Download Water Tap application]]
+
To run the memory game, simply extract the downloaded zip and double click the jar file.
<br>
+
 
 +
===== Memory Game LSC project =====
 +
 
 +
#[[Download PlayGo|Download PlayGo]].
 +
#From the 'File' menu choose New-->Example....-->PlayGo Examples-->Memory Game
 +
#Click the 'Finish' button.
 +
#The memory game example project is now part of your workspace. You can start playing with it. For details refer to [[How to Play-Out|how to play out]] and [[How_to_Play-In|how to play in]].
 +
 
 +
=== Baby Monitor ===
 +
 
 +
[[Image:BabyMonitor.Lsc12.jpg|frame|left]][[Image:BabyMonitor.png|235px]]<br><br> The baby monitor application includes 14 LSCs, each of which includes 3-4 lifelines. The specification demonstrates various features of PlayGo and the underlying language. <br>Most of the LSCs were created by [[PlayGo_Feature_List#Natural_language_play-in|NL play-in]], and others by [[Language & Concepts#Play-In|basic play-in]]. <br><br> To see the system's requirements in controlled English click [[Baby Monitor Specification|here]].
 +
 
 +
=== Water Tap ===
 +
 
 +
[[Image:WaterTap.png|420px]][[Image:WaterTapUI.jpg|400px]]<br><br>
 +
 
 +
The water tap is a simple application containing three LSCs that describe a specific water tap behavior by which a sink is filled with lukewarm water. The water tap application demonstrates the following concepts:<br>
 +
 
 +
*Modularity - each LSC is self standing and is responsible for a certain aspect of the application's behavior.
 +
*Incremental development - due to modularity, a system can be developed incrementally. Adding a new behavior affects the complete system behavior but does not require changes to existing LSCs or existing code.
 +
*Enabled Events: The Interleave LSC shows how after the 'addHot' event occurs, only the 'addCold' event is enabled; Until 'addCold' occurs, 'addHot' is not allowed to occur, thus will wait for its turn.
 +
*Loops are demonstrated here, bounded by a fixed limit (e.g., 5 times in the addHotFiveTimes LSC) or unbounded (in the Interleave LSC).
 +
 
 +
[https://weizmann.box.com/s/xe31fgyg28q7netcezel Download Water Tap application] <br>
 
[[Instructions for creating LSC project from LSC file | Instructions for playing with the Water Tap application]]
 
[[Instructions for creating LSC project from LSC file | Instructions for playing with the Water Tap application]]
 
<br><br>
 
<br><br>
  
===Wrist Watch===
+
=== Phone  ===
 +
 
 +
[[Image:SampleLSC.png]][[Image:PhoneGUI.png|200px]]<br><br>
 +
 
 +
The project describes and implements a cell phone, including some common cell phone features, such as quick dial, lock and more. This project has been implemented using [[PlayGo_Feature_List#Natural_language_play-in|NL play-in]]. Therefore, the example includes the controlled natural language to create each of the LSCs. <br> Details can be found [[Phone Specification|here]].
 +
 
 +
=== Wristwatch  ===
 +
 
 +
[[Image:WristWatchGUI.jpg|230px]]<br>
 +
 
 +
The wristwatch application includes 20 LSCs, defining its behavior and demonstrating the use in [[PlayGo Feature List#Natural_Language_Play-in|NL play-in]].<br> Details about the specification and downloads can be found [[Wristwatch Example|here]].
 +
 
 +
=== Wall Painting ===
 +
 
 +
[[Image:drone.jpg|230px]]<br> <span style="color: rgb(39,64,139);"><span style="font-family: Tahoma;">
 +
 
 +
The wall painting BP application is based on the [http://wiki.weizmann.ac.il/bp/index.php/Helicopter_flight_and_mission helicopter flight example], which uses the [https://code.google.com/p/javadrone/ ARDrone Java interface] and so it is prepared to be tested on a real ARDrone. The example also has a simulation mode with which one can run it without having an actual drone.
 +
The example uploaded here demonstrates an S2A and BPJ integrated project; while the original example was written in BPJ, in this variant of the example, we have added LSCs to control the color supply.
 +
 
 +
Details about the specification and downloads can be found [[Wall Painting Example|here]].
 +
 
 +
== LSC Design Patterns ==
 +
 
 +
=== After '''A''' occurs, '''B''' must occur, unless exception '''C''' occurs  ===
 +
 
 +
We want to specify the requirement: if event A occurs then event B must occur, unless event C occurs; meaning, if A occurs, either B or C must occur.
 +
 
 +
LSC has a hot monitor idiom (so we can specify that if A occurred B must occur), but there is no idiom for hot monitoring one event from a list of events; e.g., hot monitor of either B or C.
 +
 
 +
To specify hot monitor of event B or event C, we offer the following design pattern (see text explanation below):
 +
 
 +
<br> [[Image:BMustOccurUnlessC.png]]
 +
 
 +
Explanation:
 +
 
 +
#As long as A occurred and neither B not C occurred, LSC1 remains open in a cold cut, waiting for either C or B to occur and LSC2 remains open in a hot cut, indicating that the system as a whole is in hot global cut; i.e., the system must not stay in this state forever.
 +
#If A occurred and then B occurred, LSC1 reaches a cold false condition (named Exit) and therefore closes with a cold violation. This enables the LSC1Done event (no longer leads to the false violation in LSC1, since LSC1 closed), allowing LSC2 to complete.
 +
#If A occurred and then C occurred, similarly to the previous case, LSC1 reaches a cold false condition (named Exit) and therefore closes with a cold violation. This enables the LSC1Done event (no longer leads to the false violation in LSC1, since LSC1 closed), allowing LSC2 to complete.
 +
#The LSCs below describe test cases / simulated environment behavior that we experimented with, and which highlight the overall behavior. <br><br>
 +
 
 +
The following LSCs describe valid behavior:
 +
 
 +
[[Image:BMustOccurUnlessC validBehavior.png]] <br><br> The following LSC describes an invalid behavior, in which only A occurs and neither B not C occur (in which case, the system will remain in a hot cut):
  
Page under construction, see [http://www.wisdom.weizmann.ac.il/~michalk/Projects/ReqToLSCs/ http://www.wisdom.weizmann.ac.il/~michalk/Projects/ReqToLSCs/] for an earlier version
+
[[Image:BMustOccurUnlessC invalidBehavior.png]] <br><br>
  
[[Wrist Watch Example]]
+
[https://weizmann.box.com/s/l3a2rt13tec5ik2bauem Download this design pattern] <br> [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Instructions_for_creating_LSC_project_from_LSC_file Instructions for playing with this specification] <br><br>

Latest revision as of 11:37, 20 December 2015

Applications

Memory Game

LSCExample.pngMemoryGameUI.png

The memory game is a simple application containing a single LSC that specifies the behavior of a memory game. The memory game UI is written in Java Swing.
The memory game application demonstrates the following features:

  • Symbolic Instances: card and anotherCard lifelines are symbolic: their lifeline head is dashed to visualize just that. The memory game contains 16 cards. During play-out, the clicked cards will dynamically be bound to specific card lifelines. The memory panel is represented by a static lifeline (there is a single panel in the game). This panel will be statically bound to the panel lifeline during play-out.
  • Live copy: A second click (the second time a user clicks on a card) opens another live copy of the LSC.
  • Enable Events: After a second click, the beep event is enabled in the first live copy but is not enabled in the second live copy. The second live copy expects another click, and when this event does not occur (instead a beep event occurs) the live copy is violated and is closed.


Download the Memory Game Example

Below is a download of the memory game final application, as well as instructions for creating the memory game example in PlayGo.

Memory game final application (runnable jar)

Runnable Memory Game with Swing GUI

To run the memory game, simply extract the downloaded zip and double click the jar file.

Memory Game LSC project
  1. Download PlayGo.
  2. From the 'File' menu choose New-->Example....-->PlayGo Examples-->Memory Game
  3. Click the 'Finish' button.
  4. The memory game example project is now part of your workspace. You can start playing with it. For details refer to how to play out and how to play in.

Baby Monitor

BabyMonitor.Lsc12.jpg
BabyMonitor.png

The baby monitor application includes 14 LSCs, each of which includes 3-4 lifelines. The specification demonstrates various features of PlayGo and the underlying language.
Most of the LSCs were created by NL play-in, and others by basic play-in.

To see the system's requirements in controlled English click here.

Water Tap

WaterTap.pngWaterTapUI.jpg

The water tap is a simple application containing three LSCs that describe a specific water tap behavior by which a sink is filled with lukewarm water. The water tap application demonstrates the following concepts:

  • Modularity - each LSC is self standing and is responsible for a certain aspect of the application's behavior.
  • Incremental development - due to modularity, a system can be developed incrementally. Adding a new behavior affects the complete system behavior but does not require changes to existing LSCs or existing code.
  • Enabled Events: The Interleave LSC shows how after the 'addHot' event occurs, only the 'addCold' event is enabled; Until 'addCold' occurs, 'addHot' is not allowed to occur, thus will wait for its turn.
  • Loops are demonstrated here, bounded by a fixed limit (e.g., 5 times in the addHotFiveTimes LSC) or unbounded (in the Interleave LSC).

Download Water Tap application
Instructions for playing with the Water Tap application

Phone

SampleLSC.pngPhoneGUI.png

The project describes and implements a cell phone, including some common cell phone features, such as quick dial, lock and more. This project has been implemented using NL play-in. Therefore, the example includes the controlled natural language to create each of the LSCs.
Details can be found here.

Wristwatch

WristWatchGUI.jpg

The wristwatch application includes 20 LSCs, defining its behavior and demonstrating the use in NL play-in.
Details about the specification and downloads can be found here.

Wall Painting

Drone.jpg

The wall painting BP application is based on the helicopter flight example, which uses the ARDrone Java interface and so it is prepared to be tested on a real ARDrone. The example also has a simulation mode with which one can run it without having an actual drone. The example uploaded here demonstrates an S2A and BPJ integrated project; while the original example was written in BPJ, in this variant of the example, we have added LSCs to control the color supply.

Details about the specification and downloads can be found here.

LSC Design Patterns

After A occurs, B must occur, unless exception C occurs

We want to specify the requirement: if event A occurs then event B must occur, unless event C occurs; meaning, if A occurs, either B or C must occur.

LSC has a hot monitor idiom (so we can specify that if A occurred B must occur), but there is no idiom for hot monitoring one event from a list of events; e.g., hot monitor of either B or C.

To specify hot monitor of event B or event C, we offer the following design pattern (see text explanation below):


BMustOccurUnlessC.png

Explanation:

  1. As long as A occurred and neither B not C occurred, LSC1 remains open in a cold cut, waiting for either C or B to occur and LSC2 remains open in a hot cut, indicating that the system as a whole is in hot global cut; i.e., the system must not stay in this state forever.
  2. If A occurred and then B occurred, LSC1 reaches a cold false condition (named Exit) and therefore closes with a cold violation. This enables the LSC1Done event (no longer leads to the false violation in LSC1, since LSC1 closed), allowing LSC2 to complete.
  3. If A occurred and then C occurred, similarly to the previous case, LSC1 reaches a cold false condition (named Exit) and therefore closes with a cold violation. This enables the LSC1Done event (no longer leads to the false violation in LSC1, since LSC1 closed), allowing LSC2 to complete.
  4. The LSCs below describe test cases / simulated environment behavior that we experimented with, and which highlight the overall behavior.

The following LSCs describe valid behavior:

BMustOccurUnlessC validBehavior.png

The following LSC describes an invalid behavior, in which only A occurs and neither B not C occur (in which case, the system will remain in a hot cut):

BMustOccurUnlessC invalidBehavior.png

Download this design pattern
Instructions for playing with this specification