DiningCrypto.prot

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];

  (assume & closed)
    (agree[i]==0);

  // Same action as the other processes, but using ans[0] instead of agree[i].
  // agree[i] is set to 0 explicitly so this is an answer when it is not assumed to be 0
  // as in examplespec/DiningCrypto.prot
  puppet: ( true --> ans[0]:=coin[i-1]+coin[i]+pay[i]+agree[i-1]; agree[i]:=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];

  puppet: ( true -=> agree[i]:=coin[i-1]+coin[i]+pay[i]+agree[i-1]; );
}