include "utils.lus"


(************************************************************************
	streetcar door controler
-------------------------------------------------------------------------

   V4 - SIMPLIFIED VERSION

   - behavior of the door/ramp abstracted:
     the state becomes a simple output

   - behavior of the train abstracted:
     in_station is ``level''
     end_station is an ``event''

************************************************************************)

node door_control(
-- Commands from the user:
	ramp_req,
	door_req,
-- Informations on the train state:
	in_station,
	end_station 
	: bool
	
) returns (
-- state of door/ramp
	ramp_on,
	door_on,
-- Communication with the train:
	door_and_ramp_ok
	: bool
);

var

-- train state
	running,
	start_station,

-- state of door/ramp
	ramp_off,
	door_off,
-- Commands to the door/ramp:
	open_the_ramp,
	close_the_ramp,	
	open_the_door,
	close_the_door,

	door_is_req,
	ramp_is_req,
	accept_door_req,
	accept_ramp_req,
	end_station_is_req,
	ready_to_leave,
	departure
	: bool;

let

	-- door and ramp are "perfect"
	ramp_on = switch(false, false -> pre open_the_ramp, false -> pre close_the_ramp); 
	ramp_off = not ramp_on;
	door_on = switch(false, false -> pre open_the_door, false -> pre close_the_door); 
	door_off = not door_on;
	

(* Signals related to the train *)
	departure = xedge(running);

(* States related to the train *)
	--in_station = switch( false, start_station, departure);
	start_station = edge(in_station);
	running = not in_station;

(* ready_to_leave delayed if door/ramp is opening *)
	end_station_is_req = switch (
		false,
		in_station and end_station,
		departure
	);

	ready_to_leave = switch (
		false,
		end_station_is_req
		and not open_the_door
		and not open_the_ramp,
		departure
	);

	open_the_door = switch (false,
		in_station and 
		not end_station_is_req and
		if ramp_is_req then ramp_on
		else door_is_req,
		door_on);

	open_the_ramp = switch (false,
		in_station and
		not end_station_is_req and
		ramp_is_req,
		ramp_on);

	accept_ramp_req =
		(not in_station or not end_station_is_req) and not door_is_req ;

	ramp_is_req = switch(
		false,
		ramp_req and accept_ramp_req,
		departure
	);

	accept_door_req =
		(not in_station or not end_station_is_req);

	door_is_req = switch(
		false,
		door_req and accept_door_req,
		departure
	);

	close_the_door = ready_to_leave and 
		(door_is_req or ramp_is_req);
		
	close_the_ramp = ready_to_leave and ramp_is_req and door_off;

	door_and_ramp_ok =
		ready_to_leave and door_off and ramp_off;

tel