protocon/examplesoln/TokenRingSixState.prot at trunk · ProtocolConvergence/protocon · 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
45
46
47
48
49
50
51
52

// Token-passing around a ring
// using 6 states per process.
// Verified up to N=25

constant N := 3;
constant M := 3;

variable x[N] < M;
variable t[N] < 2;

process Bot[i < 1]
{
  read: x[i-1];  write: x[i];
  read: t[i-1];  write: t[i];
  direct action:
    ( x[i-1]!=2 && x[i]!=2 && t[i-1]<= t[i] --> x[i]:=2-t[i-1]; t[i]:=1-t[i-1]; )
    ( x[i-1]==2 && x[i]==2 && t[i-1]<= t[i] --> x[i]:=1+t[i-1]; t[i]:=1-t[i-1]; )
    ;
}
process P[i <- map tid < N-1 : tid+1]
{
  read: x[i-1];  write: x[i];
  read: t[i-1];  write: t[i];
  direct action:
    ( x[i-1]!=2 &&            t[i-1] < t[i] --> x[i]:=t[i-1]; t[i]:=t[i-1]; )
    ( x[i-1]!=2 && x[i]==2 && t[i-1]>= t[i] --> x[i]:=t[i-1];               )
    ( x[i-1]==2 &&            t[i-1] < t[i] --> x[i]:=2;      t[i]:=t[i-1]; )
    ( x[i-1]==2 && x[i]==0 && t[i-1]>= t[i] --> x[i]:=2;                    )
    ( x[i-1]==2 && x[i]==1 && t[i-1]>= t[i] --> x[i]:=2;      t[i]:=t[i-1]; )
    ;
}

// One process is enabled to act.
// The "active shadow" ensures that the protocol is live.
(future & active shadow)
  (unique i < N :
   i==0 &&
   (false
    || x[i-1]!=2 && x[i]!=2 && t[i-1]<= t[i]
    || x[i-1]==2 && x[i]==2 && t[i-1]<= t[i]
   )
   ||
   i!=0 &&
   (false
    || x[i-1]!=2 &&            t[i-1] < t[i]
    || x[i-1]!=2 && x[i]==2 && t[i-1]>= t[i]
    || x[i-1]==2 &&            t[i-1] < t[i]
    || x[i-1]==2 && x[i]==0 && t[i-1]>= t[i]
    || x[i-1]==2 && x[i]==1 && t[i-1]>= t[i]
   )
  );