WeizmannWiki - User contributions [en]

Download PlayGo

2020-12-30T12:57:38Z

HarelAdmin: /* PlayGo for Windows */

== PlayGo for Windows ==

=== Version 5.0 ===
[https://drive.google.com/file/d/1bd9OIj2au6Oepg-sznuiiqeJn4OaafAs/view?usp=sharing PlayGo version 5.0 for Windows (jre included)]

[https://drive.google.com/file/d/1TosVvv7DxSbyvfAWvGjtkaQC9exuk5Kq/view?usp=sharing PlayGo 5.0 User Guide]

=== Version 4.0 ===

[https://weizmann.box.com/s/o22m6zd0bvpp7ghkfwjn2oh3zdh3pwjd PlayGo version 4.0 for Windows (jre included)]

[https://weizmann.box.com/s/0lb70tpkjwzwj4ulyb6et7pgipy00zsn PlayGo version 4.0 for Windows (no jre) ]

[https://weizmann.box.com/s/hgjufxvyhnewpv2cr99x2dnn1mk3jdqc PlayGo version 4.0 for Windows 32-bit (no jre)]

See the [[Getting Started with PlayGo]] to start playing with PlayGo.

== PlayGo for Linux ==

=== Version 4.0 ===

[https://weizmann.box.com/s/fce9sr9uki848564fqe9jx5dukhrmt0i PlayGo version 4.0 for linux (jre included)]

[https://weizmann.box.com/s/yb63vltoyd14ytkx8z5hhiq1bbaeqymo PlayGo version 4.0 for linux (no jre)]

See the [[Getting Started with PlayGo]] to start playing with PlayGo.

PlayGo source code of version 4.0 is available for download [https://weizmann.box.com/s/878rj4ky80ax9sffjiftwuvjnswde5rk here].

Baby Monitor Specification

2014-05-01T07:14:41Z

HarelAdmin:

The list below is the Baby Monitor system's requirements in [http://en.wikipedia.org/wiki/Controlled_natural_language controlled English]. These are valid requirements that can be used for [[PlayGo_Feature_List#Natural_language_play-in|NL play-in]]. 

== Requirements ==

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="10%" | LSC Name
! scope="col" width="50%" | Requirement in Natural Language Text
! scope="col" width="35" | Comments
! scope="col" width="5%" | LSC
|-
| Lsc1
| when the user clicks the increase_temperature_button, the temperature_threshold increases
| 
| [[Image:NL1.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc2
| when the user clicks the decrease_temperature_button, the temperature_threshold decreases
|
| [[Image:NL2.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc3
| when the user clicks a TempChange, the temperature_display color changes to yellow and the temperature_display displays the temperature_threshold value
|
| [[Image:NL3.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc4
| when the baby_unit temperature changes, the temperature_display displays the baby_unit temperature and the temperature_display color changes to green 
|
| [[Image:NL4.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc5
| when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the alert_light state changes to blinking 
|
| [[Image:NL5.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc6
| when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the mobile_unit beeps
|
| [[Image:NL6.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc7
| when the alert_light state changes to blinking, as long as the mobile_unit state is on and the user does not click the reset_alert_button, the alert_light state changes to on and one second elapses and the alert_light state changes to off and two seconds elapse 
| This requirement is not parsed in the current version of the NL play-in
| [[Image:Lsc7.jpg|thumb|left|LSC]]
|-
| Lsc8
| when the user clicks the baby_unit_power_button, the baby_unit state changes to on
|
| [[Image:NL8.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc9
| when the user clicks the mobile_unit_power_button, if the mobile_unit state is off, the mobile_unit state changes to on, otherwise if the mobile_unit state is on, the mobile_unit state changes to off
|
| [[Image:NL9.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc10
| 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
| This requirement is not parsed in the current version of the natural language play-in
| [[Image:Lsc10.jpg|thumb|left|LSC]]
|-
| Lsc11
| when the baby_unit state changes to on, as long as the mobile_unit state is on, the baby_unit connects to the mobile_unit and two seconds elapse
|
| [[Image:NL11.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc12
| when the baby_unit connects to the mobile_unit, the connection_light color changes to green 
|
| [[Image:NL12.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc13
| when the user clicks the reset_button, the baby_unit resets and the antenna position changes to close and the antenna init and the antenna position changes to open
|
| [[Image:NL13.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc14
| when the baby_unit resets, the baby_unit connects to the mobile_unit, the antenna position must be open
|
| [[Image:Lsc14.jpg|thumb|left|LSC]]
|}

   

== Download the Baby Monitor Example ==

Below are downloads of the wrist watch final application, as well as of the LSC project that can be opened and modified in PlayGo.

=== Baby Monitor final application (runnable jar) ===

[[Media:BabyMonitorExampleSwingGUI.zip|Runnable Baby Monitor with Swing GUI]] 

To run the baby monitor, simply extract the downloaded zip and double click the jar file.

=== Baby Monitor LSC project ===

[[Media:BabyMonitorSwing.zip|The Baby Monitor LSC Project (for development purposes)]] 

==== Installation Instructions ====

#Extract the downloaded zip.
#[[Download PlayGo|Download PlayGo]].
#Import the downloaded project to your workspace:
##From the File menu choose Import-->General-->Existing Projects into Workspace.
##Click the 'Next' button.
##When prompted, select the directory to which you extracted the downloaded baby monitor example.
##Click finish.
#The baby monitor 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]].

Baby Monitor Specification

2014-05-01T07:14:05Z

HarelAdmin:

The list below is the Baby Monitor system's requirements in [http://en.wikipedia.org/wiki/Controlled_natural_language controlled English]. These are valid requirements that can be used for [[PlayGo Feature List#Natural_Language_Play-in|NL play-in]]. 

== Requirements ==

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="10%" | LSC Name
! scope="col" width="50%" | Requirement in Natural Language Text
! scope="col" width="35" | Comments
! scope="col" width="5%" | LSC
|-
| Lsc1
| when the user clicks the increase_temperature_button, the temperature_threshold increases
| 
| [[Image:NL1.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc2
| when the user clicks the decrease_temperature_button, the temperature_threshold decreases
|
| [[Image:NL2.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc3
| when the user clicks a TempChange, the temperature_display color changes to yellow and the temperature_display displays the temperature_threshold value
|
| [[Image:NL3.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc4
| when the baby_unit temperature changes, the temperature_display displays the baby_unit temperature and the temperature_display color changes to green 
|
| [[Image:NL4.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc5
| when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the alert_light state changes to blinking 
|
| [[Image:NL5.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc6
| when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the mobile_unit beeps
|
| [[Image:NL6.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc7
| when the alert_light state changes to blinking, as long as the mobile_unit state is on and the user does not click the reset_alert_button, the alert_light state changes to on and one second elapses and the alert_light state changes to off and two seconds elapse 
| This requirement is not parsed in the current version of the NL play-in
| [[Image:Lsc7.jpg|thumb|left|LSC]]
|-
| Lsc8
| when the user clicks the baby_unit_power_button, the baby_unit state changes to on
|
| [[Image:NL8.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc9
| when the user clicks the mobile_unit_power_button, if the mobile_unit state is off, the mobile_unit state changes to on, otherwise if the mobile_unit state is on, the mobile_unit state changes to off
|
| [[Image:NL9.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc10
| 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
| This requirement is not parsed in the current version of the natural language play-in
| [[Image:Lsc10.jpg|thumb|left|LSC]]
|-
| Lsc11
| when the baby_unit state changes to on, as long as the mobile_unit state is on, the baby_unit connects to the mobile_unit and two seconds elapse
|
| [[Image:NL11.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc12
| when the baby_unit connects to the mobile_unit, the connection_light color changes to green 
|
| [[Image:NL12.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc13
| when the user clicks the reset_button, the baby_unit resets and the antenna position changes to close and the antenna init and the antenna position changes to open
|
| [[Image:NL13.jpg|thumb|left|80x50px|LSC]]
|-
| Lsc14
| when the baby_unit resets, the baby_unit connects to the mobile_unit, the antenna position must be open
|
| [[Image:Lsc14.jpg|thumb|left|LSC]]
|}

   

== Download the Baby Monitor Example ==

Below are downloads of the wrist watch final application, as well as of the LSC project that can be opened and modified in PlayGo.

=== Baby Monitor final application (runnable jar) ===

[[Media:BabyMonitorExampleSwingGUI.zip|Runnable Baby Monitor with Swing GUI]] 

To run the baby monitor, simply extract the downloaded zip and double click the jar file.

=== Baby Monitor LSC project ===

[[Media:BabyMonitorSwing.zip|The Baby Monitor LSC Project (for development purposes)]] 

==== Installation Instructions ====

#Extract the downloaded zip.
#[[Download PlayGo|Download PlayGo]].
#Import the downloaded project to your workspace:
##From the File menu choose Import-->General-->Existing Projects into Workspace.
##Click the 'Next' button.
##When prompted, select the directory to which you extracted the downloaded baby monitor example.
##Click finish.
#The baby monitor 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]].

PlayGo Examples

2014-05-01T07:12:14Z

HarelAdmin:

== Applications ==

=== Memory Game ===

[[Image:LSCExample.png|420px]][[Image:MemoryGameUI.png|400px]] 

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 are downloads of the memory game final application, as well as of the LSC project that can be opened and modified in PlayGo.

===== Memory game final application (runnable jar) =====

[[Media:MemoryGameSwingGUI.zip|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 =====

[[Media:MemoryGame.zip|The Memory Game LSC Project (for development purposes)]] 

====== Installation Instructions ======

#Extract the downloaded zip.
#[[Download PlayGo|Download PlayGo]].
#Import the downloaded project to your workspace:
##From the File menu choose Import-->General-->Existing Projects into Workspace.
##Click the 'Next' button.
##When prompted, select the directory to which you extracted the downloaded memory game example.
##Click finish.
#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]].

=== Baby Monitor ===

[[Image:BabyMonitor.Lsc12.jpg|frame|left]][[Image:BabyMonitor.png|235px]] 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 [[PlayGo_Feature_List#Natural_language_play-in|NL play-in]], and others by [[Language & Concepts#Play-In|basic play-in]]. To see the system's requirements in controlled English click [[Baby Monitor Specification|here]]. The Baby Monitor application is included in the workspace provided with the PlayGo download.

*[[Getting Started with PlayGo]]
*[[PlayGo HowTo...|PlayGo HowTo]]

=== Water Tap ===

[[Image:WaterTap.png|420px]][[Image:WaterTapUI.jpg|400px]] 

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

[[Media:WaterTap.zip|Download Water Tap application]] 
[[Instructions for creating LSC project from LSC file | Instructions for playing with the Water Tap application]]
 

=== Phone ===

[[Image:SampleLSC.png]][[Image:PhoneGUI.png|200px]] 

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. Details can be found [[Phone Specification|here]].

=== Wristwatch ===

[[Image:WristWatchGUI.jpg|230px]] 

The wristwatch application includes 20 LSCs, defining its behavior and demonstrating the use in [[PlayGo Feature List#Natural_Language_Play-in|NL play-in]]. Details about the specification and downloads can be found [[Wristwatch Example|here]].

=== Wall Painting ===

[[Image:drone.jpg|230px]] 

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):

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

The following LSCs describe valid behavior:

[[Image: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):

[[Image:BMustOccurUnlessC invalidBehavior.png]] 

[[Media:B_or_C_must_occur.zip|Download this design pattern]] [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Instructions_for_creating_LSC_project_from_LSC_file Instructions for playing with this specification]

File:Playgo-linux 2013-06-19.gtk.x86 64-with-java-6-openjdk-amd64.zip

2013-06-20T06:20:46Z

HarelAdmin:

Download PlayGo

2013-06-20T06:18:51Z

HarelAdmin: /* PlayGo for Linux */

== PlayGo for Windows ==

PlayGo download includes 2 parts: the PlayGo tool and a workspace with examples.

[[Media:playgo_ver1.4.4.zip | playgo_ver1.4.4.zip]]

[[Media:workspace_ver1.4.4.zip | workspace_ver1.4.4.zip]]

See the [[Getting Started with PlayGo]] to start playing with PlayGo.

== PlayGo for Linux ==

PlayGo download includes 2 parts: the PlayGo tool and a workspace with examples.

[[Media:playgo-linux_2013-06-19.gtk.x86_64-with-java-6-openjdk-amd64.zip | pplaygo-linux_2013-06-19.gtk.x86_64-with-java-6-openjdk-amd64.zip]]

[[Media:workspace.zip | workspace.zip]]

See the [[Getting Started with PlayGo]] to start playing with PlayGo.

File:Workspace.zip

2013-06-20T06:13:05Z

HarelAdmin:

Wristwatch Example

2013-02-28T07:53:16Z

HarelAdmin: Unprotected "Wristwatch Example"

The wristwatch example is taken from <ref>D. Harel. "On Visual Formalisms", Commun. ACM, 31(5):514–530, 1988.</ref>, and is a simplified version of the original statecharts watch example of <ref>D. Harel, "Statecharts: A Visual Formalism for Complex Systems", Sci. Comput. Programming 8, 231-274, 1987.</ref>. Generally, the watch displays the time and can switch between different displays that show (and allow changes to) the alarm, date, time and stopwatch. It has an option for turning on the light, and an alarm that beeps when the set time is reached. The following examples demonstrate many constructs in the LSC language and the way they were created in natural lanague play-in. The model was originally described in <ref>M. Gordon and D. Harel. Generating executable scenarios fromfckLRnatural language. In Proc. 10th Int. Conf. on Computational Linguistics and Intelligent Text Processing, CICLing’09, pages 456–467. Springer-Verlag, 2009.</ref>.

== Requirements ==

=== Watch Modes ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the user clicks 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".
| Demonstrates if-else.
| [[Image:WatchModes.png|thumb|left|x50px|LSC]]
|-
| when the user clicks 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".
|
| [[Image:Modes.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the c_button , if the display mode is "alarm" then the display mode changes to "alarm minutes" , otherwise if the display mode is "alarm minutes" then the display mode changes to "alarm hours" , otherwise if the display mode is "alarm hours" then the display mode changes to "alarm".
|
| [[Image:ModesAlarm.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the b_button, if the display mode is “alarm minutes”, the display mode changes to "alarm".
|
| [[Image:ModeAlarmEnd.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the b_button, if the display mode is “alarm hours” , the display mode changes to "alarm".
|
| [[Image:ModeAlarmHoursEnd.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the a_button , if the display mode is "alarm minutes" , the alarm increases in one minute , otherwise if the display mode is "alarm hours" , the alarm increases by one hour.
|
| [[Image:IncreaseTime.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the c_button , if the display mode is "time" , the display mode changes to "update" and the update type changes to "seconds".
|
| [[Image:UpdateSeconds.png|thumb|left|x50px|LSC]]
|}

=== Updates ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the user clicks the c_button , if the update type is "seconds" , the update type changes to "minutes" otherwise if the update type is "minutes" , the update type changes to "hours" otherwise if the update type is "hours" , the update type changes to "date" otherwise if the update type is "date", the display mode changes to "time" and the update type changes to "none".
|
| [[Image:UpdateType.png|thumb|left|x50px|LSC]]
|-
| when the update type changes , if the update type equals "seconds" , the display blinks seconds , otherwise if the update type equals "minutes" , the display blinks minutes , otherwise the display blinks none.
|
| [[Image:UpdateTypeBlink.png|thumb|left|x50px|LSC]]
|-
| when the update type changes, the display mode changes to "update".
|
| [[Image:UpdateTypeChange.png|thumb|left|x50px|LSC]]
|}

=== Time ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the clock ticks, the time increases by one second.
|
| [[Image:TimeTicks.png|thumb|left|x50px|LSC]]
|-
| when the time value changes, if the display mode is "time", the display text changes to time value.
| Demonstrates a property change as a trigger.
| [[Image:ShowTime.png|thumb|left|x50px|LSC]]
|}

=== Light ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the user clicks the b_button, if the light state is on , the light state turns to off , otherwise if the light state is off , the light state turns to on.
|
| [[Image:LightState.png|thumb|left|x50px|LSC]]
|}

 

=== Alarm ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the time value changes , if the time value equals the alarm value and the alarm state is enabled then the beeper state turns to on.
|
| [[Image:AlarmState.png|thumb|left|x50px|LSC]]
|-
| when the user clicks the d_button , if the display mode is "alarm" , if the alarm state is enabled , the alarm state changes to disabled otherwise the alarm state changes to enabled.
|
| [[Image:AlarmEnable.png|thumb|left|x50px|LSC]]
|-
| when the display mode changes , if the display mode equals "alarm minutes" , the display blinks minutes , otherwise if the display mode equals "alarm hours" , the display blinks hours , otherwise the display blinks none.
|
| [[Image:AlarmBlink.png|thumb|left|x50px|LSC]]
|-
| when the beeper state changes to on, as long as the beeper state is on and two seconds elapse, the beeper beeps, the display mode may not change.
| Demonstrates loop and forbidden element.
| [[Image:AlarmBeep.png|thumb|left|x50px|LSC]]
|-
| when the user clicks any WButton , the beeper state turns to off.
| Demonstrates symbolic \ non-deterministic objects.
| [[Image:AlarmOff.png|thumb|left|x50px|LSC]]
|-
| when the display mode changes to "alarm", the display text changes to the alarm value.
|
| [[Image:DisplayAlarm.png|thumb|left|x50px|LSC]]
|}

=== Date ===

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="70%" | Natural Language Text
! scope="col" width = "15%" | Comments
! scope="col" width="15%" | LSC
|-
| when the display mode changes to "date", the display text changes to the date value.
|
| [[Image:DisplayDate.png|thumb|left|x50px|LSC]]
|}

   

== Download the Wristwatch Example ==

Below are downloads of the wrist watch final application, as well as of the LSC project that can be opened and modified in PlayGo.

===Wristwatch final application (runnable jar)===
[[Media:WristWatchExampleSwingGUI.zip|Runnable Wrist Watch with Swing GUI]] [[Media:WristWatchExampleSystemModelGUI.zip|Runnable Wrist Watch with the auto generated System Model GUI]] 

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

===Wristwatch LSC project===
[[Media:WristWatch.zip|The Wrist Watch LSC Project (for development purposes)]] 
====Installation Instructions====
#Extract the downloaded zip.
#[[Download PlayGo|Download PlayGo]].
#Import the downloaded project to your workspace:
##From the File menu choose Import-->General-->Existing Projects into Workspace.
##Click the 'Next' button.
##When prompted, select the directory to which you extracted the downloaded wrist watch example.
##Click finish.
#The wrist watch 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]].

== References ==

<references />

Chess Game Example

2013-02-19T08:50:21Z

HarelAdmin: Protected "Chess Game Example" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

This is a protected page for the Chess Game Example.

PlayGo Examples

2013-01-06T11:22:40Z

HarelAdmin:

==Applications==
===Memory Game===
[[Image:LSCExample.png |frame|left]][[Image:MemoryGameUI.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 based on [http://code.google.com/webtoolkit/ GWT]. 
The memory game application demonstrates the following features: 
*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.
 
The memory game application is included in the workspace provided with the PlayGo download.
*[[Getting Started with PlayGo]]
*[[PlayGo_HowTo | PlayGo HowTo]]

===Baby Monitor===
[[Image:BabyMonitor.Lsc12.jpg |frame|left]][[Image:BabyMonitor.png|235px]] 
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 [[PlayGo_Feature_List#Natural_language_play-in | natural language play-in]], and others by [[Language & Concepts#Play-In |basic play-in]].
 To see the system's requirements in controlled English click [[Baby Monitor Specification | here]].
 
The Baby Monitor application is included in the workspace provided with the PlayGo download.

*[[Getting Started with PlayGo]]
*[[PlayGo_HowTo | PlayGo HowTo]]

===Water Tap===
[[Image:WaterTap.png | 420px]][[Image:WaterTapUI.jpg |400px]] 

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

[[Media:WaterTap.zip | Download Water Tap application]]
 
[[Instructions for creating LSC project from LSC file | Instructions for playing with the Water Tap application]]
 

===Wrist Watch===

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

Wristwatch Example

2013-01-06T11:22:18Z

HarelAdmin: Protected "Wrist Watch Example" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

Here we will add Michal's wrist watch example.

Should have a link from the Example Page.

Wristwatch Example

2013-01-06T11:22:05Z

HarelAdmin: New page: Here we will add Michal's wrist watch example. Should have a link from the Example Page.

Here we will add Michal's wrist watch example.

Should have a link from the Example Page.

PlayGo Examples

2013-01-06T11:21:31Z

HarelAdmin: /* Wrist Watch */

Baby Monitor Specification

2013-01-06T09:09:03Z

HarelAdmin: Unprotected "Baby Monitor Specification"

The list below is the Baby Monitor system's requirements in [http://en.wikipedia.org/wiki/Controlled_natural_language controlled English]. These are valid requirements that can be used for [[PlayGo_Feature_List#Natural_language_play-in|natural language play-in]]. 

#when the user clicks the increase_temperature_button, the temperature_threshold increases [[Media:NL1.jpg|View LSC]]
#when the user clicks the decrease_temperature_button, the temperature_threshold decreases [[Media:NL2.jpg|View LSC]]
#when the user clicks a change_temperature_button, the temperature_display color changes to yellow and the temperature_display displays the temperature_threshold value [[Media:NL3.jpg|View LSC]]
#when the baby_unit temperature changes, the temperature_display displays the baby_unit temperature and the temperature_display color changes to green [[Media:NL4.jpg|View LSC]]
#when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the alert_light state changes to blinking [[Media:NL5.jpg|View LSC]]
#when the baby_unit temperature changes, if the baby_unit temperature is greater than temperature_threshold, the mobile_unit beeps [[Media:NL6.jpg|View LSC]]
#when the alert_light state changes to blinking, as long as the mobile_unit state is on and the user does not click the reset_alert_button, the light state changes to on and one second elapses and the light state changes to off and two seconds elapse [[Media:Lsc7.jpg|View LSC]]
#when the user clicks the baby_unit_power_button, the baby_unit state changes to on [[Media:NL8.jpg|View LSC]]
#when the user clicks the mobile_unit_power_button, if the mobile_unit state is off, the mobile_unit state changes to on, otherwise if the mobile_unit state is on, the mobile_unit state changes to off [[Media:NL9.jpg|View LSC]]
#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 [[Media:Lsc10.jpg|View LSC]] *
#when the baby_unit state changes to on, as long as the mobile_unit state is on, the baby_unit connects to the mobile_unit and two seconds elapse [[Media:NL11.jpg|View LSC]]
#when the baby_unit connects to the mobile_unit, the connection_light color changes to green [[Media:NL12.jpg|View LSC]]
#when the user clicks the reset_button, the baby_unit resets and the antenna position changes to close and the antenna inits and the antenna position changes to open [[Media:NL13.jpg|View LSC]]
#when the baby_unit resets, the baby_unit connects to the mobile_unit, the antenna position must be open [[Media:Lsc14.jpg|View LSC]] *

* This requirement is not parsed in the current version of the natural language play-in

Baby Monitor Specification

2013-01-06T09:06:56Z

HarelAdmin: Protected "Baby Monitor Specification" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

Download PlayGo

2010-09-05T06:58:44Z

HarelAdmin: New page: PlayGo download contains the PlayGo tool as well as a workspace with examples. See the Getting Started with PlayGo to start playing with PlayGo.

PlayGo download contains the PlayGo tool as well as a workspace with examples.

See the [[Getting Started with PlayGo]] to start playing with PlayGo.

PlayGo

2010-09-05T06:55:45Z

HarelAdmin:

Welcome to PlayGo, a comprehensive tool for scenario-based programming, built around the language of [http://www.wisdom.weizmann.ac.il/~harel Live Sequence Charts (LSC)] and its Java derivative, and the Play-in/Play-out approach.

PlayGo is intended to constitute extensive support to the vision of [http://www.wisdom.weizmann.ac.il/~harel/papers/LiberatingProgramming.pdf Liberating Programming]

* [[About PlayGo]]
* [[PlayGo Screenshots]]
* [[PlayGo Demos]]
* [[Download PlayGo]]
* [[Getting Started with PlayGo]]

== Related Tools ==
* [[The Tracer]], a prototype tool for scenario-based trace visualization and exploration.
* [[S2A]], a compiler for multi-modal UML sequence diagrams.

== Contact Information ==
E-mail us to: [mailto:playgo@weizmann.ac.il playgo@weizmann.ac.il]

PlayGo

2010-09-03T06:20:01Z

HarelAdmin: Main Page moved to PlayGo

== Getting Started with PlayGo ==

*[[Install PlayGo]]
*[[Run PlayGo with the Provided Workspace]]
*[[Create Your First LSC Project]]

Main Page

2010-09-03T06:20:01Z

HarelAdmin: Main Page moved to PlayGo

#REDIRECT [[PlayGo]]