axioms NonDet

type Status = enumeration of leader, uknown 

automaton Process (pos : Int, prev : Int, next : Int,  UID: Int)
  signature
    input RECEIVE(m: Int , const prev, const pos : Int)
    output SEND (m: Int , const pos , const next : Int)
    output leader(const UID)

  states
    pending : Int := UID,
    status : Status := uknown

  transitions
     input RECEIVE(m, j, i) where m > UID
       eff pending := m
     input RECEIVE(m, j, i) where m < UID
     input RECEIVE(m, j, i) where m = UID
       eff status := leader
     output SEND (m, i, j)
       pre status ~= leader /\ m = pending
       eff pending := 0
     output leader(UID)
       pre status = leader
       

automaton Channel(i:Int , j:Int)
  signature
    input SEND (m: Int , const i : Int, const j : Int)
    output RECEIVE(m : Int, const i : Int ,const j : Int)
  
  states
    toSend : Int := 0 

  transitions 
    input SEND (m, i, j)
      eff toSend := m 
    output RECEIVE(m,i,j)
      pre toSend = m 
      eff toSend := 0


automaton LCR
  components

   P1: Process(1, 4, 2, 7);
   P2: Process(2, 1, 3, 2);
   P3: Process(3, 2, 4, 3);
   P4: Process(4, 3, 1, 5);
   C1: Channel(1, 2);
   C2: Channel(2, 3);
   C3: Channel(3, 4);
   C4: Channel(4, 1)


  schedule
  do
    while(true) do
      fire output P1.SEND(P1.pending,1,2);
      fire output P2.SEND(P2.pending,2,3);
      fire output P3.SEND(P3.pending,3,4);
      fire output P4.SEND(P4.pending,4,1);

      fire output C1.RECEIVE(C1.toSend,1,2);
      fire output C2.RECEIVE(C2.toSend,2,3);
      fire output C3.RECEIVE(C3.toSend,3,4);
      fire output C4.RECEIVE(C4.toSend,4,1)


    od
  od