specification PETERSON [NCS0, CS0, NCS1, CS1, F0, F1, T] : noexit

library
   BOOLEAN,
   NATURAL
endlib

type COMMAND is
   sorts COMMAND
   opns
      READ (*! constructor *),
      WRITE (*! constructor *) : -> COMMAND
endtype

behaviour

      (
      P [NCS0, CS0, F0, F1, T] (0)
      |||
      P [NCS1, CS1, F1, F0, T] (1)
      )
   |[F0, F1, T]|
      (
      FLAG [F0] (false)
      |||
      FLAG [F1] (false)
      |||
      TURN [T] (0)
      )

where

   process P [NCS, CS, FJ, FI, T] (J : Nat) : noexit :=
      NCS; (* non critical section *)
         FJ !WRITE !true;
            T !WRITE !J;
               P_AUX [NCS, CS, FJ, FI, T] (J)
   endproc

   process P_AUX [NCS, CS, FJ, FI, T] (J : Nat) : noexit :=
      FI !READ ?VAL_FI:Bool;
         T !READ ?VAL_T:Nat;
            (
            [VAL_FI and (VAL_T == J)] ->
               P_AUX [NCS, CS, FJ, FI, T] (J)
            []
            [not (VAL_FI) or (VAL_T == ((J + 1) mod 2))] ->
               CS; (* critical section *)
                  FJ !WRITE !false;
                     P [NCS, CS, FJ, FI, T] (J)
            )
   endproc

   process FLAG [F] (VAL_FLAG : BOOL) : noexit :=
      F !READ !VAL_FLAG;
         FLAG [F] (VAL_FLAG)
      []
      F !WRITE ?VAL:BOOL;
         FLAG [F] (VAL)
   endproc

   process TURN [T] (VAL_TURN : NAT) : noexit :=
      T !READ !VAL_TURN;
         TURN [T] (VAL_TURN)
      []
      T !WRITE ?VAL:NAT;
         TURN [T] (VAL)
   endproc

endspec