The Multi-Bach language and its temporal logic¶

Anemone uses a process algebra called Multi-Bach language which incorporates the following features.

1. Definition of data¶

Multi-Bach allows the user to define finite sets. Concretely, such sets are defined by associating an identifier with an enumeration of elements, such as:

 eset  Cols  =  { 1, 2, 3, 4, 5, 6 }.
       Rows  =  { 1, 2, 3, 4, 5, 6 }.

1.1. Set definition¶

Sets are defined by the keyword eset followed by a list of set declarations of the form

set_identifier = set_enumeration.

where set_identifer is a string of letters and digits, starting with an upper case letter, and where set_enumeration is a comma-separated list of strings composed of letters and digits, surrounded by the { and } brackets.

Example: In the case of the Rush Hour Problem, two sets are required: one to specify the columns and the rows (ranging from 1 to 6) and one to specify the colors of the vehicles.

More specifically, our modelling declares the following sets:

eset  RCInt  =  { 1, 2, 3, 4, 5, 6 }.
      Colors =  { yellow ,  green ,  blue ,  purple ,  red ,  orange}.

1.2. Si-terms¶

Si-terms are either tokens, expressed as strings of letters and digits (possibly containing only letters or digits) or structured constructs of the form \(f(t_{1}, ..., t_{n})\) where \(f, t_{1}, ...,t_{n}\) are such strings.

Example: In the Rush Hour example, free places of the game are represented by the si-terms free(i,j) with i a row and j a column. Such si-terms indicate the places currently free on the grid, namely not occupied by a car or a truck.

1.3. Maps¶

Map rewritings are declared by using the eqn keyword together with equations of the form s = t. where s and t are si-terms.

Example: In the Rush Hour example, assuming that trucks take three cells and are identified by the upper and left-most cell they occupy, the operation down_truck determines the cell to be taken by a truck moving down:

map down_truck  :  RCInt −> RCInt.
eqn down_truck ( 1 ) = 4 . down_truck ( 2 ) = 5 . down_truck (3) = 6.

2. Agents¶

The primitives of Multi-Bach comprise the tell, ask, nask and get primitives. They can be composed to form more complex agents by using traditional composition operators from concurrency theory:

sequential composition noted “;”,
parallel composition noted “||”,
and non-deterministic choice noted “+”.

Multi-Bach adds two other mechanisms:

conditional statements of the form \(C -> A \diamondsuit A\), where c denotes a condition and \(a_{1}\) and \(a_{2}\) are agents,
generalized choices of the form \(\sum_{e \in S} A_{e}\), where \(A_{e}\) is an agent parameterized by variable e ranging in set S.

The statements of the Multi-Bach language, called agents by abuse of language, consist of the statements A generated by the following grammar:

\[A ::= Prim | Proc | A ; A | A || A | A + A | C -> A \diamondsuit A | \sum_{e \in S} A_{e}\]

where Prim represents a primitive, Proc a procedure call, C a condition, e a variable and S a set.

Example: The behavior of a vertical truck can be described as follows:

proc VerticalTruck ( r: RCInt, c: RCInt, p: Colors ) =
      ( ( r>1 & r<5) −>
              ( get ( free ( pred ( r ) , c ) ) ;
                MoveTruck (p , pred ( r ) , c ) ;
                tell ( free ( succ ( succ ( r ) ) , c ) ) ;
                VerticalTruck ( pred ( r ) , c , p) ) ).
     +
      ( ( r>=1 & r<4) −>
              ( get ( free ( down_truck ( r ) , c ) ) ;
                MoveTruck (p , succ ( r ) , c ) ;
                tell ( free ( r , c ) ) ;
                VerticalTruck ( succ ( r ) , c, p ) ) ).

The code of some trucks and cars:

proc  YellowTruck = VerticalTruck (1 ,1 , yellow ).
      GreenTruck = HorizontalTruck (6 ,3 , green ).
      RedCar = HorizontalCar (3 ,2 , red ).
      OrangeCar = VerticalCar (5 ,6 , orange ).

The code of places occupied by vertical trucks:

proc VTruckPlaces( r: RCInt ,  c:  RCInt) =
     (r<5) −> get ( free( r , c ) );
              get ( free( succ ( r ) , c ) );
              get ( free( succ ( succ ( r ) ) , c ) ).

The code of places occupied by some trucks and cars:

proc YellowTruck = VTruckPlaces ( 1 , 1 ).
     GreenTruck = HTruckPlaces ( 6 , 3 ).
     RedCar = HCarPlaces ( 3 , 2 ).
     OrangeCar = VCarPlaces ( 5 , 6 ).

3. Processes as active data¶

Multi-Bach treats processes as active data through the four primtives, tellp(Proc), askp(Proc), naskp(Proc) and getp(Proc). They are used to respectively create a thread in charge of computing the procedure call Proc, to test for its presence or absence and to remove a thread associated with Proc. For instance, tellp(YellowTruck) creates a new thread for the yellow truck, identified by the string ’YellowTruck’. Executing getp(YellowTruck) kills this thread, whatever point of execution the thread has reached.

Rush Hour problem: Animation

4. Rules¶

Multi-Bach uses rules of the form \(+t, −u −> +v, −w\) to assert that the presence of \(t\) and the absence of \(u\) implies the presence of \(v\) and the absence of \(w\).

A rule is declared by using the keyword rule together with an equation of the form

rule_name = rule_description.

The rule name is a string of letters and digits, starting with a lower case letter.
The rule description is a construct of the form quant : l_m_objects −−> l_m_objects where quant quantifies variables (represented as strings of letter and digits, starting with a lower case letter) over sets and where l_m_objects lists si-terms orprocedure calls, positively or negatively marked

Example: The following rule asserts that any time a si-term moveCar(p,r,c) appears on the store, for some color \(p\), some row number \(r\) and some column number \(c\), the procedure call MoveCar(p,r,c) should be triggered and the si-term moveCar(p,r,c)should be removed:

Code: rule end of puzzle:

rule  end_puzzle = +out −−> +puzzle_solved, +RedCarOut.

with procedure RedCarOut defined as:

proc  RedCarOut = att ( position , red_car , rhScene , out_grid ).

5. Animations¶

Animations are obtained in a twofold manner:

by describing the scene to be painted
by primitives to place widgets, to move them, to make them appear or disappear, and more generally to change their attributes.

A scene is declared by using the scene keyword together with an equation of the form

scene_name = scene_description.

The scene name consists of a string of letters and digits starting with a lower case letter.
The scene description consists of a series of equalities defining the size of the widget, the layers, the background image, a series of images as well as a series of widgets, declared by means of the widget keyword.

Example: The following listing provides an example of the definition of the scene named rhScene:

scene rhScene =
 {
      size  = (640 ,640).
      layers = {top ,  middle ,  bottom}.
      background = loadImage ( Images/ the_background_img.png ).
      green_car  = loadImage ( Images/ green_car.jpg ).
      red_car    = loadImage ( Images/ red_car.jpg ).
         widget  car =
          {
             attributes = { color  in  idColors. }
             display    = { color = green −> green_car.
                            color = red −> red_car .}
             init       = { wdX = 40.
                            wdY = 60.
                            wdL = top.
                            color = red.
                          }
            }
  }

Scenes and widgets are manipulated by means of two primitives:

draw_scene(s): to draw the scene identified by s

att(x,w,s,v): to give value v to the attribute x of the widget identified by w on scene s.

where

place_at(w,s,x,y): to place widget identified by w on scene s at the coordinates (x, y)
move_to(w,s,x,y): to move the widget identified by w on scene s from its current position to the new coordinates (x, y)
hide(w,s): to hide widget identified by w on scene s
show(w,s): to make appear widget identified by w on scene s
layer(w,s,l): to place widget identified by w on scene s on the layer l of that scene.

Code: placing trucks

proc PlaceTruck ( r: RCInt, c: RCInt, p: Colors ) =
     ( p = yellow −> place_at ( yellow_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = green  −> place_at ( green_truck , rhScene , x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = bleu   −> place_at ( bleu_truck , rhScene , x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = purple −> place_at ( purple_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) ).

proc MoveTruck ( r: RCInt, c: RCInt, p: Colors ) =
     ( p = yellow −> move_to ( yellow_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = green  −> move_to ( green_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = bleu   −> move_to ( bleu_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) )
     +
     ( p = purple −> move_to ( purple_truck , rhScene ,x_vehicle ( c ) , y_vehicle ( r ) ) ).

6. A fragment of tempral logic¶

The Anemone workbench uses a fragment of PLTL with, as main goal, to check the reachability of states. It defined by the following grammar:

TF ::= PF | Next TF | PF Until TF     % Where PF is a propositional formula.

Example : If the red car indicates that it leaves the grid by placing out on the store, a solution to the rush problem is obtained by verifying the formula:

true Until(#out= 1)

Such formulae being very often used, they are abbreviated in Anemone as:

Reach(#out= 1)

Anemone 1.0.0 documentation