protocon/examplesoln/OrientRingViaToken.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
53
54
55
56
57
58
59

// Ring orientation
// Title: Uniform Self-Stabilizing Ring Orientation
// Author: Amos Israeli
// Author: Marc Jalfon
// Year: 1993

constant N := 3;

direct variable c[N] < 3;
puppet variable tok[N] < 3; // R S I
direct variable way[(2*N)] < 2;


process P[i < N]
{
  symmetric (j, way_idx, adj_way_idx, adj_way_idx_far)
    <- {# (i-1, 2*i, 2*i-1, 2*i-2), (i+1, 2*i+1, 2*i+2, 2*i+3) #}
  {
    read: c[j];
    read: tok[j];
    read: way[adj_way_idx];
    read: way[adj_way_idx_far];
    write: way[way_idx];
  }
  read: c[i];
  write: tok[i];

  (assume & closed) (c[i] != c[i-1]);
  (assume & closed)
    (way[2*i] != way[2*i+1]);

  predicate depsat :=
    way[2*i-2]!=way[2*i-1] && way[2*i+0]!=way[2*i+1] && way[2*i+2]!=way[2*i+3]
    &&
    c[i-1]!=c[i] && c[i]!=c[i+1]
    ;

  puppet action:
    // 1
    ( depsat && tok[i-1]==1 && way[2*i-1]==1 && tok[i]==2 --> tok[i]:=0; way[2*i+0]:=0; way[2*i+1]:=1; )
    ( depsat && tok[i+1]==1 && way[2*i+2]==1 && tok[i]==2 --> tok[i]:=0; way[2*i+1]:=0; way[2*i+0]:=1; )
    // 2
    ( depsat && tok[i-1]==0 && way[2*i-1]==0 && tok[i]==1 && way[2*i+0]==1 && way[2*i+1]==0 --> tok[i]:=2; )
    ( depsat && tok[i+1]==0 && way[2*i+2]==0 && tok[i]==1 && way[2*i+1]==1 && way[2*i+0]==0 --> tok[i]:=2; )
    // 3
    ( depsat && !(tok[i-1]==1 && way[2*i-1]==1) && tok[i]==0 && way[2*i+0]==0 --> tok[i]:=1; )
    ( depsat && !(tok[i+1]==1 && way[2*i+2]==1) && tok[i]==0 && way[2*i+1]==0 --> tok[i]:=1; )
    // 4
    ( depsat && tok[i-1]==1 && way[2*i-1]==1 && tok[i]==1 && way[2*i+0]==1 && c[i-1]==(c[i]+1)%3 --> tok[i]:=0; way[2*i+0]:=0; way[2*i+1]:=1; )
    ( depsat && tok[i+1]==1 && way[2*i+2]==1 && tok[i]==1 && way[2*i+1]==1 && c[i+1]==(c[i]+1)%3 --> tok[i]:=0; way[2*i+1]:=0; way[2*i+0]:=1; )
    // 5
    ( depsat && tok[i-1]==2 && way[2*i-1]==1 && tok[i]==2 && way[2*i+0]==1 && c[i-1]==(c[i]+1)%3 --> tok[i]:=1; )
    ( depsat && tok[i+1]==2 && way[2*i+2]==1 && tok[i]==2 && way[2*i+1]==1 && c[i+1]==(c[i]+1)%3 --> tok[i]:=1; )
    ;
}

((future & shadow) % puppet)
  (forall i < N : way[2*i-1] == way[2*i+1]);