%% DATA TYPES
% Trains
% We have 2 main trains and two spare trains.
sort Train = struct t1 | t2 | sp1 | sp2;
% We have several sections;
sort Section = struct
finishA | finishB | waitA | waitB |
mergeWait | unload | forkSafety |
safetySpotA | safetyPass | safetySpotB |
mergeSafety | load | forkStart |
startA | startB |
raceA1 | raceB1 | raceA2 | raceB2 | raceA3 | raceB3 | raceA4 | raceB4 | raceA5 | raceB5;

sort SectionList = List(Section);
map finishSections : SectionList;
	waitSections : SectionList;
	mustMoveSections : SectionList;

eqn finishSections = [finishA, finishB];
	waitSections = [waitA, waitB];
	mustMoveSections = [raceA1, raceA2, raceA3, raceA4, raceA5,
						raceB1, raceB2, raceB3, raceB4, raceB5,
						finishA, finishB,
						forkSafety, forkStart,
						mergeWait, mergeSafety,
						safetyPass
						];


% position of a switch.
sort Position = struct A | center | B;
% Moving indicator.
sort Movement = struct Moving | Stationary;
% Up down position
sort BinaryPosition = struct Up | Down;
% Occupancy
sort Occupancy = struct Occupied | Free;
% Section occupancy map
sort SectionOccupancy = Section -> Occupancy;
% Train section map
sort TrainSection = Train -> Section;
% Train movement map
sort TrainMovement = Train -> Movement;
% Switch position map
sort SwitchPosition = Section -> Position;

%% ACTIONS
act
	% Switch actions
	% Request switch to move
	switch_move : Section # Position;
	% Switch indicating the switch is moving or stationary
	switch_moving : Section # Movement;
	% Switch indicating the current position of the switch
	switch_pos : Section # Position;

	% Train actions
	% train step, i.e. the train is moving and stepping to the next section
	train_step : Train;
	% train moving indicator, i.e. the train sents to the controller it is moving or stationary
	train_moving: Train # Movement;
	% train stop, i.e. the train receives a stop signal from the controller
	train_stop : Train;
	% train move, i.e. the train receives a move signal from the controller
	train_move : Train;
	% train indicating wheter it is empty or not
	train_empty : Train # Occupancy;

	% Flag actions
	flag_move : Section # BinaryPosition; % Request flag to move
	flag_pos : Section # BinaryPosition; % Flag indicating the current position of the flag

	% bar actions
	bars_move : Train # BinaryPosition; % Request bars to move
	bars_pos : Train # BinaryPosition; % Bars indicating the current position of the bars

	% Section actions
	% Section indicating it is occupied or free
	occupied : Section # Occupancy;

	% The control panel buttons
	loaded;
	emergency;
	add_train : Bool;

	% Maintenance calls
	maintenance_train : Train;
	maintenence_defect_train : Train;
	maintenance_defect_switch : Section;
	maintenance_object_on_section : Section;

	%% Communicating actions
	load : Train; load_in : Train; load_out : Train;
	load_done; load_done_in; load_done_out;
	unload : Train; unload_in : Train; unload_out : Train;
	unload_done; unload_done_in; unload_done_out;
	emergency_propagation; emergency_propagation_in; emergency_propagation_out;
	safety_maintenance : Train; safety_maintenance_in : Train; safety_maintenance_out : Train;
	verify_train_move : Train; verify_train_move_in : Train; verify_train_move_out : Train;
	verify_switch_move : Section; verify_switch_move_in : Section; verify_switch_move_out : Section;
	verify_section_occupancy : TrainSection; verify_section_occupancy_in : TrainSection; verify_section_occupancy_out : TrainSection;
	spare_trains : Bool; spare_trains_in : Bool; spare_trains_out : Bool;


map safetySection : Position -> Section;
var p : Position;
eqn (p == A) -> safetySection(p) = safetySpotA;
	(p == B) -> safetySection(p) = safetySpotB;
	(p == center) -> safetySection(p) = safetyPass;

map startSection : Position -> Section;
var p : Position;
eqn (p == A) -> startSection(p) = startA;
	(p == B) -> startSection(p) = startB;

map occupiedSection : TrainSection # Section -> Bool;
var ts : TrainSection;
	s : Section;
eqn occupiedSection(ts, s) =  ts(t1) == s || ts(t2) == s || ts(sp1) == s || ts(sp2) == s;

% Returns whether the next two sections of the given train is not occupied
map clearHeadWay2 : TrainSection # SwitchPosition # Train -> Bool;
var ts : TrainSection;
	sp : SwitchPosition;
	t : Train;
eqn clearHeadWay2(ts, sp, t) = !(exists u : Train . (u != t) && (
			(ts(u) in [
				nextSection(ts(t), sp),
				nextSection(nextSection(ts(t), sp), sp)
			])
	));

% Given a section and the positions of both switches, give the next section.
% Argument 2 is the position of the safety fork
% Argument 3 is the position of the start fork
map nextSection: Section # SwitchPosition -> Section;
var s : Section;
	sp : SwitchPosition;
	q : Nat;
eqn (startA == s) -> nextSection(s, sp) = raceA1;
	(raceA1 == s) -> nextSection(s, sp) = raceA2;
	(raceA2 == s) -> nextSection(s, sp) = raceA3;
	(raceA3 == s) -> nextSection(s, sp) = raceA4;
	(raceA4 == s) -> nextSection(s, sp) = raceA5;
	(raceA5 == s) -> nextSection(s, sp) = finishA;

	(startB == s) -> nextSection(s, sp) = raceB1;
	(raceB1 == s) -> nextSection(s, sp) = raceB2;
	(raceB2 == s) -> nextSection(s, sp) = raceB3;
	(raceB3 == s) -> nextSection(s, sp) = raceB4;
	(raceB4 == s) -> nextSection(s, sp) = raceB5;
	(raceB5 == s) -> nextSection(s, sp) = finishB;

	(finishA == s) -> nextSection(s, sp) = waitA;
	(finishB == s) -> nextSection(s, sp) = waitB;
	(waitA == s) -> nextSection(s, sp) = mergeWait;
	(waitB == s) -> nextSection(s, sp) = mergeWait;
	(mergeWait == s) -> nextSection(s, sp) = unload;
	(unload == s) -> nextSection(s, sp) = forkSafety;

	(forkSafety == s) -> nextSection(s, sp) = safetySection(sp(forkSafety));

	(safetySpotA == s) -> nextSection(s, sp) = mergeSafety;
	(safetyPass == s) -> nextSection(s, sp) = mergeSafety;
	(safetySpotB == s) -> nextSection(s, sp) = mergeSafety;
	(mergeSafety == s) -> nextSection(s, sp) = load;
	(load == s) -> nextSection(s, sp) = forkStart;

	(forkStart == s) -> nextSection(s, sp) = startSection(sp(forkStart));


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Parallel controller components
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
proc movement_manager_proc(ts : TrainSection, tm : TrainMovement, sp : SwitchPosition, raiseFlag : Bool, spare_enabled : Bool, emergency_enabled : Bool) =
	emergency_enabled -> (
		emergency_propagation_in . movement_manager_proc(ts, tm, sp, raiseFlag, spare_enabled, true)
	) <> (
		% Request the movement of switches (TODO: not always)
		emergency_propagation_in . train_stop(t1) . train_stop(t2) . train_stop(sp1) . train_stop(sp2) . movement_manager_proc(ts, tm, sp, raiseFlag, spare_enabled, false)
		+ !occupiedSection(ts, forkStart) ->
		(
			(occupiedSection(ts, startA) && sp(forkStart) == A) -> switch_move(forkStart, B) . verify_switch_move_out(forkStart) . movement_manager_proc(ts, tm, sp, raiseFlag, spare_enabled, false)
 			+ (!occupiedSection(ts, startA) && sp(forkStart) == B) -> switch_move(forkStart, A) . verify_switch_move_out(forkStart) . movement_manager_proc(ts, tm, sp, raiseFlag, spare_enabled, false)
		)
		+ verify_section_occupancy_out(ts) . movement_manager_proc(ts, tm, sp, raiseFlag, spare_enabled, false)
		% Update switch position map when the switches indicate a new position
		+ sum p : Position . switch_pos(forkSafety, p) . movement_manager_proc(ts, tm, sp[forkSafety -> p], raiseFlag, spare_enabled, false)
		+ sum p : Position . (p != center) -> switch_pos(forkStart, p) . movement_manager_proc(ts, tm, sp[forkStart -> p], raiseFlag, spare_enabled, false)
		% Train is moving, raise flag if the next section is a finish section and the raiseFlag boolean is true
		+ sum t : Train . (tm(t) == Moving) -> train_step(t). (
			(nextSection(ts(t), sp) in finishSections) ->
			(
				raiseFlag -> flag_move(nextSection(ts(t), sp), Up) . movement_manager_proc(ts[t->nextSection(ts(t), sp)], tm, sp, false, spare_enabled, false)
				<>
				movement_manager_proc(ts[t->nextSection(ts(t), sp)], tm, sp, true, spare_enabled, false)
			)
			<>
			((nextSection(ts(t), sp) in waitSections) ->
				flag_move(finishA, Down) . flag_move(finishB, Down) . movement_manager_proc(ts[t->nextSection(ts(t), sp)], tm, sp, raiseFlag, spare_enabled, false)
				<>
				movement_manager_proc(ts[t->nextSection(ts(t), sp)], tm, sp, raiseFlag, spare_enabled,false)
			)
		)
		+ sum u, v : Train . (ts(u) == waitA && ts(v) == waitB && clearHeadWay2(ts, sp, u)) -> train_move(u).verify_train_move_out(u).movement_manager_proc(ts, tm[u->Moving], sp, raiseFlag, spare_enabled, false)

		+ sum u : Train . (ts(u) == waitB && !occupiedSection(ts, waitA) && clearHeadWay2(ts, sp, u)) -> train_move(u).verify_train_move_out(u).movement_manager_proc(ts, tm[u->Moving], sp, raiseFlag, spare_enabled, false)

		+ sum u : Train . (ts(u) == unload && clearHeadWay2(ts, sp, u)) -> unload_out(u).unload_done_in.switch_moving(forkSafety, Stationary).train_move(u).verify_train_move_out(u).movement_manager_proc(ts, tm[u->Moving], sp, raiseFlag, spare_enabled, false)

		+ sum u : Train . (ts(u) == load && clearHeadWay2(ts, sp, u)) -> load_out(u).load_done_in.switch_moving(forkStart, Stationary).train_move(u).verify_train_move_out(u).movement_manager_proc(ts, tm[u->Moving], sp, raiseFlag, spare_enabled, false)

		+ sum u, v : Train . (ts(u) == startA && ts(v) == startB && clearHeadWay2(ts, sp, u) && clearHeadWay2(ts, sp, v)) -> train_move(u).train_move(v).verify_train_move_out(u).verify_train_move_out(v).movement_manager_proc(ts, tm[u->Moving][v->Moving], sp, raiseFlag, spare_enabled, false)

		+ sum u : Train . (spare_enabled && (ts(u) == safetySpotA || ts(u) == safetySpotB) && clearHeadWay2(ts, sp, u)) -> train_move(u).verify_train_move_out(u).movement_manager_proc(ts, tm[u->Moving], sp, raiseFlag, spare_enabled, false)
		% TODO explain
		+ sum t : Train . (clearHeadWay2(ts, sp, t) && ts(t) in mustMoveSections)->
		(
			train_move(t).verify_train_move_out(t).movement_manager_proc(ts, tm[t->Moving], sp, raiseFlag, spare_enabled, false)
		)
		<>
		(
			train_stop(t).movement_manager_proc(ts, tm[t->Stationary], sp, raiseFlag, spare_enabled, false)
		)
		+ sum b : Bool . spare_trains_in(b) . movement_manager_proc(ts, tm, sp, raiseFlag, b, emergency_enabled)
	);

proc maintenance_manager_proc =
	sum t : Train . safety_maintenance_in(t) . maintenance_train(t) . maintenance_manager_proc
	% Verify the train is actually moving
	+ sum t : Train . verify_train_move_in(t) . (train_moving(t, Moving) + (train_moving(t, Stationary) . maintenence_defect_train(t) . emergency_propagation_out)) . maintenance_manager_proc
	% Verify the switch is actually moving
	+ verify_switch_move_in(forkSafety) . (switch_moving(forkSafety, Moving) + (switch_moving(forkSafety, Stationary) . maintenance_defect_switch(forkSafety) )) . maintenance_manager_proc
	+ verify_switch_move_in(forkStart) . (switch_moving(forkStart, Moving) + (switch_moving(forkStart, Stationary) . maintenance_defect_switch(forkStart) )) . maintenance_manager_proc
	% Verify no object is on the track (that is not a train)
	+ sum ts : TrainSection . verify_section_occupancy_in(ts) . ( sum s : Section . occupied(s, Occupied) . (
			(ts(t1) != s && ts(t2) != s && ts(sp1) != s && ts(sp2) != s) ->  maintenance_object_on_section(s) . emergency_propagation_out
	  ) ) . maintenance_manager_proc;

proc operator_manager_proc(emergency_enabled : Bool, add_train_position : Bool) =
	emergency_enabled -> (
		emergency_propagation_out . operator_manager_proc(true, add_train_position)
	) <> (
		% Train load request
		sum t : Train . load_in(t) . bars_move(t, Up) . bars_pos(t, Up) . loaded . bars_move(t, Down) . bars_pos(t, Down) . load_done_out . operator_manager_proc(false, add_train_position)
		% Train unload request
		+ sum t : Train . unload_in(t) . bars_move(t, Up) . bars_pos(t, Up) . train_empty(t, Free) . bars_move(t, Down) . bars_pos(t, Down) . unload_done_out . operator_manager_proc(false, add_train_position)
		% Ignore button presses when no load in progress
		+ loaded . operator_manager_proc(false, add_train_position)
		+ emergency . emergency_propagation_out . operator_manager_proc(true, add_train_position)
		+ sum b : Bool . add_train(b) . (b != add_train_position) -> ( spare_trains_out(b) . operator_manager_proc(false, b) )
	);

glob dummySection : Section;
	 dummyPosition : Position;

%init switch_proc(mergeWait, center) || switch_proc(forkSafety, center);
init hide({
		train_stop, emergency, switch_move, switch_pos,
		flag_move
	},
	allow({
		train_move, train_moving, train_step, train_stop, train_empty,
		switch_move, switch_moving, switch_pos,
		flag_move, flag_pos,
		bars_move, bars_pos,
		loaded, add_train, emergency,
		occupied, load, load_done, unload, unload_done,
		safety_maintenance, verify_train_move,
		verify_switch_move, verify_section_occupancy,
		maintenance_train, maintenance_defect_train, maintenance_defect_switch, maintenance_object_on_section,
		emergency_propagation
		},
	comm({
		load_in | load_out -> load,
		unload_in | unload_out -> unload,
		load_done_in | load_done_out -> load_done,
		unload_done_in | unload_done_out -> unload_done,
		safety_maintenance_in | safety_maintenance_out -> safety_maintenance,
		verify_train_move_in | verify_train_move_out -> verify_train_move,
		verify_switch_move_in | verify_switch_move_out -> verify_switch_move,
		verify_section_occupancy_in | verify_section_occupancy_out -> verify_section_occupancy,
		emergency_propagation_in | emergency_propagation_out -> emergency_propagation
		},
		movement_manager_proc(
		(lambda t : Train . dummySection)
			[t1  -> startA]
			[t2  -> startB]
			[sp1 -> safetySpotA]
			[sp2 -> safetySpotB],
		(lambda t : Train . Moving),
		(lambda s : Section . dummyPosition)
			[forkSafety -> center]
			[forkStart  -> A],
		true, false, false)
		|| operator_manager_proc(false, false)
	)));