mtype = {approaches, leaves, lower, raise, atgate, faraway, up, down};

chan control_link = [0] of {mtype, byte};
chan gate_link [8] = [0] of {mtype};

mtype bar[8] = down;
bool on_shared_track[2] = false;
bool shared_track_open = false

proctype train(byte current_gate, id) {

   mtype position = atgate;

   control_link!approaches,current_gate;
   do :: atomic {
            position==faraway ->
		if :: current_gate==3 -> current_gate = 0; assert(id==0)
               :: current_gate==7 -> current_gate = 4; assert(id==1)
               :: else -> current_gate++;
            fi;
            control_link!approaches,current_gate; position = atgate}
      :: atomic { 
            (bar[current_gate]==up && position==atgate) -> 
            if :: (current_gate==(id*4)) -> on_shared_track[id] = true
               :: else -> skip
            fi;
            position = faraway; control_link!leaves,current_gate;
            if :: (current_gate==(id*4+1)) -> on_shared_track[id] = false
               :: else -> skip
            fi
         }
   od
}

proctype controller() {

   mtype message;
   byte current_gate;

   do :: control_link?message,current_gate ->
         if :: atomic { 
                  message==approaches -> 
                  gate_link[current_gate]!raise
               }
            :: atomic { 
                  message==leaves -> 
                  gate_link[current_gate]!lower
               }
         fi
   od
}
 
proctype gate(byte id) {

   mtype message;

   do :: gate_link[id]?message ->
         if :: atomic {
                  message==lower -> 
                  bar[id] = down
               }
            :: atomic {
                  message==raise -> bar[id] = up
               }
         fi
   od
}

proctype shared_gate(byte id) {

   mtype message;

   do :: gate_link[id]?message ->
         if :: atomic {
                  message==lower -> 
                  bar[id] = down;
                  assert(shared_track_open); 
                  shared_track_open = false
               }
            :: message==raise ->
lock:          if :: atomic {
                        ((!on_shared_track[0]) && (!on_shared_track[1]) && 
                         (!shared_track_open)) -> 
                        shared_track_open = true; bar[id] = up
                     }
                  :: else -> goto lock
               fi
         fi
   od
} 

init {
   atomic {
      run controller();
      run shared_gate(0); run gate(1); run gate(2); run gate(3);
      run shared_gate(4); run gate(5); run gate(6); run gate(7);
      run train(2,0); run train(6,1);
   }
}