WeizmannWiki - User contributions [en]

PlayGo Feature List

2014-04-30T15:45:22Z

Yaaritn: /* Java API for LSC Creation */

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

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.

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

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

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

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

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 <ref>S. Maoz and Y. Sa’ar, “Counter Play-Out: Executing Unrealizable Scenario-Based Specifications,” to appear in ICSE'13 (2013)</ref>.

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

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. 

[http://www.youtube.com/watch?v=dDSszMjanXs 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 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 <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 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>.

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

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

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

 [[Image:Tracer.png|800px|A trace of a pacman game in the Tracer tool]]

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

[[Image:TraceVis.png|800px|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.

[[Image:SIVExample.png|800px|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:

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

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

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

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>void createMemoryGameMoveLSC()
{

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

} </big></code>

 

This code represents the LSC shown in the figure below: 

[[Image:LSCExample.png|frame|left|An LSC describing the basic rule of a memory game]] 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

[[Java API|More about Java API]]

== References ==

<references />

Baby Monitor Specification

2014-03-11T13:44:08Z

Yaaritn: /* Requirements */

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 Features 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-03-11T13:40:06Z

Yaaritn: /* Requirements */

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 Features 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 change_temperature_button, 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]].

File:WteKingPosition.png

2014-03-11T13:32:48Z

Yaaritn: uploaded a new version of "Image:WteKingPosition.png": replace image, the previous image used object square instead of class Square

File:BlkKingPosition.png

2014-03-11T13:29:20Z

Yaaritn: uploaded a new version of "Image:BlkKingPosition.png": replace image, previous image uses object square instead of class Square

Chess Game Example

2014-03-11T13:20:42Z

Yaaritn: /* Example 1 with NL-Play-In */

This is a protected page for the Chess Game Example.

The '''chess game example''' demonstrates the creation of a chess game for two-players. Chess game has many rules which we have implemented in this example, see [[http://en.wikipedia.org/wiki/Chess chess]]. On his turn, the user plays by mouse clicking the game pieces and the chess board's squares. A click on a square highlights valid user moves for the selected piece. The game GUI is implemented with [http://en.wikipedia.org/wiki/Swing_(Java) Swing], and the game behavior is implemented with LSCs. This example demonstrates LSCs creation in two different ways, which also generates different LSCs: 
# Using the [[PlayGo_Feature_List#Natural_language_play-in | natural language interface to LSCs]] (NL-Play-In).
# Using the LSC Editor. 

== Game Board ==

[[Image:ChessGUIScreenShot.png]]

 

 

== Example 1 with NL-Play-In ==

The LSCs in this section were created using [[PlayGo Feature List#Natural_language_play-in|NL-Play-In]].

 

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="15%" | Name
! scope="col" width="70%" | Requirement in Natural Language Text
! scope="col" width="15%" | LSC
|-
| SelectSource
| when the user clicks any Square, if the board sourcetargetValue is "0" and the Square type is not "vacent" then the Square selectSource and the board sourcetargetValue changes to "1". 
|
[[Image:SelectSource.png|thumb|left|LSC]]

|-
| SetPossiblePosition
| when any Square selectSource then the Square setPossibleSquares .  
|
[[Image:SetPossiblePositionNL.png|thumb|left|LSC]]

|-
| SelectTarget
| when the user clicks any Square, if the board sourcetargetValue is "1" then the Square selectTarget and the board sourcetargetValue changes to "0". 
|
[[Image:SelectTarget.png|thumb|left|LSC]]

|-
| CheckPossibility
| when any Square selectTarget then the Square checkPossibility.  
|
[[Image:CheckPossibility.png|thumb|left|LSC]]

|-
| MovePiece
| when any Square checkPossibility, if the Square possibility is "true" then the Square MovePiece.  
|
[[Image:MoveSource.png|thumb|left|LSC]]

|-
| ChangeTurn
| when any Square MovePiece, if the board state is "black" then the board state changes to "white" otherwise if the board state is "white" then the board state changes to "black" .  
|
[[Image:TurnChange.png|thumb|left|LSC]]

|-
| WrongTurn
| when any Square selectSource, if the Square type is "black" and the board state is "white" then the Square showMessage.  
|
[[Image:WrongTurn1.png|thumb|left|LSC]]

|-
| WrongTurn2
| when any Square selectSource, if the Square type is "white" and the board state is "black" then the Square showMessage.  
|
[[Image:WrongTurn2.png|thumb|left|LSC]]

|-
| ResetBoard
| when any Square showMessage then the board sourcetargetValue changes to "0".  
|
[[Image:ResetBoard.png|thumb|left|LSC]]

|-
| checkmate
| when any Square MovePiece then the Square check_CheckMate  
|
[[Image:Checkmate-NL.png|thumb|left|LSC]]

|-
| BlkKingPosition
| when any Square MovePiece, if the Square piecename is "blkking" then the board BlkkingPosition changes to the Square position 
|
[[Image:BlkKingPosition.png|thumb|left|LSC]]

|-
| WteKingPosition
| when any Square MovePiece, if the Square piecename is "wteking" then the board WtekingPosition changes to the Square position  
|
[[Image:WteKingPosition.png|thumb|left|LSC]]

|-
| Newgame
| when the user click the newgame then the newgame loadnewgame and the board reset  
|
[[Image:NewGame.png|thumb|left|LSC]]

|-
| ShowScoreblack
| when the board state change then the BlkScore show the board blackPoint  
|
[[Image:ShowScoreblack.png|thumb|left|LSC]]

|-
| ShowScorewhite
| when the board state change then the WteScore show the board whitePoint  
|
[[Image:ShowScorewhite.png|thumb|left|LSC]]

|-
| ShowNextTurn
| when the board state change then the NextTurndisplay show the board state  
| [[Image:ShowNextTurn.png|thumb|left|LSC]]
|-
| ResetPossiblePosition
| when any Square selectTarget then the Square reset  
| [[Image:ResrPossiblePositionNL.png|thumb|left|LSC]]
|-
| WrongTurnReset
| when any Square showMessage then the Square reset  
| [[Image:WrongTurnReset.png|thumb|left|LSC]]
|}

    

=== Download the ChessProject Example ===

Below are links for downloading the ChessProject final application, as well as the LSC project that can be opened and modified in PlayGo. 

==== ChessProject final application (runnable jar) ====

[[Media:ChessProjectSwingGUI.zip|Runnable ChessProject with Swing GUI]] To run the ChessProject, simply extract the downloaded zip and double click the jar file.  

==== ChessProject LSC project ====

[[Media:ChessProject.zip|The ChessProject 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 ChessProject example.
##Click finish.
#The ChessProject 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]].

== Example 2 ==

The following LSCs were created using the LSC editor. Our intention was to create a specification with more than one symbolic lifeline in the LSCs, which was not supported by NL-Play-In.

 

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="15%" | Name
! scope="col" width="70%" | Requirement
! scope="col" width="15%" | LSC
|-
| PieceClick
| When the user click any square Sq1, and then click any square Sq2, if the board next turn is equals to the Sq1 piece type and if the Sq1 is a source then the square Sq1 check_Move square Sq2. 
|
[[Image:ClickonPiece.png|thumb|left|LSC]]

|-
| MovePiece
| When a square Sq1 check_Move square Sq2, canmove is assigned with whether the movement of piece from square Sq1 to Sq2 is possible,  if the piece canmove and Sq1 piecetype is not equals to Sq2 piecetype then the square Sq1 move_Piece to square Sq2.
| [[Image:MovePiece.png|thumb|left|LSC]]
|-
| Square RemovePiece
| When the square Sq1 move_Piece to square Sq2,  then the square Sq2 emptyPiece the square Sq2.
| [[Image:RemovePiece.png|thumb|left|LSC]]
|-
| NextMove
| When the square Sq1 move_Piece to square Sq2, if the board next turn is "white" the board next turn changes to "black" otherwise if the board next turn is "black" the board next turn changes to "white".
| [[Image:NextMove.png|thumb|left|LSC]]
|-
| SetSource
| When the user click any square Sq1, if the Issource is "empty" then the square Sq1's possible positions are set and the IsSource changes to "set".  
| [[Image:SetSource.png|thumb|left|LSC]]
|-
| ShowMessage
| When the user click any square Sq1, if the square IsSource is "empty" and the board next turn not equals the Sq1 piecetype then the square showmessage and the Issource is set to "empty".
| [[Image:ShowMessage.png|thumb|left|LSC]]
|-
| ShowMessageReset
| When the user click any square Sq1, if the square IsSource is "empty" and the board next turn not equals the Sq1 piecetype then the square showmessage and the Issource is set to "empty".
| [[Image:ShowmessageReset.jpg|thumb|left|LSC]]
|-
| ResetPossiblePosition
| When the user click any square Sq1, the square Sq1 setPossiblePosition and the user click any other square Sq2 then the Sq2 resetPossiblePosition of the Sq1.
| [[Image:ResetPossiblePosition.png|thumb|left|LSC]]
|-
| CheckMate
| When the any square Sq2 emptypiece any square Sq1, then isCheck is assigned whether there is any checkmate, if the checkmate is true then the square show the checkmate otherwise square removecheckmate.
| [[Image:Checkmate.png|thumb|left|LSC]]
|-
| kingposition
| When the any square Sq2 emptypiece any square Sq1, if the Sq2 piecname is wteking then the Sq1 removecheckMate and the board wtekingposition is set to the Sq2 position else if the Sq2 piecname is blkking then the Sq1 removecheckMate and the board blkkingposition is set to the Sq2 position .
| [[Image:Kingposition.png|thumb|left|LSC]]
|-
| showturn
| When the board set the Next_turn to any then the NextTurn show the board Next turn.
| [[Image:Showturn.png|thumb|left|LSC]]
|-
| BlackPiecepoint
| When the any square Sq2 emptypiece any square Sq1, if the board Next_turn is white then the blk_score show the black point.
| [[Image:Blackpiecepoint.png|thumb|left|LSC]]
|-
| WhitePiecepoint
| When the any square Sq2 emptypiece any square Sq1, if the board Next_turn is black then the wte_score show the white point.
| [[Image:Whitepiecepoint.png|thumb|left|LSC]]
|-
| GameOver
| When the any square Sq1 movePiece to any square Sq2, if the board black point is 0 then the white won the game otherwise if the board white point is 0 then the black won the game
| [[Image:GameOver.png|thumb|left|LSC]]
|-
| Loadgame
| when the user click NewGame then the NewGame load new game
| [[Image:LoadGame.png|thumb|left|LSC]]
|}

   

=== Download the ChessGame Example ===

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

==== ChessGame final application (runnable jar) ====

[[Media:ChessGameSwingGUI.zip|Runnable Chess Game with Swing GUI]] To run the ChessGame, simply extract the downloaded zip and double click the jar file.  

==== ChessGame LSC project ====

[[Media:ChessGame.zip|The ChessGame 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 ChessGame example.
##Click finish.
#The ChessGame 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]].

 

== Graph and Connections ==

'''Example1-ChessProject'''   [[Image:SivChessGame.png|SIV Graph]] Dependency graph for example #1. This graph shows clusters (communities). The LSC MovePiece is selected here and the connected LSCs are colored (blue or pink). Green edges indicate unified messages between LSCs. For details, see [[http://www.weizmann.ac.il/mediawiki/harelgroup/index.php/SIV_Plugin | SIV-Plugin]].   

'''Example2-ChessGame'''   [[Image:ChessSIV-example2.png|SIV Graph]] Dependency graph for example #2. This graph shows clusters (communities). The LSC MovePiece is selected here and the connected LSCs are colored (blue or pink). Green edges indicate unified messages between LSCs. Note: messages were unified here regardless of the parameters, since parameters are symbolic, e.g., MovePiece(String piecename). For details, see[[http://www.weizmann.ac.il/mediawiki/harelgroup/index.php/SIV_Plugin | SIV-Plugin]].

   

== SystemModel ==

   Example1-ChessProject  [[Image:ChessProjectSystemModel.png|SystemModel]]   Example2-ChessGame  [[Image:ChessGameSystemmodel.png|System Model]]

Chess Game Example

2014-03-10T11:39:09Z

Yaaritn: /* Example 1 with NL-Play-In */

This is a protected page for the Chess Game Example.

The '''chess game example''' demonstrates the creation of a chess game for two-players. Chess game has many rules which we have implemented in this example, see [[http://en.wikipedia.org/wiki/Chess chess]]. On his turn, the user plays by mouse clicking the game pieces and the chess board's squares. A click on a square highlights valid user moves for the selected piece. The game GUI is implemented with [http://en.wikipedia.org/wiki/Swing_(Java) Swing], and the game behavior is implemented with LSCs. This example demonstrates LSCs creation in two different ways, which also generates different LSCs: 
# Using the [[PlayGo_Feature_List#Natural_language_play-in | natural language interface to LSCs]] (NL-Play-In).
# Using the LSC Editor. 

== Game Board ==

[[Image:ChessGUIScreenShot.png]]

 

 

== Example 1 with NL-Play-In ==

The LSCs in this section were created using [[PlayGo Feature List#Natural_language_play-in|NL-Play-In]].

 

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="15%" | Name
! scope="col" width="70%" | Requirement in Natural Language Text
! scope="col" width="15%" | LSC
|-
| SelectSource
| when the user clicks any Square, if the board sourcetargetValue is "0" and the Square type is not "vacent" then the Square selectSource and the board sourcetargetValue changes to "1". 
|
[[Image:SelectSource.png|thumb|left|LSC]]

|-
| SetPossiblePosition
| when any Square selectSource then the Square setPossibleSquares .  
|
[[Image:SetPossiblePositionNL.png|thumb|left|LSC]]

|-
| SelectTarget
| when the user clicks any Square, if the board sourcetargetValue is "1" then the Square selectTarget and the board sourcetargetValue changes to "0". 
|
[[Image:SelectTarget.png|thumb|left|LSC]]

|-
| CheckPossibility
| when any Square selectTarget then the Square checkPossibility.  
|
[[Image:CheckPossibility.png|thumb|left|LSC]]

|-
| MovePiece
| when any Square checkPossibility, if the Square possibility is "true" then the Square MovePiece.  
|
[[Image:MoveSource.png|thumb|left|LSC]]

|-
| ChangeTurn
| when any Square MovePiece, if the board state is "black" then the board state changes to "white" otherwise if the board state is "white" then the board state changes to "black" .  
|
[[Image:TurnChange.png|thumb|left|LSC]]

|-
| WrongTurn
| when any Square selectSource, if the Square type is "black" and the board state is "white" then the Square showMessage.  
|
[[Image:WrongTurn1.png|thumb|left|LSC]]

|-
| WrongTurn2
| when any Square selectSource, if the Square type is "white" and the board state is "black" then the Square showMessage.  
|
[[Image:WrongTurn2.png|thumb|left|LSC]]

|-
| ResetBoard
| when any Square showMessage then the board sourcetargetValue changes to "0".  
|
[[Image:ResetBoard.png|thumb|left|LSC]]

|-
| checkmate
| when any Square MovePiece then the Square check_CheckMate  
|
[[Image:Checkmate-NL.png|thumb|left|LSC]]

|-
| BlkKingPosition.png
| when any Square MovePiece, if the Square piecename is "blkking" then the board BlkkingPosition changes to the Square position 
|
[[Image:BlkKingPosition.png|thumb|left|LSC]]

|-
| WteKingPosition
| when any Square MovePiece, if the Square piecename is "wteking" then the board WtekingPosition changes to the Square position  
|
[[Image:WteKingPosition.png|thumb|left|LSC]]

|-
| Newgame
| when the user click the newgame then the newgame loadnewgame and the board reset  
|
[[Image:NewGame.png|thumb|left|LSC]]

|-
| ShowScoreblack
| when the board state change then the BlkScore show the board blackPoint  
|
[[Image:ShowScoreblack.png|thumb|left|LSC]]

|-
| ShowScorewhite
| when the board state change then the WteScore show the board whitePoint  
|
[[Image:ShowScorewhite.png|thumb|left|LSC]]

|-
| ShowNextTurn
| when the board state change then the NextTurndisplay show the board state  
| [[Image:ShowNextTurn.png|thumb|left|LSC]]
|-
| ResetPossiblePosition
| when any Square selectTarget then the Square reset  
| [[Image:ResrPossiblePositionNL.png|thumb|left|LSC]]
|-
| WrongTurnReset
| when any Square showMessage then the Square reset  
| [[Image:WrongTurnReset.png|thumb|left|LSC]]
|}

    

=== Download the ChessProject Example ===

Below are links for downloading the ChessProject final application, as well as the LSC project that can be opened and modified in PlayGo. 

==== ChessProject final application (runnable jar) ====

[[Media:ChessProjectSwingGUI.zip|Runnable ChessProject with Swing GUI]] To run the ChessProject, simply extract the downloaded zip and double click the jar file.  

==== ChessProject LSC project ====

[[Media:ChessProject.zip|The ChessProject 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 ChessProject example.
##Click finish.
#The ChessProject 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]].

== Example 2 ==

The following LSCs were created using the LSC editor. Our intention was to create a specification with more than one symbolic lifeline in the LSCs, which was not supported by NL-Play-In.

 

{| width="100%" border="1" align="left" cellpadding="1" cellspacing="1"
|-
! scope="col" width="15%" | Name
! scope="col" width="70%" | Requirement
! scope="col" width="15%" | LSC
|-
| PieceClick
| When the user click any square Sq1, and then click any square Sq2, if the board next turn is equals to the Sq1 piece type and if the Sq1 is a source then the square Sq1 check_Move square Sq2. 
|
[[Image:ClickonPiece.png|thumb|left|LSC]]

|-
| MovePiece
| When a square Sq1 check_Move square Sq2, canmove is assigned with whether the movement of piece from square Sq1 to Sq2 is possible,  if the piece canmove and Sq1 piecetype is not equals to Sq2 piecetype then the square Sq1 move_Piece to square Sq2.
| [[Image:MovePiece.png|thumb|left|LSC]]
|-
| Square RemovePiece
| When the square Sq1 move_Piece to square Sq2,  then the square Sq2 emptyPiece the square Sq2.
| [[Image:RemovePiece.png|thumb|left|LSC]]
|-
| NextMove
| When the square Sq1 move_Piece to square Sq2, if the board next turn is "white" the board next turn changes to "black" otherwise if the board next turn is "black" the board next turn changes to "white".
| [[Image:NextMove.png|thumb|left|LSC]]
|-
| SetSource
| When the user click any square Sq1, if the Issource is "empty" then the square Sq1's possible positions are set and the IsSource changes to "set".  
| [[Image:SetSource.png|thumb|left|LSC]]
|-
| ShowMessage
| When the user click any square Sq1, if the square IsSource is "empty" and the board next turn not equals the Sq1 piecetype then the square showmessage and the Issource is set to "empty".
| [[Image:ShowMessage.png|thumb|left|LSC]]
|-
| ShowMessageReset
| When the user click any square Sq1, if the square IsSource is "empty" and the board next turn not equals the Sq1 piecetype then the square showmessage and the Issource is set to "empty".
| [[Image:ShowmessageReset.jpg|thumb|left|LSC]]
|-
| ResetPossiblePosition
| When the user click any square Sq1, the square Sq1 setPossiblePosition and the user click any other square Sq2 then the Sq2 resetPossiblePosition of the Sq1.
| [[Image:ResetPossiblePosition.png|thumb|left|LSC]]
|-
| CheckMate
| When the any square Sq2 emptypiece any square Sq1, then isCheck is assigned whether there is any checkmate, if the checkmate is true then the square show the checkmate otherwise square removecheckmate.
| [[Image:Checkmate.png|thumb|left|LSC]]
|-
| kingposition
| When the any square Sq2 emptypiece any square Sq1, if the Sq2 piecname is wteking then the Sq1 removecheckMate and the board wtekingposition is set to the Sq2 position else if the Sq2 piecname is blkking then the Sq1 removecheckMate and the board blkkingposition is set to the Sq2 position .
| [[Image:Kingposition.png|thumb|left|LSC]]
|-
| showturn
| When the board set the Next_turn to any then the NextTurn show the board Next turn.
| [[Image:Showturn.png|thumb|left|LSC]]
|-
| BlackPiecepoint
| When the any square Sq2 emptypiece any square Sq1, if the board Next_turn is white then the blk_score show the black point.
| [[Image:Blackpiecepoint.png|thumb|left|LSC]]
|-
| WhitePiecepoint
| When the any square Sq2 emptypiece any square Sq1, if the board Next_turn is black then the wte_score show the white point.
| [[Image:Whitepiecepoint.png|thumb|left|LSC]]
|-
| GameOver
| When the any square Sq1 movePiece to any square Sq2, if the board black point is 0 then the white won the game otherwise if the board white point is 0 then the black won the game
| [[Image:GameOver.png|thumb|left|LSC]]
|-
| Loadgame
| when the user click NewGame then the NewGame load new game
| [[Image:LoadGame.png|thumb|left|LSC]]
|}

   

=== Download the ChessGame Example ===

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

==== ChessGame final application (runnable jar) ====

[[Media:ChessGameSwingGUI.zip|Runnable Chess Game with Swing GUI]] To run the ChessGame, simply extract the downloaded zip and double click the jar file.  

==== ChessGame LSC project ====

[[Media:ChessGame.zip|The ChessGame 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 ChessGame example.
##Click finish.
#The ChessGame 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]].

 

== Graph and Connections ==

'''Example1-ChessProject'''   [[Image:SivChessGame.png|SIV Graph]] Dependency graph for example #1. This graph shows clusters (communities). The LSC MovePiece is selected here and the connected LSCs are colored (blue or pink). Green edges indicate unified messages between LSCs. For details, see [[http://www.weizmann.ac.il/mediawiki/harelgroup/index.php/SIV_Plugin | SIV-Plugin]].   

'''Example2-ChessGame'''   [[Image:ChessSIV-example2.png|SIV Graph]] Dependency graph for example #2. This graph shows clusters (communities). The LSC MovePiece is selected here and the connected LSCs are colored (blue or pink). Green edges indicate unified messages between LSCs. Note: messages were unified here regardless of the parameters, since parameters are symbolic, e.g., MovePiece(String piecename). For details, see[[http://www.weizmann.ac.il/mediawiki/harelgroup/index.php/SIV_Plugin | SIV-Plugin]].

   

== SystemModel ==

   Example1-ChessProject  [[Image:ChessProjectSystemModel.png|SystemModel]]   Example2-ChessGame  [[Image:ChessGameSystemmodel.png|System Model]]

PlayGo

2012-07-08T21:46:53Z

Yaaritn:

Welcome to PlayGo, a comprehensive tool for behavioral, scenario-based, programming, built around the language of [[live sequence charts| ''live sequence charts'' (LSC)]] and its Java derivative, and the play-in/play-out methods for programming and execution.

PlayGo is intended to provide extensive support for the vision of [http://www.wisdom.weizmann.ac.il/~harel/papers/LiberatingProgramming.pdf "liberating programming"]

A description of the LSC language and the basic research underlying PlayGo can
be found in [http://www.wisdom.weizmann.ac.il/~playbook/Updates/ComeLetsPlay.pdf D. Harel and R. Marelly, ''Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine''].
 For more information about the principles of behavioral programming, which were originally part of the basis of LSC, and for links to the implementations of behavioral programming in Java and Erlang, see [http://www.b-prog.org www.b-prog.org].

* [[About PlayGo]]
* [[Language & Concepts]]
* [[PlayGo Feature List]]
* [[PlayGo Screenshots]]
* [[PlayGo Demos]]
* [[PlayGo Examples]]
* [[Download PlayGo]]
* [[Getting Started with PlayGo]]
* [[PlayGo HowTo | PlayGo HowTo...]]

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

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