BP Wiki - New pages [en]

Dining Philosophers

2014-05-12T08:56:24Z

Assaf: /* Dining Philosophers */

= Dining Philosophers =
In this example one can see (a) how multiple behaviors coexist independently of each other, with very simple rules for each and (b) how model-checking can help find conflicts and other desired and undesired properties.

The example can be found in the BPJ project in the source package bp.state.unittest.ph .

= Problem Description =

In the famous dining philosophers problem several philosophers are sitting at a circular table, and are either eating or thinking. At the center is a large bowl of spaghetti, which requires two forks to serve and to eat. A fork is placed in between each pair of adjacent philosophers. Each philosopher may only use the fork to her left and the fork to her right. When a philosopher finishes eating, she puts down the two forks and begins thinking again. Our present goal is to check whether deadlocks, or other starvation conditions, may occur under various philosopher behaviors.

The problem is programmed/modeled behaviorally as follows:
== Events ==
The events are the picking up and the putting down of a given fork by a given philosopher (e.g., PickUp-F2-by-P2 or PutDown-F1-by-P2)

== B-Threads ==
There is a b-thread for the behavior of each philosopher and a b-thread for each fork. In the classical
version, each philosopher b-thread repeatedly requests the sequence of events representing her picking up the fork to her right, picking up the fork to her left, putting down the right-hand fork, and then putting down the left-hand one. Each fork's b-thread
repeatedly waits for an event of picking up the fork by either of its two adjacent philosophers and then blocks its picking up
(again)until the fork is put down.

The application assists the model-checking search by labeling the four philosopher behavior states
T(thinking -- forks down), 1 (one fork up), E (eating -- two forks up) and F (finished eating -- one fork down).

The fork b-thread states are D (down) and U (up).

We use model-checking to look for violations of liveness properties, and
detect the deadlock conditions that are possible under this classical behavior.

For example, a path to a deadlock state in the case of 3 philosophers is displayed as:

Verification failed:
init->[T, D, T, D, T, D]
PickUp-F2-by-P2->[T, D, T, D, 1, U]
PickUp-F1-by-P1->[T, D, 1, U, 1, U]
PickUp-F0-by-P0->[1, U, 1, U, 1, U]
[1, U, 1, U, 1, U] is a deadlock state

where each line of the form "<event> -> <State>" describes a composite states of the entire program along the path and the event whose triggering led the program to transition from the preceding state to the current.

In the symmetry breaking approach one of the philosophers is left-handed, and thus first picks up the fork to her left, rather than the one to her right. As expected, this setup is then proven by model-checking to be deadlock-free, following checking of all possible states.

For liveness testing, the philosophers behavior b-threads marks the non-eating states as hot, and the model-checker is then
able to detect the starvation conditions that are possible if fairness is weak.

Learning

2014-04-27T18:41:31Z

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.

BP Blockly User Guide

2014-04-16T14:30:23Z

Assaf:

= BP Blockly User Guide =

= Introduction =

BP in Google Blockly is an experimental platform set to illustrate visually the basic capabilities of behavioral programming.

It is implemented in Blockly by introducing new programming blocks, and by using the co-routines (generators) facility of JavaScript.
Behavioral programs written in Blockly are translated into and executed as JavaScript programs.

= Installation / Getting started =
* Install Firefox browser version 15.0.1 or later.
* For online use: open with FireFox the designated [http://www.b-prog.org/BP_Code/apps/BP Blockly link]
* For offline/local use on your computer:
** Download the zip file containing the Blockly and JavaScript package from the download screen;
** Extract the zip file, preserving directory structure;
** Open with Firefox the file BP_Code\apps\BP\index.html;
* Look at example projects in the examples drop down, additional examples linked from this site, and the [http://bp-new-blockly.appspot.com/ tutorial]

= User Interface =

== Tabs ==
The BP Blockly interface introduces four tabs:
* Blocks: In this tab, on the left is the 'pallet' or menu of Blockly blocks to choose from, and on the right is the canvas where the application is developed.
* HTML: In this tab you program the HTML interfaces of your application, especially sensors and actuators.
* Project Blocks: In this tab you can define new application-specific blocks. For example, application specific events.
* JavaScript: This tab, shown in "debug" mode, shows the executable JavaScript generated from the Blockly code
* XML: This tab, shown in "debug" mode, shows the text file where the entire application is stored.

== Navigation ==
* To scroll click and drag the canvas up or down, or use the scroll bar.
* Note that at initial loading parts of an application may be hidden and you may need to scroll up.
* Actions: Right click offers a popup menu

= Programming =
* To create an application drag blocks onto the canvas
* To start the application click on the red "Play" button
* To provide HTML information, look at templates of existing projects and at [http://www.b-prog.org/pres/agere2012AuthorVersion.pdf AGERE!2012 paper].
* Sensor example: for translating a button click into a behavioral event
input value="StartGame"
type="button"
onclick="startGame();"
style="position:relative;background-color:LightPink;"
* To create an actuator, code
when_<eventName> = ... < mycode >
* Example actuator which changes a screen display:
input value='Status: Playing '
type="button"
when_DisplayWin ="value='Status: *** Successful*** ';alert(' !!! You Won !!! ');"
when_DisplayLose="value='Status: !!! Game Lost !!! ';alert(' !!! Game Lost !!! ');"
style="position:relative;background-color:LightPink;"

* Your application is not required to have its own GUI and HTML – you can experiment with creating interwoven behavioral flow just with events
* B-thread priority:
** Round robin: All b-threads have same priority. Events that are requested and not blocked are chosen from the different b-threads in turn.
** Strict priority: All b-threads are ordered, as determined by their top down and left-to-right placement on the canvas (presently disabled).
* Loading an existing project: Click "Load project", and browse and select an XML file where a project has been saved.
* Saving a project: Click "Save Project" and use standard browser functions to save the XML file. Close the extra tabs.
* Debugging and Event Logging:
** Use Firefox console native, or
** Use [ http://getfirebug.com/ Firebug tool]:
*** Start the application
*** In the application GUI screen – click on the firebug icon;
*** You may have to reload the application GUI screen;
*** In the firebug display click console tab;
*** In the console drop-down - make sure console is enabled;
*** Start the application
*** Watch the events in the console log.
* Do not edit the compiled JavaScript or XML file;
* Avoid spaces or periods in strings and variable names
* Sometimes the XML file may be corrupted. To avoid losing your data, save frequently in different file names and verify the file can be loaded.

= BP Programming Blocks =
With BP you have in Blockly the following new programming blocks:
* B-thread: In the version of BP for Blockly there is no separate block for behavior threads. Each contiguous set of execution blocks forms a b-thread. You can add a comment to the b-thread, indicating its name or function, but this is not mandatory. An earlier version of BP there is a container block for a b-threads.
** However, the block called "instantiate with" enables the creation of multiple b-threads with different parameters. See example in the Tic-Tac-Toe game.
* Event: Defines a e behavioral event. The event name should be entered a string inside this event block.
* Request <event>: Request an event. The event is requested and the program continues when the event is triggered.
* Wait for <event >: wait for and event. The program continues when the event is triggered.
* Blocking <event>: This container block, forbids the specified event until the code contained in it completes
* Break upon <event>: This container block executes the code contained in it, but the execution is interrupted if and when the specified event is triggered.
* b-Sync: This block is available in an earlier version of BP for Blockly, and it can specify requested, waited-for and blocked events.
* Application specific blocks: These blocks are defined by the user in the application blocks tab, and can then be used from the pallet. They can be used for events, lists and more. For example, to code an application event block, the easiest way is to copy and paste the following code changing the text "MYEVENT" to your event name (in four places).

custom.bp_event_MYEVENT = {
helpUrl: 'http://www.example.com/',
init: function() {
this.setColour(290);
this.appendDummyInput()
.appendTitle("MYEVENT");
this.setOutput(true, 'event');
this.setTooltip('');
}
};
Blockly.JavaScript.bp_event_MYEVENT = function () {
return ['"MYEVENT"', Blockly.JavaScript.ORDER_NONE];
};

= Example: Alternating Taps =

* When in BP for Blockly (under FireFox), click the drop-down menu and select "Hot and Cold".

This example contains three enabled b-threads and one disabled b-thread.

* 1. Requesting the event addHot 10 times.
* 2. Requesting the event addCold 10 times.
* 3. Forcing the alternation of the two events by waiting for two occurrences of addHot event and blocking the addCold, and vice versa, in a loop.

Experimenting:
* Try disabling the third b-thread. Both remaining b-threads will run and events will alternate, per the round robin scheduling in this version of BP for Blockly.
* Then try disabling the first b-thread. Only addCold events will be triggered.
* Then enable the third b-thread, and run the program again. No events will be triggered due the blocking of addCold.
* Click on the HTML tab and examine the HTML actuator code that displays the event text upon triggering of the events. In another implementation this code could call a JavaScript method that actually opens a water tap for a few seconds.
* The 4th b-thread was loaded disabled. This is an "actuator" b-thread that reacts to the addHot and addCold events. In this case, by displaying a window with the event text. Again, this b-thread could call a JavaScript method that performs a desired action.

= Example: The Rocket Landing Game Example =

* Download the zipped version of BP Blockly.
* To load this example click "Load Project" and browse and select bp_code/apps/bp/examples/RocketLanding.xml.

In this game the player attempts to land a rocket on a landing pad on the surface of a planet. The rocket moves downward at a fixed speed in the vertical direction. Using GUI buttons, the player can move the rocket north, south, east and west, with the goal of positioning it directly above the landing pad. The player can also press an Up button to create an exhaust burst that
suspends the rocket and prevents it from going down in the next time unit. The landing pad keeps moving on the ground either randomly or subject to an unknown plan. Four walls mark the sides of the playing area, and the rocket cannot move past them (but
does not crash when it touches them). The game is won when the rocket lands exactly on the landing pad, and is lost when it touches the ground without being fully on the pad. The rocket movement is in three dimensions and the view of the entire game scene can be manipulated (tilt, pan, etc.) in 3D.

=== Sensor Events ===

* BtnEast: User clicked East
* BtnWest: User clicked West
* BtnNorth: User clicked North
* BtnSouth: User clicked South
* TimeTick: A unit of time passed
* RocketTouchedEastWall: Rocket arrived at east wall
* RocketAwayFromEastWall: Rocket departed from east wall
* (Same for west, north and south) . . .
* TouchDown: Rocket touched launch pad and is aligned with it
* Missed: Rocket reached or passed launch pad without being aligned with it

=== Actuator Events ===
* RocketWest: Request to redraw rocket 10 pixels further to the west
* RocketEast: Request to redraw rocket 10 pixels further to the east
* RocketNorth: Request to redraw rocket 10 pixels further to the north
* RocketSouth: Request to redraw rocket 10 pixels further to the south
* RocketDown: Request to redraw rocket 10 pixels down
* PadWest: The application wishes the pad to move 10 pixels further to the west
* PadEast: The application wishes the pad to move 10 pixels further to the east
* PadNorth: The application wishes the pad to move 10 pixels further to the north
* PadSouth: The application wishes the pad to move 10 pixels further to the south
* DisplayWin: The application determined that the player won
* DisplayLose: The application determined that the player lost
* GameOver: The application determined that the game should be stopped

== The B-threads ==

The b-threads in the application can be seen on the canvas.
They react to:
* User pressing a button - request rocket move
* Time ticks - Rocket descending
* Time ticks - Landing pad moves
* Rocket reaching a wall - block movements
* Rocket departing from a wall - allow movements
* Rocket touching the ground - loss
* Rocket landing on the landing pad - win
* Etc.

A key point to observe is that the behavior when rocket reaches the walls is independent and is by blocking of a move past the wall.

= Additional Examples =

The dropdown menu provides two additional examples
* A nullification game: See explanation in [http://www.wisdom.weizmann.ac.il/~bprogram/pres/agere2012AuthorVersion.pdf AGERE 2012 paper]
* A basic game of Tic-Tac-Toe: This example, with very basic strategies, demonstrates the instantiation of a b-thread according to a parameter list. For example, the application block "all Squares" represents a list of all possible squares, and a b-thread is instantiated for each one of these, waiting for a user click in this square, and requesting an X event in the same square.

Flight of a flock of birds

2014-04-15T11:56:45Z

Assaf: /* Requirements - from each bird */

= 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.
* [http://www.wisdom.weizmann.ac.il/~bprogram/videos/flock25Gather.avi Movie: 25 birds gathering and flying]
* [http://www.wisdom.weizmann.ac.il/~bprogram/videos/flockScare.mp4 Movie: Birds disperse in reaction to a "scare" action]

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

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

Sudoku

2014-04-15T11:17:37Z

Assaf: /* Playing b-threads */

= 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.
* PlaceANumberInABox: With an instance for each digit and each place in the box, this b-thread tries to place a particular digit in the box. 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.

Water Tap

2014-04-15T10:02:09Z

Assaf: /* Alternating Taps Example */

= Alternating Taps Example =

Below is the full source code of the alternating water taps example. It is part of the BPJ package.

== Events ==
* addHot
* addCold

== b-Threads ==
* addHotThreeTimes: requests addHot 3 times
* addColdThreeTimes: requests addCold 3 times
* Interleave: Causes alternation between addHot and addCold events by blocking one while waiting for the other and vice versa.

An additional b-thread DisplayEvents (commented out) indicate how one could use these events to drive external outputs, such as real water tap actuators.

== Source Code ==

public class AlternatingTaps implements BApplication {
@SuppressWarnings("serial")
static class TapEvent extends Event {

public TapEvent(String name) {
this.setName(name);
}

}

static TapEvent addHot = new TapEvent("AddHot");
static TapEvent addCold = new TapEvent("AddCold");

@SuppressWarnings("serial")
public class AddHotThreeTimes extends BThread {
public void runBThread() throws BPJException {
for (int i = 1; i <= 3; i++) {
bp.bSync(addHot, none, none);
}
}
}

@SuppressWarnings("serial")
public class AddColdThreeTimes extends BThread {
public void runBThread() throws BPJException {
for (int i = 1; i <= 3; i++) {
bp.bSync(addCold, none, none);
}
}
}

@SuppressWarnings("serial")
public class Interleave extends BThread {
public void runBThread() throws BPJException {
while (true) {
bp.bSync(none, addHot, addCold);
bp.bSync(none, addCold, addHot);
}
}
}

@SuppressWarnings("serial")
public class DisplayEvents extends BThread {
public void runBThread() throws BPJException {
while (true) {
bp.bSync(none, all, none);
System.out.println("Physically turned water tap per event: " + bp.lastEvent);
}
}
}

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

bp.startAll();
}

static public void main(String arg[]) {
try {

BProgram.startBApplication(AlternatingTaps.class, "bp.unittest");

} catch (Exception e) {
e.printStackTrace();
}
}

}

Helicopter flight and mission

2014-04-07T08:33:45Z

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.

Tic-Tac-Toe

2014-04-07T07:35:35Z

Assaf: /* Verification Example */

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

BPJ Programming Examples

2014-04-07T07:29:19Z

Assaf: /* BPJ Programming Examples */

JavaFlow

2014-01-16T11:35:03Z

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.

BPmcAPI

2014-01-16T05:24:30Z

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.

Z3BP

2014-01-16T05:01:05Z

Assaf: /* Verifying your application */

= Verifying behavioral programs with the Z3 Theorem Prover / SMT Solver =

== Installation ==
* See [http://www.wisdom.weizmann.ac.il/~bprogram/emsoft13 reference materials ]
* Required Environment: Windows 7, Eclipse.
* Install latest version of Z3 from Z3 Web Site (at the time of writing this page the version is 4.1). Note that the software is under a Microsoft Research folder.
* Install Python version 2.7.3 from Python web site. Presently the latest version of Z3 does not support the latest version of Python version. The following instructions assume that you have installed Python into C:\Python27\ on your computer.
* Install PyDev from Pydev web site as follows: find and copy the link for PyDev Eclipse plugin. Open Eclipse. Click "help" and "install new software". Add the plugin location and install. During installation check and approve the certificate trust.
* Create a Z3 project. Eclipse -> "file" -> "import project" -> "general" -> "existing project into workspace" (do not copy into workspace). The project will be marked red.
* Define Interpreter: In Eclipse, open PyDev perspective, right click on the project, select "properties" and then "python interpreter". Define as C:\Python27\python.exe.
* Define PYTHONPATH: In Eclipse: Select "Window" -> "Preferences" -> "PyDev" -> "Interpreter PYTHON" -> "PYTHONPATH" -> "New Folder". Add to the Python path the Python folder within Z3, e.g., C:\Program Files (x86)\Microsoft Research\Z3-4.1\python.
* Define Windows Path: Add to windows system path variable the bin folder of z3 C:\Program Files (x86)\Microsoft Research\Z3-4.1\bin.
* Change appearance: In Eclipse, select "Window" -> "Preferences" -> "PyDev" -> "Editor" (click on it) -> "Aptana themes" -> "Eclipse".

== Verifying your application ==
* See Z3 information for Z3 syntax and its Python interface.
* See examples in the provided project how to define b-thread properties.
* Modify the example, introducing new b-thread properties, but preserving BP composition properties.
* Run the model.