val N:ℕ; // the number of processes
val M:ℕ; // the maximum value of a counter
axiom notNull ⇔ N ≠ 0;

type Process = ℕ[N-1];
type Counter = ℤ[-2⋅M,M];

type Color = ℕ[2]; 
val MSG = 0; val WHITE = 1; val BLACK = 2;
type Message = Record[tag:Color,counter:Counter];
val MESSAGE = ⟨tag:MSG,counter:0⟩;
type Channel = Record[empty:Bool,message:Message];

// the empty channel
val empty:Channel = ⟨empty:true,message:MESSAGE⟩;

// adds message "m" to channel "c"
fun add(c:Channel,m:Message):Channel
  requires c.empty;
= ⟨empty:false,message:m⟩;

// returns the oldest message in "c"
fun first(c:Channel):Message 
  requires ¬c.empty;
= c.message;

// removes the oldest message from "c"
fun remove(c:Channel):Channel
  requires ¬c.empty;
= empty;

shared system DijkstraSafra
{
  var left:  Array[N,Channel] = Array[N,Channel](empty);
  var right: Array[N,Channel] = Array[N,Channel](empty);
  var token: Array[N,Channel] = Array[N,Channel](empty);
  
  var passive: Array[N,Bool] = Array[N,Bool](false);
  var termination: ℕ[2] = 0; // 0: no detection, 1: started, 2: completed

  var counter: Array[N,Counter] = Array[N,Counter](0);
  var color: Array[N,Color] = Array[N,Color](WHITE);

  action sendMessageLeft(i:Process) with
    ¬passive[i] ∧ left[(i+N-1)%N].empty ∧ counter[i] < M;
  {
    left[(i+N-1)%N] ≔ add(left[(i+N-1)%N],MESSAGE);
    counter[i] = counter[i]+1;
  }
  
  action sendMessageRight(i:Process) with
    ¬passive[i] ∧ right[(i+N-1)%N].empty ∧ counter[i] < M;
  {
    right[(i+N-1)%N] ≔ add(right[(i+N-1)%N],MESSAGE);
    counter[i] = counter[i]+1;
  }
  
  action receiveMessageLeft(i:Process) with
    ¬left[i].empty ∧ left[i].message.tag = MSG;
  {
    left[i] ≔ remove(left[i]);
    passive[i] ≔ false;
    counter[i] = counter[i]-1;
    color[i] = BLACK;
  }
  
  action receiveMessageRight(i:Process) with
    ¬right[i].empty ∧ right[i].message.tag = MSG;
  {
    right[i] ≔ remove(right[i]);
    passive[i] ≔ false;
    counter[i] = counter[i]-1;
    color[i] = BLACK;
  }
  
  action getPassive(i:Process) with
    ¬passive[i];
  {
    passive[i] = true;
  }
}