Consider the following scheduling problem. Four soldiers are heavily injured, and try to flee ot their home land. The enemy is chasing them and in the middle of the night they arrive at a bridge that has been damaged and can only carry two soldiers at a time. Furthermore, several land mines have been placed on the bridge and a torch is needed to move the mines out of the way. The enemy is approaching, so the soldiers know that they only have 60 minutes to cross the bridge. The soldiers only have a single torch and they are not equally injured; the crossing time (one-way!) for the soldiers is 5 min, 10 min, 20 min and 25 minutes.
A partial specification of the soldier problem in Promela is given below.
This specification consists of two
processes, Safe and Unsafe. In the beginning all
soldiers are at the Unsafe side, and the goal is to bring them
all to the Safe side. We start our model of the soldiers problem
by modeling the bridge.
chan unsafe_to_safe = [0] of {soldier, soldier};
chan safe_to_unsafe = [0] of {soldier};
The bridge is modeled with two channels. The channel unsafe_to_safe models the unsafe->safe direction, whereas safe_to_unsafe models the safe->unsafe direction.
Every time two soldiers have made it to the safe side, on of the men on the safe side has to go back with the torch. It is clear that it is not very helpful to go back with two men. For that reason, the channel safe_to_unsafe only passes a single soldier.
The four soldiers are identified by integers in the range 0..N-1, where N is defined as follows:
#define N 4
This means that a soldier is represented by a byte:
#define soldier byte
byte time;
byte val[N];
The variable time is the number of minutes that have elapsed since the soldiers have started to move. Every time a soldier reaches to the other side of the bridge, the variable time is updated.
The array val holds the times it takes the soldiers to cross the bridge. Because Promela does not support constant arrays, the array val has to be initialized in the init process:
val[0] = 5; val[1] = 10; val[2] = 20; val[3] = 25;
As specified in the problem description, the times for the soldiers to cross the bridge are 5, 10, 20 and 25 minutes, respectively.
Crossing the bridge is modeled by soldiers that are passed between two processes: Unsafe and Safe. In the beginning, all soldiers are at the Unsafe side, and the goal is to get all soldiers to the Safe side. In the reminder we only define the process Unsafe.
We model the location of the soldiers byte the bit-array here. If here[i] is 1, then soldier i is at the unsafe side of the bridge.
bit here[N];
Initially. all soldiers are on the unsafe side of the bridge, so the
body of Unsafe starts by initializing the array
here:
here[0] = 1; here[1] = 1; here[2] = 1; here[3] = 1;
The rest of Unsafe's body is responsible for crossing the bridge. In every iteration two soldiers are sent to the other side and one soldier is expected back with the torch. In the first part. we need to randomly chose a soldier that is still at the unsafe side. For this purpose we introduce the macro select_soldier(x)
#define select_soldier(x) \
if
\
:: here[0] -> x = 0 \
:: here[1] -> x = 1 \
:: here[2] -> x = 2 \
:: here[3] -> x = 3 \
fi;
\
here[x] = 0
Only the guards for which here[i] is 1 are executable. One of these executable guards is randomly chosen and the variable x gets the number of this soldier.
If there are no soldiers left at the unsafe side, the do-loop of the Unsafe process should be terminated. This break is really needed here, because otherwise the Unsafe process will be blocked (i.e. an invalid endstate in Spin) by select_soldier(s2) if there is only one soldier at the unsafe side.
The soldier s1 is the soldier that gets back with the torch. The time is updated accordingly to the time it took soldier s1 to cross the bridge.
do
:: select_soldier(s1);
select_soldier(s2);
unsafe_to_safe!s1, s2;
IF all_gone -> break FI;
safe_to_unsafe?s1;
here[s1] = 1;
time = time + val[s1];
od;
The IF-costruction uses the following macro definition:
#define IF if ::
#define FI :: else fi
#define all_gone (!here[0] && !here[1] && !here[2]
&& !here[3])
The IF-FI combination implements a single IF clause
and the all_gone predicate is true when all values in
the here array are 0.