BP Wiki - User contributions [en]

Helicopter flight and mission

2014-05-20T07:32:35Z

BpAdmin: /* Downloads */

= Helicopter Flight Examples =
The examples below demonstrates the control of a toy helicopter - AR DRONE by Parrot Inc.

= Basic Composite Behavior =
The following movies show flight of the helicopter, as well as simulation. The flight was generated by independent concurrent LSCs - where one directs the helicopter through a rectangular flight path without changing altitude, and another directs the helicopter to go up and down without changing its horizontal location. The result is a composite motion, traveling the prescribed path while going up and down.

{{#ev:youtube|nMTbQc_iq5Y|640}}

{{#ev:youtube|sMp8QTetobc|640}}

= Detailed Example: Wall Painting =
In this example, the mission here is to paint a wall with different colors. This can be considered as an analogy to a photography mission where a particular area as to be covered.

The example is implemented with a simulator.

Below we describe the requirements and the associated b-threads, along with screen images and a movie of the helicopter behavior as it evolves with the addition of new b-threads.

== Requirements==
The requirements below were added incrementally, and b-threads were added to deal with each requirement. In the simulator - the painting of the wall is by drawing a line on the screen.

*The helicopter should go up and down along the wall.
*When the helicopter reaches the ceiling or the floor it should move to the right
*Every fixed number of pixels the paint color should be changed
*Since the line drawn by the helicopter is thin, after every small vertical move, the helicopter should move right and left with horizontal brush strokes, before moving vertically again.
*The helicopter may move from its present location due to wind.
*If the helicopter is moved by wind, it should return to its last known location.

In the integration with LSC, two more requirements were added
*The amount of paint is limited. After a certain number of points is painted - the paint runs out.
*When paint of a certain color runs out, this color can no longer be used.
*When all paint colors run out, the helicopter must stop.
*Paint cans may be re-filled. This is simulated by a user clicking on a button on the screen.

== Events ==

== General control events ==
* BeginPainting: Start the painting process
* StopPainting: End the painting process
* MoveDown: Move down a fixed number of pixels.
* EndOfColUp: End painting wall going up
* DoColDownL Start painting wall going down
* EndOfColDown: End painting wall going up
* DoRowRight: Start painting wall going right
* EndOfRowRight: Stop moving right.
* ChangeColor: This is an event class of which there are four events, indicating a request to change the painting color to the corresponding one in the event name:
** eChangeColorBLACK
** eChangeColorRED
** eChangeColorBLUE
** eChangeColorGreen
* UpdateArrived: simulate information from a GPS with actual helicopter location

=== Move Events ===

The following events indicate the desire to move a fixed number of pixels in the desired direction. These events have a data field - indicating whether the movement is for a mission or for maintenance, which serves in correcting wind shifts.

* MoveUp: Move down a fixed number of pixels
* MoveDown: Move down a fixed number of pixels
* MoveLeft: Move left a fixed number of pixels
* MoveRight: Move right a fixed number of pixels

== BPJ b-threads ==

=== General control b-threads ===
* DoColD2U: Controls coloring in the up direction;
* YAxis: Reports when helicopter reaches top or bottom end of wall (ceiling of floor)
* EndColUp: Handle reaching of ceiling. Stop moving vertically, start moving right.
* DoRowL2R: Left to right painting - waits for DoRowRight and then repeatedly requests movement to the right until end of right movement is reached.
* XAxis: Monitor horizontal coordinates. Report reaching of right and left borders of wall, and report end of movement right to start a new column
* DoColU2D: Controls coloring in the up direction
* EndColDown: Handles reaching the floor - requests a movement to the right
* BrushMove: Move the brush right and left (horizontal moves) to create a thicker line and paint continuous area. This b-thread performs its actions between any two vertical moves.

=== Actuator b-threads ===

The following b-threads wait for the corresponding move event and call the helicopter API (or the simulator) to cause the actual movement.
* MovingRight
* MovingLeft
* MovingDown
* MovingUp

=== Color control b-threads ===
* ChangePaintingColor: Waits for the need to change color and changes the color randomly.

=== Location correction b-threads ===
* FixWind: When a report comes in that the helicopter is not where it is supposed to be - stop painting movement and return to last known location.

=== Environment Simulation ===

* ColorControl: Counts movements and announces the need to change color.
* Wind: Every certain random number of steps, report a random location of the helicopter

= Incremental Development Notes =

{{#ev:youtube|6cSqPGvRWw0|640}}

With only basic movements and no color change b-threads:

[[Image: Black - thin.jpg]]

Basic movements with color changes:

[[Image: Color-thin.jpg]]

Adding horizontal brush movements:

[[Image: Color-thick.jpg]]

Random movements due to wind, and return by horizontal movement and then vertical to last known location:

[[Image: FixWind.jpg]]

= LSC Integration =

The BPJ-based system was then integrated with the LSC language via PlayGo.
For details how to integrate a BPJ application with LSC see a separate section in this documentation.

The following LSC (scenario) was added

* PaintCanEmpty: Waits for a certain number of movements with a given color and block subsequent changes to that color, simulating and empty can, until an event of PaintFilled arrives. This event is generated by the user clicking on a corresponding GUI Button.

= Design Notes =

The following design patterns and choices can be seen throughout the example.

* Events can be distinguishes from each other by
** Class - different classes of events
** Name - multiple instances of an events of the same class distinguished by their name (e.g. the color change events).
** Data field - Two instances of events of the same class, with arbitrary names can be distinguished by a value in one of the event data fields (e.g. the maintenance vs. mission indicator in the move events).

* One activity can interfere with another by using
** priority - (relative priority among b-thread)
** blocking the events of the other activity (which can be distinguished as described above)

* Distinguishing internal and external events - those generated by the system/application and those generated by the environment (and which may be reported by sensors).

** External events should not be blocked (enforced by convention only).
** When external events are produced by simulator, the concepts of Logical Execution Time should be enforced by convention, where all internal events reacting to the last external event should be processed before generating the next external event.

= Download =
== Download the wall painting example ==
# Click [[Media:Helicopter.zip | here]] to download the wall painting example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The helicopter example projects are now part of your workspace.
### The example includes three projects:
#### BDrone - The main project that includes the b-threads that implement the drawing/scanning tasks.
#### HeliSim - A simple java-based simulator.
#### il.ac.wis.cs.rovtool.blender - A blender-based simulator.
##Refer to the BDrone/HowToRun.txt file for execution instructions.

Helicopter flight and mission

2014-05-20T07:26:53Z

BpAdmin: /* Download */

= Helicopter Flight Examples =
The examples below demonstrates the control of a toy helicopter - AR DRONE by Parrot Inc.

= Basic Composite Behavior =
The following movies show flight of the helicopter, as well as simulation. The flight was generated by independent concurrent LSCs - where one directs the helicopter through a rectangular flight path without changing altitude, and another directs the helicopter to go up and down without changing its horizontal location. The result is a composite motion, traveling the prescribed path while going up and down.

{{#ev:youtube|nMTbQc_iq5Y|640}}

{{#ev:youtube|sMp8QTetobc|640}}

= Detailed Example: Wall Painting =
In this example, the mission here is to paint a wall with different colors. This can be considered as an analogy to a photography mission where a particular area as to be covered.

The example is implemented with a simulator.

Below we describe the requirements and the associated b-threads, along with screen images and a movie of the helicopter behavior as it evolves with the addition of new b-threads.

== Requirements==
The requirements below were added incrementally, and b-threads were added to deal with each requirement. In the simulator - the painting of the wall is by drawing a line on the screen.

*The helicopter should go up and down along the wall.
*When the helicopter reaches the ceiling or the floor it should move to the right
*Every fixed number of pixels the paint color should be changed
*Since the line drawn by the helicopter is thin, after every small vertical move, the helicopter should move right and left with horizontal brush strokes, before moving vertically again.
*The helicopter may move from its present location due to wind.
*If the helicopter is moved by wind, it should return to its last known location.

In the integration with LSC, two more requirements were added
*The amount of paint is limited. After a certain number of points is painted - the paint runs out.
*When paint of a certain color runs out, this color can no longer be used.
*When all paint colors run out, the helicopter must stop.
*Paint cans may be re-filled. This is simulated by a user clicking on a button on the screen.

== Events ==

== General control events ==
* BeginPainting: Start the painting process
* StopPainting: End the painting process
* MoveDown: Move down a fixed number of pixels.
* EndOfColUp: End painting wall going up
* DoColDownL Start painting wall going down
* EndOfColDown: End painting wall going up
* DoRowRight: Start painting wall going right
* EndOfRowRight: Stop moving right.
* ChangeColor: This is an event class of which there are four events, indicating a request to change the painting color to the corresponding one in the event name:
** eChangeColorBLACK
** eChangeColorRED
** eChangeColorBLUE
** eChangeColorGreen
* UpdateArrived: simulate information from a GPS with actual helicopter location

=== Move Events ===

The following events indicate the desire to move a fixed number of pixels in the desired direction. These events have a data field - indicating whether the movement is for a mission or for maintenance, which serves in correcting wind shifts.

* MoveUp: Move down a fixed number of pixels
* MoveDown: Move down a fixed number of pixels
* MoveLeft: Move left a fixed number of pixels
* MoveRight: Move right a fixed number of pixels

== BPJ b-threads ==

=== General control b-threads ===
* DoColD2U: Controls coloring in the up direction;
* YAxis: Reports when helicopter reaches top or bottom end of wall (ceiling of floor)
* EndColUp: Handle reaching of ceiling. Stop moving vertically, start moving right.
* DoRowL2R: Left to right painting - waits for DoRowRight and then repeatedly requests movement to the right until end of right movement is reached.
* XAxis: Monitor horizontal coordinates. Report reaching of right and left borders of wall, and report end of movement right to start a new column
* DoColU2D: Controls coloring in the up direction
* EndColDown: Handles reaching the floor - requests a movement to the right
* BrushMove: Move the brush right and left (horizontal moves) to create a thicker line and paint continuous area. This b-thread performs its actions between any two vertical moves.

=== Actuator b-threads ===

The following b-threads wait for the corresponding move event and call the helicopter API (or the simulator) to cause the actual movement.
* MovingRight
* MovingLeft
* MovingDown
* MovingUp

=== Color control b-threads ===
* ChangePaintingColor: Waits for the need to change color and changes the color randomly.

=== Location correction b-threads ===
* FixWind: When a report comes in that the helicopter is not where it is supposed to be - stop painting movement and return to last known location.

=== Environment Simulation ===

* ColorControl: Counts movements and announces the need to change color.
* Wind: Every certain random number of steps, report a random location of the helicopter

= Incremental Development Notes =

{{#ev:youtube|6cSqPGvRWw0|640}}

With only basic movements and no color change b-threads:

[[Image: Black - thin.jpg]]

Basic movements with color changes:

[[Image: Color-thin.jpg]]

Adding horizontal brush movements:

[[Image: Color-thick.jpg]]

Random movements due to wind, and return by horizontal movement and then vertical to last known location:

[[Image: FixWind.jpg]]

= LSC Integration =

The BPJ-based system was then integrated with the LSC language via PlayGo.
For details how to integrate a BPJ application with LSC see a separate section in this documentation.

The following LSC (scenario) was added

* PaintCanEmpty: Waits for a certain number of movements with a given color and block subsequent changes to that color, simulating and empty can, until an event of PaintFilled arrives. This event is generated by the user clicking on a corresponding GUI Button.

= Design Notes =

The following design patterns and choices can be seen throughout the example.

* Events can be distinguishes from each other by
** Class - different classes of events
** Name - multiple instances of an events of the same class distinguished by their name (e.g. the color change events).
** Data field - Two instances of events of the same class, with arbitrary names can be distinguished by a value in one of the event data fields (e.g. the maintenance vs. mission indicator in the move events).

* One activity can interfere with another by using
** priority - (relative priority among b-thread)
** blocking the events of the other activity (which can be distinguished as described above)

* Distinguishing internal and external events - those generated by the system/application and those generated by the environment (and which may be reported by sensors).

** External events should not be blocked (enforced by convention only).
** When external events are produced by simulator, the concepts of Logical Execution Time should be enforced by convention, where all internal events reacting to the last external event should be processed before generating the next external event.

= Downloads =
== Download the wall painting example ==
# Click [[Media:Helicopter.zip | here]] to download the wall painting example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The helicopter example projects are now part of your workspace.
### The example includes three projects:
#### BDrone - The main project that includes the b-threads that implement the drawing/scanning tasks.
#### HeliSim - A simple java-based simulator.
#### il.ac.wis.cs.rovtool.blender - A blender-based simulator.
##Refer to the BDrone/HowToRun.txt file for execution instructions.

== Download the drone BP infrastructure ==
# Click [[Media:rovtool.zip | here]] to download the drone BP infrastructure.

Helicopter flight and mission

2014-05-20T07:25:47Z

BpAdmin: /* Download the helicopter example */

Helicopter flight and mission

2014-05-20T07:25:02Z

BpAdmin: /* Download */

= Helicopter Flight Examples =
The examples below demonstrates the control of a toy helicopter - AR DRONE by Parrot Inc.

= Basic Composite Behavior =
The following movies show flight of the helicopter, as well as simulation. The flight was generated by independent concurrent LSCs - where one directs the helicopter through a rectangular flight path without changing altitude, and another directs the helicopter to go up and down without changing its horizontal location. The result is a composite motion, traveling the prescribed path while going up and down.

{{#ev:youtube|nMTbQc_iq5Y|640}}

{{#ev:youtube|sMp8QTetobc|640}}

= Detailed Example: Wall Painting =
In this example, the mission here is to paint a wall with different colors. This can be considered as an analogy to a photography mission where a particular area as to be covered.

The example is implemented with a simulator.

Below we describe the requirements and the associated b-threads, along with screen images and a movie of the helicopter behavior as it evolves with the addition of new b-threads.

== Requirements==
The requirements below were added incrementally, and b-threads were added to deal with each requirement. In the simulator - the painting of the wall is by drawing a line on the screen.

*The helicopter should go up and down along the wall.
*When the helicopter reaches the ceiling or the floor it should move to the right
*Every fixed number of pixels the paint color should be changed
*Since the line drawn by the helicopter is thin, after every small vertical move, the helicopter should move right and left with horizontal brush strokes, before moving vertically again.
*The helicopter may move from its present location due to wind.
*If the helicopter is moved by wind, it should return to its last known location.

In the integration with LSC, two more requirements were added
*The amount of paint is limited. After a certain number of points is painted - the paint runs out.
*When paint of a certain color runs out, this color can no longer be used.
*When all paint colors run out, the helicopter must stop.
*Paint cans may be re-filled. This is simulated by a user clicking on a button on the screen.

== Events ==

== General control events ==
* BeginPainting: Start the painting process
* StopPainting: End the painting process
* MoveDown: Move down a fixed number of pixels.
* EndOfColUp: End painting wall going up
* DoColDownL Start painting wall going down
* EndOfColDown: End painting wall going up
* DoRowRight: Start painting wall going right
* EndOfRowRight: Stop moving right.
* ChangeColor: This is an event class of which there are four events, indicating a request to change the painting color to the corresponding one in the event name:
** eChangeColorBLACK
** eChangeColorRED
** eChangeColorBLUE
** eChangeColorGreen
* UpdateArrived: simulate information from a GPS with actual helicopter location

=== Move Events ===

The following events indicate the desire to move a fixed number of pixels in the desired direction. These events have a data field - indicating whether the movement is for a mission or for maintenance, which serves in correcting wind shifts.

* MoveUp: Move down a fixed number of pixels
* MoveDown: Move down a fixed number of pixels
* MoveLeft: Move left a fixed number of pixels
* MoveRight: Move right a fixed number of pixels

== BPJ b-threads ==

=== General control b-threads ===
* DoColD2U: Controls coloring in the up direction;
* YAxis: Reports when helicopter reaches top or bottom end of wall (ceiling of floor)
* EndColUp: Handle reaching of ceiling. Stop moving vertically, start moving right.
* DoRowL2R: Left to right painting - waits for DoRowRight and then repeatedly requests movement to the right until end of right movement is reached.
* XAxis: Monitor horizontal coordinates. Report reaching of right and left borders of wall, and report end of movement right to start a new column
* DoColU2D: Controls coloring in the up direction
* EndColDown: Handles reaching the floor - requests a movement to the right
* BrushMove: Move the brush right and left (horizontal moves) to create a thicker line and paint continuous area. This b-thread performs its actions between any two vertical moves.

=== Actuator b-threads ===

The following b-threads wait for the corresponding move event and call the helicopter API (or the simulator) to cause the actual movement.
* MovingRight
* MovingLeft
* MovingDown
* MovingUp

=== Color control b-threads ===
* ChangePaintingColor: Waits for the need to change color and changes the color randomly.

=== Location correction b-threads ===
* FixWind: When a report comes in that the helicopter is not where it is supposed to be - stop painting movement and return to last known location.

=== Environment Simulation ===

* ColorControl: Counts movements and announces the need to change color.
* Wind: Every certain random number of steps, report a random location of the helicopter

= Incremental Development Notes =

{{#ev:youtube|6cSqPGvRWw0|640}}

With only basic movements and no color change b-threads:

[[Image: Black - thin.jpg]]

Basic movements with color changes:

[[Image: Color-thin.jpg]]

Adding horizontal brush movements:

[[Image: Color-thick.jpg]]

Random movements due to wind, and return by horizontal movement and then vertical to last known location:

[[Image: FixWind.jpg]]

= LSC Integration =

The BPJ-based system was then integrated with the LSC language via PlayGo.
For details how to integrate a BPJ application with LSC see a separate section in this documentation.

The following LSC (scenario) was added

* PaintCanEmpty: Waits for a certain number of movements with a given color and block subsequent changes to that color, simulating and empty can, until an event of PaintFilled arrives. This event is generated by the user clicking on a corresponding GUI Button.

= Design Notes =

The following design patterns and choices can be seen throughout the example.

* Events can be distinguishes from each other by
** Class - different classes of events
** Name - multiple instances of an events of the same class distinguished by their name (e.g. the color change events).
** Data field - Two instances of events of the same class, with arbitrary names can be distinguished by a value in one of the event data fields (e.g. the maintenance vs. mission indicator in the move events).

* One activity can interfere with another by using
** priority - (relative priority among b-thread)
** blocking the events of the other activity (which can be distinguished as described above)

* Distinguishing internal and external events - those generated by the system/application and those generated by the environment (and which may be reported by sensors).

** External events should not be blocked (enforced by convention only).
** When external events are produced by simulator, the concepts of Logical Execution Time should be enforced by convention, where all internal events reacting to the last external event should be processed before generating the next external event.

= Download =
== Download the helicopter example ==
# Click [[Media:Helicopter.zip | here]] to download the helicopter example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The helicopter example projects are now part of your workspace.
### The example includes three projects:
#### BDrone - The main project that includes the b-threads that implement the drawing/scanning tasks.
#### HeliSim - A simple java-based simulator.
#### il.ac.wis.cs.rovtool.blender - A blender-based simulator.
##Refer to the BDrone/HowToRun.txt file for execution instructions.

== Download the drone BP infrastructure ==
# Click [[Media:rovtool.zip | here]] to download the drone BP infrastructure.

RunMode

2014-04-29T08:41:01Z

BpAdmin: /* Application-specific parameters */

= BPJ Model Checking Parameters =
==Specifying Run Modes ==

BPJ model checking is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:

=== -DrunMode=Det ===
* Description: “Normal” / standard / deterministic run.
* Use: when you want the program to “do something”.
* Nondeterminism specification: Ignored. All priorities are considered distinct.
* Event Selection: Always the first requested event that is not blocked.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.

=== -DrunMode=MCSafety ===
* Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
* Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
* Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false

=== -DrunMode=MCLiveness ===
* Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
* Use: Model checking for liveness properties - (with fairness assumptions),.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections.
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events

=== -DrunMode=Random ===
* Description: One possible run out of many.
* Use: Demonstration or manual exploration of different possible runs.
* Nondeterminism specification: Allowed.
* Event selection: Random among all nondeterministic choices.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.
* Additional related parameters: -DrandomSeed= nnnn.

=== -DrunMode=Iter ===
* Description: An iterative run – explore all possible executions.
* Use: to assess traces and results of all possible runs resulting from nondeterministic choices.
* Nondeterminism specification: Allowed.
* Event selection: Systematically makes all possible combinations of event selections - in different runs.
* Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice.
* Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted).

=== -DrunMode=MCDet ===
Description: A deterministic run, with model-checking instrumentation. No nondeterminism. The event selection mechanism always picks the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.

=== -DrunMode=Learning/Training ===
(In development)

== Run-control Parameters ==

=== -Dsearch=BFS or -Dsearch=DFS ===
Breadth-first or depth-first search.

=== -Drecursive=true ===
Depth first search by recursive calls instead of by a application-maintained stack

=== -DdisableStateHashing ===
BPJ will not recognize previously visited states.

=== -DestimatedStates ===
Control initial space allocation for state hashing

=== -DsuppressDeadlock=true ===
deadlocks will not cause a verification failure.

=== -DlogBacktracking=true ===
Issues a message with every visited BProgram state

=== -ea ===
Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.

=== -noverify ===
Resolving Java7 compatibility issues with the bytecode instrumentation.

== Memory Management Parameters ==
=== -DShallow=true/false ===

This parameter controls the serialization of objects not on the stack for backtracking during execution. See details in "Enabling your application for Model Checking".
=== -Xmn=,-Xms=,-Xmx= ===
These parameters are standard Java memory allocation parameters, and are used to define sufficient memory for large model-checking run. E.g.:

-Xmn200M
-Xms700M
-Xmx700M

Explanation:

* As Java starts, it creates within the systems memory a Java Virtual Machine (JVM). JVM is where the complete processing of any Java program takes place. All Java applications (including IQv6) by default allocate & reserve up to 64 MB of memory resource pool from the system on which it is running.
* The Xms is the initial / minimum Java memory (heap) size within the JVM. Setting the initial memory (heap) size higher can help in a couple of ways. First, it will allow garbage collection (GC) to work less which is more efficient. The higher initial memory value will cause the size of the memory (heap) not to have to grow as fast as a lower initial memory (heap) size, thereby saving the overhead of the Java VM asking the OS for more memory.
* The Xmx is the maximum Java memory (heap) size within the Java Virtual Memory (JVM). As the JVM gets closer to fully utilizing the initial memory, it checks the Xmx settings to find out if it can draw more memory from the system resources. If it can, it does so. For the JVM to allocate contiguous memory to itself is a very expensive operation. So as the JVM gets closer to the initial memory, the JVM will use aggressive garbage collection (to clean the memory and if possible avoid memory allocation), increasing the load on the system.
* If JVM is in need of memory beyond the value set in Xmx, the JVM will not be able to draw more memory from system resource (even if available) and run out of memory. Hence, the -Xms and -Xmx memory parameters should be increased depending upon the demand estimation of the system. Ideally both should be the same value (set at maximum possible as per demand estimation). This ensure that the maximum memory is allocated right at the start-up eliminating the need for extra memory allocation during program execution. It is sometimes recommended to use aggressive maximum memory (heap) size of between 1/2 and 3/4 of physical memory.
* -Xmn: the size of the heap for the young generation.
See more details in general Java reference information.

= Application-specific parameters =
You can pass parameters to your own application, and process them in standard Java techniques. E.g.,
* - nPhils=5 number of philosophers.
* leftyPhil=false is any of the philosophers left handed.

static int nPhils; // number of philosophers
static boolean leftyPhil = false; // Last Philosopher is left handed.
static {
nPhils = Integer.parseInt(System.getProperty("nPhils", "3"));
parmString += "nPhils=" + nPhils;
leftyPhil = (System.getProperty("leftyPhil","false").equals("true"));
parmString += ", leftyPhil=" + leftyPhil;
System.out.println(parmString);
}

Run Configuration Examples:

-DrunMode=MCSafety
-Drecursive=true
-Dshallow=true
-noverify

-DrunMode=MCSafety
-Dsearch=DFS
-Xms300M
-Xmx1000M
-DestimatedStates=10000
-DlogBacktracking=false
-ea
-noverify

RunMode

2014-04-29T08:40:00Z

BpAdmin: /* Run-control Parameters */

= BPJ Model Checking Parameters =
==Specifying Run Modes ==

BPJ model checking is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:

=== -DrunMode=Det ===
* Description: “Normal” / standard / deterministic run.
* Use: when you want the program to “do something”.
* Nondeterminism specification: Ignored. All priorities are considered distinct.
* Event Selection: Always the first requested event that is not blocked.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.

=== -DrunMode=MCSafety ===
* Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
* Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
* Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false

=== -DrunMode=MCLiveness ===
* Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
* Use: Model checking for liveness properties - (with fairness assumptions),.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections.
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events

=== -DrunMode=Random ===
* Description: One possible run out of many.
* Use: Demonstration or manual exploration of different possible runs.
* Nondeterminism specification: Allowed.
* Event selection: Random among all nondeterministic choices.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.
* Additional related parameters: -DrandomSeed= nnnn.

=== -DrunMode=Iter ===
* Description: An iterative run – explore all possible executions.
* Use: to assess traces and results of all possible runs resulting from nondeterministic choices.
* Nondeterminism specification: Allowed.
* Event selection: Systematically makes all possible combinations of event selections - in different runs.
* Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice.
* Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted).

=== -DrunMode=MCDet ===
Description: A deterministic run, with model-checking instrumentation. No nondeterminism. The event selection mechanism always picks the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.

=== -DrunMode=Learning/Training ===
(In development)

== Run-control Parameters ==

=== -Dsearch=BFS or -Dsearch=DFS ===
Breadth-first or depth-first search.

=== -Drecursive=true ===
Depth first search by recursive calls instead of by a application-maintained stack

=== -DdisableStateHashing ===
BPJ will not recognize previously visited states.

=== -DestimatedStates ===
Control initial space allocation for state hashing

=== -DsuppressDeadlock=true ===
deadlocks will not cause a verification failure.

=== -DlogBacktracking=true ===
Issues a message with every visited BProgram state

=== -ea ===
Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.

=== -noverify ===
Resolving Java7 compatibility issues with the bytecode instrumentation.

== Memory Management Parameters ==
=== -DShallow=true/false ===

This parameter controls the serialization of objects not on the stack for backtracking during execution. See details in "Enabling your application for Model Checking".
=== -Xmn=,-Xms=,-Xmx= ===
These parameters are standard Java memory allocation parameters, and are used to define sufficient memory for large model-checking run. E.g.:

-Xmn200M
-Xms700M
-Xmx700M

Explanation:

* As Java starts, it creates within the systems memory a Java Virtual Machine (JVM). JVM is where the complete processing of any Java program takes place. All Java applications (including IQv6) by default allocate & reserve up to 64 MB of memory resource pool from the system on which it is running.
* The Xms is the initial / minimum Java memory (heap) size within the JVM. Setting the initial memory (heap) size higher can help in a couple of ways. First, it will allow garbage collection (GC) to work less which is more efficient. The higher initial memory value will cause the size of the memory (heap) not to have to grow as fast as a lower initial memory (heap) size, thereby saving the overhead of the Java VM asking the OS for more memory.
* The Xmx is the maximum Java memory (heap) size within the Java Virtual Memory (JVM). As the JVM gets closer to fully utilizing the initial memory, it checks the Xmx settings to find out if it can draw more memory from the system resources. If it can, it does so. For the JVM to allocate contiguous memory to itself is a very expensive operation. So as the JVM gets closer to the initial memory, the JVM will use aggressive garbage collection (to clean the memory and if possible avoid memory allocation), increasing the load on the system.
* If JVM is in need of memory beyond the value set in Xmx, the JVM will not be able to draw more memory from system resource (even if available) and run out of memory. Hence, the -Xms and -Xmx memory parameters should be increased depending upon the demand estimation of the system. Ideally both should be the same value (set at maximum possible as per demand estimation). This ensure that the maximum memory is allocated right at the start-up eliminating the need for extra memory allocation during program execution. It is sometimes recommended to use aggressive maximum memory (heap) size of between 1/2 and 3/4 of physical memory.
* -Xmn: the size of the heap for the young generation.
See more details in general Java reference information.

= Application-specific parameters =
You can pass parameters to your own application, and process them in standard Java techniques. E.g.,
* - nPhils=5 number of philosophers.
* leftyPhil=false is any of the philosophers left handed.

static int nPhils; // number of philosophers
static boolean leftyPhil = false; // Last Philosopher is left handed.
static {
nPhils = Integer.parseInt(System.getProperty("nPhils", "3"));
parmString += "nPhils=" + nPhils;
leftyPhil = (System.getProperty("leftyPhil","false").equals("true"));
parmString += ", leftyPhil=" + leftyPhil;
System.out.println(parmString);
}

Run Configuration Examples:

-DrunMode=MCSafety
-Drecursive=true
-Dshallow=true

-DrunMode=MCSafety
-Dsearch=DFS
-Xms300M
-Xmx1000M
-DestimatedStates=10000
-DlogBacktracking=false
-ea

File:Sudoku1.zip

2014-04-29T08:36:09Z

BpAdmin:

Sudoku

2014-04-29T08:35:50Z

BpAdmin:

= Sudoku =
In this example one can see two properties of behavioral programming
* How different heuristics and pieces of knowledge about the problem domain can be used separately to program an application
* How model-checking can be used to help find a desired scenario.

= Requirements =
In the cells of a 9X9 grid which is also divided into 9 3X3 boxes, place the digits 1-9 such that in each row, column and box, each digit appears exactly once.

= Events =

* Move: A single event class with 9X9X9 = 721 instances, indicating the writing of a given digit in a given cell. The class has the following data fields:

** number: the digit written in the cell (1-9)
** row: The row of the cell (1-9)
** col: the column of the cell (1-9)
** boxrow: The row of the 3X3 box in which this cell resides (1-3)
** boxcol: the column of the 3X3 box in which this cell resides (1-3)

When enough data is provided, the strategies below are sufficient for solving the game.
When not enough data is provided, model checking explores the different possibilities until a solution is found.

== Playing b-threads ==
* MakeGivenMoves: This b-thread provides the opening input to the riddle - filling in the known cells.
* DefaultMove: Each of the 81 instances of this b-thread class, is associated with a cell, and requests all possible 9 digits. Once an event occurs, all other events for the cell are blocked.
* DetectWin: This b-thread simply counts until 81 events have been triggered. The correctness of the solution is guaranteed
* EliminateTwoInABox: This b-thread tries to write a number in a cell after the same number was written in two other columns of this box. It does not check if the cell is occopied or if the digit was already written in the present column - this is provided by event-blocking in other b-threads.
* PlaceANumberInARow: With an instance for each digit and each row, this b-thread tries to place a particular digit in the row. It waits till there is only one place to put it, and then requests the corresponding event.
* PlaceANumberInAColumn: With an instance for each digit and each row, this b-thread tries to place a particular digit in the Column. It waits till there is only one place to put it, and then requests the corresponding event.
* EliminateEight: For each cell, an instance of this b-thread checks the possibilities for the cell, and eliminates possibilities as conflicting events occur elsewhere. When the number of remaining possibilities is one, the b-thread requests the remaining digit.

== b-threads that support model-checking ==
PruneWhenNoSolution: This b-thread requests an event at a low priority. If it is triggered, it means that all move events are blocked, hence the game has failed. It then calls the model-checking API to prune the search.

== Design Notes ==
* The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads, as well as the GivenMoves b-thread.

== Download ==
# Click [[Media:Sudoku1.zip | here]] to download the sudoku example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The sudoku example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

Learning

2014-04-28T10:03:15Z

BpAdmin: /* Reference Materials */

= Adaptive Behavioral Programming =

We introduce a way to program adaptive reactive
systems, using behavioral programming.
Extending the semantics of BPJ with reinforcements
allows the programmer not only to specify what
the system should do or must not do, but also what it should
try to do, in an intuitive and incremental way. By integrating
behavioral programs with reinforcement learning methods,
the program can adapt to the environment, and try to achieve
the desired goals.

== Reference Materials ==
* Paper: [http://www.wisdom.weizmann.ac.il/~harel/papers/Adaptive%20BP.pdf Adaptive Behavioral Programming]
* [http://www.wisdom.weizmann.ac.il/~bprogram/code/ReinforcementLearningBPJ.zip Code and examples]: 
** A base version of BPJ.
** A Java library with extensions to BPJ for reinforcement learning. Import and add to the classpath.
** Example: A Salad cutting robot. The b-threads provide an incomplete specification for a simulated robot that needs to pick up vegetables, cut them and serve them to customers. Using reinforcement learning, the robot learns the correct order in which to execute these actions.
** Example: Tic Tac Toe, where the application learns how to play despite underspecification.

File:Helicopter.zip

2014-04-17T09:22:22Z

BpAdmin:

Helicopter flight and mission

2014-04-17T09:16:31Z

BpAdmin:

= Helicopter Flight Example =
This example demonstrates the control of a toy helicopter. The mission here is to paint a wall with different colors. This can be considered as an analogy to a photography mission where a particular area as to be covered.

== Requirements==
The requirements below were added incrementally, and b-threads were added to deal with each requirement. In the simulator - the painting of the wall is by drawing a line on the screen.

*The helicopter should go up and down along the wall.
*When the helicopter reaches the ceiling or the floor it should move to the right
*Every fixed number of pixels the paint color should be changed
*Since the line drawn by the helicopter is thin, after every small vertical move, the helicopter should move right and left with horizontal brush strokes, before moving vertically again.
*The helicopter may move from its present location due to wind.
*If the helicopter is moved by wind, it should return to its last known location.

In the integration with LSC, two more requirements were added
*The amount of paint is limited. After a certain number of points is painted - the paint runs out.
*When paint of a certain color runs out, this color can no longer be used.
*When all paint colors run out, the helicopter must stop.
*Paint cans may be re-filled. This is simulated by a user clicking on a button on the screen.

== Events ==

== General control events ==
* BeginPainting: Start the painting process
* StopPainting: End the painting process
* MoveDown: Move down a fixed number of pixels.
* EndOfColUp: End painting wall going up
* DoColDownL Start painting wall going down
* EndOfColDown: End painting wall going up
* DoRowRight: Start painting wall going right
* EndOfRowRight: Stop moving right.
* ChangeColor: This is an event class of which there are four events, indicating a request to change the painting color to the corresponding one in the event name:
** eChangeColorBLACK
** eChangeColorRED
** eChangeColorBLUE
** eChangeColorGreen
* UpdateArrived: simulate information from a GPS with actual helicopter location

=== Move Events ===

The following events indicate the desire to move a fixed number of pixels in the desired direction. These events have a data field - indicating whether the movement is for a mission or for maintenance, which serves in correcting wind shifts.

* MoveUp: Move down a fixed number of pixels
* MoveDown: Move down a fixed number of pixels
* MoveLeft: Move left a fixed number of pixels
* MoveRight: Move right a fixed number of pixels

== BPJ b-threads ==

=== General control b-threads ===
* DoColD2U: Controls coloring in the up direction;
* YAxis: Reports when helicopter reaches top or bottom end of wall (ceiling of floor)
* EndColUp: Handle reaching of ceiling. Stop moving vertically, start moving right.
* DoRowL2R: Left to right painting - waits for DoRowRight and then repeatedly requests movement to the right until end of right movement is reached.
* XAxis: Monitor horizontal coordinates. Report reaching of right and left borders of wall, and report end of movement right to start a new column
* DoColU2D: Controls coloring in the up direction
* EndColDown: Handles reaching the floor - requests a movement to the right
* BrushMove: Move the brush right and left (horizontal moves) to create a thicker line and paint continuous area. This b-thread performs its actions between any two vertical moves.

=== Actuator b-threads ===

The following b-threads wait for the corresponding move event and call the helicopter API (or the simulator) to cause the actual movement.
* MovingRight
* MovingLeft
* MovingDown
* MovingUp

=== Color control b-threads ===
* ChangePaintingColor: Waits for the need to change color and changes the color randomly.

=== Location correction b-threads ===
* FixWind: When a report comes in that the helicopter is not where it is supposed to be - stop painting movement and return to last known location.

=== Environment Simulation ===

* ColorControl: Counts movements and announces the need to change color.
* Wind: Every certain random number of steps, report a random location of the helicopter

= Incremental Development Notes =

With only basic movements and no color change b-threads

[[Image: Black - thin.jpg]]

Basic movements with color changes

[[Image: Color-thin.jpg]]

Adding horizontal brush movements

[[Image: Color-thick.jpg]]

Random movements due to wind, and return by horizontal movement and then vertical to last known location

[[Image: FixWind.jpg]]

= LSC Integration =

The BPJ-based system was then integrated with the LSC language via PlayGo.
For details how to integrate a BPJ application with LSC see a separate section in this documentation.

The following LSC (scenario) was added

* PaintCanEmpty: Waits for a certain number of movements with a given color and block subsequent changes to that color, simulating and empty can, until an event of PaintFilled arrives. This event is generated by the user clicking on a corresponding GUI Button.

= Design Notes =

The following design patterns and choices can be seen throughout the example.

* Events can be distinguishes from each other by
** Class - different classes of events
** Name - multiple instances of an events of the same class distinguished by their name (e.g. the color change events).
** Data field - Two instances of events of the same class, with arbitrary names can be distinguished by a value in one of the event data fields (e.g. the maintenance vs. mission indicator in the move events).

* One activity can interfere with another by using
** priority - (relative priority among b-thread)
** blocking the events of the other activity (which can be distinguished as described above)

* Distinguishing internal and external events - those generated by the system/application and those generated by the environment (and which may be reported by sensors).

** External events should not be blocked (enforced by convention only).
** When external events are produced by simulator, the concepts of Logical Execution Time should be enforced by convention, where all internal events reacting to the last external event should be processed before generating the next external event.

= Download =
# Click [[Media:Helicopter.zip | here]] to download the helicopter example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The helicopter example projects are now part of your workspace.
### The example includes three projects:
#### BDrone - The main project that includes the b-threads that implement the drawing/scanning tasks.
#### HeliSim - A simple java-based simulator.
#### il.ac.wis.cs.rovtool.blender - A blender-based simulator.
##Refer to the BDrone/HowToRun.txt file for execution instructions.

File:Flock.zip

2014-04-17T08:04:47Z

BpAdmin:

Flight of a flock of birds

2014-04-17T08:03:46Z

BpAdmin: /* Download */

= Simulating Flight of a Flock of Birds =
In this example we simulate the flight of a flock of birds, with each bird having a simple set of rules implemented as b-threads.
The example highlights
* Multi-agent activity
* Emergent group behaviors - emanating from individual agent behavior
* Implementation of animation with BPJ - and handling of associated design issues.

= Requirements - from each bird =
* Always try to move towards the center of the flock
* Always avoid colliding with other birds
* When getting close to a wall - change direction - in the same "reflection" angle
* When the "Scare" button is hit - fly away from the center of the flock.

A video example of the result can be seen here ** add link **

= Download =
# Click [[Media:Flock.zip | here]] to download the flock of birds example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The flock of birds example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

Tic-Tac-Toe

2014-04-17T07:57:19Z

BpAdmin:

= A behavioral program for the game of Tic-Tac-Toe =

== Game Description ==
Two players, X and O, alternately mark squares on a 3X3 grid whose squares are identified by <row,column> pairs: <0,0>, <0,1>, ...,<2,2>. The winner is the player who manages to form a full horizontal, vertical or diagonal line with three of his/her marks.
If the entire grid becomes marked but no player has formed a line, the result is a draw.

In our example, player X should be played by a human user, and player O is played by the application. Each move (marking of a square by a player) is represented by an event, X_<row,col> or O_<row,col>. Three additional events, XWin, OWin, and draw$, represent the respective victories and a draw.

A play of the game may be described as a sequence of events. E.g., the sequence
X_<0,0>, O_<1,1>, X_<2,1>, O_<0,2>, X_<2,0>, O_<1,0>, X_<2,2>, XWin describes a play in which X wins, and whose final configuration is:

[[Image:TTT01.jpg ]]

== b-Threads ==
Below are listed the b-threads of the application.

=== Rules of the game ===
* SquareTaken: block further marking of a square already marked by X or O.
* EnforceTurns: alternately block O moves while waiting for X moves, and vice versa (we assume that X always plays first).
* DetectXWin: wait for placement of three X marks in a line and request XWin.
* DetectOWin: wait for placement of three O marks in a line and request OWin.
* DetectDraw: wait for nine moves and request draw event.

=== Strategies ===
*DefaultMoves: a b-thread that repeatedly requests all nine possible O moves in the following order of center, corners and edges: O_<1,1>,O_<0,0>,O_<0,2>,O_<2,0>,O_<2,2>, O_<0,1>,O_<1,0>,O_<1,2>,O_<2,1>.
*PreventThirdX: when two Xs are noticed in a line, add an O in that line (and prevent an immediate loss).
*AddThirdO: when two Os are located on a single line, add a third O (and win).
*PreventXFork: when two Xs are noticed, in a corner and opposing edge such that X may force a win, mark an O in the intersection corner of the potential fork, thus preventing its creation.
*PreventAnotherXFork: when the first two Xs are marked in two opposite corners and the first O is marked at the center, request O_<0,1>.
In the spirit of ``the best defense is a good offense'', this move creates an attack that forces X to play X_<2,1>, and seems to avoid the immediate fork threat.
*PreventYetAnotherXFork: when two Xs are noticed in two edge squares that are adjacent to a common corner, mark an O in that corner.

== Other Classes ==
*ExternalApp: The main class of the application. Loads and starts the b-threads
*GUI: Manages the display

== Design Notes ==
For some b-threads such as DefaultMoves there is a single instance. Other b-threads, such as AddThirdO are parametric, and there is a separate instance of the b-thread for each ordering of the three events in each row, column and diagonal. Thus, in the present design such b-threads do not maintain a copy of the board, but instead are simply waiting for very specific two events in a given order and responding with other events. Other designs are of course possible> for example a b-thread can be responsible for three events in any order, wait for any two in any order and then request the third. In another design a b-thread can maintain a copy of the board, wait for almost any event, keep track of board configuration changes, look for lines to complete, and request the corresponding move events.

== Download ==
# Click [[Media:TicTacToe.zip | here]] to download the tic-tac-toe example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The tic-tac-toe example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

Flight of a flock of birds

2014-04-17T07:56:38Z

BpAdmin:

= Simulating Flight of a Flock of Birds =
In this example we simulate the flight of a flock of birds, with each bird having a simple set of rules implemented as b-threads.
The example highlights
* Multi-agent activity
* Emergent group behaviors - emanating from individual agent behavior
* Implementation of animation with BPJ - and handling of associated design issues.

= Requirements - from each bird =
* Always try to move towards the center of the flock
* Always avoid colliding with other birds
* When getting close to a wall - change direction - in the same "reflection" angle
* When the "Scare" button is hit - fly away from the center of the flock.

A video example of the result can be seen here ** add link **

= Download =
# Click [[Media:TicTacToe.zip | here]] to download the flock of birds example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The flock of birds example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

Tic-Tac-Toe

2014-04-17T07:48:50Z

BpAdmin: /* A behavioral program for the game of Tic-Tac-Toe */

= A behavioral program for the game of Tic-Tac-Toe =

# Click [[Media:TicTacToe.zip | here]] to download the tic-tac-toe example.
# Installation Instructions:
##Import the downloaded project to your workspace:
###From the 'File' menu choose 'Import'-->'General'-->'Existing Projects into Workspace'.
###Click the 'Next' button.
###Click the 'Select archive file' option and then click the 'Browse...' button to select the downloaded zip file.
###Click 'Finish'.
##The tic-tac-toe example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

== Game Description ==
Two players, X and O, alternately mark squares on a 3X3 grid whose squares are identified by <row,column> pairs: <0,0>, <0,1>, ...,<2,2>. The winner is the player who manages to form a full horizontal, vertical or diagonal line with three of his/her marks.
If the entire grid becomes marked but no player has formed a line, the result is a draw.

In our example, player X should be played by a human user, and player O is played by the application. Each move (marking of a square by a player) is represented by an event, X_<row,col> or O_<row,col>. Three additional events, XWin, OWin, and draw$, represent the respective victories and a draw.

A play of the game may be described as a sequence of events. E.g., the sequence
X_<0,0>, O_<1,1>, X_<2,1>, O_<0,2>, X_<2,0>, O_<1,0>, X_<2,2>, XWin describes a play in which X wins, and whose final configuration is:

[[Image:TTT01.jpg ]]

== b-Threads ==
Below are listed the b-threads of the application.

=== Rules of the game ===
* SquareTaken: block further marking of a square already marked by X or O.
* EnforceTurns: alternately block O moves while waiting for X moves, and vice versa (we assume that X always plays first).
* DetectXWin: wait for placement of three X marks in a line and request XWin.
* DetectOWin: wait for placement of three O marks in a line and request OWin.
* DetectDraw: wait for nine moves and request draw event.

=== Strategies ===
*DefaultMoves: a b-thread that repeatedly requests all nine possible O moves in the following order of center, corners and edges: O_<1,1>,O_<0,0>,O_<0,2>,O_<2,0>,O_<2,2>, O_<0,1>,O_<1,0>,O_<1,2>,O_<2,1>.
*PreventThirdX: when two Xs are noticed in a line, add an O in that line (and prevent an immediate loss).
*AddThirdO: when two Os are located on a single line, add a third O (and win).
*PreventXFork: when two Xs are noticed, in a corner and opposing edge such that X may force a win, mark an O in the intersection corner of the potential fork, thus preventing its creation.
*PreventAnotherXFork: when the first two Xs are marked in two opposite corners and the first O is marked at the center, request O_<0,1>.
In the spirit of ``the best defense is a good offense'', this move creates an attack that forces X to play X_<2,1>, and seems to avoid the immediate fork threat.
*PreventYetAnotherXFork: when two Xs are noticed in two edge squares that are adjacent to a common corner, mark an O in that corner.

== Other Classes ==
*ExternalApp: The main class of the application. Loads and starts the b-threads
*GUI: Manages the display

== Design Notes ==
For some b-threads such as DefaultMoves there is a single instance. Other b-threads, such as AddThirdO are parametric, and there is a separate instance of the b-thread for each ordering of the three events in each row, column and diagonal. Thus, in the present design such b-threads do not maintain a copy of the board, but instead are simply waiting for very specific two events in a given order and responding with other events. Other designs are of course possible> for example a b-thread can be responsible for three events in any order, wait for any two in any order and then request the third. In another design a b-thread can maintain a copy of the board, wait for almost any event, keep track of board configuration changes, look for lines to complete, and request the corresponding move events.

File:TicTacToe.zip

2014-04-17T07:42:59Z

BpAdmin:

Tic-Tac-Toe

2014-04-17T07:36:02Z

BpAdmin:

= A behavioral program for the game of Tic-Tac-Toe =

# Click [[Media:TicTacToe.zip | here]] to download the tic-tac-toe example.
# Installation Instructions:
##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 downloaded zip file.
###Click finish.
##The tic-tac-toe example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

== Game Description ==
Two players, X and O, alternately mark squares on a 3X3 grid whose squares are identified by <row,column> pairs: <0,0>, <0,1>, ...,<2,2>. The winner is the player who manages to form a full horizontal, vertical or diagonal line with three of his/her marks.
If the entire grid becomes marked but no player has formed a line, the result is a draw.

In our example, player X should be played by a human user, and player O is played by the application. Each move (marking of a square by a player) is represented by an event, X_<row,col> or O_<row,col>. Three additional events, XWin, OWin, and draw$, represent the respective victories and a draw.

A play of the game may be described as a sequence of events. E.g., the sequence
X_<0,0>, O_<1,1>, X_<2,1>, O_<0,2>, X_<2,0>, O_<1,0>, X_<2,2>, XWin describes a play in which X wins, and whose final configuration is:

[[Image:TTT01.jpg ]]

== b-Threads ==
Below are listed the b-threads of the application.

=== Rules of the game ===
* SquareTaken: block further marking of a square already marked by X or O.
* EnforceTurns: alternately block O moves while waiting for X moves, and vice versa (we assume that X always plays first).
* DetectXWin: wait for placement of three X marks in a line and request XWin.
* DetectOWin: wait for placement of three O marks in a line and request OWin.
* DetectDraw: wait for nine moves and request draw event.

=== Strategies ===
*DefaultMoves: a b-thread that repeatedly requests all nine possible O moves in the following order of center, corners and edges: O_<1,1>,O_<0,0>,O_<0,2>,O_<2,0>,O_<2,2>, O_<0,1>,O_<1,0>,O_<1,2>,O_<2,1>.
*PreventThirdX: when two Xs are noticed in a line, add an O in that line (and prevent an immediate loss).
*AddThirdO: when two Os are located on a single line, add a third O (and win).
*PreventXFork: when two Xs are noticed, in a corner and opposing edge such that X may force a win, mark an O in the intersection corner of the potential fork, thus preventing its creation.
*PreventAnotherXFork: when the first two Xs are marked in two opposite corners and the first O is marked at the center, request O_<0,1>.
In the spirit of ``the best defense is a good offense'', this move creates an attack that forces X to play X_<2,1>, and seems to avoid the immediate fork threat.
*PreventYetAnotherXFork: when two Xs are noticed in two edge squares that are adjacent to a common corner, mark an O in that corner.

== Other Classes ==
*ExternalApp: The main class of the application. Loads and starts the b-threads
*GUI: Manages the display

== Design Notes ==
For some b-threads such as DefaultMoves there is a single instance. Other b-threads, such as AddThirdO are parametric, and there is a separate instance of the b-thread for each ordering of the three events in each row, column and diagonal. Thus, in the present design such b-threads do not maintain a copy of the board, but instead are simply waiting for very specific two events in a given order and responding with other events. Other designs are of course possible> for example a b-thread can be responsible for three events in any order, wait for any two in any order and then request the third. In another design a b-thread can maintain a copy of the board, wait for almost any event, keep track of board configuration changes, look for lines to complete, and request the corresponding move events.

Tic-Tac-Toe

2014-04-17T07:34:59Z

BpAdmin:

= A behavioral program for the game of Tic-Tac-Toe =

# Click [[Media:BPJ_1.1.0.zip | here]] to download the tic-tac-toe example.
# Installation Instructions:
##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 downloaded zip file.
###Click finish.
##The tic-tac-toe example project is now part of your workspace.
##Refer to the readme.txt file for execution instructions.

== Game Description ==
Two players, X and O, alternately mark squares on a 3X3 grid whose squares are identified by <row,column> pairs: <0,0>, <0,1>, ...,<2,2>. The winner is the player who manages to form a full horizontal, vertical or diagonal line with three of his/her marks.
If the entire grid becomes marked but no player has formed a line, the result is a draw.

In our example, player X should be played by a human user, and player O is played by the application. Each move (marking of a square by a player) is represented by an event, X_<row,col> or O_<row,col>. Three additional events, XWin, OWin, and draw$, represent the respective victories and a draw.

A play of the game may be described as a sequence of events. E.g., the sequence
X_<0,0>, O_<1,1>, X_<2,1>, O_<0,2>, X_<2,0>, O_<1,0>, X_<2,2>, XWin describes a play in which X wins, and whose final configuration is:

[[Image:TTT01.jpg ]]

== b-Threads ==
Below are listed the b-threads of the application.

=== Rules of the game ===
* SquareTaken: block further marking of a square already marked by X or O.
* EnforceTurns: alternately block O moves while waiting for X moves, and vice versa (we assume that X always plays first).
* DetectXWin: wait for placement of three X marks in a line and request XWin.
* DetectOWin: wait for placement of three O marks in a line and request OWin.
* DetectDraw: wait for nine moves and request draw event.

=== Strategies ===
*DefaultMoves: a b-thread that repeatedly requests all nine possible O moves in the following order of center, corners and edges: O_<1,1>,O_<0,0>,O_<0,2>,O_<2,0>,O_<2,2>, O_<0,1>,O_<1,0>,O_<1,2>,O_<2,1>.
*PreventThirdX: when two Xs are noticed in a line, add an O in that line (and prevent an immediate loss).
*AddThirdO: when two Os are located on a single line, add a third O (and win).
*PreventXFork: when two Xs are noticed, in a corner and opposing edge such that X may force a win, mark an O in the intersection corner of the potential fork, thus preventing its creation.
*PreventAnotherXFork: when the first two Xs are marked in two opposite corners and the first O is marked at the center, request O_<0,1>.
In the spirit of ``the best defense is a good offense'', this move creates an attack that forces X to play X_<2,1>, and seems to avoid the immediate fork threat.
*PreventYetAnotherXFork: when two Xs are noticed in two edge squares that are adjacent to a common corner, mark an O in that corner.

== Other Classes ==
*ExternalApp: The main class of the application. Loads and starts the b-threads
*GUI: Manages the display

== Design Notes ==
For some b-threads such as DefaultMoves there is a single instance. Other b-threads, such as AddThirdO are parametric, and there is a separate instance of the b-thread for each ordering of the three events in each row, column and diagonal. Thus, in the present design such b-threads do not maintain a copy of the board, but instead are simply waiting for very specific two events in a given order and responding with other events. Other designs are of course possible> for example a b-thread can be responsible for three events in any order, wait for any two in any order and then request the third. In another design a b-thread can maintain a copy of the board, wait for almost any event, keep track of board configuration changes, look for lines to complete, and request the corresponding move events.

JavaFlow

2014-03-19T09:49:01Z

BpAdmin: /* Enabling your application for model checking */

=Enabling your application for model checking=
In addition to the controls described in earlier sections, there are certain constraints on how the application should be coded to enable model checking.
BPJ uses the package Javaflow to perform backtracking as needed for model checking. Depending on the run mode, BPJ instruments the application for Javaflow. As part of traversing all possible execution paths, BPJ model checking uses Javaflow for backtracking and saves and restores the thread’s stack using an object called "continuation". The stack contains the non-static fields/variables from the b-thread class and the variables defined in-line in the runBThread method. Objects (which are not on the stack) are saved and restored by the BPJ model checking using serialization and deserialization of the continuation object. Serialization translates each field and each object pointed to from the continuation into a bit stream. Deserialization turns such bit streams into program objects and fully restores the state.

= Programming Requirement 1=
When two pointers on the stack point to the same object, Javaflow deserialization creates two copies of the object, and the application that relied on the two being one object no longer works. Therefore, do not use the operator "==" to compare objects that are part of the b-thread's state. Instead, use the equals() method. A default equals() method based on object ids already exists for events.

=Programming Requirement 2=
Serialization and desrialization may significantly slow the application. Therefore, if you have objects that do not change from one bt-state to another, mark them as transient static (for the class or for the instance, as needed). Objects marked as transient are not processed by serialization and deserialization resets them to their initial value.

=Programming Tip=
If all the objects pointed to from the stack can be transient as defined above, you do not have to specify them as transient, and instead you can just specify static, and specify the run time parameter "–Dshallow=true" (the default
is "-Dshallow=false"). Then, the when BPJ uses Javaflow to save and restore the stack(s) it does not perform serialization and deserialization.

[[Image:Dshallow.png | 600px | Object serialization ]]

Example:
Examine the code snippet below:

Integer x = new Integer(5);
bSync(...)
x++;
bSync(...)

If -Dshallow=true is specified, in the second visit to the second bSync (after backtracking to try an execution with a different choice of event in the first bSync) the value of X will be 7, because X was not restored. Solution: Use int and not Integer - and then the variable is on the stack, and is always restored with backtracking, or use
-Dshallow=false, to force full serialization.

Nondeterminism

2014-03-19T09:47:52Z

BpAdmin: /* Nondeterministic execution in BPJ model checking */

RunMode

2014-03-19T09:46:28Z

BpAdmin: /* BPJ Model Checking Parameters */

= BPJ Model Checking Parameters =
==Specifying Run Modes ==

BPJ model checking is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:

=== -DrunMode=Det ===
* Description: “Normal” / standard / deterministic run.
* Use: when you want the program to “do something”.
* Nondeterminism specification: Ignored. All priorities are considered distinct.
* Event Selection: Always the first requested event that is not blocked.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.

=== -DrunMode=MCSafety ===
* Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
* Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
* Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false

=== -DrunMode=MCLiveness ===
* Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
* Use: Model checking for liveness properties - (with fairness assumptions),.
* Nondeterminism specification: Allowed (actually required by definition).
* Event selection: Systematically makes all possible combinations of event selections.
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
Stops: When counterexample is found, or when verification of all transitions / states is complete.
* Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events

=== -DrunMode=Random ===
* Description: One possible run out of many.
* Use: Demonstration or manual exploration of different possible runs.
* Nondeterminism specification: Allowed.
* Event selection: Random among all nondeterministic choices.
* Backtracking: none.
* Stops: When all b-threads end, or when there are no enabled events.
* Additional related parameters: -DrandomSeed= nnnn.

=== -DrunMode=Iter ===
* Description: An iterative run – explore all possible executions.
* Use: to assess traces and results of all possible runs resulting from nondeterministic choices.
* Nondeterminism specification: Allowed.
* Event selection: Systematically makes all possible combinations of event selections - in different runs.
* Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice.
* Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted).

=== -DrunMode=MCDet ===
Description: A deterministic run, with model-checking instrumentation. No nondeterminism. The event selection mechanism always picks the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.

=== -DrunMode=Learning/Training ===
(In development)

== Run-control Parameters ==

=== -Dsearch=BFS or -Dsearch=DFS ===
breadth or depth first search.

=== -Drecursive=true ===
Depth first search by recursive calls instead of by a application-maintained stack (ToDo...elaborate)

=== -DdisableStateHashing ===
BPJ will not recognize previously visited states.

=== -DestimatedStates ===
Control initial space allocation for state hashing

=== -DsuppressDeadlock=true ===
deadlocks will not cause a verification failure.

=== -DlogBacktracking=true ===
Issues a message with every visited BProgram state

=== -ea ===
Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.

== Memory Management Parameters ==
=== -DShallow=true/false ===

This parameter controls the serialization of objects not on the stack for backtracking during execution. See details in "Enabling your application for Model Checking".
=== -Xmn=,-Xms=,-Xmx= ===
These parameters are standard Java memory allocation parameters, and are used to define sufficient memory for large model-checking run. E.g.:

-Xmn200M
-Xms700M
-Xmx700M

Explanation:

* As Java starts, it creates within the systems memory a Java Virtual Machine (JVM). JVM is where the complete processing of any Java program takes place. All Java applications (including IQv6) by default allocate & reserve up to 64 MB of memory resource pool from the system on which it is running.
* The Xms is the initial / minimum Java memory (heap) size within the JVM. Setting the initial memory (heap) size higher can help in a couple of ways. First, it will allow garbage collection (GC) to work less which is more efficient. The higher initial memory value will cause the size of the memory (heap) not to have to grow as fast as a lower initial memory (heap) size, thereby saving the overhead of the Java VM asking the OS for more memory.
* The Xmx is the maximum Java memory (heap) size within the Java Virtual Memory (JVM). As the JVM gets closer to fully utilizing the initial memory, it checks the Xmx settings to find out if it can draw more memory from the system resources. If it can, it does so. For the JVM to allocate contiguous memory to itself is a very expensive operation. So as the JVM gets closer to the initial memory, the JVM will use aggressive garbage collection (to clean the memory and if possible avoid memory allocation), increasing the load on the system.
* If JVM is in need of memory beyond the value set in Xmx, the JVM will not be able to draw more memory from system resource (even if available) and run out of memory. Hence, the -Xms and -Xmx memory parameters should be increased depending upon the demand estimation of the system. Ideally both should be the same value (set at maximum possible as per demand estimation). This ensure that the maximum memory is allocated right at the start-up eliminating the need for extra memory allocation during program execution. It is sometimes recommended to use aggressive maximum memory (heap) size of between 1/2 and 3/4 of physical memory.
* -Xmn: the size of the heap for the young generation.
See more details in general Java reference information.

= Application-specific parameters =
You can pass parameters to your own application, and process them in standard Java techniques. E.g.,
* - nPhils=5 number of philosophers.
* leftyPhil=false is any of the philosophers left handed.

static int nPhils; // number of philosophers
static boolean leftyPhil = false; // Last Philosopher is left handed.
static {
nPhils = Integer.parseInt(System.getProperty("nPhils", "3"));
parmString += "nPhils=" + nPhils;
leftyPhil = (System.getProperty("leftyPhil","false").equals("true"));
parmString += ", leftyPhil=" + leftyPhil;
System.out.println(parmString);
}

Run Configuration Examples:

-DrunMode=MCSafety
-Drecursive=true
-Dshallow=true

-DrunMode=MCSafety
-Dsearch=DFS
-Xms300M
-Xmx1000M
-DestimatedStates=10000
-DlogBacktracking=false
-ea

BPJ Model Checking API

2014-03-19T09:45:15Z

BpAdmin: /* BPJ Model Checking API: Enabling your application for model-checking and controlling its verification */

= Enabling your application for model-checking and controlling its verification =

Before verifying an application, the application must be enabled for model checking.
This includes at least:
* Creating b-threads which simulate the environment, when applicable.
* Assigning names to states
* Determining alternative execution paths - by identifying equal priority b-threads and equal priority event requests.

B-threads can call the following API methods of the BProgram where the b-thread is added/registered
to control the model checking.

Throughout, the term Next Verification State refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.

== bSync(none,none,none)==
While in regular runs a b-thread can terminate, in a model-checking run a b-thread should not terminate. You should precede or replace the return from runBthread method with a call to bSync(none,none,none). In a regular run this call will cause normal terminatation of the b-thread but in a model checking run it will suspend the b-thread in a state prior to terminating and allow backtracking from this state.

== labelNextVerificationState(<label>)==
This API calls provides a label for the next b-thread state and indirectly to the next composite system state.

* It is the programmer's responsibility to disambiguate all relevant b-thread states of each relevant b-thread.
* The (composite) BP-state name is the concatenation all constituent bt-states.
* When BPJ model checking reaches a BP-state that was already fully checked – it backtracks.
* If a b-thread does not label its states – it is considered to have one state – and it does not increase the size of the Cartesian product. E.g. a b-thread that only counts events theoretically has infinitely many states. However, if this b-thread is known to never request or block events, it cannot affect the application flow, and if the counts do not matter in the counterexamples, there is no need to keep track of its exact state during back tracking.
* A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
* Meaningful state names can help in debugging, but since since most b-threads are simple this is not critical. E.g., the states of a "linear" b-thread can be just numbered as 1/2/3 etc. The states of a b-thread can be labeled also based on the values of the variables that determine the state change.
* State names are local to the b-thread and must be unique only within a b-thread. The BPJ model checking infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.

== markNextVerificationStateAsBad()==
Indicates detection by the b-thread of a violation of a safety property. Model checking stops and prints the sequence of events (the path) to this point as a counter example.
== markNextVerificationStateAsHot()==
This call is used for checking of liveness properties. States that are not marked as hot are considered cold. If the model checking detects a cycle in the state graph that does not contain a cold state, it stops and prints the path to this cycle and the cycle as a counter example.
== pruneSearchNow()==
This forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. This call can be used by a b-thread to accelerate the model checking by eliminating states that weren't explored, but are known to lead to results that are known or are symmetric to other states, or are otherwise not relevant in the present run.
== pruneAtNextVerificationState()==
This call forces backtracking after all b-threads reach the next state and after its badness is determined.

== setBThreadEpsilon(<double epsilon>) ==
This call defines nondeterminism between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of nondeterministic execution, backtracking and exploration of alternative execution paths.

BPJ Model Checking

2014-03-19T09:43:13Z

BpAdmin: /* Additional Information */

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BPJ execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* An application must be first enabled for model checking.

== Additional Information ==
* [[BPJ Model Checking API| BPJ Model Checking API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

BPmcAPI

2014-03-19T09:42:32Z

BpAdmin: BPmcAPI moved to BPJ Model Checking API

#REDIRECT [[BPJ Model Checking API]]

BPJ Model Checking API

2014-03-19T09:42:32Z

BpAdmin: BPmcAPI moved to BPJ Model Checking API

= BPmc API: Enabling your application for model-checking and controlling its verification =

Before verifying an application, the application must be enabled for model checking.
This includes at least:
* Creating b-threads which simulate the environment, when applicable.
* Assigning names to states
* Determining alternative execution paths - by identifying equal priority b-threads and equal priority event requests.

B-threads can call the following API methods of the BProgram where the b-thread is added/registered
to control the model checking.

Throughout, the term Next Verification State refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.

== bSync(none,none,none)==
While in regular runs a b-thread can terminate, in a model-checking run a b-thread should not terminate. You should precede or replace the return from runBthread method with a call to bSync(none,none,none). In a regular run this call will cause normal terminatation of the b-thread but in a model checking run it will suspend the b-thread in a state prior to terminating and allow backtracking from this state.

== labelNextVerificationState(<label>)==
This API calls provides a label for the next b-thread state and indirectly to the next composite system state.

* It is the programmer's responsibility to disambiguate all relevant b-thread states of each relevant b-thread.
* The (composite) BP-state name is the concatenation all constituent bt-states.
* When BPmc reaches a BP-state that was already fully checked – it backtracks.
* If a b-thread does not label its states – it is considered to have one state – and it does not increase the size of the Cartesian product. E.g. a b-thread that only counts events theoretically has infinitely many states. However, if this b-thread is known to never request or block events, it cannot affect the application flow, and if the counts do not matter in the counterexamples, there is no need to keep track of its exact state during back tracking.
* A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
* Meaningful state names can help in debugging, but since since most b-threads are simple this is not critical. E.g., the states of a "linear" b-thread can be just numbered as 1/2/3 etc. The states of a b-thread can be labeled also based on the values of the variables that determine the state change.
* State names are local to the b-thread and must be unique only within a b-thread. The BPmc infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.

== markNextVerificationStateAsBad()==
Indicates detection by the b-thread of a violation of a safety property. BPmc stops and prints the sequence of events (the path) to this point as a counter example.
== markNextVerificationStateAsHot()==
This call is used for checking of liveness properties. States that are not marked as hot are considered cold. If BPmc detects a cycle in the state graph that does not contain a cold state, it stops and prints the path to this cycle and the cycle as a counter example.
== pruneSearchNow()==
This forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. This call can be used by a b-thread to accelerate the model checking by eliminating states that weren't explored, but are known to lead to results that are known or are symmetric to other states, or are otherwise not relevant in the present run.
== pruneAtNextVerificationState()==
This call forces backtracking after all b-threads reach the next state and after its badness is determined.

== setBThreadEpsilon(<double epsilon>) ==
This call defines nondeterminism between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of nondeterministic execution, backtracking and exploration of alternative execution paths.

Nondetermism

2014-03-19T09:40:16Z

BpAdmin: /* Nondeterministic execution in BPmc */

= Nondeterministic execution in BPJ model checking =
In common processing event selection in BP is deterministic.
However, in some cases it is desired to specify nondetermistic choices - e.g., when simulating environment behavior using b-threads as part of model checking. The BPJ model checking capability explores all possible execution paths defined by this nondeterminism.
In fact, often, the only non-determinism in execution is in b-threads that simulate the environment.

== Specifiying nondeterminism ==
* In BP, event selection is deteremined by the unique priority of each b-thread, and by the order of events in the requested event set.
* When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads are considered of same priority. For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part. (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by the method call setBthreadEpsilon().
* Additionally, during model checking if an event in a requested event set of any b-thread is selected (requested and not blocked, and non-deterministic execution actually selected it), then if the event was in a nested second-level set, then all other events in the same nested second-level set are considered to be of the same priority. For example, if the requested even set is R={{e1,e2},e3,{e4,e5,e6,e7},e8} - then if e5 was selected (say, all preceding events were blocked), then e6 and e7, and only them are considered of the same priority and will be explored in non-deterministic execution. This priority processing is relevant only to the first event selection in b-thread. Once the selected second-level set is exhausted, (or if the event was a first level in the first place), non-deterministic execution continues with the next b-thread of the "same" priority as the previous b-thread.
See execution below for more details.

== Nondeterministic execution ==

When executing in model-checking mode, nondeterministic event selection is performed according to the following algorithm :

* Scan b-threads in order of priority
* Scan the requested event set of each b-thread in event order (the set is enumerable).
* When the first event that is requested and not blocked is found it is remembered as one alternative.
* If the selected event was in a second level event set (a set within a set), all its siblings in the same second level set that are not blocked are considered having the same priority, and are added as alternatives.
* If the event is in a first level of the requested event set, this event is the only one from this b-thread.
* After exploring all execution subtrees anchored at the alternatives from one b-thread go to the next b-thread of “same” priority as defined with epsilon, and repeat the above . At most one second-level set will be selected from the requested events of that b-thread, but not necessarily the first one.
* When all alternatives in a given execution path are explored the execution returns to the next higher level in the nondeterministic execution path to select the next alternative at that level.
* BPJ model checking uses the Java package javaflow to restore the stack of all b-threads in order to resume execution of another subtree at a previously visited synchronization point.

== Programming Constraints ==
* While in regular runs a b-thread can terminate, in a MC run A b-thread should not terminate, to allow BPJ model checking to backtrack. Precede/replace the return with bSync(none,none,none); In a regular run this will just terminate. In MC run it will allow the b-thread to backtrack from the end.

== Example ==

User Guide

2014-03-19T09:37:22Z

BpAdmin:

'''BPJ User Guide   ''' Contents:  

*[[Download | Downloading, installing and configuring the BPJ library, related tools and examples]]
*[http://www.wisdom.weizmann.ac.il/~bprogram/pres/BPJ%20Introduction.pdf A slide presentation: general introduction to behavioral programming]
*[[The_BPJ_Library | The BPJ library: about b-threads, events, b-programs, etc.]]
*Designing, developing and running your application (TBA. Meanwhile use general introduction prersentation and examples).
*[[Dynamic b-threads | Symbolic and dynamic and b-threads]]
*[[ TraceVis | Tracing and visualizing behavioral Java programs with TraceVis]]
*[[BPJ Model Checking | Verifying your application with the BPJ model checking ]]
*Using BPJ for hybrid fuzzy control with BFUZ (To be added).
*[[Z3BP | Working with Z3 Theorem Prover / SMT Solver ]]

BPJ Model Checking

2014-03-19T09:34:55Z

BpAdmin: /* Introduction */

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BPJ execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* An application must be first enabled for model checking.

== Additional Information ==
* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

User Guide

2014-03-19T09:34:19Z

BpAdmin:

'''BPJ User Guide   ''' Contents:  

*[[Download | Downloading, installing and configuring the BPJ library, related tools and examples]]
*[http://www.wisdom.weizmann.ac.il/~bprogram/pres/BPJ%20Introduction.pdf A slide presentation: general introduction to behavioral programming]
*[[The_BPJ_Library | The BPJ library: about b-threads, events, b-programs, etc.]]
*Designing, developing and running your application (TBA. Meanwhile use general introduction prersentation and examples).
*[[Dynamic b-threads | Symbolic and dynamic and b-threads]]
*[[ TraceVis | Tracing and visualizing behavioral Java programs with TraceVis]]
*[[BPMC | Verifying your application with the BPJ model checking ]]
*Using BPJ for hybrid fuzzy control with BFUZ (To be added).
*[[Z3BP | Working with Z3 Theorem Prover / SMT Solver ]]

BPJ Model Checking

2014-03-19T09:33:30Z

BpAdmin: BPMC moved to BPJ Model Checking

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BP execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* An application must be first enabled for model checking.

== Additional Information ==
* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

BPMC

2014-03-19T09:33:30Z

BpAdmin: BPMC moved to BPJ Model Checking

#REDIRECT [[BPJ Model Checking]]

BPJ Model Checking

2014-02-12T09:23:10Z

BpAdmin: /* Introduction */

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BP execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* An application must be first enabled for model checking.

== Additional Information ==
* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

BPJ Model Checking

2014-02-12T09:22:47Z

BpAdmin: /* Introduction */

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BP execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* [[BPmcAPI#pruneSearchNow.28.29 | An application must be first enabled for model checking]].

== Additional Information ==
* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

BPJ Model Checking

2014-02-12T09:20:27Z

BpAdmin:

= Verifying programs with BP model checking =

== Introduction ==
* You can find bugs and under-specification in behavioral programs using model checking.
* The model checking capability of BP (abbr. BPmc) is part of the overall BP execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
* An application must be first enabled for model checking.

== Additional Information ==
* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
* [[RunMode | Run modes and execution parameters for model-checking]]
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[JavaFlow | More information about enabling your application for model-checking]]

The BPJ Library

2013-08-05T10:48:23Z

BpAdmin:

See examples, e.g., BPJ/BPJCore110 -> bp.src.unittest.helloworld BPJ/Examples -> TicTacToe
Events B-threads B-Program(s) A main method:

 

== Events ==

*Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
*Instantiate or extend Event class
*Optional string name in constructor or in setName();
*Optional data fields
*See later on Event Sets

== B-Threads ==

*Contain the logic of your application
*Instantiate or extend the BThread class.
*You code runBThread() method
*Use events to affect system behavior
*Call bSync() method to request, wait for or block events
*You code import static bp.BProgram.bp
*Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
*Avoid or minimize side effects and external dependencies that are not event-driven
*Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
*You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
*Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==

*The execution environment and event-selection mechanism and for the application b-threads.
*An object of the class BProgram
*One instance of BProgram, called bp, is instantiated and made public and static for ready use by the application programmer.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The B-Application ==

*A container and entry point for the application program.
*Class BApplication
*The programmer provides an instance of this class by implementing the main method and runBApplication method.
*The method main() should starts the b-application providing the class name of the application program and the package where it can be found. Be sure to specify these correctly as problems in loading the main class may not be reported correctly.

Example:

static public void main(String arg[]) {
try {
BProgram.startBApplication(AlternatingTaps.class, "bp.unittest");
} catch (Exception e) {
e.printStackTrace();
}
}

*In the method runBApplication the programmer starts the b-threads.

Example:

 public void runBApplication() { System.out.println("runBApplication () at " + this); bp.add(new AddHotThreeTimes(), 1.0); bp.add(new AddColdThreeTimes(), 3.0); bp.add(new Interleave(), 4.0);

bp.startAll(); }

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for waited-for and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for waited-for and blocked events.
**The method contains() determines membership in the EventSetInterface object.
**This set can describe very large or infinite sets of events, or be used to filter events.
**The set can contain another EventSetInterface (neesting of sets).
**Cannot be used as the requested events parameter of bSync(), because it does not provide an interator over the concrete events.
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set - contains no event. Used in calls to bSync() when one of the three parameters should be empty.
*All: contains all events. Most commonly used in bSync() when a b-thread such as a logger waits for all events.
*EventsOfClass: all events of a given class.
*Composable event sets
**Available in BPJContrib (***ToDo: add BPJContrib to the package)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )

anyOf( A, B, theEventSet(C).and(not(d)) )

== The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*You need to provide the method runBApplicatio. In it:
** Instantiate and add b-threads to the b-program
** Start the b-threads
** You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
** Start any other parts (non-BP) of your application.
** runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):

import static bp.BProgram.bp;
public class my-app-class implements BApplication {
public void runBApplication() {
bp.add(new my-Bthread-1(), mypriority1);
bp.add(new my-Bthread-2(), mypriority2);
. . .
bp.startAll();
}
}

== Dynamic B-Threads ==

* New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...

See examples in...

== Injecting External Events ==

ToDo: add text here

[[Download | Prev]] [[BPMC|Model Checking with BPmc]]

The BPJ Library

2013-08-05T10:45:38Z

BpAdmin: /* The B-Application */

See examples, e.g., BPJ/BPJCore110 -> bp.src.unittest.helloworld BPJ/Examples -> TicTacToe
Events B-threads B-Program(s) A main method:

 

== Events ==

*Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
*Instantiate or extend Event class
*Optional string name in constructor or in setName();
*Optional data fields
*See later on Event Sets

== B-Threads ==

*Contain the logic of your application
*Instantiate or extend the BThread class.
*You code runBThread() method
*Use events to affect system behavior
*Call bSync() method to request, wait for or block events
*You code import static bp.BProgram.bp
*Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
*Avoid or minimize side effects and external dependencies that are not event-driven
*Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
*You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
*Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==

*The execution environment and event-selection mechanism and for the application b-threads.
*An object of the class BProgram
*One instance of BProgram, called bp, is instantiated and made public and static for ready use by the application programmer.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The B-Application ==

*A container and entry point for the application program.
*Class BApplication
*The programmer provides an instance of this class by implementing the main method and runBApplication method.
*The method main() should starts the b-application providing the class name of the application program and the package where it can be found. Be sure to specify these correctly as problems in loading the main class may not be reported correctly.

Example:

static public void main(String arg[]) {
try {
BProgram.startBApplication(AlternatingTaps.class, "bp.unittest");
} catch (Exception e) {
e.printStackTrace();
}
}

*In the method runBApplication the programmer starts the b-threads.

Example:

public void runBApplication() { System.out.println("runBApplication () at " + this); bp.add(new AddHotThreeTimes(), 1.0); bp.add(new AddColdThreeTimes(), 3.0); bp.add(new Interleave(), 4.0);

bp.startAll(); }

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for waited-for and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for waited-for and blocked events.
**The method contains() determines membership in the EventSetInterface object.
**This set can describe very large or infinite sets of events, or be used to filter events.
**The set can contain another EventSetInterface (neesting of sets).
**Cannot be used as the requested events parameter of bSync(), because it does not provide an interator over the concrete events.
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set - contains no event. Used in calls to bSync() when one of the three parameters should be empty.
*All: contains all events. Most commonly used in bSync() when a b-thread such as a logger waits for all events.
*EventsOfClass: all events of a given class.
*Composable event sets
**Available in BPJContrib (***ToDo: add BPJContrib to the package)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )

anyOf( A, B, theEventSet(C).and(not(d)) )

== The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*You need to provide the method runBApplicatio. In it:
** Instantiate and add b-threads to the b-program
** Start the b-threads
** You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
** Start any other parts (non-BP) of your application.
** runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):

import static bp.BProgram.bp;
public class my-app-class implements BApplication {
public void runBApplication() {
bp.add(new my-Bthread-1(), mypriority1);
bp.add(new my-Bthread-2(), mypriority2);
. . .
bp.startAll();
}
}

== Dynamic B-Threads ==

* New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...

See examples in...

== Injecting External Events ==

ToDo: add text here

[[Download | Prev]] [[BPMC|Model Checking with BPmc]]

User Guide

2013-08-05T10:44:05Z

BpAdmin:

'''BPJ User Guide   ''' Contents:  

*[[Download | Download, install and configure the BPJ library and examples]]
*[http://www.wisdom.weizmann.ac.il/~bprogram/pres/BPJ%20Introduction.pdf A general introduction to behavioral programming presentation]
*[[The_BPJ_Library | The BPJ library: b-threads, events, b-programs, etc.]]
*Designing and developing your application
*Running your application
*[[Dynamic b-threads | Dynamic b-threads]]
*[[ TraceVis | Tracing and visualizing behavioral Java programs with TraceVis]]
*[[BPMC | Verifying your application with BPmc]]
*Using BPJ for hybrid fuzzy control with BFUZ

[[Main Page|Prev]] [[UserGuidePage1|Next]]

User Guide

2013-08-04T08:01:16Z

BpAdmin:

'''BPJ User Guide   ''' Contents:  

*[[Download | Downloading, Installation and configuration ]]
*[[The_BPJ_Library | The BPJ library]]
*Designing and developing your application
*Running your application
*Debugging with TraceVis
*Verifying your application with BPmc
*Using BPJ for hybrid fuzzy control with BFUZ
*See introduction to behavioral programming in the BP Overview presentation 

[[Main Page|Prev]] [[UserGuidePage1|Next]]

User Guide

2013-08-04T08:00:18Z

BpAdmin:

'''BPJ User Guide   ''' Contents:  

*[[Download | Downloading, Installation and configuration ]]
*[[The BPJ library]]
*Designing and developing your application
*Running your application
*Debugging with TraceVis
*Verifying your application with BPmc
*Using BPJ for hybrid fuzzy control with BFUZ
*See introduction to behavioral programming in the BP Overview presentation 

[[Main Page|Prev]] [[UserGuidePage1|Next]]

Download

2013-06-26T12:04:20Z

BpAdmin: Protected "Download" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

= Download and Installation =

*Operating System:
** So far BPJ was tested mainly on Windows. It should run on Linux as well.
*IDE Requirements:
** BPJ does not depend on any specific environment. The library and examples can be used with the latest version of Eclipse, or in any other Java programming environment.
* Downloading Eclipse:
** Download Eclipse classic for Java from http://www.eclipse.org/.
** Extract the downloaded files – no installation is needed.
*Downloading and Configuring BPJ:
** Download [http://www.wisdom.weizmann.ac.il/~bprogram/code/BPJZip.zip BPJzip.zip]
** In Eclipse, import the project BPJCore110 as follows:
*** File -> Import -> General -> Existing Project into Work Space -> BPJCore110
** Rebuild the project.
** Import run configurations (optional -- Required mainly for running model-checking examples):
*** File -> Import -> Run/Debug. Then select all available configurations

[[User Guide| Prev]] | [[The BPJ Library | Next ]]

----
[http://www.b-prog.org BP Web Site]

The BPJ Library

2013-06-26T12:01:12Z

BpAdmin: Protected "The BPJ Library" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

See examples, e.g., BPJ/BPJCore110 -> bp.src.unittest.helloworld BPJ/Examples -> TicTacToe
Events B-threads B-Program(s) A main method:

 

== Events ==

*Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
*Instantiate or extend Event class
*Optional string name in constructor or in setName();
*Optional data fields
*See later on Event Sets

== B-Threads ==

*Contain the logic of your application
*You code runBThread() method
*Use events to affect system behavior
*Call bSync() method to request, wait for or block events
*You code import static bp.BProgram.bp
*Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
*Avoid or minimize side effects and external dependencies that are not event-driven
*Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
*You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
*Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==

*A container and execution environment for b-threads.
*You only need to instantiate it.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for watched and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for watched and blocked events.
**Contains() method determines membership
**Can contain very large or infinite sets of events, or be used to filter events.
**Can contain eventSetInterface
**Is not sufficient as the requested events parameter of bSync()
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set
*All: contains all events
*EventsOfClass: all events of a given class
*Composable event sets
**Available in BPJContrib (***?? What to do???)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )

anyOf( A, B, theEventSet(C).and(not(d)) )

== The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*In the method runBApplication you start the execution of your application
*Instantiate and add b-threads to the b-program
*Start the b-threads
*You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
*runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):

import static bp.BProgram.bp; public class my-app-class implements BApplication { public void runBApplication() bp.add(new my-Bthread-1(), mypriority1); bp.add(new my-Bthread-2(), mypriority2); … bp.startAll();

== Dynamic B-Threads ==

*New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...

See examples in...

== Injecting External Events ==

add text

[[Download | Prev] | [[BPMC|Model Checking with BPmc]]

The BPJ Library

2013-06-26T12:00:05Z

BpAdmin:

See examples, e.g., BPJ/BPJCore110 -> bp.src.unittest.helloworld BPJ/Examples -> TicTacToe
Events B-threads B-Program(s) A main method:

 

== Events ==

*Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
*Instantiate or extend Event class
*Optional string name in constructor or in setName();
*Optional data fields
*See later on Event Sets

== B-Threads ==

*Contain the logic of your application
*You code runBThread() method
*Use events to affect system behavior
*Call bSync() method to request, wait for or block events
*You code import static bp.BProgram.bp
*Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
*Avoid or minimize side effects and external dependencies that are not event-driven
*Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
*You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
*Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==

*A container and execution environment for b-threads.
*You only need to instantiate it.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for watched and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for watched and blocked events.
**Contains() method determines membership
**Can contain very large or infinite sets of events, or be used to filter events.
**Can contain eventSetInterface
**Is not sufficient as the requested events parameter of bSync()
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set
*All: contains all events
*EventsOfClass: all events of a given class
*Composable event sets
**Available in BPJContrib (***?? What to do???)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )

anyOf( A, B, theEventSet(C).and(not(d)) )

== The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*In the method runBApplication you start the execution of your application
*Instantiate and add b-threads to the b-program
*Start the b-threads
*You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
*runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):

import static bp.BProgram.bp; public class my-app-class implements BApplication { public void runBApplication() bp.add(new my-Bthread-1(), mypriority1); bp.add(new my-Bthread-2(), mypriority2); … bp.startAll();

== Dynamic B-Threads ==

*New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...

See examples in...

== Injecting External Events ==

add text

[[Download | Prev] | [[BPMC|Model Checking with BPmc]]

The BPJ Library

2013-06-26T11:57:39Z

BpAdmin:

See examples, e.g.,
BPJ/BPJCore110 -> bp.src.unittest.helloworld
BPJ/Examples -> TicTacToe
Events
B-threads
B-Program(s)
A main method:

== Events ==
*Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
*Instantiate or extend Event class
*Optional string name in constructor or in setName();
*Optional data fields
*See later on Event Sets

== B-Threads ==
*Contain the logic of your application
*You code runBThread() method
*Use events to affect system behavior
*Call bSync() method to request, wait for or block events
*You code import static bp.BProgram.bp
*Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
*Avoid or minimize side effects and external dependencies that are not event-driven
*Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
*You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
*Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==
*A container and execution environment for b-threads.
*You only need to instantiate it.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for watched and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for watched and blocked events.
**Contains() method determines membership
**Can contain very large or infinite sets of events, or be used to filter events.
**Can contain eventSetInterface
**Is not sufficient as the requested events parameter of bSync()
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set
*All: contains all events
*EventsOfClass: all events of a given class
*Composable event sets
**Available in BPJContrib (***?? What to do???)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )
anyOf( A, B, theEventSet(C).and(not(d)) )

==The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*In the method runBApplication you start the execution of your application
*Instantiate and add b-threads to the b-program
*Start the b-threads
*You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
*runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):
import static bp.BProgram.bp;
public class my-app-class implements BApplication { public void runBApplication() bp.add(new my-Bthread-1(), mypriority1); bp.add(new my-Bthread-2(), mypriority2); … bp.startAll();

== Dynamic B-Threads ==
*New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...
See examples in...

== Injecting External Events ==

add text

[[Download | Prev] | [[BPMC | Model Checking with BPmc]]

The BPJ Library

2013-06-26T11:56:32Z

BpAdmin:

See examples, e.g.,
BPJ/BPJCore110 -> bp.src.unittest.helloworld
BPJ/Examples -> TicTacToe
Events
B-threads
B-Program(s)
A main method:

== Events ==
Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
Instantiate or extend Event class
Optional string name in constructor or in setName();
Optional data fields
See later on Event Sets

== B-Threads ==
Contain the logic of your application
You code runBThread() method
Use events to affect system behavior
Call bSync() method to request, wait for or block events
You code import static bp.BProgram.bp
Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
Avoid or minimize side effects and external dependencies that are not event-driven
Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==
*A container and execution environment for b-threads.
*You only need to instantiate it.
*BProgram externalizes the public variable lastEvent that can be seen by b-threads.
*Usually – there is just one BProgram per application, running all your b-threads, but you may have several b-programs in parallel.
*You may change run-time parameters of the b-program by calling methods to set them.

== The bSync() Method ==

*bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
*Three parameters:
**Requested Events:
**Waited-for events (a.k.a “watched events”)
**Blocked events
*Drives the collective execution mechanism:
**Synchronizes the b-thread with the others – waits until all b-threads call bSync().
**When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set.
**All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
**B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify this field; don’t rely on it past another bSync() call.
**This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces ==

*The parameters to bSync are three sets of events, or sets of sets.
*Nesting of set containment is allowed, and not limited.
*RequestableEventInterface:
**Required for requested event parameter of bSync();
**Can be used also for watched and blocked.
**Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
**Implemented by RequestedEventsSet
*EventSetInterface:
**Can be used for watched and blocked events.
**Contains() method determines membership
**Can contain very large or infinite sets of events, or be used to filter events.
**Can contain eventSetInterface
**Is not sufficient as the requested events parameter of bSync()
**Implemented by EventSet
*RequestableEventSet: Implements both interfaces above
*EventSet: implements only EventSetInterface
*Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets ==

*None: the empty set
*All: contains all events
*EventsOfClass: all events of a given class
*Composable event sets
**Available in BPJContrib (***?? What to do???)
**Allows specification of, e.g., theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )
anyOf( A, B, theEventSet(C).and(not(d)) )

==The Application and the Main Method ==

*In the main method insert the line BProgram.startBApplication(my-app-class, my-package);
*In the method runBApplication you start the execution of your application
*Instantiate and add b-threads to the b-program
*Start the b-threads
*You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
*runBApplication may exit, or may wait for all b-threads to end.
*Example (see BPJ package for more detail):
import static bp.BProgram.bp;
public class my-app-class implements BApplication { public void runBApplication() bp.add(new my-Bthread-1(), mypriority1); bp.add(new my-Bthread-2(), mypriority2); … bp.startAll();

== Dynamic B-Threads ==
*New b-threads may be added by external (non behavioral) applications modules, or by b-threads
*A running Java thread may be registered as a b-thread and subsequently deregistered as follows:...
See examples in...

== Injecting External Events ==

add text

[[Download | Prev] | [[BPMC | Model Checking with BPmc]]

The BPJ Library

2013-06-26T11:46:10Z

BpAdmin: New page: See examples, e.g., BPJ/BPJCore110 -> bp.src.unittest.helloworld BPJ/Examples -> TicTacToe Events B-threads B-Program(s) A main method: == Events == Reflect the elements of behavior of...

See examples, e.g.,
BPJ/BPJCore110 -> bp.src.unittest.helloworld
BPJ/Examples -> TicTacToe
Events
B-threads
B-Program(s)
A main method:

== Events ==
Reflect the elements of behavior of your application (and its environment) – what you want to see in a trace.
Instantiate or extend Event class
Optional string name in constructor or in setName();
Optional data fields
See later on Event Sets

== B-Threads ==
Contain the logic of your application
You code runBThread() method
Use events to affect system behavior
Call bSync() method to request, wait for or block events
You code import static bp.BProgram.bp
Use Java freely – but don’t wait for slow things (GUI interaction should be done separately).
Avoid or minimize side effects and external dependencies that are not event-driven
Events should be natural system behavior - minimize usage of events for pure inter-b-thread communication.
You may instantiate multiple instances of same b-thread class – possibly with constructor parameters
Parameters may be manually specified during instantiation or generated by the application - see Tic-Tac-Toe example.

== The B-Program ==
A container and execution environment for b-threads.
You only need to instantiate it.
BProgram externalizes the public variable lastEvent that can be seen by b-threads.
Usually – there is just one BProgram per application, running all your b-threads, but you may have several BPrograms in parallel.
You may change run-time parameters by calling methods to set them.

== The bSync() Method

bSync(RequestableEventInterface,EventSetInterface,EventSetInterface)
Three parameters:
Requested Events:
Waited-for events (a.k.a “watched events”)
Blocked events
Drives the collective execution mechanism:
Synchronizes the b-thread with the others – waits until all b-threads call bSync().
When all b-threads are waiting in bSync – the first event that is requested and is not blocked is selected. The search order is by b-thread priority, and within it – order of events in requestable event set
All b-threads that have the selected event in their requested events set or in their waited-for event set are resumed.
B-threads can examine the event triggered by the last bSync in bp.lastEvent. Don’t modify it this field; don’t rely on it past another bSync() call.
This synchronization assumes that all b-threads will be good citizens and will not wait long (e.g., will not be involved in GUI input)

== Event Sets and Interfaces

The parameters to bSync are three sets of events, or sets of sets with unlimited nesting of set containment is allowed
RequestableEventInterface
Required for requested event parameter of bsynC();
Can be used also for watched and blocked.
Must contain an ordered set of concrete events, or ordered sets of requestableEventInterface (nesting of sets).
Implemented by RequestedEventsSet
EventSetInterface
Can be used for watched and blocked events.
Contains() method determines membership
Can contain very large or infinite sets of events, or be used to filter events.
Can contain eventSetInterface
Is not sufficient as the requested events parameter o bSync()
Implemented by EventSet
RequestableEventSet: Implements both interfaces above
EventSet: implements only EventSetInterfacs
Event: The Event class implements the above interfaces. An individual event can be used instead of any of these sets. An event is also a set that contains the event.

== Special Event Sets

None: the empty set
All: contains all events
EventsOfClass: all events of a given class
Composable event sets
Available in BPJContrib (***?? What to do???)
Allows specification of, e.g.,
theEventSet(A).and( not( theEventSet(B).or(C) ).xor( theEventSet(A).nand(c) ) )
anyOf( A, B, theEventSet(C).and(not(d)) )

==The Application and the Main Method ==

In the main method insert the line ��BProgram.startBApplication(my-app-class, my-package);

In the method runBApplication you start the execution of your application
Instantiate and add b-threads to the b-program
Start the b-threads
You must assign unique real number priority to each b-thread. The smaller the value, the higher the priority.
runBApplication may exit, or may wait for all b-threads to end.
Example (see BPJ package for more detail): ��import static bp.BProgram.bp; �public class my-app-class implements BApplication {� public void runBApplication()� bp.add(new my-Bthread-1(), mypriority1);� bp.add(new my-Bthread-2(), mypriority2);� … � bp.startAll(); ��

== Dynamic B-Threads ==
New b-threads may be added by external (non behavioral) applications modules, or by b-threads
A running Java thread may be registered as a b-thread and subsequently deregistered
See examples in...

== Injecting External Events ==

add text

[[Download | Prev] | [[BPMC | Model Checking with BPmc]]

Download

2013-06-26T11:40:03Z

BpAdmin:

Download

2013-06-26T11:30:22Z

BpAdmin:

Download

2013-06-26T11:29:57Z

BpAdmin:

= Download and Installation =

*Operating System:
** So far BPJ was tested only on Windows. But it should run on Linux as well.
*IDE Requirements:
** BPJ does not depend on any specific environment. The library and examples can be used with the latest version of Eclipse, or in any other Java programming environment.
* Downloading Eclipse:
** Download Eclipse classic for Java from http://www.eclipse.org/.
** Extract the downloaded files – no installation is needed.
*Downloading and Configuring BPJ:
** Download [http://www.wisdom.weizmann.ac.il/~bprogram/code/BPJZip.zip BPJzip.zip]
** In Eclipse, import the project BPJCore110 as follows:
*** File -> Import -> General -> Existing Project into Work Space -> BPJCore110
** Rebuild the project.
** Import run configurations (optional -- Required mainly for running model-checking examples):
*** File -> Import -> Run/Debug. Then select all available configurations

----
[http://www.b-prog.org BP Web Site]

Main Page

2013-06-26T11:10:40Z

BpAdmin:

= Behavioral Programming in Imperative Languages =

----
== BP in Java ==
[[BPJ User Guide]]

== BP in Erlang ==

== BP in Blockly and JavaScript ==

User Guide

2013-06-25T09:09:23Z

BpAdmin: Protected "User Guide" [edit=autoconfirmed:move=autoconfirmed:read=autoconfirmed]

'''BPJ User Guide   ''' Contents:  

*[[Download | Downloading, Installation and configuration ]]
*The BPJ library
*Designing and developing your application
*Running your application
*Debugging with TraceVis
*Verifying your application with BPmc
*Using BPJ for hybrid fuzzy control with BFUZ
*See introduction to behavioral programming in the BP Overview presentation 

[[Main Page|Prev]] [[UserGuidePage1|Next]]