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

chan control_link = [0] of {mtype, pid};
chan gate_link_2 = [0] of {mtype};
chan gate_link_3 = [0] of {mtype};
chan gate_link_4 = [0] of {mtype};
chan gate_link_5 = [0] of {mtype};
chan gate_link_6 = [0] of {mtype};
chan gate_link_7 = [0] of {mtype};
chan gate_link_8 = [0] of {mtype};
chan gate_link_9 = [0] of {mtype};

mtype bar[12] = down;
bool on_shared_track[12] = false;
bool shared_track_open = false

proctype train(pid current_gate) {

   mtype position = atgate;

   control_link!approaches,current_gate;
   do :: atomic { 
            position==faraway ->
            if :: current_gate==2-> current_gate = 3
               :: current_gate==3-> current_gate = 4
               :: current_gate==4-> current_gate = 5
               :: current_gate==5 -> current_gate = 2; assert(_pid==10)
               :: current_gate==6 -> current_gate = 7
               :: current_gate==7 -> current_gate = 8
               :: current_gate==8 -> current_gate = 9
               :: current_gate==9 -> current_gate = 6; assert(_pid==11)
            fi;
            control_link!approaches,current_gate; position = atgate
         }
      :: atomic { 
            (bar[current_gate]==up && position==atgate) -> 
            if :: ((_pid==10 && current_gate==2)||
                   (_pid==11 && current_gate==6)) -> 
                  on_shared_track[_pid] = true
               :: else -> skip
            fi;
            position = faraway; control_link!leaves,current_gate;
            if :: ((_pid==10 && current_gate==3)||
                   (_pid==11 && current_gate==7)) -> 
                  on_shared_track[_pid] = false
               :: else -> skip
            fi
         }
   od
}

inline send(id,msg) {
   if
      :: id==2 -> gate_link_2!msg
      :: id==3 -> gate_link_3!msg
      :: id==4 -> gate_link_4!msg
      :: id==5 -> gate_link_5!msg
      :: id==6 -> gate_link_6!msg
      :: id==7 -> gate_link_7!msg
      :: id==8 -> gate_link_8!msg
      :: id==9 -> gate_link_9!msg
   fi
}

proctype controller() {

   mtype message;
   pid current_gate;

   do :: control_link?message,current_gate ->
         if :: atomic {
                  message==approaches -> 
                  send(current_gate,raise)
               }
            :: atomic {
                  message==leaves -> 
                  send(current_gate,lower)
               }
         fi
   od
}
 
proctype gate(chan link) {

   mtype message;

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

proctype shared_gate(chan link) {

   mtype message;

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

init {
   atomic {
      run controller(); run shared_gate(gate_link_2); 
      run gate(gate_link_3); run gate(gate_link_4); 
      run gate(gate_link_5); run shared_gate(gate_link_6); 
      run gate(gate_link_7); run gate(gate_link_8); 
      run gate(gate_link_9); run train(4); run train(8);
   }
}