![]() |
In this tutorial, we model and solve (by reachability analysis) a classic
puzzle, known as bridge crossing puzzle using PAT. The following is the puzzle
description. All four people start out on the southern side of the bridge, namely the
King, Queen, a young Lady and a Knight. The goal is for everyone to arrive at
the castle- the north of the bridge, before the time runs out. The bridge can
hold at most two people at a time and they must be carrying the torch when
crossing the bridge. The King needs 5 minutes to cross, the Queen 10 minutes,
the Lady 2 minutes and the Knight 1 minute. The question is given a specific
amount of time, whether all people can cross the bridge in time. The parital declaration part The above also defines the variables in the system, where var is a reserved
keyword for introducing variables or arrays. Notice that PAT has a weak type
system. Variable Knight is used to model whether the knight is at the southern
side of the bridge or the northern side. It is of value 0 if the knight hasn't
crossed the bridge, otherwise 1. Similarly, we define the rest. Variable time
records the number of time units spent by far. The default value is
0. The two numbers between "{}" is the lower bound and upper bound
values of the variable. When user selectd the BDD selection in the Verification
Dialog, these numbers are very helpful to the program to calculate the number of
bits needed to represent that variable. The process P1 has two states North and South. Each transtion from North to
South corresponds the case when someone go from North to South and vice versa.
The label of the transition is in the following
form: Informally, it means that if the guard is true, then the action can occur,
i.e., the program attached with the action can be executed. Notice that program
here could contain while-loops, if-then-else, etc. For instance, at the first
line, the guard states that the Knight and the Lady are both at the
southern side of the bridge. If this is true, then the action go_knight_lady can
occur, which in terms means that the variable Knight and Lady are set to be 1
(meaning they have crossed the bridge) and time is incremented by the number of
time units needed by the lady. After that, the system behaves as process North
because the torch must come back from North to South. Similarly, we can
enumerate all possible ways of crossing the bridge, e.g., the knight goes
together with the king or queen, the king goes with the lady or queen, and the
queen goes with the lady. Having modeled all possible behaviors of the systems as the above processes,
we are now ready to reason about the system. The question we are interested is whether it is feasible to cross the bridge
within Max number of time unit. The above shows one of the questions. The first
line defines that the system only includes the process P1. The second line
defines a proposition named goal, which states that the time taken should be not
greater than Max and all people should be on the northern side of the bridge.
The third line is the assertion, where #assert is a reserved keyword.
'reaches' is also a keyword. Informally, the assertion says that starting from
process South() (because the state South is the initial state of the process
P1), we will reach a state at which the proposition goal is true.
////////////////The
Model//////////////////
#define Max 17;
#define KNIGHT 1;
#define
LADY 2;
#define KING 5;
#define QUEEN 10;
var Knight: {0..1} = 0;
var Lady: {0..1} = 0;
var King: {0..1}= 0;
var Queen: {0..1} = 0;
var time: {0..17} = 0;
The declaration includes some definitions of
the constants in this model, where #define is a reserved keyword for
defining a synonymy for a (integer or Boolean) constant or a proposition.
Max represents the maximum number of time units. KNIGHT stands for the number of
time units the knight needs. Similarly, we define the rest ones. We remark
the users shall use constants (instead of variables) whenever possible. Because
constants never change, during verification they are not excluded from the
system state information, and hence, using constants instead of variables save
memory and maybe time also.
[guard]event{program}
The rest of the
declaration part
System = P1();
#define goal (Knight==1 && Lady==1
&& King==1 && Queen==1 && time <= Max);
#assert
System reaches goal;