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

constant N := 3;

// Hold whether a cryptographer pays.
// Must be derived from the state of the Bot process.
shadow variable ans[1] < 2;

// These can be puppet variables, but they don't have to be
// since the invariant is (future & future silent).
variable coin[N] < 2;
variable agree[N] < 2;
variable pay[N] < 2;

// ans[0] holds whether a cryptographer pays.
(future & future silent)
  (ans[0] == 1
   <=>
   exists i < N : pay[i] == 1
  );

// Assume exactly zero or one cryptographers pay.
(assume & closed)
  (!(exists i < N : pay[i]==1)
   ||
   (unique i < N : pay[i]==1)
  );


process Bot[i < 1]
{
  read: pay[i];
  read: coin[i-1], agree[i-1];
  read: coin[i];
  write: agree[i];
  write: ans[0];
}

process P[j < (N-1)]
{
  let i := j+1;
  read: pay[i];
  read: coin[i-1], agree[i-1];
  read: coin[i];
  write: agree[i];
}