Blocks World (Directed Model Checking)

In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1).

For this we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it). The goal is, given a starting position, to find a plan for the robot to achieve a certain goal (here: block a is on top of b, which is on top of c, ...).

In B we can model this task as follows. We have two operations, on to move a block onto the table and one to move a block onto another one. The initial configuration is specified in the INITIALISATION; the target is specified by the GOAL definition (which the ProB model checker recognises).

MACHINE BlocksWorldGeneric6
SETS
 Objects={a,b,c,d,e,f}
DEFINITIONS
      GOAL == (on = ongoal);
      ongoal == {a|->b, b|->c, c|->d, d|->e, e|->f}
VARIABLES on
INVARIANT
  on: Objects +-> Objects
INITIALISATION
  on := {a|->b, c|->a}
OPERATIONS
  move_on_table(obj) = PRE obj /: ran(on) & obj : dom(on) THEN
    on := {obj} <<| on
  END;
  move_on_object(obj,onobj) = PRE obj/:ran(on) & onobj /:ran(on) & obj /= onobj THEN
      on(obj) := onobj
  END
END

Adding a graphical visualization

Adding a graphical visualization is independent of the model checking, but helps visualising the traces found by the model checker. For this we can add ANIMATION_FUNCTION and ANIMATION_FUNCTION_DEFAULT definition, as specified in the complete model at the end of this page.

The initial state of our model then looks as follows, when loaded using ProB Tcl/Tk:

The complete model for reference

MACHINE BlocksWorldGeneric6
SETS
 Objects={a,b,c,d,e,f}
DEFINITIONS
      ANIMATION_FUNCTION_DEFAULT == {r,c,img|r:1..card(Objects) & img=0 & c:1..card(Objects)};
      ANIMATION_FUNCTION == (  {r,c,i| r=card(Objects) & i:Objects & c:Objects & c=i & i/:dom(on)} \/
                               {r,c,i| r:1..(card(Objects)-1) & i:Objects & c:Objects &
                                       i|->c:iterate(on,card(Objects)-r) & c/:dom(on)}
                              );
      ANIMATION_IMG0 == "images/empty_box_white.gif";
      ANIMATION_IMG1 == "images/A.gif";
      ANIMATION_IMG2 == "images/B.gif";
      ANIMATION_IMG3 == "images/C.gif";
      ANIMATION_IMG4 == "images/D.gif";
      ANIMATION_IMG5 == "images/E.gif";
      ANIMATION_IMG6 == "images/F.gif";
      GOAL == (on = ongoal);
      ongoal == {a|->b, b|->c, c|->d, d|->e, e|->f};
      DIFF(A,TARGET) == (card(A-TARGET) - card(TARGET /\ A));
      HEURISTIC_FUNCTION == DIFF(on,ongoal);
VARIABLES on
INVARIANT
  on: Objects +-> Objects
INITIALISATION
  on := {a|->b, c|->a}
OPERATIONS
  move_on_table(obj) = PRE obj /: ran(on) & obj : dom(on) THEN
    on := {obj} <<| on
  END;
  move_on_object(obj,onobj) = PRE obj/:ran(on) & onobj /:ran(on) & obj /= onobj THEN
      on(obj) := onobj
  END
END