ByzantineGenerals.prot

// The Byzantine Generals Problem adapted from
// Title: The Byzantine Generals Problem
// Author: Leslie Lamport
// Author: Robert Shostak
// Author: Marshall Pease
// Year: 1982

// The number of liutenant generals is fixed at 3.

constant N := 3;
constant D := 2;

// A general can be loyal or disloyal.
direct variable loyal[(N+1)] < 2;

// Each general will choose a plan (e.g., attack or retreat).
direct variable plan[(N+1)] < D;
puppet variable cplan[N] < D;

// Variables used for communication.
puppet variable y[(2*N)] < D;


// There must be at least 3 loyal generals.
(assume & closed)
  (N <= loyal[0] + loyal[1] + loyal[2] + loyal[3]);

// Eventually, every loyal general should agree.
((future & silent) % puppet)
  (exists val < D :
   (forall i < 4 : loyal[i]==0 || plan[i]==val)
  );

// Captain General.
// The captain is represented by N processes,
// where each one communicates to a different lieutenant.
process Captain[i < N]
{
  read: loyal[N];

  // The captain has a plan that will not change.
  read: plan[N];

  write: cplan[i];

  // No actions are allowed when this general is disloyal.
  forbid:
    ( loyal[N]==0 --> );

  puppet:
   ( loyal[N]==1 && cplan[i]!=plan[N] --> cplan[i]:=plan[N]; );
}

// Lieutenant General.
process Lieutenant[i < N]
{
  read: loyal[i];
  write: plan[i];

  read: cplan[i]; // Read decision from captain.

  // Communicate with both other lieutenants.
  symmetric (xlink, olink) <- {# (2*i-1, 2*i+0), (2*i+2, 2*i+1) #}
  {
    read: y[xlink];  // Incoming link with neighbor.
    write: y[olink]; // Outgoing link with neighbor.
  }

  // No actions are allowed when this general is disloyal.
  forbid:
    ( loyal[i]==0 --> );
}