Welcome

BPjs is a library for executing behavioral programs written in Javascript. It can be used from the commandline, or embedded in a Java application.

BPjs is an open source project, maintained by a research group in Ben-Gurion University of the Negev, Israel. The code is available on GitHub. This project, as well as the concepts behind it, were presented at Devoxx Belgium 2018.

Here you can learn about writing and executing BPjs programs, embedding BPjs programs in larger Java systems (or any JVM-based systems, really), and extending and modifying BPjs’ behavior.

What’s Here

• Learn Behavioral Programming: If you are new to Behavioral Programming (that’s alright, it’s a fairly new concept), you’re invited to read the quick intro.
• Use BPjs from a console/commandline: see Running BPjs from the Commandline.
• Use BPjs as a library in a software system: If you’re using maven, just add BPjs as a dependency. Otherwise, you can download a .jar file.
• Verify BPjs Programs/Models see Verification.
• Learn more about how to use, embed, and extend BPjs: Read below.
• How to Cite If you use BPjs in an academic work, please consider citing it as mentioned here.

Topics:

Obtaining BPjs

BPjs is available in multiple packagings. Selecting the which packaging is right for you depends on the way you plan to use it.

Running BPjs from the Commandline

This is a .jar file containing all the dependencies needed for running BPjs, so it’s the only file you need. Useful for running BPjs stand-alone. This file is available at our release page, with the suffix “.uber.jar”.

Using Maven

BPjs is on Maven Central! Just add the following dependency to your <dependencies> section in pom.xml:

<dependency>
    <groupId>com.github.bthink-bgu</groupId>
    <artifactId>BPjs</artifactId>
    <version>[0.8.0, 0.9.9]</version>
</dependency>

Using .jar Files

BPjs is released using two .jar files, available at our release page:

• BPjs-{version}.jar Contains only BPjs’ classes. Use this if you want to manage the BPjs’ dependencies yourself.
• BPjs-{version}.uber.jar Contains BPjs and its dependencies. Use this to execute BPjs programs, or if you are certain BPjs’ dependencies are different from the dependencies of the rest of your project. Otherwise, classpath clashes might occur.

Compile from Source

BPjs is built using Apache Maven. Thus, you need to install Maven, or have an IDE that supports it. The BPjs team uses mostly NetBeans, but Eclipse and IntelliJ IDEA should work too.

1. Download the sources from BPjs’ GitHub repo, either by cloning, or as a .zip file.
2. To build a regular .jar, use mvn package
3. To build an “über” jar, containing all program dependencies, use mvn package -P uber-jar

Writing Programs in BPjs

BPjs is an environment for running Behavioral Programming programs written in Javascript. After completing this tutorial, you will be familiar with the basic concepts of Behavioral Programming, and will be able to write and run programs in BPjs.

What is Behavioral Programming?

Behavioral Programming, or BP for short, is based on scenarios. BP programs are composed of threads of behavior, called b-threads. B-threads run in parallel to coordinate a sequence of events via a synchronized protocol. During program execution, when a b-thread wants to synchronize with its peers, it submits a statement to the central event arbiter using the bp.sync statement.

A bp.sync statement declares which events the b-thread requests, which events it waits for (but does not request), and which events it would like to block (that is, prevent from being selected). Blocked and waited-for events can be described using a predicate or a list. Requested events have to be specified explicitly.

After calling bp.sync, the b-thread is blocked, waiting for the rest of the b-threads to synchronize (call bp.sync) as well. When all b-threads have submitted their statements, the arbiter selects an event that was requested but not blocked. It then wakes up the b-threads that requested or waited for that event. The rest of the b-threads remain blocked, until an event they requested or waited for is selected.

Behavioral Programming was introduced by Harel, Marron and Weiss in 2012 in a paper published at the Communications of the ACM.

Note

The bp.sync in BPjs expands on the “classic” bsync defined in the ACM paper: it contains an interrupt event set, and may contain a hint to the event selection strategy.

How come BPjs does not use bsync?

The classic BP literature uses the term bsync for behavioral synchronization between b-threads. BPjs used to have a bsync pseudo-keyword, but we replaced it with bp.sync. This change packs almost everything BP under the bp object, and also makes it easier to synchronize from any code executed by the b-thread (including called functions). Equally important, is does not add a new keywords to Javascript.

Tutorial

This tutorial will introduce you to BP principles and to the BPjs api. After completing it, you will be able to write BPjs programs. That’s the technical part, though. Properly thinking in BP and in general scenario-based programming - well, that would probably take longer, as with any new programming paradigm.

Hello BPjs World

Let’s start by writing the traditional hello, world! program. Instead of writing characters to the console, our program will generate two events, in the following order:

1. A “Hello” event
2. A “World” event

We assume you have downloaded and installed BPjs. This process is explained in Obtaining BPjs.

The Sequential Version

The “Hello, World” version below (source) contains a single b-thread, requesting the two events in sequence. Since it is the only b-thread in the program, these events are not blocked by anyone, and are the only available events. Thus, the arbiter select each one of them as they are requested.

bp.registerBThread(function(){
  bp.sync({request:bp.Event("hello")});
  bp.sync({request:bp.Event("world")});
})

This is not a very complicated example, but it does show a few basics worth mentioning. First, b-threads are normal javascript functions that take no parameters. They are added to the b-program using bp.registerBThread. Note that the b-program is never explicitly started by the client code. Starting the b-program is done by BPjs for you.

Lines 2 and 3 contain a very simple bp.sync statement, requesting an event. The events are created using the event factory bp.Event(...). This code uses the simple version of bp.Event, passing the event name only. We’ll see more of bp.XXX and bp.sync soon, but first let’s run this program and see what happens.

Running this example

Assuming bpjs.jar is the name of the BPjs jar, and that is it available at the system’s PATH, running the program is done like so:

 1 $ java -jar bpjs.jar hello-world-seq.js
 2 #  [READ] /path/to/hello-world-seq.js
 3 -:BPjs Added autoadded-1
 4 #  [ OK ] hello-world-seq.js
 5 ---:BPjs Started
 6  --:BPjs Event [BEvent name:hello]
 7  --:BPjs Event [BEvent name:world]
 8 ---:BPjs No Event Selected
 9 ---:BPjs Ended

Lines 2 and 4 logs the loading and successful execution of the source file hello-world-seq.js. Line 3 records the addition of a b-thread (done in line 1 of the source). Lines 5-9 follow the execution of our little program. It starts, then the events are selected (“hello” and “world”, as required). Then, no event is selected, so the program termintes.

Note the lifecycle of the program: files are first loaded and interpreted, and only then the b-program start all its b-threads. This will be important later, when we add b-threads dynamically. More on that later. Now, let’s create a more complex version of “hello, world!”.

Hello World with Wait

Below is an updated version (source), containing two b-threads. One b-thread, called bt-hi, requests the “hello” event and then terminates. The other b-thread, “bt-world”, waits for the first event (line 2), and then requests the “world” event. The b-threads are named using the two-argument version of bp.registerBThread, whose first parameter is the name of the b-thread, and second parameter is the b-thread itself.

The trace, or sequence of events generated by this program, is equivalent to that of The Sequential Version. The program structure, on the other hand, is very different, as each requested event is done by a specific b-thread. However, bt-world is quite coupled to bt-hi, as it waits for a specific event it emits. If the greeting would change to "shalom", "holà", or "goodbye", the program will break, unless bt-world is updated. This makes total sense in an eight-lines program, but in real world we would like to reduce coupling and increase cohesion. Let’s see BP’s take on this challenge.

bp.registerBThread("bt-world",function(){
  bp.sync({waitFor:bp.Event("hello")});
  bp.sync({request:bp.Event("world")});
})

bp.registerBThread("bt-hi", function(){
  bp.sync({request:bp.Event("hello")});
})

Hello Block World

Here is what we’d ideally like to have (source):

bp.registerBThread("bt-hi", function(){
  bp.sync({request:bp.Event("hello")});
})

bp.registerBThread("bt-world",function(){
  bp.sync({request:bp.Event("world")});
})

Each b-thread is responsible for requesting its event only, so the code is very cohesive. But alas, the program may generate the events in the wrong order. This is because the event arbiter can choose which event to select first. In the example below, we have two runs generating different traces.

 1 $ java -jar bpjs.jar hello-world-decoupled.js
 2 #  [READ] /path/to/hello-world-decoupled.js
 3   -:BPjs Added bt-hi
 4   -:BPjs Added bt-world
 5 #  [ OK ] hello-world-decoupled.js
 6 ---:BPjs Started
 7  --:BPjs Event [BEvent name:hello]
 8  --:BPjs Event [BEvent name:world]
 9 ---:BPjs No Event Selected
10 ---:BPjs Ended
11 
12 $ java -jar bpjs.jar hello-world-decoupled.js
13 ...
14 ---:BPjs Started
15  --:BPjs Event [BEvent name:world]
16  --:BPjs Event [BEvent name:hello]
17 ...

To prevent the wrong order of events, we can add this additional b-thread (source). It solves the “world before hello” issue by blocking the world event from being selecting, until the hello event is. This is done by passing bp.Event("world") as the block parameter of bp.sync.

bp.registerBThread("hello world Patch", function(){
  bp.sync({waitFor:bp.Event("hello"), block:bp.Event("world")});
})

We can now run both files in a single b-program, like so. Note that we are passing two files to the bpjs runtime:

 1 #  [READ] /Users/michael/Documents/PhD/Thesis/code/bThink-BGU/BPjs/docs/source/BPjsTutorial/code/hello-world-decoupled.js
 2 -:BPjs Added bt-hi
 3 -:BPjs Added bt-world
 4 #  [ OK ] hello-world-decoupled.js
 5 #  [READ] /Users/michael/Documents/PhD/Thesis/code/bThink-BGU/BPjs/docs/source/BPjsTutorial/code/hello-world-decoupled-patch.js
 6   -:BPjs Added hello world Patch
 7 #  [ OK ] hello-world-decoupled-patch.js
 8 ---:BPjs Started
 9  --:BPjs Event [BEvent name:hello]
10  --:BPjs Event [BEvent name:world]
11 ---:BPjs No Event Selected
12 ---:BPjs Ended

The last example demonstrate how BP is suited for incremental, modular software development. We have changed the overall behavior of our b-program by adding new code, rather than by changing existing one. This change can be pulled out with no change to the rest of the program, in case we decide the order of the events does not matter.

Hello BPjs World

Finally, let’s change the program such that its trace read “hello BPjs world”. Again, this can be done by adding the following b-thread (source).

bp.registerBThread("bpjs addition", function(){
  bp.sync({waitFor:bp.Event("hello")});
  bp.sync({request:bp.Event("BPjs"), block:bp.Event("world")});
})

Result:

 1 $ java -jar bpjs.jar hello-world-decoupled.js hello-world-decoupled-patch.js hello-world-bpjs.js
 2 #  [READ] /path/to/hello-world-decoupled.js
 3 -:BPjs Added bt-hi
 4 -:BPjs Added bt-world
 5 #  [ OK ] hello-world-decoupled.js
 6 #  [READ] /path/to/hello-world-decoupled-patch.js
 7 -:BPjs Added hello world Patch
 8 #  [ OK ] hello-world-decoupled-patch.js
 9 #  [READ] /path/to/hello-world-bpjs.js
10 -:BPjs Added bpjs addition
11 #  [ OK ] hello-world-bpjs.js
12 ---:BPjs Started
13 --:BPjs Event [BEvent name:hello]
14 --:BPjs Event [BEvent name:BPjs]
15 --:BPjs Event [BEvent name:world]
16 ---:BPjs No Event Selected
17 ---:BPjs Ended

Event Sets

When a b-thread requests an event, it has to be specific. That is, the b-thread has to provide an event instance as a parameter to bp.sync. This is not the case for waited-for and blocked events: these are specified by an event set. An event set contains other events. It is a set in the mathematical sense - it does not have to store the events it contains in a data structure, just to answer yes or no when asked whether it contains them. Accordingly, an event set is defined by a function that accepts an event and returns true or false.

An event is a special type of event set - an event set that contains only itself. So we get that:

const eventA = bp.Event("A");
const eventB = bp.Event("B");

eventA.contains(eventA); // true
eventA.contains(eventB); // false

An event set can be specified in the following ways:

• If the set contains a single event, the event itself serves as an event set. We used this in the Hello BPjs World example.

• By composing events through their composition methods or, and, negate, xor, nor, and nand:

  const aOrB = bp.Event("A").or( bp.Event("B") ); // contains events "A" and "B"
  const notA = bp.Event("A").negate(); // all events except "A"
  const notAOrB = bp.Event("A").or( bp.Event("B") ).negate(); // contains all events
                                                              // except for "A" and "B"
  

• By using the bp.eventSets utility object:

  const aOrB = bp.eventSets.anyOf( bp.Event("A"), bp.Event("B") );
  const conj = bp.eventSets.allOf( es1, es2 ); // events that are members of event sets ``es1`` and ``es2``.
  const notA = bp.eventSets.not( bp.Event("A") ); // all events except "A".
  

• By an EventSet object. These have name and a predicate that takes an event and returns a boolean result: true if the event is a member of the set, and false otherwise. This way of defining event sets is verbose, but allows for fine-grained control over the set containment logic:

bp.EventSet( "eventsWhoseNameStartsWithA", function(evt){
  return (evt.name.indexOf("A")==0);
});

• An array of event sets is a translated to a disjunction (or) of those events (however, this is an old form which is not encouraged anymore, since it’s not intuitive whether the semantics are of AND or of an OR).:

bp.sync({waitFor:[evt1, evt2, evt3], block:evt500}); // same as evt1.or(evt2).or(evt3)

Tip

The utility object bp.eventSets has two useful event set constants: bp.eventSets.all, which contains all events, and bp.eventSets.none, which is an empty set.

Example: Keep Serving Coffee

Consider a coffee shop that serves some teas, sparkling water, and – surprise – coffees. Customers come and request their drink. To make sure the coffee is always freshly ground, the ground coffee container is just large enough to contain the amount needed for ten cups. Thus, after the tenth coffee, the baristas has to stop taking coffee orders and go grind some coffee. They can serve other orders, though. The code below (full source) models this.

First off, we need to generate the orders. Nothing fancy here, just your usual event requesting for-loop.

bp.registerBThread("orders", function(){
  var drinks=["black tea", "green tea", "espresso coffee", "flatwhite coffee",
              "latte coffee", "sparkling water"];
  // order 100 drinks
  for (var i = 0; i < 100; i++) {
    var idx = Math.floor(Math.random()*drinks.length);
    bp.sync({request:bp.Event(drinks[idx])});
  }
});

The “orders” b-thread generates one hundred random orders. We now need to detect which orders are coffee orders, and then count them. We could list all the coffee order events in an array, but since their names end with “coffee”, a more elegant solution would be using a predicate that detects this, and wrapping it in an EventSet. This event set is defined in lines 2-4 in the listing below.

bp.registerBThread("coffee supply", function() {
  var coffeeOrderES = bp.EventSet( "coffee orders", function(evt){
    return evt.name.endsWith("coffee");
  });
  while ( true ) {
    for ( var i=0; i<10; i++ ) {
      bp.sync({waitFor:coffeeOrderES});
    }
    bp.sync({request:bp.Event("Grind more coffee!"),
           block:coffeeOrderES});
  }
});

Danger

At the moment, JavaScript arrow functions are only partially supported for event sets; They work great when running, but might break verification. Until this gets fixed in Rhino, we recommend using old-school functions for event sets (and everywhere else when writing BPjs code).

After defining the event set for coffee orders, the “coffee supply” b-thread loops forever, waiting for coffee order events (line 7). After ten orders, when it’s time to grind more coffee, it blocks coffee orders from happening, and requests a coffee grinding event (the bp.sync at lines 10-11). Until the coffee grinding event is selected, no coffee order can be selected.

Note

Rather than counting how many coffees were made using some variable, the “coffee supply” b-thread loops for 10 times, waiting for coffee to be ordered. This is an example for the classic scenario style: X has to happen Y times, and then we do Z.

Here’s a sample output of this b-program (annotated):

$ java -jar BPjs.jar eventsets.js
#  [READ] /.../eventsets.js
  -:BPjs Added orders
  -:BPjs Added coffee supply
#  [ OK ] eventsets.js
---:BPjs Started
 --:BPjs Event [BEvent name:green tea]
 --:BPjs Event [BEvent name:green tea]
 --:BPjs Event [BEvent name:espresso coffee]  «1»
 --:BPjs Event [BEvent name:latte coffee]     «2»
 --:BPjs Event [BEvent name:sparkling water]
 --:BPjs Event [BEvent name:espresso coffee]  «3»
 --:BPjs Event [BEvent name:black tea]
 --:BPjs Event [BEvent name:espresso coffee]  «4»
 --:BPjs Event [BEvent name:latte coffee]     «5»
 --:BPjs Event [BEvent name:black tea]
 --:BPjs Event [BEvent name:black tea]
 --:BPjs Event [BEvent name:sparkling water]
 --:BPjs Event [BEvent name:sparkling water]
 --:BPjs Event [BEvent name:espresso coffee]  «6»
 --:BPjs Event [BEvent name:flatwhite coffee] «7»
 --:BPjs Event [BEvent name:espresso coffee]  «8»
 --:BPjs Event [BEvent name:latte coffee]     «9»
 --:BPjs Event [BEvent name:black tea]
 --:BPjs Event [BEvent name:espresso coffee]  «10»
 --:BPjs Event [BEvent name:Grind more coffee!] «**Grind**»
 --:BPjs Event [BEvent name:flatwhite coffee] «11»
 --:BPjs Event [BEvent name:sparkling water]
 --:BPjs Event [BEvent name:black tea]
 ... continues ...

Creating Complex Behaviors Using Simpler Ones

The coffee shop program also serves as an example for the BP way of composing complex behavior from simpler ones. Baristas serves drinks when they are ordered. They also grind coffee when the ground coffee supply is low. Using BP, these behaviors can be described separately by the programmer, so they are easy to maintain and reason about. At runtime, the BP execution engine – BPjs, in our case – combines them into the required complex behavior.

Logging

As our programs become more complex, some logging/printf capabilities are needed (sorry, no debugger yet). So, let’s take a short break from Behavioral Programming in BPjs, and meet bp.log.

bp.log is a logger object. Logging is done to standard out (System.out, to be specific). There are four log levels, so while developing you can turn messages on and off, to help you focus on the problematic areas. The below program exercises the logger a bit:

bp.log.info("registering b-threads - start");
var LOG_LEVELS = ["Fine", "Info", "Warn", "Off"];

bp.registerBThread( "event generator", function(){
  for (var i = 0; i < LOG_LEVELS.length; i++) {
    bp.sync({request:bp.Event("event " + String(i))});
  }
});

bp.registerBThread( "event logging", function() {
  var idx = 0;
  while (true) {
    var evt = bp.sync({waitFor:bp.all});
    bp.log.setLevel(LOG_LEVELS[idx]);
    bp.log.warn( evt.name );
    bp.log.info( evt.name );
    bp.log.fine( evt.name );
    idx++;
  }
})

bp.log.info("registering b-threads - done");

The “event generator” creates four events, one for each logging level. The “event logging” b-thread waits for all events (note the use of bp.all), sets the logger level (line 14), and attempts to log in all three log methods (lines 15-17). Here is the program output. Note that after event 3, where the level is set to "Off", no messages are emitted at all.

#  [READ] /.../logging.js
[JS][Info] registering b-threads - start
  -:BPjs Added event generator
  -:BPjs Added event logging
[JS][Info] registering b-threads - done
#  [ OK ] logging.js
---:BPjs Started
 --:BPjs Event [BEvent name:event 0]
[JS][Warn] event 0
[JS][Info] event 0
[JS][Fine] event 0
 --:BPjs Event [BEvent name:event 1]
[JS][Warn] event 1
[JS][Info] event 1
 --:BPjs Event [BEvent name:event 2]
[JS][Warn] event 2
 --:BPjs Event [BEvent name:event 3]
---:BPjs No Event Selected
---:BPjs Ended

Caution

Later versions might integrate BPjs with a full-blown logging system, such as logback or log4j2. Programs relying on the exact logging format may need to change once the logging is updated. If you need to write a program that relies on accurate interpretation a b-program life cycle and selected events, consider implementing a BProgramRunnerListener.

Note

Logging does not have to go to System.out. Client code can set its destination PrintStream by calling BProgram#setLoggerOutputStreamer.

Message Formatting

The BPjs logger formats messages using Java’s MessageFormat. Under the hood, JavaScript objects are printed using a special formatter, which gives more information that the default cryptic [object object]. The code below contains some formatting examples:

const obj = {hello: "World", idioms:["request","waitFor","block"]};
const stuff = new Set();
stuff.add("thing 1");
stuff.add("thing 2");
stuff.add("thing 42");

bp.log.info("Here is field hello: {0} of object {1}", obj.hello, obj);
bp.log.info("Here is are some {1}: {0}", stuff, "stuff");

bp.log.info("I have a {0,number} reasons to block this event.", 1000000);
bp.log.info("{0} {0,number,#.##} {0,number,#.####}", 3.14159);

[BP][Info] Here is field hello: World of object {JS_Obj hello:"World", idioms:[JS_Array 0:"request" | 1:"waitFor" | 2:"block"]}
[BP][Info] Here is are some stuff: {JS_Set "thing 1", "thing 2", "thing 42"}
[BP][Info] I have a 1,000,000 reasons to block this event.
[BP][Info] 3.142 3.14 3.1416

Caution - Array Ambiguity

A curious API edge-case occurs when using message formatting, and passing a single variable for printing, AND said single variable is an array. The system auto-spreads the array, and only the first item of the array is printed. So the following code:

bp.registerBThread("t1",function(){
  bp.log.info("array:{0}", ["x","y","z"]);
});

Prints this:

[BP][Info] array:x

To work around this, either include a dummy variable, or wrap the array in another array:

bp.log.info("array:{0}", [["x","y","z"]]);
bp.log.info("array:{0}", ["x","y","z"], "dummy val");

Events with Data

All events in BPjs have a name. A name alone can get you quite far, but sometimes a programmer wants to send data in a more structured way, and without to- and from- string roundtrips. For this reason, events also contain a data field, which holds a standard Javascript object. The event’s name is available through its name field. Client code can initialize an event with data like so:

var anEvent = bp.Event("answer", {value:42, scope:"everything"});
bp.log.info(anEvent.name); // logs "answer"
bp.log.info(anEvent.data.value); // logs 42
bp.log.info(anEvent.data.scope); // logs "everything"

Adding data to events allows for a more complex interaction between b-threads. The b-threads in the example (source) below collaborate in order run to count to 10.

The first b-thread requests three events: two with no data, and one with a counter type and a 0 value. Note that the use of type here is convention only; there’s no static type system in place to enforce type correctness.

bp.registerBThread("starter", function(){
  bp.sync({request:bp.Event("Just an Event")});
  bp.sync({request:bp.Event("withData", {type:"counter",value:0})});
  bp.sync({request:bp.Event("Just an Event")});
});

The next b-thread is responsible for increasing the counter. Note the event set in charge of detecting counter events. Code accessing the data field of an event must use caution, as that field is often null.

bp.registerBThread("Increaser", function(){
  var counterEvents = bp.EventSet("counters", function(evt) {
    return (evt.data==null) ?
              false :
              evt.data.type && evt.data.type=="counter";
  });
  var counterEvt = bp.sync({waitFor:counterEvents});
  while (true) {
    bp.log.info( counterEvt.name + ": " + counterEvt.data.value );
    var next = bp.Event(counterEvt.name, {type:counterEvt.data.type,
                                         value:counterEvt.data.value+1});
    counterEvt = bp.sync({request:next});
  }
});

Finally, a third b-thread prevents the counter from reaching 10. Apart from the event set detecting counter events with value of 10, the body of the “Capper” b-thread consists of a single bp.sync which blocks these events. This is a common idiom in BP, in order to prevent something that “should never happen”.

bp.registerBThread("Capper", function() {
  var countersAt10 = bp.EventSet("done", function(evt) {
    return (evt.data==null) ?
            false :
            evt.data.type=="counter" && evt.data.value==10;
  });
  bp.sync({block:countersAt10});
});

Interrupting Event Set

Sometimes, given an event, it’s pointless to continue a certain behavior. For example, while preparing a cake, one needs to:

1. Buy the Ingredients
2. Mix them (it is a very simple cake)
3. Bake the mixture
4. Decorate the cake
5. Serve!

If the baking stage fails, it is pointless to decorate and serve, and so this entire behavior has to terminate.

In order to help modeling such scenarios, BPjs allows passing a set of interrupting events to bp.sync. When an event that’s a member of the interrupting event set of a given b-thread is selected, that b-thread is terminated. This is demonstrated in the code below (source).

var CAKE_REQUEST = bp.Event("Cake Please");
var CAKE_READY   = bp.Event("Cake Served");

bp.registerBThread("Customer", function(){
  bp.sync({request:CAKE_REQUEST});
  bp.sync({waitFor:CAKE_READY});
});

The first b-thread requests a cake. Nothing much to note here, except the usage of a global variable (CAKE_REQUEST) to store an event shared between a few b-threads. Let’s look at the oven:

bp.registerBThread("Oven", function(){
  bp.sync({waitFor:bp.Event("Bake Start")});
  if ( bp.random.nextBoolean() ) {
    bp.sync({request:bp.Event("Cake Burnt"), block:bp.Event("Bake End")});
  } else {
    bp.sync({request:bp.Event("Cake Ready"), block:bp.Event("Bake End")});
  }
});

The “Oven” b-thread waits for a "Bake Start" event. When this event is selected, it starts baking the cake - but has a 50% chance of burning it. This is something the the “baker” b-thread has to protect itself against.

Note

The “Oven” b-thread code uses bp.random.nextBoolean() rather than Javascript’s standard Math.random(). This is done in order to allow model checking: we can execute the code once and enforce nextBoolean to return true, and then run it again and make it return false.

bp.registerBThread("Baker", function() {
  bp.sync({waitFor:CAKE_REQUEST});
  bp.sync({request:bp.Event("Buy Ingredients")});
  bp.sync({request:bp.Event("Mix Ingredients")});
  bp.sync({request:bp.Event("Bake Start")});
  bp.sync({waitFor:bp.Event("Cake Ready"),
       interrupt:bp.Event("Cake Burnt")});
  bp.sync({request:bp.Event("Decorate")});
  bp.sync({request:CAKE_READY});
});

The “baker” b-thread is a classic scenario, listing the stages of making a cake, once it’s requested. Classic, except for the bp.sync at line 6, where the Cake Burnt event is declared to be interrupting. If, while waiting for the baking to complete, the cake burns, the baker terminates. Which is preferable to decorating and serving a burnt cake.

Note

Interrupting events do not add new capabilities to BP. This can be modeled by adding them as a waitFor parameter to bp.sync, and then examining whether it is a member of the interrupting event set. Still, declaring event as interrupting adds declarative expressiveness (which, in turn, aids program analysis), and is more convenient.

Here’s the output of an unsuccessful baking attempt:

$ java -jar BPjs.jar interrupts.js
#  [READ] /.../interrupts.js
  -:BPjs Added cake request
  -:BPjs Added Oven
  -:BPjs Added baker
#  [ OK ] interrupts.js
---:BPjs Started
 --:BPjs Event [BEvent name:Cake]
 --:BPjs Event [BEvent name:Buy Ingredients]
 --:BPjs Event [BEvent name:Mix Ingredients]
 --:BPjs Event [BEvent name:Bake Start]
 --:BPjs Event [BEvent name:Cake Burnt]
  -:BPjs Removed baker
---:BPjs No Event Selected
---:BPjs Ended

Final Acts of an Interrupted B-Thread

A b-thread can specify a handler function for interrupting events. If the b-thread is interrupted, that function is invoked, with the interrupting event as a parameter.

The function can be used for clean up and logging, but as it is not executed as a b-thread, it cannot call ``bp.sync``. It can, however, enqueue events externally. Let’s revisit the last example, and enqueue a “sorry, no cake” event to inform the customer (source). The enqueued event is presented to the b-program as an external event; this is because the interrupt handler is external to the b-program (as it is not a b-thread).

bp.registerBThread("Baker", function() {
  bp.setInterruptHandler( function(evt) {
    bp.log.warn("Error making cake: " + evt);
    bp.enqueueExternalEvent(bp.Event("No cake for you!"));
    bp.enqueueExternalEvent(bp.Event("Come back - 1 month!"));
  });
  bp.sync({waitFor:CAKE_REQUEST});
  bp.sync({request:bp.Event("Buy Ingredients")});
  bp.sync({request:bp.Event("Mix Ingredients")});
  bp.sync({request:bp.Event("Bake Start")});
  bp.sync({waitFor:bp.Event("Cake Ready"),
       interrupt:bp.Event("Cake Burnt")});
  bp.sync({request:bp.Event("Decorate")});
  bp.sync({request:CAKE_READY});
});

Lines 2-6 of the baker b-thread set a handler for handling the unfortunate event of the burnt cake. The handler first logs why the b-thread was interrupted (line 3), and then enqueues two events to declare that no cake will be served (lines 4-5).

$ java -jar BPjs.jar interrupt-handler.js
#  [READ] /.../interrupts-handler.js
-:BPjs Added Customer
-:BPjs Added Oven
-:BPjs Added Baker
#  [ OK ] docs/source/BPjsTutorial/code/interrupts-handler.js
---:BPjs Started
--:BPjs Event [BEvent name:Cake Please]
--:BPjs Event [BEvent name:Buy Ingredients]
--:BPjs Event [BEvent name:Mix Ingredients]
--:BPjs Event [BEvent name:Bake Start]
--:BPjs Event [BEvent name:Cake Burnt]
-:BPjs Removed Baker
[JS][Warn] Error making cake: [BEvent name:Cake Burnt]
--:BPjs Event [BEvent name:No cake for you!]
--:BPjs Event [BEvent name:Come back - 1 month!]
---:BPjs No Event Selected
---:BPjs Ended

Note

External events are polled only when there are live b-threads in the b-program. If all b-threads terminate while the external event queue contains events, these events will never be selected.

Tip

Enqueueing external events can also be done from regular b-threads. This can serve as a sort of asynchronous event request. Note that events requested this way may never be selected, even if they were not blocked (see previous note).

Adding B-Threads Dynamically

Let’s count to 4 in an arbitrary order! That is, let’s have 4 events, labeled e0 to e3, and not care about the order in which they occur. For this, we need four b-threads, each requesting a numbered event. But since they all do the same, we might want to create them from a loop, like so:

var COUNT=4;
for ( var i=0; i<COUNT; i++ ) {
    bp.registerBThread("requestor-"+i, function(){
       bp.sync({request:bp.Event("e"+i)});
    });
};

If we run this, however, we do not get what we want:

 1 $ java -jar BPjs.jar dynamic-bthread-bad.js
 2 #  [READ] /.../dynamic-bthread-bad.js
 3 -:BPjs Added requestor-0
 4 -:BPjs Added requestor-1
 5 -:BPjs Added requestor-2
 6 -:BPjs Added requestor-3
 7 #  [ OK ] dynamic-bthread-bad.js
 8 ---:BPjs Started
 9 --:BPjs Event [BEvent name:e4]
10 ---:BPjs No Event Selected
11 ---:BPjs Ended

This may seem weird: in lines 3 to 6, the value of i goes from 0 to 3, as expected. But there’s only one event selected, and it’s e4.

The reason for this is that Javascript is a late-binding language, so i’s value is looked up as late as possible. For the logging, i has to be evaluated immediately, while the runtime builds a string to pass to the logger. The call to bp.Event("e"+i), on the other hand, is evaluated only when the b-thread is started.

Alas, the b-thread is started after the javascript file is evaluated. At this point, i is equal to 4. So in effect, we had four b-threads, named requestor-0 to requestor-3, all asking for event e4.

To get four different events, we need to create a scope for each iteration. This is easy, since Javascript supports functions as first-class-citizens (source).

var COUNT=4;
for ( var i=0; i<COUNT; i++ ) {
    (function(j){
        bp.registerBThread("requestor-" + j, function(){
           bp.sync({request:bp.Event("e"+j)});
        });
    })(i);
};

Lines 4-6 are the same as before, but now they are wrapped in an anonymous function (line 3) that’s immediately called, with i as the parameter (line 7). This results in the b-thread function having its own scope (or, to be technically exact, activation object). That scope keeps the value of i at the iteration the scope was created in - that value is put in the parameter j.

Thus, each b-thread gets its own scope and correct value of i (except that it’s calling it j at this point).

$ java -jar BPjs.jar dynamic-bthread-ok.js
#  [READ] /.../dynamic-bthread-ok.js
-:BPjs Added requestor-0
-:BPjs Added requestor-1
-:BPjs Added requestor-2
-:BPjs Added requestor-3
#  [ OK ] dynamic-bthread-ok.js
---:BPjs Started
--:BPjs Event [BEvent name:e2]
--:BPjs Event [BEvent name:e1]
--:BPjs Event [BEvent name:e3]
--:BPjs Event [BEvent name:e0]
---:BPjs No Event Selected
---:BPjs Ended

The bp Object

In the code snippets we’ve seen so far, one object kept coming up: bp. This object gives access to the behavioral programming infrastructure that runs the program. It allows registering b-threads, creating events and event sets, and interacting with the external world (e.g. logging).

Another role bp holds is abstraction layer for values that change, such as random numbers generation and time. This abstraction is needed to allow program verification – when BP code that uses such values is verified, the verifier needs to iterate over the possible return values. To enable this, the verifier will be able to decide on the values methods such as bp.random.nextInt(7) will return. For regular program execution, however, calling these methods is just like calling the regular Javascript objects, such as Math.random().

bp is implemented on the Java side by an object called il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.jsproxy.BProgramJsProxy - look at its JavaDoc for full reference. Below are the noteworthy methods.

Methods of Note

bp.Event(name, [data])

Creates an event with name and possible data object.

• name: Name of event. String.
• data: Optional object. Additional data for the object.

bp.EventSet(name, predicate)

Creates an event set: basically a named predicate that accepts events and returns true for set members.

• name: Name of the event set. String.
• predicate: The set membership predicate. Function that takes one parameter (event) and returns boolean.

bp.enqueueExternalEvent(event)

Enqueues an event to the program’s external event queue. See Final Acts of an Interrupted B-Thread.

• event: The event to be enqueued. Event.

bp.registerBThread([name], bthreadFunction)

Registers a new b-thread into the running b-program. The caller may specify a name (useful for making sense of the logs, for example). If no name is specified, an automatic name is generated.

• name: Optional. Name of the b-thread. String.
• bthreadFunction: A no-parameter function that is the body of the b-thread.

Tip

Two (or more) b-threads can have the same name. A unique, meaningful name for each b-thread makes debugging/analysis easier, but it does not effect b-program’s semantics. (Having said that, a b-program of 219 b-threads all named “my b-thread” might not be, um, ideal).

bp.fork()

Splits the calling b-thread to two identical b-threads. On the “parent” b-thread, fork returns 0. On the child b-thread, it returns 1. Similar to fork in, e.g., C.

bp.log

Provides access to the logger. See Logging.

bp.eventSets

Provides access to useful event sets methods and constant:

• bp.eventSets.all: All events (an event set that contains all events).
• bp.eventSets.none: An event set that does not contain any event.
• bp.eventSets.anyOf(e1, e2, e3): An event set that contains e1, e2, and e3. Similar to e1.or(e2).or(e3).
• bp.eventSets.allOf(s1, s2, s3): An event set that is the conjunction of s1, s2, and s3 (so, contains only events that are in s1 and s2 AND s3). Similar to e1.and(e2).and(e3).
• bp.eventSets.not(es42): An event set containing all events that are not in es42.

Note

Recall that events are event sets themselves (technically, an event is an event set that contains a single event - itself). So whenever a method expects an event _set_, you can pass a regular event to it.

bp.random

provides an access to a random number generator, supporting the following methods:

• bp.random.nextFloat(): Generate a random number between 0 and 1.
• bp.random.nextInt(bound): Generate a random number between 0 (inclusive) and bound (non-inclusive).
• bp.random.nextBoolean(): Toss a coin, report the caller.

bp.getTime()

Returns the current time in milliseconds since January 1st, 1970. To get the current date, call new Date(bp.getTime());

B-Program Life Cycle in BPjs

The life cycle of a b-program in BPjs is divided into two stages: program start and BP cycle. These are detailed below the diagram that describes them.

B-Program’s life cycle in BPjs. First, the Javascript program is executed and registers b-thread. When the Javascript program terminates, the BP cycle begins.

1. BPjs Program Start

This stage is responsible for registering the b-threads that the b-program will start with (note that b-threads can be added by other b-threads during program execution). Technically, this stage consists of executing a Javascript program. This program registers b-threads by calling bp.registerBThread([name],b-thread-function) multiple times. The Javascript code is free to call any external resources it needs; for example, it can read a file or query a database, and register b-threads according to the results. When the Javascript code terminates, all registered b-threads are executed concurrently, until they reach their first synchronization point. Then, the next stage begins.

2. Classic BP-Cycle

This stage is the classic behavioral programming cycle. In it, b-threads run in parallel. Each b-threads executes its own logic, until it decides to synchronize with its peers, by calling bp.sync({...}). When all b-threads requested synchronization, the b-program is said to arrive at a synchronization point. Then, the BPjs runtime selects an event that was requested and not blocked. B-threads that requested or waited-for that event are resumed. The rest of the b-threads remain paused. They may be resumed at the next synchronization point, if an event they requested or waited-for is selected.

Environments and Interruptions

A b-program may remain at a synchronization point indefinitely, if there are no selectable events. This is not a bug - in fact, it’s one of the main features of BP, and here’s why: A “stuck” b-program can still listen to external events, end resume active execution when an external event that is wait-for-ed by some b-threads occurs. This allows for b-programs to react to their environment in a natural way, and forms the foundation on which BP-based reactive systems are built upon.

When calling bp.sync(), b-threads can also define which events makes them irrelevant. For example, if a b-thread should handle a FileReceived event, and instead the b-program receives a NoMoreFiles event from its environment, it is a bit pointless to keep that b-thread around, and it should be gracefully terminated. This feature is called interrupting event, and is covered here.

Thus, we can slightly elaborate over the previous life cycle diagram:

B-Program’s life cycle in BPjs. First, the Javascript program is executed and registers b-thread. When the Javascript program terminates, all b-threads are executed concurrently until they reach their first synchronization point. Then, the BP cycle begins. During synchronization points, the BPjs runtime may accept events from the b-program’s environment. In practice, this environment is often a host Java application (or any other JVM language, really). B-threads can define which events make them irrelevant. When an event that makes a b-thread irrelevant is selected, that b-thread is interrupted, and is removed from the b-program.

Data Storage in BPjs

Aside from variables, BPjs allows storing data object for each b-thread, and in a b-program-level map. While this is not a part of “classic” bp, it allows for some useful techniques which the BPjs community found useful.

B-Thread Data Object

B-threads can store data in bp.thread.data. This field is only visible to the storing b-thread. It is useful for storing information that is globally relevant to a b-thread in a given state. For example, if we want our b-thread to block certain events, we can store these events at the b-thread level:

bp.thread.data = bp.EventSet("blocked", [eventA, eventB, eventC]);

Then, we can use our own synchronization function that also reads from the b-thread data field:

function sync(stmt) {
    stmt.block = bp.thread.data;
    bp.sync(stmt);
}

Danger

For verification to work, the data object stored in the b-thread has to implement state-based hashCode and equals.

B-threads can be started with a pre-defined data object. This is done by passing that object to bp.registerBThread, as shown in the below code:

bp.registerBThread("BTwDT", {some:"Data", num:17}, function(){
    bp.log.info("BT data: {0}", bp.thread.data);
    bp.sync({request:bp.Event(bp.thread.data.some)});
});

Which prints out the below:

---:BPjs Started
[BP][Info] BT data: {JS_Obj some:"Data", num:17.0}
--:BPjs Event [BEvent name:Data]
-:BPjs Done BTwDT
---:BPjs Ended

B-Program Data Store

BP focuses on behaviors and events, and does not look so much into shared data storage. In particular, b-threads are only supposed to share data using events. This works for the most part, but sometimes it is easier to be able to share data in other ways. The B-Program data store allows sharing data using a map, reachable from any thread using bp.store.

The storage model for the b-program store is transactional. Changes made by a given b-thread are visible only to that b-thread, until is requests synchronization. When entering a synchronization point, BPjs tries to consolidate all storage modifications. If the consolidation succeeds, the changes are applied and will be visible to the rest of the b-threads at the next cycle. If the consolidation fails, the b-program enters a failed state, similar to the one it enters after an assertion fails.

Note

Developers can react to b-program store modifications, as well as change them, and attempt to fix storage conflicts. This is done by implementing the StorageModificationStrategy interface, and registering it with a BProgram. See StorageModificationStrategy javadoc for details.

B-Program Data Store API

The b-program data store is a map, where the keys are strings, and the values can be any object. Available methods include:

put(k,v):Puts v (any object) in field k (which must be a string). get(k):returns the value in k, or null. has(k):returns true if the storage has a value under k, and false otherwise. remove(k):removes the value under k, if any. keys():returns a set of all keys. size():returns the number of keys.

Danger

For verification to work, the values in the b-program storage map should have state-based hashCode and equals. This is the default for JavaScript objects. When using Java objects - especially custom ones - ensure these methods are implemented.

Executing BPjs Programs

From the Commandline

You’ll need:

1. Java
2. BPjs’s über-jar (the jar that contains BPjs and its dependencies). See Obtaining BPjs.
3. Your code files

Once you have all of the above, running your BPjs programs is easy:

java -jar <path-to-uber-jar> <your-code-1>.js <your-code-2>.js ... <your-code-n>.js

Replace <path-to-uber-jar> with the actual path to the uber jar file, <your-code-1>.js to the path to the actual code file, etc.

An alternative to using code files is having some program send the code to BPjs via stdin. This is useful, e.g., if you have a program that generates BPjs code from a model, or if you’ve copied some code to the clipboard. In order to have BPjs read code from its stdin, add a dash (-) to the list of source files.

The example below executes the code from f1.js and the clipboard. pbpaste is a utility program (on Macs) that pushes the clipboard content to stdout:

pbpaste | java -jar <path-to-uber-jar> f1.js -

Tip

Unsure about why an event was or was not selected? Add a -v (for “verbose”) switch to the above commandline. BPjs will print the synchronization statement for each BThread during program synchronization points.

From Java Code

BPjs programs can be embedded in larger Java (or any JVM language) applications. To learn how to run and interact with a BPjs program from a host application, see Embedding BPjs in an Application.

Analysis and Verification

BPjs programs can be analyzed by traversing their possible runtime states. In other words, given enough time and resources, it is possible to visit each state a b-program might reach. Such traversal can be used to verify both that all states are OK (for some formal definition of “OK”) and that transitions between states conform to certain constraints. Like in any verification/formal analysis system, the “enough” part in “enough time and resources” might translate to a prohibitive amount. However, because BP looks at program states at a higher level than traditional formal analysis systems, formal analysis of non-trivial b-programs is useful and practical even on a regular laptop.

Note

Analysis is done directly on the b-program source code. No model transformation is involved in the process.

BPjs supports verification of both safety and liveness properties. As a safety example, BPjs can be used to verify that a b-program will never end up in a deadlock, or that a certain event could never be selected. As for liveness, BPjs can be used to verify that a certain event will happen eventually.

Analysis is not limited to verification — it is also possible to generate drawings of the runtime state-space, to collect statistics about the paths in its underlying graph, etc. BPjs’ modular structure allows performing such analyses by registering a listener, as explained below. We should start with some quick theory, though.

DFS over B-Program States

Program analysis is done by scanning all possible states a b-program can be in, and all the transitions between those states. These states and transitions form a graph, called “state space”. This is of course quite complex, as often the amount of states a program can be in is very large, or even unbounded. Some techniques for alleviating this problems exist; however, they are beyond the scope of this document.

In the state space graph of a b-program, synchronization points are the vertices and events are the edges. The outgoing edges from a given vertex are the events that are requested and not blocked at the synchronization point said vertex represents. See the image below for a simple example.

A state space of a sample b-program with 3 b-threads. Synchronization points are vertices, and events that are requested and not blocked serve as edges that connect between them.

In order to traverse the state space, we use a DfsBProgramVerifier, like so:

BProgram program = new SingleResourceBProgram("....");         // create a regular b-program
DfsBProgramVerifier vrf = new DfsBProgramVerifier();           // ... and a verifier
vrf.setProgressListener(new BriefPrintDfsVerifierListener());  // add a listener to print progress
VerificationResult res = vrf.verify(program);                  // this might take a while

res.isViolationFound();  // true iff a counter example was found
res.getViolation();      // an Optional<Violation>
res.getViolation().ifPresent( v -> v.getCounterExampleTrace() );
     // ExecutionTrace leading to the violation.

The verifier performs a DFS (depth-first search) on the state space. This is of course quite a naive algorithm that can be improved on (we certainly plan to). Still, DFS works pretty well, since it finds errors that are away from the program’s starting point. Errors that are close to that point are typically found by the programmer, using the good old technique known as “read the code and understand what it does”. In case the depth of a run is unbounded, the length of the scanned path can be limited.

Classes Involved in Analysis

The analysis process involves a few classes of note. When writing new types of analyses, consider sub-classing some of the below, as it may save you hard work.

DfsBProgramVerifier

Orchestrates the analysis/verification process: starts the b-program, manages state traversal, runs the DFS, etc.

DfsBProgramVerifier.ProgressListener

A listener to the analysis process. Notified when a violation is found, and can decided whether analysis should continue. Also notified about “usual” lifecycle events, such as verification starting and ending.

ExecutionTraceInspection

An inspection object, which takes an execution trace, and decides whether it violates some contract. During analysis, a DfsBProgramVerifier instance holds a set of these. Each time a new vertex or a new loop is found, the verifier sends them to these objects for inspection. BPjs ships with multiple such inspections, as static fields in the ExecutionTraceInspections utility class (note extra s at the end, like in other Java utility classes, such as java.nio.file.Paths).

Violation

When an ExecutionTraceInspection instance finds a trace that violates some requirement, it describes that discovery using an instance of this class.

VisitedStateStore

In order to detect cycles in a b-program’s execution graph, the verifier needs to know whether a given state was already visited. This is done using an instance of this class. BPjs ships with three implementations: One that looks at the entire state of the b-program, on that looks only at the hash code of that state, and one that assumes that all states are new.

Tip

The forgetful visited state store (ForgetfulVisitedStateStore) is useful for traversing all graph’s edges, since it does not stop a scan when it arrives at a node it already visited. The scan is still resilient to cycles - these are detected by looking at the DFS stack, not the visited state store.

Verifying Safety Properties

BPjs models are verified for most safety properties using assertions. During execution, b-threads may call bp.ASSERT(cond, message). If cond evaluates to false, the b-program is considered in violation of its requirements. This mechanism allows intuitive verification of requirements such as while flying, the doors can’t be opened:

bp.registerBThread(function(){
  while ( true ) {
    bp.sync({waitFor:FLYING});
    bp.sync({waitFor:DOOR_OPENED, interrupt:LANDED});
    bp.ASSERT(false, "Can't open the doors when flying");
  }
});

Assertions can be used with any boolean expression. They can be used at runtime too, where a false assertion causes a b-program to terminate.

An interesting corner case for safety properties is deadlock detection. When in deadlock, none of the b-threads can advance. In particular, when a b-program is deadlocked, none of its b-threads can invoke a false assertion. Thus, deadlocks are detected using a specific inspector, and not using a b-thread.

Tip

message is an optional parameter explaining, in human-readable terms, what went wrong.

Verifying Liveness Properties

Liveness properties require that “something good will happen eventually”. In order to specify this, BPjs borrows the concept of “hot” locations from its ancestor, Live Sequence Charts (LSC). A b-thread can declare a sync as “hot”, which means that it must eventually advance beyond it. For example, a requirement such as any request must receive a response, can be verified using the following b-thread:

bp.registerBThread(function(){
  while ( true ) {
    var req = bp.sync({waitFor:ANY_REQUEST});
    bp.hot(true).sync({waitFor:responseFor(req)});
  }
});

The first bp.sync is a non-hot (“cold”) sync, which means the writer of the b-thread is fine with that b-thread being stuck there forever (for example, if requests stop arriving). The second sync, on the other hand, is marked as hot (by calling bp.hot(true) before calling sync). This means that the writer of the b-thread does not allow the b-thread to be stuck there forever; eventually, the b-thread must move beyond this synchronization point. Here, this means a response to the received request must be sent. It is possible to specify abort conditions for this requirement, by providing values for waitFor and interrupt. This is similar to regular (“cold”) synchronization points.

Types of Liveness Violations

A liveness violation occurs when some set of b-thread remains hot forever. This can happen on two cases: a) there’s cycle in the b-program’s state space, where at least a single b-thread is hot at each point; or b) the program can terminate while at least one of its b-threads is hot. These violation types are described in more detail below, and in the accompanying figure.

Note

Not all hot cycles are bugs! Some systems must be able to advance infinitely. One example would be a traffic light controller, which must be able to infinitely cycle between its lights.

Hot Run (of a group of b-threads)

There exists a group of b-threads that can get into an infinite loop where at least one of its member b-threads is hot at each synchronization point. This means, semantically, that these b-threads are never “satisfied” and must always advance. In the below diagram, b-threads 1, 2, and 3 form a group which has a hot run (states A→B→C→A…). If we only consider b-threads 1 and 2, on the other hand, there is no hot run, since none of them is hot at state C.

Hot System Violation

A case where the b-program, as a whole, might find itself in a cycle whose synchronization points are all hot. This is a private case of a hot run, where the considered group contains all the b-program’s b-threads. In the below diagram, the described system has a hot system violation, because of the cycle A→B→C→A.

Hot B-Thread Violation

A case where a single b-thread can get into a cycle were it is always hot. This is a private case of Hot Run, where the group that has the hot run contains a single thread. Normally, this situation indicates that some business requirement was violated, or that there might have been a programming error. In the below diagram, b-thread 5 has a hot b-thread violation, because of the cycle A→B→C→A.

Hot Termination

A case where a b-program terminates when one or more of its b-threads is hot. This is technically a safety violation, since the run is finite. However, these cases can be augmented to a Hot B-Thread violation, by adding a trivial self transition, from the terminal state to itself. In the below diagram, a run that ends at state X would be a hot termination violation. The dotted transition to and from state X is the augmentation to a hot b-thread violation.

A sample state graph of a b-program. This graph contains 5 states (A, B, C, X, Z). In each, there are five b-threads (1-5). At each state, hot b-threads are marked with a red background. This state graph contains various liveness violations, as described above.

Note

It is possible to select which inspections are preformed during verification. A DfsBProgramVerifier holds a set of inspectors, which can be added to by calling its addInspector methods. If no inspectors are added, a default set will be used.

From the Command Line

To verify a b-program from the commandline, simply add the --verify switch. Use --full-state-storage to force the verification to use the full state data when determining whether a state was visited (requires more memory). To concentrate on liveness violations, add the --liveness switch. To limit the (possibly infinite) depth of the scan, use --max-trace-length:

$ java -jar bpjs.jar --verify hello-possibly-broken-world.js
$ java -jar bpjs.jar --verify --full-state-storage hello-possibly-broken-world.js
$ java -jar bpjs.jar --verify --liveness --full-state-storage hello-possibly-broken-world.js

Assertions During Runtime

During normal execution (i.e. by a BProgramRunner), failed assertion cause program execution to terminate. The execution BProgramRunner’s listeners are notified of this failure. This approach is sometimes called “runtime verification”, and is useful to implement “emergency shutdown” mechanisms.

Note

• A more in-depth discussion of verification in BPjs, including some techniques, can be found in the BPjs paper at arXiv.
• Sample verification code can be found in the test code, in package il.ac.bgu.cs.bp.bpjs.verification.examples.

Embedding BPjs in an Application

Overview

The BPjs library can be embedded in larger Java programs. The setting is useful in cases where you want the control logic to be implemented using behavioral programming, and thus need to translate incoming signals to BP events, and selected BP events to instructions to, e.g. actuators, databases, or web-services.

The layers of an application running a BPjs BProgram are described in the figure below. The BP code (top layer) is the BPjs code, written in Javascript. It can interact with the BPjs runtime using the The bp Object. The host application can make other Java objects available to the Javascript code, as will be explained later.

The BPjs layer serves as a runtime environment for the BProgram. The host application has to instantiate a BProgram object, and pass it to a BProgramRunner. The host application can listen to events of the running b-program (such as start, end, b-thread added, and - of course - b-event selected). Additionally, the host application can provide custom event selection strategy, in case the default one it not good enough.

The layers of a running BPjs program. The BP program, written in Javascript, it the top layer. It interacts with the BPjs runtime using bp, a Javascript object added to its context. The hosting Java application controls the BPjs runtime via its API. It can push event to the BProgram’s external event queue, and register listeners that are invoked when events are selected.

Class diagram describing the structure of an embedded b-program. The client code generates a BProgram and a BProgramRunner. The runner object consults the b-program’s event selection strategy when selecting events for the b-program it runs. A list of listener objects are informed whenever an event of interest, such as b-thread addition or b-event selection, occurs. Some methods and properties have been omitted for brevity.

Note

Why is ``BProgram`` separated from ``BProgramRunner``?

Because a b-program is also a model that can be verified rather than ran. The same BProgram object can be passed to a verifier object for verification.

Steps for B-Program Embedding

Code setup

Add BPjs to your classpath.

See Obtaining BPjs.

Decide which BProgram subclass you need.

BProgram is an abstract class. Its concrete sub-classes differ on how they obtain their source code. ResourceBProgram reads the code from a resource included with the code (typically, a .js file bundled in the project’s .jars). StringBProgram, on the other hand, takes a Java String as source. Of course, BProgram can be directly extended as needed.

Write the BPjs code.

The code will interact with the runtime using the bp object. Additional Java classes can be made available to it by using Rhino’s import directives, or by adding Java objects to the program’s scope (see below).

At Runtime

• Instantiate the proper BProgram sub-class, and supply it with the source BPjs code.
• If needed, set a new EventSelectionStrategy. When no strategy is supplied, SimpleEventSelectionStrategy will by used. This strategy randomly selects an event from the set of events that are requested and not blocked.
• If needed, add Java objects to the global b-program scope using putInGlobalScope.
• If the host Java program will push external events to the b-program, make the b-program wait for these events by calling bprog.setWaitForExternalEvents(true).
• Instantiate a BProgramRunner object, and supply it with the BProgram instance.
• Add listeners to the runner.
• In the common case when the program needs to wait for external events (such as GUI interactions), set the isWaitForExternalEvents property of the BProgram to true.
• Call BProgramRunner::start().

The BProgram will start running. Life-cycle and behavioral events will be passed to the listener objects. In case the host application would like to push an external event to the embedded b-program (e.g. because of a network request, or a user click), it should use the BProgram’s enqueueExternalEvent method.

Tip

BPjs’ source code contains many examples of embedded BPjs programs - most of the unit tests that involve a b-program. For a more complete example, refer to the RunFile class, which implements the command-line tool for running BPjs code.

Tip

SampleBPjsProject can serve as a template project for embedding BPjs in a Java application. You can fork it on GitHub and start building your application from there.

External Events vs. Internal Events

There is no difference between external and internal events – both are instances of the Java BEvent class, or a subclass of it. However, there may be a difference in how these events are treated by the event selection strategy. External events are made available to the strategy using an “external event queue”. An event selection strategy may choose to ignore this queue whenever it can choose an event requested by a b-thread. But a strategy can also decide to choose an event from the queue even when there are internal events that are requested and not blocked.

All event selection strategies currently included with BPjs ignore external events when there are internal ones available for selection. This choice makes the system easier to reason about, as it gets to complete its reaction to one external event before it starts reacting to a new one. But this does not have to be the case.

Redirecting BPjs’ Log

By default, BPjs’ log (used by b-programs through, e.g., bp.log.info("hi!") ) is written to standard out. It is possible to redirect this log into other streams, by calling:

BProgram#setLoggerOutputStreamer(PrintStream newOut)

Changing BPjs’ Executor Services

BPjs uses Java’s executor services for b-program execution and verification. Normally, BPjs uses a fixed thread pool, with one thread per CPU. Client code can change this, by passing a customized ExecutionServiceMaker instance to BPjs#setExecutorServiceMaker.

This type of customization is useful when, for example, an application wants to use BPjs in a single-threaded manner, or when an application needs to preserve CPUs for other tasks.

Packages and Classes

BPjs is divided into three main parts, following from its leading principle that b-programs are really models, which can be executed just as well as analysed. Thus, the package structure (shown below) is divided into:

model

Contains core BP concepts, such as BProgram and BEvent.

analysis

Contains classes required for analyzing a b-program.

execution

Contains classes for executing b-programs.

Main classes and packages of BPjs.

BPjs contains other packages as well, but they are technical in nature:

bprogramio

Deals with storing and loading b-program state.

mains

Command-line applications and utilities. Some of the classes in this package may grow up to become full-fledged applications, and leave to their own repository.

exceptions

Holds exceptions related to BPjs.

Extending BPjs

Out of its proverbial box, BPjs enables “classic” behavioral programming: running multiple b-threads who coordinate through events. It’s a start, and quite often it’s enough. But sometimes one needs BPjs to behave a bit differently. This section of the manual discusses how to alter BPjs’ default behavior to suite your specific needs.

Tip

If you develop an interesting or a useful extension, please consider making it available to others, e.g. by opening the source. Thanks!

Alter Event Selection Algorithm

In standard behavioral programming, the b-thread coordinator, or b-program, is allowed to choose any event that is requested and not blocked. Even on modestly sized b-programs, this leaves the event selection algorithm with plenty of wiggle room to make its choice. By default, BPjs will randomly select a requested-and-not-blocked event. Algorithms that make more informed choices are, of course, possible. BPjs makes it easy to develop them, and make them reusable.

Meet EventSelectionStrategy

Each b-program has an event selection strategy, implementing the EventSelectionStrategy interface. Given a b-program state at a synchronization point, an EventSelectionStrategy object can generate a set of selectable events, and then select a single event out of them. Accordingly, the EventSelectionStrategy interface defines only two methods: selectableEvents(...) and select(...).

The event selection strategy is used during both program execution and verification. During verification, the strategy is used to generate the possible selectable events; during execution, the strategy both generates the selectable eventset and selects a single event.

Both of EventSelectionStrategy’s methods accept the program’s state at the synchronization point. This state is composed of all the b-sync statements of participating b-threads, and the external event queue. selectableEvents returns a plain-old Java Set, that can also possibly be empty. During execution, select receives the program’s state as well as the selectable event set obtained from the call to selectableEvents. It does not return an Event, though – it returns a richer Optional<EventSelectionResult> object.

The EventSelectionResult object holds a selected event, and a set of indices to events in the external event queue. When receiving an EventSelectionResult, the b-program will remove the external events at those indices. This allows an event selection strategy a considerable degree of freedom for dealing with external event sets. For example, it can make the event list act like a set, by passing all the indices of events that are equal to the selected event.

Hinted bp.syncs

Some event selection strategies may depend on internal b-thread state. For example, a b-thread may define a HOT/COLD modality, as defined by Live Sequence Charts. A b-thread in a “HOT” state must advance, whereas a b-thread in a “COLD” state can forever stay in its current position without violating the system’s specification.

To this end, the bp.sync statement in BPjs has an optional second parameter. BPjs makes no assumptions about the type of this parameter - it just stores it in the b-thread’s synchronization statement, where is it made available to the event selection strategy through the getData() method.

Sample Strategy: Priority-Based Selection

Let’s look at a sample event selection strategy, based on priority. Under this strategy, the b-threads may add to their bp.sync statements a “priority” integer. The strategy finds a b-thread with the lowest priority, and selects an event that it requested, and was not blocked. Here’s the code, followed by a short discussion.

class PriorityEss implements EventSelectionStrategy {

    @Override
    public Set<BEvent> selectableEvents(Set<BSyncStatement> statements, List<BEvent> externalEvents) {

         EventSet blocked = ComposableEventSet.anyOf(statements.stream()
                .filter( stmt -> stmt!=null )
                .map(BSyncStatement::getBlock )
                .filter(r -> r != EventSets.none )
                .collect( Collectors.toSet() ) );

        Iterator<BSyncStatement> stmts = statements.iterator();
        if ( stmts.hasNext() ) {
            BSyncStatement firstStmt = stmts.next();
            Set<BEvent> selectable = getNotBlocked(firstStmt, blocked);
            int minValue = getValue( firstStmt );

            while ( stmts.hasNext() ) {
                BSyncStatement curStmt = stmts.next();
                int curValue = getValue(curStmt);
                if ( curValue < minValue ) {
                    minValue = curValue;
                    selectable = getNotBlocked(curStmt, blocked);
                }
            }
            return new HashSet<>(selectable);
        } else {
            return Collections.emptySet();
        }
    }

    @Override
    public Optional<EventSelectionResult> select(Set<BSyncStatement> statements, List<BEvent> externalEvents, Set<BEvent> selectableEvents) {
        if ( selectableEvents.isEmpty() ) {
            return Optional.empty();
        } else {
            return Optional.of( new EventSelectionResult(selectableEvents.iterator().next()));
        }
    }

    private int getValue( BSyncStatement stmt ) {
        return stmt.hasData() ? ((Number)stmt.getData()).intValue() : Integer.MAX_VALUE;
    }

    private Set<BEvent> getNotBlocked(BSyncStatement stmt, EventSet blocked) {
        try {
            Context.enter();
            return stmt.getRequest().stream()
                    .filter( req -> !blocked.contains(req) )
                    .collect( toSet() );
        } finally {
            Context.exit();
        }
    }
}

The selectableEvents method begins by creating a set of all blocked events (lines 6-10). It then iterates over the BSyncStatements, maintaining the minimal value it found so far. If a lower value is found, it creates a set of the events it requested and were not blocked (lines 15 and 23). Lastly, it returns the last such set found (line 26).

Since all of the work was done in the selectableEvents method, the select method has very little left to do: it selects the first event from the selectable event set passed to it. If that set is empty, it returns the empty Optional.

There are two other interesting methods in this code. getValue (lines 41-43) extracts the priority integer from the statement. Note that the strategy also deals with a case where no such integer was provided.

getNotBlocked (lines 45-54) takes a BSyncStatement and a blocked EventSet, and returns the non-blocked subset of events requested by the statement. Note that EventSet is not Set<Event> – EventSet is a predicate, an interface consisting of a single method: contains. Quite often it will include one or more Javascript functions that have to be evaluated. For this reason, getNotBlocked has to enter and exit a Javascript execution context (lines 47 and 52, respectively).

The b-program using this event selection strategy is shown below. Note that b-threads “bt-1” and “bt-2” provide a priority integer, while “bt-3” does not.

bp.registerBThread("bt-1", function () {
    bp.sync({ request: bp.Event("1") }, 1);
});

bp.registerBThread("bt-2", function () {
    bp.sync({ request: bp.Event("2") }, 2);
});

// Has no extra data on the bp.sync call.
bp.registerBThread("bt-3", function () {
    bp.sync( {request: bp.Event("3")} );
});

Warning

The above strategy is intended for explanatory purposes, and is probably too simplistic for real-world use. It ignores external events, assumes priorities are unique, and if all the events requested by the b-thread with the lowest priority are blocked, it claims there are no selectable events.

Tip

The above strategy and b-program are part of BPjs’ unit tests.

Interacting with the B-Program’s Context

Todo

Write about how to interact with the context.

Sub-classing Events

The built-in BEvent class can hold data in its name, and in a data field. However, sometimes the need arises for a more structured data storage, or one that’s easier to create and read from the Java layer. To this end, it is possible to sub-class BEvent.

Warning

Event sub-classes MUST implement state-based equals() and hashCode(), and implement java.io.Serializable. Otherwise, event unification and program verification would not work.

Terms Used in this documentation

Scenario-Based Programming

Todo

explain

Behavioral Programming

Todo

explain

b-program

Todo

explain

b-thread

Todo

explain

Trace

The sequence of events selected by a b-program during its execution. To executions are considered equivalent if (and only if) they have equal traces.

Examples

Here are some examples you can learn from:

Example - Hot/Cold Bath

This program models a system that fills a bath with six parts water: three cold, and three hot. There are two faucets in the system: one for hot water and one for cold. The system defines an event for activating each of these faucets: HOT causes the hot faucet to release a single part of water, and COLD has a similar effect on the cold water faucet. Listing 1 shows a naive controller program: it registers a single b-thread that requests the events at an arbitrary order. For the purpose of this program, we assume HOT and COLD are defined outside of the b-program itself, as they have to be known to the faucet physical controllers; BPjs offers an easy way of achieving this, and so the listed code is realistic.

bp.registerBThread(function(){
	bp.sync({request:COLD});
	bp.sync({request:COLD});
	bp.sync({request:COLD});
	bp.sync({request:HOT});
	bp.sync({request:HOT});
	bp.sync({request:HOT});
});

Listing 1. A naive implementation of bath-filling controller.

The code in Listing 1 is not incorrect, but it also does not use the power of behavioral programming: it leaves no decision room for the event selection mechanism. Thus, when read as a specification, it is over-restrictive. An improved b-program is shown at Listing 2.

bp.registerBThread("add-hot", function(){
	bp.sync({request:HOT});
	bp.sync({request:HOT});
	bp.sync({request:HOT});
});

bp.registerBThread("add-cold", function(){
	bp.sync({request:COLD});
	bp.sync({request:COLD});
	bp.sync({request:COLD});
});

Listing 2. A more lenient version of the bath-filling controller.

The code in Listing 2 consists of two b-threads: add-hot, which adds the hot water, and add-cold, hich adds the cold water. This improves on the previous version in a number of ways. First, any order in which the water parts are added is supported, as the event selection mechanism of the b-program can choose between two events at most synchronization points. Second, the program’s structure is now closer to the original program requirements, as it does not dictate the order in which the water are added to the bath. Lastly, naming the bthreads increases readability of code, model-checking results, and program logs. It also makes it easier to debug a program.

The code in Listing 2 may be a bit too lenient, though: it allows a scenarios where the bath becomes too hot or too cold while being filled (for example, when all add_hot runs to completion first, and adds the three part hot water before add_cold adds a single cold water part). This may be a problem if we want to, e.g., put a baby in the bath before it is full.

To prevent these unbalanced scenarios, we can add an additional b-thread, that will make sure the water temperature is balanced during the filling process. One such possible bthread is listed in Listing 3.

The control-temp b-thread ensures the temperature of the bath water is safe by blocking the addition of each part of hot water until a part of cold water is added. It is interesting to note that this b-thread can be added and removed without affecting the other b-threads. Thus, if there is a baby in the bath, we may (should?) choose to add this b-thread to the controller. Better yet, we can solve this within the b-program: add a bp.sync({waitFor:BABY_IN}) statement at the beginning of control-temp, so it starts working only when a baby is in the bath.

bp.registerBThread("control-temp", function() {
	while ( true ) {
		bp.sync({waitFor:COLD, block:HOT});
		bp.sync({waitFor:HOT, block:COLD});
	}
});

Listing 3. A b-thread that ensures safe water temperature by ensuring cold water are added before hot water are.

As a useful exercise, we invite the reader to further elaborate the hot-cold example, e.g. by supporting the insertion of the baby while filling the bath (which would require blocking of the BABY_IN event when the water temperature is too high), or by altering control-temp to be more permissive.

Example - Dining Philosophers

The Dining Philosophers is a classic concurrent programming challenge, first proposed as an exercise in an exam by Edsger Dijkstra in 1965. Imagine a group of philosophers, sitting at a round table. Each has a plate with food. For utensils, they have chopsticks - a single chopstick between each two plates (this setting correctly models the event budget of many Philosophy departments). In order to eat, each philosopher has to obtain both chopsticks adjacent to her. The concurrency challenge is, of course, mutual exclusivity: A chopstick may only be held by a single philosopher at any given moment, and so they have to either coordinate, or experience hunger-induced existential crisis. This problem is illustrated in Figure 1.

The philosophers in our dining philosophers b-program use a naive algorithm, listed in Listing 1: a philosopher picks up the chopstick to their right, then the one to their left, eats, puts the left chopstick down, puts the right chopstick down, and then starts over again. While intuitive, this algorithm reaches a deadlock in a certain scenario we will automatically discover later.

The code in Listing 1 consists of a regular JavaScript function. This function adds the new b-thread to the b-program, based on the parameters it was invoked with. Functions like these can be viewed as parametrized b-thread templates. In this example, b-thread templates are used to reduce code duplication.

We now turn our attention to the chopsticks. In the modeled setting, each chopstick is shared by the two philosophers adjacent to it. Each of these philosophers can pick up and release said chopstick.

Dijkstra’s Dining Philosophers problem. Each two philosophers share the chopstick between them. In order to eat, a philosopher has to pick up both sticks. After eating, a philosopher releases the sticks and thinks. Since only a single philosopher can use a stick at any given moment, this setting poses many mutual exclusion challenges.

function addPhil(philNum) {
	bp.registerBThread("Phil"+philNum, function() {
		while (true) {
			// Request to pick the right stick
			bp.sync({request: bp.Event("Pick"+philNum+"R")});
			// Request to pick the left stick
			bp.sync({request: bp.Event("Pick"+philNum+"L")});
			// Request to release the left stick
			bp.sync({request: bp.Event("Rel"+philNum+"L")});
			// Request to release the right stick
			bp.sync({request: bp.Event("Rel"+philNum+"R")});
		}
	});
};

A function for adding a philosopher to the dining philosophers b-program. A dining philosopher repeatedly attempts to pick the chopstick to her right, then the one to her left, and then releases them in the same order. For the purpose of this program, there’s no need to add an EAT or THINK event.

Some restriction apply, though: a philosopher can only pick up a chopstick when it lays on the table, and can only release a chopstick after picking it up. Additionally, a chopstick can be picked up by at most a single philosopher at a time. Consequentially, if one philosopher have picked a chopstick up, the other philosopher has to wait for the first philosopher to release the chopstick, prior to picking it up herself. Imposing these constraints is done by the chopstick b-thread. The code for adding a these b-threads is shown in Listing 2.

The implementation of chopstick b-threads demonstrates some interesting features of BP and BPjs. First, note the usage of event sets in lines 5 and 9. These are used to detect the pick up and release event of the stick being modeled.

function addStick(i) {
	var j = (i%PHILOSOPHER_COUNT)+1;

	bp.registerBThread("Stick"+i, function () {
		var pickMe = bp.EventSet("pick"+i, function(e) {
			return (e.name === "Pick"+i+"R"
				|| e.name === "Pick"+j+"L");
		});
		var releaseMe = [bp.Event("Rel"+i+"R"),
					bp.Event("Rel"+j+"L")];

		while (true) {
			var e = bp.sync({waitFor: pickMe,
					block: releaseMe});

			var wt = (e.name === "Pick"+i+"R") ?
					"Rel"+i+"R" : "Rel"+j+"L";
			bp.sync({waitFor: bp.Event(wt),
				block: releaseMe});
		}
	});
}

A function for adding a chopstick to the dining philosophers bprogram. This b-thread ensures that the chopstick it models can be picked up by at most a single philosopher at a time. Note the usage of event sets for detecting Pick and Release events — this is needed, since philosophers adjacent to a stick refer to it using different names. For example, the stick between philosophers 3 and 4 would be referred to as 3R by philosopher 3, and 4L by philosopher 4.

The philosophers adjacent to a stick refer to it using different names. Thus, picking up stick #2 can be done using events Pick2R or Pick3L. These events are contained in the pickMe event set defined in line 5. Set membership is determined by examining the event name, which is a regular JavaScript string object. Event sets created in BPjs are similar to mathematical sets: a predicate over events (although BPjs allows naming them too). Unlike set implementations in common collection frameworks, it is impossible to iterate over their members. Consequentially, it is meaningless to request such an event set during a bsync. doing so will cause BPjs’ runtime engine to throw an error.

The releaseMe event set, on the other hand, is an array of event objects. When such arrays are passed to bsync , they are treated as an event set. This type of event set can be requested during a bp.sync, using the same syntax for requesting a single event. The exact semantics of requesting an event array are decided by the event selection strategy. It can ignore the order of elements, giving the array mathematical set semantics. Alternatively, it can consider the order of elements and select the first element that is not blocked by other bthreads, giving the array preference queue semantics. Event selection strategies are covered in detail in Subsection VIII-A. Having described the philosophers and chopsticks, it is now time to bring them all to the table. This is done using a regular JavaScript loop, shown in Listing 3.

Discussion: The dining philosophers b-program described here can serve both as a simulation program and as a model to be checked. For simulation purposes, this b-program is run (see Section V), and its event log can be analyzed, e.g. to get statistics about stick wait times. For verification, the b-program is passed to a verification engine, as shown in Section VI.

if (!PHILOSOPHER_COUNT) PHILOSOPHER_COUNT = 5;

for (var i=1; i<=PHILOSOPHER_COUNT; i++) {
	addStick(i);
	addPhil(i);
}

The loop instantiating a dining philosophers model. If PHILOSOPHER_COUNT was not passed by the containing Java application, it defaults to 5.

A maze, described using our maze-description DSL (left), and a maze solution, found by a generic b-program model checker (right). The model checker output, an event sequence, was post-processed by the program to visualize the solution on the maze’s map. In both cases, the exact same code is used — no translation is necessary when transitioning between code execution and verification.

This example uses parametrized templates to create its bthreads. B-thread templates are a versatile and commonly used design pattern, applicable in various contexts. When creating simulations, b-thread templates can be used to generate heterogeneous b-thread population, where the template parameters are sampled from a given distribution. In the next section, they are used to create an interpreter for a small DSL.

Example - Mazes

In this subsection, we demonstrate how to use BPjs to define executable semantics of a domain specific language (DSL). The result of parsing a program written in said DSL is a bprogram, which can be executed or verified against a formal specification. Below, we define a DSL for describing twodimensional mazes, the dynamic behaviors of each type of maze cell, and see how to use model-checking to solve a maze. Cell behaviors will by generated by one or more b-threads per cell.

Our maze-description DSL uses ASCII drawings. A maze is described using an array of strings, each of which describes a row of maze cells. The characters of each string describe the maze cells — one character per cell. There are three characters with special semantics; the rest are considered “walls” (see left side of Figure 1).

Fig. 1. A maze, described using our maze-description DSL (left), and a maze solution, found by a generic b-program model checker (right). The model checker output, an event sequence, was post-processed by the program to visualize the solution on the maze’s map. In both cases, the exact same code is used — no translation is necessary when transitioning between code execution and verification.

The special characters are:

• (space) A space cell: A cell the maze walker can enter.
• s A start cell: A space cell a maze walker starts in.
• t S target cell: A space cell the maze walker should arrive at.

To create a model from a maze written in this DSL, a parser iterates over the characters in each of the strings, maintaining the coordinates (row, column) for each character. Based on the character it encounters, it constructs zero or more b-threads, and adds them to the program. We refer to these b-threads as construct agent b-threads (or CABs), since they act on behalf of a linguistic construct when a model is analyzed or being run.

The CABs generated for each cell type are: Wall Cells: No CABs are generated for wall cells under the described implementation. Space Cells: Space cells attract the maze walker when it is in a cell adjacent to them. To do this, they repeatedly wait for an entry event to any of their neighboring cells, and then request an entry event into them. The b-thread template for generating b-threads implementing this behavior, is shown in Listing 1.

function addSpaceCell( col, row ) {
	bp.registerBThread("cell(c:"+col+" r:"+row+")",
		function() {
			while ( true ) {
				bp.sync({waitFor: adjacentCellEntries(col, row)});
				bp.sync({request: enterEvent(col, row), waitFor: anyEntrance});
			}
		}
	);
}

Listing 1. B-thread template for adding a space cell at row, col. Space cells wait for the maze walker to enter a cell adjacent to them, and then request that it enters them. If the event selection mechanism chose another cell for the maze walker to enter, the entry request is removed. This is achieved by waiting on the event set anyEntrance. The function adjacentCellEntries returns an event set containing cell entry events for the four cells that share an edge with the passed cell. The full code is available at the code appendix.

Target Cells: Target cells are regular space cells, with one additional trait: when the maze walker enters them, a special event celebrating the fact that the target have been found should be fired. To do this, the parser creates two CABs for a target cell: the space cell b-thread mentioned above, and a b-thread awaiting an entry to the cell, before announcing that the target was found. This additional CAB is shown in Listing 2. This CAB uses event blocking in order to ensure that, once requested, the TARGET_FOUND_EVENT will be selected before any other event is.

bp.registerBThread("target", function () {
	bp.sync({waitFor: enterEvent(col, row)});

	bp.sync({request: TARGET_FOUND_EVENT,
		block: bp.allExcept(TARGET_FOUND_EVENT)});
});

Listing 2. B-thread template for announcing a target located at (row, col) was found. In order to ensure that the announcement recognizes the correct cell, the bsync requesting the announcement event blocks all other events.

Start Cell: A start cell is, too, a space cell with one additional behavior: when the maze program starts, it already has a maze walker in it. Thus, the maze parser adds two CABs to the b-program when it encounters a start cell: the space cell b-thread, and a b-thread requesting an entry event to the starting cell (see Listing 3).

function addStartCell(col, row) {
	bp.registerBThread("startCell", function() {
		bp.sync({request: enterEvent(col,row)});
	});
}

Listing 3. B-thread template for a start cell located at (row, col).

Discussion: In this example, we use BPjs to define the executable semantics of a DSL for describing two dimensional mazes using ASCII drawings. Both the technique and the model raise a few interesting points. Language semantics definitions done using construct agent b-threads can be modular and easy to navigate, as well as executable and verifiable. Thus, such definitions make it is easy for language developers to define, discuss, and experiment with semantics of various constructs. In the above example, for a reader to understand the semantics of t, it is enough to see which b-threads are added to the program when the parser encounters the character ‘t’. Moreover, definitions of constructs with similar aspects can share code. In such cases, code re-use is not merely an engineering gain; semantically, it means that the re-used b-threads capture a linguistic concept common to the language constructs sharing the code. Thus, creating a language definition using CABs may help the discovery and crystallization of hidden language concepts.

The maze models illustrates one of the differences between Object-Oriented Programming and Behavioral Programming. Consider the target cell, which is a space cell with additional functionality. Under classic OOP, we would model this relationship using two classes and inheritance: define a SpaceCell class implementing the common functionality, and add a subclass TargetCell, extending it with additional functionality. Under BP, the same feat is achieved through composition: for a space cell we add a cell b-thread (Listing 1). For a target cell, we add a cell b-thread for the base functionality, and an additional target b-thread (Listing 2) for the additional functionality.

The notion of CABs was first introduced by Bar-Sinai, Weiss, and Marron in M. Bar-Sinai, G. Weiss, and A. Marron, “Defining semantic variations of diagrammatic languages using behavioral programming and queries” where it is described at greater detail.

Some aspects of the way mazes are modeled in the above example might be surprising. For example, there are no bthreads modeling the maze walker, or the walls. These concepts are not needed at runtime: the movement of the maze walker is recorded by the series of Enter(x,y) events. Wall cells do not request Enter events, and are thus never visited by the walker. Note that none of the b-thread in this model hold state, except for their program counter. All they do is describe a scenario. The model correctness relies on the bprogram selecting a proper event each cycle.

Another way of modeling a maze is to model the maze walker and the walls, instead of the space and start cells. Under such modeling, the maze walker can be statefull bthread, maintaining its current position. At each bp.sync, the maze walker requests an entry event to all its surrounding cells. Wall cells are modeled using a very small b-thread, blocking the Enter(x,y) event, where x and y are the coordinates of the said wall cell (see Listing 4). The rules of Behavioral Programming require that every sync cycle a single event that is requested and not blocked is chosen. Thus, every cycle, the b-program will select a single entry event to a cell that is not a wall (and therefore a space cell that the maze walker is semantically allowed to enter). This type of model additionally requires a mechanism for preventing the maze walker from wandering off the maze. One way of accomplishing that is adding logic to constrain the set of entry events the maze walker b-thread requests. This, however, will complicate the code by adding more conditional statements. A better, more BP-oriented approach, would be to add b-threads blocking all entry events for cells outside of the maze.

Notably, the target b-thread (Listing 2) can be used in the alternative model with no changes.

function addStartCell(col, row) {
	bp.registerBThread("startCell", function() {
		bp.sync({request: enterEvent(col,row)});
	});
}

Listing 4. A b-thread template for a wall, in an alternative maze model. This construct agent b-thread blocks entry to the cell it models for the entire duration of the program. Thus, entry requests to the modeled cell, made by the maze walker b-thread, will never be selected.

The second bp.sync statement used by the target b-thread (Listing 2) might look problematic: it blocks all events except for TARGET_FOUND_EVENT. It is indeed problematic, in the sense that the block all except X idiom does not scale. If, somewhere else in the code, another b-thread uses the same idiom with a different event, the b-program will deadlock. The model needs this type of blocking, though, to nsure that TARGET_FOUND_EVENT is selected immediately after the target cell was entered.

Under the default semantics of BPjs, which allow any event that is requested and not blocked to be selected, using the block all except idiom is a sensible way of achieving this immediate selection. Other alternatives might use blocking an event set that contains all other events we want to block in this situation — an event set that will have to be updated each time an event is added to the system. Fortunately, BPjs’ generalized nature allows for a better alternative.

BPjs supports pluggable event selection strategies, enabling programmers to refine the event selection mechanism used by a b-program. Here, one could define a strategy that prioritizes events: when it can choose between TARGET_FOUND_EVENT and an Enter event, it will always choose the former (provided that it is not blocked). Using such strategy, the target bthread will not have to use blocking at all, alleviating the risk of deadlocks. Event selection strategies are discussed in Subsection VIII-A.

Solving a maze: Parsing a maze description results in a bprogram modeling the maze. Running the b-program will make the maze walker perform a valid random walk through the maze. It will start at the start cell, will not pass through walls, and if it will stumble on the target cell, TARGET_FOUND_EVENT will be fired. However, a random walk is a very inefficient way of discovering the target cell.

In order to efficiently solve a maze, we can verify a bprogram modeling it. Our formal requirement will be that TARGET_FOUND_EVENT is never fired. Assuming the maze has a solution, BPjs’ model checker will find a run where the maze walker reaches the target, and output it as a counterexample. A minimal code for performing this is shown in Listing 5. Similar setup was used to generate the solution presented at the right side of Figure 3.

SingleResourceBProgram bprog = new SingleResourceBProgram("mazes.js");
bprog.putInGlobalScope("MAZE_NAME", mazeName);
bprog.putInGlobalScope("TARGET_FOUND_EVENT", targetFoundEvent);
DfsBProgramVerifier vfr = new DfsBProgramVerifier();
vfr.setRequirement(new EventNotPresent(targetFoundEvent));
vfr.setVisitedNodeStore(new FullVisitedNodeStore());
VerificationResult res = vfr.verify(bprog);

Listing 5. A code excerpt for verifying the mazes b-program using BPjs.

Verification of a maze b-program can take a long time and generate an arbitrarily long counter example. This is because of the random walk: while a counterexample will be found, the length of the path it uses to get to the target cell is unbounded. This is easily solvable in a way that further exemplifies the additive nature of BP: for model checking only, we can add another b-thread, preventing a the maze walker from entering the same cell twice (see Listing 6). This thread turns the random walk into a walk that enters a new cell at every step, until it gets terminally stuck. The verification process examines all such possible walks, and returns one that ends up at the target cell. BPjs has facilities to programmatically add code to a b-program to support such cases.

bp.registerBThread("onlyOnce", function(){
	var block = [];
	while (true) {
		var evt = bp.sync({waitFor: anyEntrance, block: block});
		block.push(evt);
	}
});

Listing 6. A b-thread preventing a the maze walker from entering a cell twice. This b-thread can be used during verification, in order to shorten the execution paths examined.

Example - Tic Tac Toe

This example is borrowed, with modifications, from D. Harel, A. Marron, and G. Weiss - “Programming coordinated scenarios in java”. Its main feature is that it presents the concept of aligning bthreads to requirements. Meaning, each b-thread represents a rule, or a part of the tactics in the game of Tic-Tac-Toe.

First, let us describe the (classical) game of Tic-Tac-Toe, and the events that represent the expected behaviors. Two players, X and O, alternately mark squares on a 3 X 3 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. Below, we assume player X is played by a human user, and player O is played by the application.

The goal of the programmer here is to implement the tactics for the O player such that the computer never loses. To check this main requirement, we use our model-checking tool that we will present soon. The game rules translate into b-threads as follows:

bp.registerBThread("EnforceTurns", function() {
	while (true) {
		bp.sync({waitFor:[X(0,0),X(0,1),...,X(2,2)],
			block:[O(0,0),O(0,1),...,O(2,2)]});

		bp.sync({waitFor:[O(0,0),O(0,1),...,O(2,2)],
			block:[X(0,0),X(0,1),...,X(2,2)]});
	}
});

Listing 1. A b-thread that implements the requirement that X and O play alternatively.

bp.registerBThread("SqrTkn("+row+","+col+")", function(){
		while (true) {
			bp.sync({waitFor:[X(row,col), O(row,col)]});
			bp.sync({block:[X(row,col), O(row,col)]});
	}
});

Listing 2. A b-thread that implements the requirement that a square may only be marked once. Given the variables row and col that represent the coordinates of a square on the grid, the b-thread waits for a move on that square and blocks further moves on the same square.

var move = bp.EventSet("Mvs", e=>e instanceof Move);

bp.registerBThread("DetectDraw", function() {
	for (var i=0; i<9; i++) {
		bp.sync({waitFor:[move]});
	}
	bp.sync({request:[draw]}, 90);
});

Listing 3. A b-thread that implements the draw ending condition. It waits for nine moves and then requests to announce a draw. The variable move is a representation of all events of type Move. The number 90 specifies the priority of the request.

bp.registerBThread("DetectXWin", function() {
	while (true) {
		bp.sync({waitFor:[X(l[p[0]].x, l[p[0]].y)]});
		bp.sync({waitFor:[X(l[p[1]].x, l[p[1]].y)]});
		bp.sync({waitFor:[X(l[p[2]].x, l[p[2]].y)]});
		bp.sync({request:[XWin]}, 100);
	}
});

Listing 4. A b-thread that implements the X winning condition. Given a permutation p and a line l (row, column, or diagonal), the b-thread waits for three X events on the line, in the order specified by the permutation, and then requests to announce that X wins the game.

bp.registerBThread("DetectOWin", function() {
	while (true) {
		bp.sync({waitFor:[O(l[p[0]].x, l[p[0]].y)]});
		bp.sync({waitFor:[O(l[p[1]].x, l[p[1]].y)]});
		bp.sync({waitFor:[O(l[p[2]].x, l[p[2]].y)]});
		bp.sync({request:[OWin]}, 100);
	}
});

Listing 5. A b-thread that implements the O winning condition. Given a permutation p and a line l (row, column, or diagonal), the b-thread waits for three O events on the line, in the order specified by the permutation, and then requests to announce that O wins the game.

bp.registerBThread("Clck("+r+","+c+")", function() {
	while (true) {
		bp.sync({waitFor:[Click(r,c)]});
		bp.sync({request:[X(r,c)]});
	}
});

Listing 6. A b-thread that implements the detection of user’s (player X) click.

bp.registerBThread("GameEnd",function() {
	bp.sync({waitFor: [OWin, XWin, draw]});
	bp.sync({block: [X(0,0), X(0,1),...,O(2,2)]});
});

Listing 7. A b-thread that implements the requirement that no moves are allowed once the game ends.

We now present the main part of the specification: a strategy for player O implemented by b-threads. While there are many implementations of strategies for this game, our approach here is to break the strategy to elements that correspond to the way parents teach their children how to win (or, at least, avoid losing) the game. Arguably, we claim that people do not usually use the minimax algorithm that most computers are programmed to apply. Instead, we argue that most people use some set of intuitive rules of thumb. An example of a set of such rules is modeled by the b-threads below.

bp.registerBThread("Center",function() {
	while (true)
		bp.sync({request:[O(1,1)]},35);
});

Listing 8. A b-thread that implements the thumb-rule that, if no other thumbrule applies, it is best to put an O in the center square.

bp.registerBThread("Corners",function() {
	while (true)
		bp.sync({request:[O(0,0),O(0,2),O(2,0),O(2,2)]},20);
});

Listing 9. A b-thread that implements the thumb-rule that, if no other thumbrule applies, and the center square is taken, it is best to put an O in a corner square.

bp.registerBThread("Sides",function() {
	while (true) {
		bp.sync({request:[O(0,1),O(1,0),O(1,2),O(2,1)]},10);
	}
});

Listing 10. A b-thread that implements the thumb-rule that, if no other thumbrule applies, and the center and all corner squares are taken, put an O in a side square.

Note that the requests of the last three b-threads are with priorities 35, 20, and 10, respectively. These are the lowest priorities among all the b-threads that implement the thumbrules. This means that the event selection mechanism will only obey these requests if no other thumb-rule applies. It also means that we prefer to use the center over corners and corners over sides. We proceed to describe the thumb-rules that relate to scenarios in the game:

bp.registerBThread("AddThirdO", function() {
	while (true) {
		bp.sync({waitFor:[ O(l[p[0]].x, l[p[0]].y)]});
		bp.sync({waitFor:[ O(l[p[1]].x, l[p[1]].y)]});
		bp.sync({request:[ O(l[p[2]].x, l[p[2]].y)]}, 50);
	}
});

Listing 11. A b-thread that implements the thumb-rule of putting an O in a line with two other O’s, in order to win the game. Given a permutation p and a line l (row, column, or diagonal), the b-thread waits for two O events on the line, in the order specified by the permutation, and then requests to mark its final O.

Note that the priority of the AddThirdO b-thread is higher than the priority of PreventThirdX. This is because we prefer to win a game if possible.

bp.registerBThread("PreventThirdX", function() {
	while (true) {
		bp.sync({waitFor:[ X(l[p[0]].x, l[p[0]].y)]});
		bp.sync({waitFor:[ X(l[p[1]].x, l[p[1]].y)]});
		bp.sync({request:[ O(l[p[2]].x, l[p[2]].y)]}, 40);
	}
});

Listing 12. A b-thread that implements the thumb-rule of putting an O in a line with two X’s, in order to prevent a win of player X in the next move. Given a permutation p and a line l (row, column, or diagonal), the b-thread waits for two X events on the line, in the order specified by the permutation, and then requests to mark an O on the third square.

The last type of thumb-rules in our strategy handle the so called “fork situations”, when player X tries to complete two lines at the same time. We only list one of them here, the PreventFork00X b-thread, that identifies one of the three ‘fork situations’. There are three more similar b-threads to handle the other similar situations.

bp.registerBThread("PreventFork00X", function() {
	while (true) {
		bp.sync({waitFor:[X(f[p[0]].x, f[p[0]].y)]});
		bp.sync({waitFor:[X(f[p[1]].x, f[p[1]].y)]});
		bp.sync({request:[O(0,0),O(0,2),O(2,0)]}, 30);
	}
});

Listing 13. A b-thread that implements the thumb-rule of preventing from player X to complete two lines at the same time. Given a permutation p and a “fork situation line” f (row or column), the b-thread waits for two X events on the line, in the order specified by the permutation, and then requests to mark an O on one of a given set of squares.

bp.registerBThread("PreventDiagForkX", function() {
	while (true) {
		bp.sync({waitFor:[X(f[p[0]].x, f[p[0]].y)]});
		bp.sync({waitFor:[X(f[p[1]].x, f[p[1]].y)]});
		bp.sync({request:[O(0,1),O(1,0),O(1,2),O(2,1)]},28);
	}
});

Listing 14. A b-thread that implements the thumb-rule of preventing player X from completing two lines at the same time using one of the diagonals. Given a permutation p and a “fork situation diagonal’ f, the b-thread waits for two X events on the diagonal, in the order specified by the permutation, and then requests to mark an O on one of a given set of squares.

Notice that the b-threads in listings 3-5 and 20-26 involve the priority option so the application can best detect the situation its facing. For example, in listing 3-5, the DetectXWin and DetectOWin b-threads have priority 100 to ensure that the application detects these before it detects a draw. Also, in listing 11, the priority of AddThirdO is higher than that of PreventThirdX because we want the application to prefer to win the game over a draw, or worse, giving the user (player X) another possibility to win the game in the next round (in case of a fork situation). The priority number is passed as an additional data to the bp.sync request. The additional data field is a general mechanism that can be used to attach meta-tdata, such as priorities, to synchronization statements. This data can, as done here, be used by the event selection mechanism to guide its selections.

The Tic-Tac-Toe example shows that it is possible to maintain an intuitive one-to-one relation between requirements and b-threads. It also demonstrates the usage of a customized event selection strategy, that takes priorities into account when selecting events.

Fig. 1. BPjs program stack, used for b-program execution. Parts that can be provided by client code appear in white. The behavioral code (written in JavaScript) is at the top level. This code can interact with its BPjs infrastructure using a special object exposed by BPjs, called bp. BPjs runs the standard JavaScript parts of the b-program code using the Mozilla Rhino JavaScript engine. Event selection is done using an event selection strategy object. When custom event selection logic is required, the host Java application can provide a custom EventSelectionStrategy instance to BPjs. The host application can interact with BPjs and the program it currently executes using an API, and by pushing events to a queue. It can listen to event selections and other b-program life cycle events by providing a listener object to the BProgramRunner running the b-program.

Note that the priority event selection mechanism in BPjs is pluggable. Thus, programmers can implement and use other types of prioritization schemes instead of the default event selection strategy, which uses a random arbiter.

BPjs tips

Mainly for commands that are useful, but not in frequent use.

Build jar with tests

Useful for running long verifications outside of NetBeans

mvn jar:test-jar

NOTE: The build must use jdk8 for now. Execution can be done on any jdk (at least, worked for us with jdk11).

Running verifications that live in the tests directory from the terminal

to run the actual test, also build the uber-jar:

mvn package -P uber-jar

Now both live in the target directory. You can now run the test using Java, as usual, with both jars in the -cp parameter:

java -cp target/BPjs-0.9.2-SNAPSHOT.uber.jar:target/BPjs-0.9.2-SNAPSHOT-tests.jar il.ac.bgu.cs.bp.bpjs.TicTacToe.TicTacToeVerMain

Event comparison

Better to use non-strict JavaScript object comparison for now. So prefer

var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)});
if ( evt.name == ADD_WETS.name ) {
  ...

over

var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)});
if ( evt === ADD_WETS ) {
  ...

as the latter may return a false negative, especially during verification.

Implementing Custom Events and Using Custom Objects as Event Data

ALWAYS make sure that you have state-based, meaningful equals() and hashCode(), and that serialization and de-serialization works. Or verification fails.

State minimization

(yes, this is informed by the “data minimization” directive of privacy by design) It’s better to store least amount of data. E.g. in the fruitRatio.js file, this version of the b-threads yields three states:

bp.registerBThread( "RaspberryAdder", function(){
    var fruitIndex=0;
    while (true) {
        var evt = null;
        if ( fruitIndex > 0 ) {
            evt = bp.hot(true).sync({request:ADD_RASPB,
                                     waitFor:ADD_FRUIT});
        } else {
            evt = bp.sync({waitFor:ADD_FRUIT});
        }
        fruitIndex = fruitIndex +
                    evt.data.blueberries-evt.data.raspberries;
    }
});

Where this version yields 4 (note different location of var evt) :

bp.registerBThread( "RaspberryAdder", function(){
    var fruitIndex=0;
    var evt = null;
    while (true) {
        if ( fruitIndex > 0 ) {
            evt = bp.hot(true).sync({request:ADD_RASPB,
                                     waitFor:ADD_FRUIT});
        } else {
            evt = bp.sync({waitFor:ADD_FRUIT});
        }
        fruitIndex = fruitIndex +
                    evt.data.blueberries-evt.data.raspberries;
    }
});

That’s because the former does not store the event from the previous iteration.

Variables Defined in Loops

When defining variables in loops, prefer let to const. This is because const won’t change after the first iteration, and the assignment attempt will fail silently.

E.g. :

for ( let i=0; i<10; i++ ) {
    let evtName = bp.thread.data.eventPrefix + String(i);
    req(evtName); // convenience function for bp.sync({request... (non-standard)
}

Will yield a series of events event-0 to event-9, whereas:

for ( let i=0; i<10; i++ ) {
    const evtName = bp.thread.data.eventPrefix + String(i);
    req(evtName); // convenience function for bp.sync({request... (non-standard)
}

Will yield a series of 10 events named event-0.

Working with Java Strings

Java strings are a bit different from JavaScript strings – they are equal, but not strictly equal. For example, say that j is a java.lang.String, and n is a JavaScript string, we get j==n but not j===n.

BPjs uses wrapping to iron out these inequalities, which can turn ugly when strings do a round-trip from JavaScript to Java and back. The only case in which BPjs programmers need to worry about this is in when directly instantiating Java strings in JS code (see example below).

var jString = java.lang.String("hello"); // Java String
var jsString = "hello";                  // JavaScript String
var list = java.util.ArrayList();
list.add(jString);
var rString = list.get(0);    // Java String that have done a round-trip

bp.log.info( jString  == jsString );  // true
bp.log.info( jString === jsString );  // false
bp.log.info( rString  == jsString );  // true
bp.log.info( rString === jsString );  // true

Working in Java with Objects from JavaScript

When invoking methods on objects that come from Rhino, it is often required that these methods are invoked in a context. This context can be obtained by calling BPjs.enterRhinoContext(). However, this method requires the client code to ensure that the context is closed properly.

An alternative would be to use the consumer pattern, with BPjs.withContext():

BProgram bprog = createBProgram(); // create b-program
bprog.setup(); // run initial part
JsEventSet es = bprog.getFromGlobalScope("esA", JsEventSet.class).get();

// es now holds a JsEventSet, which includes a Rhino function,
// and so, must be run within a context.

BPjs.withContext((c)->{
    assertTrue( es.contains(BEvent.named("AAA")));
});

Citing BPjs

If you use BPjs in an academic work, please consider citing it as follows:

Bar-Sinai M., Weiss G. (2021) Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. ISoLA 2020. Lecture Notes in Computer Science, vol 12479. Springer, Cham. https://doi.org/10.1007/978-3-030-83723-5_14

BibTex

@InProceedings{bpjs-liveness,
    author="Bar-Sinai, Michael
    and Weiss, Gera",
    editor="Margaria, Tiziana
    and Steffen, Bernhard",
    title="Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs",
    booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends",
    year="2021",
    publisher="Springer International Publishing",
    address="Cham",
    pages="199--215",
    isbn="978-3-030-83723-5",
    doi="10.1007/978-3-030-83723-5_14",
    url="https://doi.org/10.1007/978-3-030-83723-5_14"
}

Download

Indices and tables

• Index
• Search Page