protocon/examplespec/ColorChain.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

constant N := 3;

variable x[N] < 2;

(future & silent)
  (forall i < (N-1) : x[i]!=x[i+1])
  ;

process Bot[i < 1]
{
  write: x[i];
  read: x[i+1];
}

process P[j < (N-2)]
{
  let i := j+1;
  read: x[i-1];
  write: x[i];
  read: x[i+1];
}

process Top[j < 1]
{
  let i := N-1;
  read: x[i-1];
  write: x[i];
}