protocon/examplespec/Sat.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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

// This is a protocol used to show NP-completeness of adding convergence.
// An instance of 3-SAT corresponds to this protocol.
// A stabilizing protocol can be synthesized if and only if the corresponding
// 3-SAT instance can be satisfied.
//
// For the satisfiable case, the example 3-SAT instance is:
//   phi = ( v0 ||  v1 ||  v2) &&
//         (!v1 || !v1 || !v2) &&
//         (!v1 || !v1 ||  v2) &&
//         ( v1 || !v2 || !v0)
// where v0, v1, and v2 are boolean variables.
//
// For unsatisfiable case, the example 3-SAT instance
// is the same as the above case but with two more clauses:
//   phi = ...                 &&
//         ( v2 ||  v2 ||  v1) &&
//         ( v0 ||  v1 ||  v0)
//
// This formula defines the protocol's $x[0..2]$ domains (via the constant $M$)
// and the legitimate states.

constant ExpectSat := 1;

// Number of variables in 3-SAT formula.
constant M := 3;

//////////////////////////////////////////////////////////////////////////////
//// System Variables

variable x[3] < M;
variable y[3] < 2;
variable sat[1] < 2;

//////////////////////////////////////////////////////////////////////////////
// Instance-Specific Predicates

predicate SatClauses := true
  //       v0         v1         v2
  && (x[0]!=0 || x[1]!=1 || x[2]!=2 ||
      y[0]==1 || y[1]==1 || y[2]==1)
  //      !v1        !v1        !v2
  && (x[0]!=1 || x[1]!=1 || x[2]!=2 ||
      y[0]==0 || y[1]==0 || y[2]==0)
  //      !v1        !v1         v2
  && (x[0]!=1 || x[1]!=1 || x[2]!=2 ||
      y[0]==0 || y[1]==0 || y[2]==1)
  //       v1        !v2        !v0
  && (x[0]!=1 || x[1]!=2 || x[2]!=0 ||
      y[0]==1 || y[1]==0 || y[2]==0)
  ;

predicate UnsatClauses := SatClauses
  //       v2         v2         v1
  && (x[0]!=2 || x[1]!=2 || x[2]!=1 ||
      y[0]==1 || y[1]==1 || y[2]==1)
  //       v0         v1         v0
  && (x[0]!=0 || x[1]!=0 || x[2]!=1 ||
      y[0]==1 || y[1]==1 || y[2]==1)
  ;


//////////////////////////////////////////////////////////////////////////////
//// Invariant

predicate Iden :=
  (forall i < 3 :
   (forall j < 3 :
    (x[i] != x[j]) || (y[i] == y[j])));

predicate Clauses :=
  (ExpectSat==1 && SatClauses)
  ||
  (ExpectSat==0 && UnsatClauses)
  ;

(future & closed)
  (Iden && Clauses && (sat[0] == 1));

// Use the (future & future silent) instead of (future & closed) above
// if you want to allow the invariant to shrink.
// When allowing this, a process P[i] might get two actions for some a and b:
//   (sat[0]==0 && x[i]==a && y[i]==  b --> y[i]:=1-b;)
//   (sat[0]==1 && x[i]==a && y[i]==1-b --> y[i]:=  b;)
// Always interpret the action where sat[0]==1 if it exists.


//////////////////////////////////////////////////////////////////////////////
//// Topology

process P[i < 3]
{
  read: sat[0];
  read: x[i];
  write: y[i];
}

// Use these processes instead of P[0..2] instead if you want to allow asymmetry.
// (Hint: The processes will still be symmetric!)
//process P0[i < 1] { read: sat[0], x[0]; write: y[0]; }
//process P1[i < 1] { read: sat[0], x[1]; write: y[1]; }
//process P2[i < 1] { read: sat[0], x[2]; write: y[2]; }

process P3[i < 1]
{
  read: x[0], x[1], x[2];
  read: y[0], y[1], y[2];
  write: sat[0];
}