 1 #define true 1
 2 #define false 0
 3 bool ain,bin;
 4 bool cA,cB;
 5 int turn;

6

 7 proctype A()
 8 {
 9  cA=true;
10  turn = 1;

11

12  do
13  :: cB && turn != 0 ->
14 accept: skip;
15  :: !cB || turn==0 ->
16 progress: break;
17  od;

18

19  ain=true;
20  assert(bin==false);
21  ain=false;
22  turn=1;
23  cA=false;

24 }

25

26 proctype B()

27 {

28  cB=true;
29  turn = 0;
30  do
31  ::  cA && turn != 1 ->
32 accept:  skip;
33  ::  !cA || turn == 1 ->
34 progress: break;
35  od;

36

37  bin=true;

38  assert(ain==false);
39  bin=false;
40  turn=0;
41  cB=false;

42 }

43 44 45

46 init

47 {

48  cA=false;cB=false;
49  turn=0;
50  ain=false;
51  bin=false;
52  atomic{
53  run A();
54  run B();

55 } 56 }

57 58 59