spin_tutorial/dekker_1.pml at main · titech-os/spin_tutorial · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
mtype = { TurnP, TurnQ };
bool wantp = false, wantq = false;
mtype turn = TurnP;
int ncs = 0;

active proctype P() {
  do :: wantp = true;
        do :: wantq ->
              if :: (turn == TurnQ) ->
                    wantp = false;
                    turn == TurnP;
                    wantp = true;
                 :: else -> skip;
              fi
           :: else -> break;
        od;
progress:
        ncs++;
        assert(ncs == 1);
        ncs--;
        turn = TurnQ;
        wantp = false;
  od
}

active proctype Q() {
  do :: wantq = true;
        do :: wantp ->
              if :: (turn == TurnP) ->
                    wantq = false;
                    turn == TurnQ;
                    wantq = true;
                 :: else -> skip;
              fi
           :: else -> break;
        od;
        ncs++;
        assert(ncs == 1);
        ncs--;
        turn = TurnP;
        wantq = false;
  od
}