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.