MODULE main DEFINE N := 5;

VAR

  loc[1]  : 0..4;
  y[1]    : 0..N;
  loc[2]  : 0..4;
  y[2]    : 0..N;
  loc[3]  : 0..4;
  y[3]    : 0..N;
  loc[4]  : 0..4;
  y[4]    : 0..N;
  loc[5]  : 0..4;
  y[5]    : 0..N;

  P[1] : process CM(1,y,loc,N);
  P[2] : process CM(2,y,loc,N);
  P[3] : process CM(3,y,loc,N);
  P[4] : process CM(4,y,loc,N);
  P[5] : process CM(5,y,loc,N);
  Id   : process Idle;

INIT
  y[1]=0 & y[2]=0 & y[3]=0 & y[4]=0 & y[5]=0 &
  loc[1]=0 & loc[2]=0 & loc[3]=0 & loc[4]=0 & loc[5]=0

MODULE Idle

MODULE CM(i,y,loc,N)

DEFINE
  cond23 := ((1 = i) | (y[1] = 0) | (y[1] > y[i])) &
            ((2 = i) | (y[2] = 0) | (y[2] > y[i])) &
            ((3 = i) | (y[3] = 0) | (y[3] > y[i])) &
            ((4 = i) | (y[4] = 0) | (y[4] > y[i])) &
            ((5 = i) | (y[5] = 0) | (y[5] > y[i])) ;

  condup  := (loc = 1) & (next(loc) = 2);

  condown := (loc = 4) & (next(loc) = 0);

  pres_but := (i=1 | next(y[1])=y[1]) &
              (i=2 | next(y[2])=y[2]) &
              (i=3 | next(y[3])=y[3]) &
              (i=4 | next(y[4])=y[4]) &
              (i=5 | next(y[5])=y[5]);

  pres_loc_but := (i=1 | next(loc[1])=loc[1]) &
                  (i=2 | next(loc[2])=loc[2]) &
                  (i=3 | next(loc[3])=loc[3]) &
                  (i=4 | next(loc[4])=loc[4]) &
                  (i=5 | next(loc[5])=loc[5]);

  pres_all := pres_but & next(y[i])=y[i];

  new_max :=  (i=1 | next(y[i]) > next(y[1])) &
              (i=2 | next(y[i]) > next(y[2])) &
              (i=3 | next(y[i]) > next(y[3])) &
              (i=4 | next(y[i]) > next(y[4])) &
              (i=5 | next(y[i]) > next(y[5]));

  zero_pres := (i=1 | ((next(y[1])=0) <-> (0=y[1]))) &
               (i=2 | ((next(y[2])=0) <-> (0=y[2]))) &
               (i=3 | ((next(y[3])=0) <-> (0=y[3]))) &
               (i=4 | ((next(y[4])=0) <-> (0=y[4]))) &
               (i=5 | ((next(y[5])=0) <-> (0=y[5]))) ;

  ord_pres := (i=1 | i=2 | (y[1]<y[2] <-> next(y[1])<next(y[2]))  &
                           (y[1]>y[2] <-> next(y[1])>next(y[2]))) & 
              (i=1 | i=3 | (y[1]<y[3] <-> next(y[1])<next(y[3]))  &
                           (y[1]>y[3] <-> next(y[1])>next(y[3]))) &
              (i=1 | i=4 | (y[1]<y[4] <-> next(y[1])<next(y[4]))  &
                           (y[1]>y[4] <-> next(y[1])>next(y[4]))) &
              (i=1 | i=5 | (y[1]<y[5] <-> next(y[1])<next(y[5]))  &
                           (y[1]>y[5] <-> next(y[1])>next(y[5]))) &
              (i=2 | i=3 | (y[2]<y[3] <-> next(y[2])<next(y[3]))  &
                           (y[2]>y[3] <-> next(y[2])>next(y[3]))) &
              (i=2 | i=4 | (y[2]<y[4] <-> next(y[2])<next(y[4]))  &
                           (y[2]>y[4] <-> next(y[2])>next(y[4]))) &
              (i=2 | i=5 | (y[2]<y[5] <-> next(y[2])<next(y[5]))  &
                           (y[2]>y[5] <-> next(y[2])>next(y[5]))) &
              (i=3 | i=4 | (y[3]<y[4] <-> next(y[3])<next(y[4]))  &
                           (y[3]>y[4] <-> next(y[3])>next(y[4]))) &
              (i=3 | i=5 | (y[3]<y[5] <-> next(y[3])<next(y[5]))  &
                           (y[3]>y[5] <-> next(y[3])>next(y[5]))) &
              (i=4 | i=5 | (y[4]<y[5] <-> next(y[4])<next(y[5]))  &
                           (y[4]>y[5] <-> next(y[4])>next(y[5]))) ;
                     

TRANS

  pres_loc_but &
  ((loc[i]=0 & next(loc[i]) in {0,1} & pres_all)                             |
   (loc[i]=1 & next(loc[i])=2 & zero_pres & new_max & ord_pres)              |
   (loc[i]=2 & pres_all & (cond23 & next(loc[i])=3                           |
                          !cond23 & next(loc[i])=2  ))                       | 
   (loc[i]=3 & next(loc[i])=4 & pres_all)                                    |
   (loc[i]=4 & next(loc[i])=0 & pres_but & next(y[i])=0))
  

JUSTICE
    loc[i] != 1,  !((loc[i] = 2) & cond23), loc[i] != 3, loc[i] != 4