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