MODULE main

DEFINE

  N := 6;
  Err := P[1].Err | P[2].Err | P[3].Err | P[4].Err | P[5].Err
                  | P[6].Err;
-- |P[7].Err;
--P[8].Err;


VAR

  fork : array 1..N of boolean;
  
  P[1] : process MP(fork[1],fork[2]);
  P[2] : process MP(fork[2],fork[3]);
  P[3] : process MP(fork[3],fork[4]);
  P[4] : process MP(fork[4],fork[5]);
  P[5] : process MP(fork[5],fork[6]);
--  P[6] : process MP(fork[6],fork[7]);
  P[N] : process MP(fork[1],fork[N]);
--  P[7] : process MP(fork[7],fork[8]);
--  P[8] : process MP(fork[1],fork[8]);
  Idle : process ID;


MODULE ID

MODULE MP(first,second)
DEFINE

  Err := (neverl1 & (loc = 1) & first) | (neverl2 & (loc = 2) & second);

VAR
  neverl1 : boolean;
  neverl2 : boolean;
  loc: 0..3  kind of own;

ASSIGN
  init(first) := 1;
  init(second) := 1;
  init(loc) := 0;
  init(neverl1) := 0;
  init(neverl2) := 0;

  next(loc) :=  case
                  loc = 0		: 1;
                  loc = 1 & first 	: 2;
                  loc = 2 & second	: 3;
                  loc = 3 		: 0;
                  1			: loc;
                esac;

  next(first) := case
                 loc = 1 & next(loc) = 2 : 0;
                 loc = 3 & next(loc) = 0 : 1;
                 1                       : first;
                esac;

  next(second) := case
                   loc = 2 & next(loc) = 3 : 0;
                   loc = 3 & next(loc) = 0 : 1;
                   1                       : second;
                 esac;

  next(neverl1) := case
		     !neverl1		     : {0,1};
                     1			     : neverl1;
                   esac;

  next(neverl2) := case
                     !neverl2		      : {0,1};
                     1			      : neverl2;
                   esac;

JUSTICE
  neverl1 | loc != 1,
  neverl2 | loc != 2,
  loc != 3