spin_tutorial/dekker_2.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
44
mtype = { TurnP, TurnQ };
bool wantp = false, wantq = false;
mtype turn = TurnP;

active proctype P() {
  do :: skip;
try:    wantp = true;
        do :: wantq ->
              if :: (turn == TurnQ) ->
                    wantp = false;
                    turn == TurnP;
                    wantp = true;
                 :: else -> skip;
              fi
           :: else -> break;
        od;
cs:     turn = TurnQ;
        wantp = false;
  od
}

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


ltl safety { []!(P@cs && Q@cs) }

ltl liveness1 { []<>P@cs }

ltl liveness2 { [](P@try -> <>P@cs) }