-- train-gate-controller

var
	x,      -- distance 
	y,      -- angle of gate
	t	-- dcontrollers timer
	: analog;

 -- -------------------------------------------------------------- *)
	-- furthest distance of train from intersection

	-- distance from the intersection at which an  
			--      approaching train is detected by sensor

	-- distance from the intersection at which an  
			--      exiting train is detected by sensor

automaton train
synclabs : app, 	-- (send) approach signal for train
	   exit;	-- (send) signal that train is leaving

initially far & x>=1000;

loc far: while x>=1000  wait {dx in [-50,-40]} 
	when x=1000 sync app goto near;
	
loc near: while x>=0   wait {dx in [-50,-30]}
	when x=0 goto past;

loc past: while x<=100 wait {dx in [ 30, 50]}
	when x=100 do {x' = 1000} sync exit goto far;

end -- train

automaton controller
synclabs: app, 
	  exit, 
	  lower, 	-- lower command sent to the gate
	  raise;        -- raise command sent to the gate
initially idle & True;

loc idle: while True wait {dt = 0}	-- wait for a signal from train
	when True sync app do {t' = 0} goto about_to_lower;
	when True sync exit do {t' = 0} goto about_to_raise;

loc about_to_lower: while 0<=t & t<=5 wait {dt = 1}
	when True sync app goto about_to_lower;
	when True sync exit do {t' = 0} goto about_to_lower;
	-- send lower signal any time before t<=alpha;
	when True sync lower goto idle;

loc about_to_raise: while 0<=t & t<=5 wait {dt in [1,1]}
	when True sync app do {t' = 0} goto about_to_lower;
	when True sync exit  goto about_to_raise;
	-- send raise signal any time before t<=alpha
	when True sync raise  goto idle;

end -- controller

automaton gate
synclabs: raise, lower;
initially open & y=90;

loc up: while y<=90 wait {dy in [9,9]}	-- gate is being raised
	-- gate is fully raised
	when y=90 goto open;
	-- selfloops for receptiveness
	when True sync raise goto up;
	when True sync lower goto down ;

loc open: while True wait {dy in [0,0]}	-- wait for command
	when True sync raise goto open;
	when True sync lower goto down;

	
loc down: while y>=0 wait {dy in [-9,-9]} -- gate is being lowered
	-- gate is fully down
	when y=0 goto closed;
	when True sync lower goto down;
	when True sync raise goto up;

loc closed: while True wait {dy in [0,0]} -- wait for command
	when True sync raise goto up;	
	when True sync lower goto closed;

end -- gate


-- analysis commands

var init_reg, final_reg, reached: region;

init_reg := loc[train]=far & x>=2000 & 
	    loc[controller]=idle &
	    loc[gate]=open & y=90;
final_reg := loc[gate] = up & x<=10 | loc[gate]=open & x<=10 | loc[gate] = down & x<=10;

reached := reach forward from init_reg endreach;

if empty(reached&final_reg)
	then prints "Train-gate controller maintains safety requirement";
	else prints "Train-gate controller violates safety requirement";
endif;