0.3 Modeling concurrent processes  (Page 7/21)

Random walk 1

The following code illustrates use of the do statement, the primary iteration statement. 1 #define STARTING_DISTANCE 2 2 show int dist = STARTING_DISTANCE;3 4 active proctype stumble()5 { 6 do7 :: true ->dist--; /* Approach. */ 8 :: true ->dist++; /* Retreat. */ 9 :: dist<= 0 ->break; /* Success! */ 10 :: dist>= STARTING_DISTANCE*2 ->break; /* Give up. */ 11 od;12 }

This process consists solely of a loop from do to the matching od . The loop contains four guarded statements as alternatives,each prefaced with double colons ( :: ). On each iteration, all guards are evaluated. From those evaluatingto true , only one is chosen arbitrarily, and its body executed.(What if none are true? We'll see soon .)

Random walk 2

The following code is a variation on the previous, illustrating the if statement and the else keyword. 1 #define STARTING_DISTANCE 2 2 show int dist = STARTING_DISTANCE;3 4 active proctype stumble()5 { 6 do7 :: (!(dist<= 0)&&8 !(dist>= STARTING_DISTANCE*2)) ->9 if 10 :: true ->dist--; /* Approach. */ 11 :: true ->dist++; /* Retreat. */ 12 fi;13 :: else ->break; 14 od;15 }

First, consider the do loop. It has two guarded expressions,one with the guard else . On each iteration, if there are anyenabled clauses, one is chosen arbitrarily, as before. But, if none are enabled the else clause, if any, is chosen. There may be only one else clause. An else clause is not the same as one with a true guard, as it can only be executed if no other clause is enabled.

Here, this means that the first clause of the do , i.e. , the entire if statement, is used whenever the distance is withinthe specified range. Otherwise, the loop is exited. Thus, unlike the previous example , the loop is alwaysexited once the distance is 0 or STARTING_DISTANCE*2 .

Inside this loop, we have an if statement, which itself has two clauses. Like the do , it chooses arbitrarily among theenabled clauses, and may have an else clause.