icd.aadl

package icd


public

with base_types;
with data_model;

data pedal_value
end pedal_value;

data implementation pedal_value.impl
subcomponents
	val : data base_types::integer;
end pedal_value.impl;


data error
end error;

data implementation error.impl
subcomponents
	disagreement : data base_types::boolean;
end error.impl;


data speed extends base_types::integer
end speed;

data deceleration extends base_types::integer
end deceleration;

data implementation deceleration.impl
end deceleration.impl;


data command_msg
end command_msg;

data pressure_value extends base_types::integer
end pressure_value;

data braking_value extends base_types::integer
end braking_value;

data implementation command_msg.impl
subcomponents
	braking_value 	: data braking_value;
	braking_mode 	: data braking_mode;
end command_msg.impl;


data braking_mode
properties
	data_model::data_representation => enum;
	data_model::enumerators => ("off", "low", "medium", "high");
end braking_mode;


-------------------------------------------------
--  Hydraulic control message
-------------------------------------------------
data hydraulic_ctrl_msg
end hydraulic_ctrl_msg;

data implementation hydraulic_ctrl_msg.impl
subcomponents
	normal_selector_valve : data base_types::integer;
	normal_servo_valve    : data braking_value;
	alternate_servo_valve : data braking_value;
end hydraulic_ctrl_msg.impl;

-------------------------------------------------
--  implementation of the panel data
-------------------------------------------------

data panel_interface
end panel_interface;


data implementation panel_interface.buttons
subcomponents
	low_pushed  : data base_types::boolean;
	med_pushed  : data base_types::boolean;
	high_pushed : data base_types::boolean;
end panel_interface.buttons;

data implementation panel_interface.light
subcomponents
	low_light  : data base_types::boolean;
	med_light  : data base_types::boolean;
	high_light : data base_types::boolean;
end panel_interface.light;


data implementation panel_interface.radio_button
properties
	data_model::data_representation => enum;
	data_model::enumerators => ("off", "low", "medium", "high");
end panel_interface.radio_button;



data sync_msg
end sync_msg;


data implementation sync_msg.impl
subcomponents
	is_master : data base_types::boolean;
end sync_msg.impl;

end icd;

sandbox.aadl

package sandbox
public
	
with icd;
with spgs;
	
thread com 
features
	compute_valve 	: provides subprogram access spgs::compute_brake_value;
	pedals 			: in data port icd::pedal_value.impl;
	speed  			: in data port icd::speed;
	decel 	 		: in data port icd::deceleration.impl;
	cmd    			: out data port icd::command_msg.impl;
properties 
	period => 20ms;
annex EMV2 {**
	use types errorlibrary;
	use behavior wbs::errorlib::simple;
	
	error propagations
		pedals 	: in propagation {valueerror};
		speed 	: in propagation {valueerror};
		decel 	: in propagation {valueerror};
		cmd 	: out propagation {valueerror};
	end propagations;
**};
end com;

thread com_sampling extends com
features
	compute_mode 		: provides subprogram access spgs::compute_autobrake_buttons.impl;
	panel_buttons  		: in data port icd::panel_interface.buttons;
end com_sampling;

thread com_event extends com
features
	compute_mode 		: provides subprogram access spgs::compute_autobrake_buttons.impl;
	panel_buttons  		: in event data port icd::panel_interface.buttons;
end com_event;


thread com_radio extends com
features
	panel_button  		: in data port icd::panel_interface.radio_button;
end com_radio;

----------------------------------------------
--  Thread implementation
----------------------------------------------

thread implementation com.generic
subcomponents
	braking_mode 	: data icd::braking_mode; 
	braking_value 	: data icd::braking_value;
	newcmd       	: data icd::command_msg.impl;
end com.generic;

thread implementation com_sampling.impl extends com.generic
annex behavior_specification {**
    states
		init 			: initial complete state;
		idle 			: complete state;
		change_state 	: state;
		compute_cmd  	: state; 
	transitions
		t0 : init -[on dispatch]-> idle; 
		t1 : idle -[on dispatch]-> change_state
				{spgs::compute_autobrake_buttons.impl!(panel_buttons,braking_mode);
				 newcmd.braking_mode := braking_mode
				};
		t2 : change_state -[]-> compute_cmd 
				{spgs::compute_brake_value! (pedals,speed,decel,braking_mode,braking_value); 
				 newcmd.braking_value := braking_value
				};
		t3 : compute_cmd -[]-> idle 
				{cmd := newcmd};
**};
end com_sampling.impl;


thread implementation com_event.impl extends com.generic
annex behavior_specification {**
    states
		init 			: initial complete state;
		idle 			: complete state;
		change_state 	: state;
		compute_cmd  	: state;  
	transitions
		t0 : init -[on dispatch]-> idle;
		t1 : idle -[on dispatch]-> change_state
				{spgs::compute_autobrake_mode.push_buttons!(panel_buttons,braking_mode);
				 newcmd.braking_mode := braking_mode
				};
		t2 : change_state -[]-> compute_cmd 
				{spgs::compute_brake_value! (pedals,speed,decel,braking_mode,braking_value); 
				 newcmd.braking_value := braking_value
				}; 
		t3 : compute_cmd -[]-> idle 
				{cmd := newcmd};
**};
end com_event.impl;


thread implementation com_radio.impl extends com.generic
annex behavior_specification {**
    states
		init 			: initial complete state;
		idle 			: complete state;
		change_state 	: state;
		compute_cmd  	: state;
	transitions
		t0 : init -[on dispatch]-> idle;
		t1 : idle -[on dispatch]-> change_state
			{
				if (panel_buttons = "off")
				 {
				 	   braking_mode := "off"
				 }
				 end if;
				 if (panel_buttons = "low")
				 {
				 	   braking_mode := "low"
				 }
				 end if;
				 if (panel_buttons = "medium")
				 {
				 	   braking_mode := "medium"
				 }
				 end if;
				 if (panel_buttons = "high")
				 {
				 	   braking_mode := "high"
				 }
				 end if;
				 newcmd.braking_mode := braking_mode
			};
		t2 : change_state -[]-> compute_cmd 
				{spgs::compute_brake_value! (pedals,speed,decel,braking_mode,braking_value); 
				 newcmd.braking_value := braking_value
				};
		t3 : compute_cmd -[]-> idle 
				{cmd := newcmd};
**};
end com_radio.impl;

end sandbox;

subprograms.aadl

package spgs

public

with icd;
with base_types;

subprogram compute_autobrake	
end compute_autobrake;

subprogram compute_autobrake_buttons extends compute_autobrake
features
	panel_buttons : in parameter icd::panel_interface.buttons;
	braking_mode  : requires data access icd::braking_mode;
end compute_autobrake_buttons;

subprogram compute_autobrake_radio extends compute_autobrake
features
	panel_button  : in parameter icd::panel_interface.radio_button;
	braking_mode  : requires data access icd::braking_mode;
end compute_autobrake_radio;




subprogram implementation compute_autobrake_buttons.impl
annex behavior_specification {**
    states
		manual : initial final state;
		low    : state;
		med    : state;
		hig    : state;
	transitions
		manual_to_low : manual 	-[ panel_buttons.low_pushed  ]-> low     	{braking_mode := "low"};
		low_to_manual : low 	-[ panel_buttons.low_pushed  ]-> manual    	{braking_mode := "manual"};
		manual_to_med : manual 	-[ panel_buttons.med_pushed  ]-> med    	{braking_mode := "medium"}; 
		med_to_manual : low 	-[ panel_buttons.med_pushed  ]-> manual     {braking_mode := "manual"};		
		manual_to_hig : manual 	-[ panel_buttons.high_pushed ]-> hig     	{braking_mode := "high"};
		hig_to_manual : hig 	-[ panel_buttons.high_pushed ]-> manual     {braking_mode := "manual"};
**};
end compute_autobrake_buttons.impl;


--
--  These subprograms are here to compute the different values
--  for braking at different autobraking modes.
--

subprogram compute_brake_value
features
	pedals 			: in parameter icd::pedal_value.impl;
	speed  			: in parameter icd::speed;
	decel  			: in parameter icd::deceleration.impl;
	braking_mode 	: in parameter icd::braking_mode;
	outv  			: out parameter icd::braking_value;
annex behavior_specification {**
    states
		init       : initial state;
		compute    : state;
		done    	: final state;
	transitions
		t0 : init -[ ]-> compute;
		t1 : compute -[ braking_mode = "low"]-> done {compute_brake_value_low!(pedals,speed,decel,outv)};
		t2 : compute -[ braking_mode = "medium"]-> done {compute_brake_value_low!(pedals,speed,decel,outv)};
		t3 : compute -[ braking_mode = "high"]-> done {compute_brake_value_low!(pedals,speed,decel,outv)};
**};
end compute_brake_value;

subprogram compute_brake_value_low
features
	pedals : in parameter icd::pedal_value.impl;
	speed  : in parameter icd::speed;
	decel  : in parameter icd::deceleration.impl;
	outv  : out parameter icd::braking_value;
end compute_brake_value_low;

subprogram compute_brake_value_medium
features
	pedals : in parameter icd::pedal_value.impl;
	speed  : in parameter icd::speed;
	decel  : in parameter icd::deceleration.impl;
	outv  : out parameter icd::braking_value;
end compute_brake_value_medium;

subprogram compute_brake_value_high
features
	pedals : in parameter icd::pedal_value.impl;
	speed  : in parameter icd::speed;
	decel  : in parameter icd::deceleration.impl;
	outv    : out parameter icd::braking_value;
end compute_brake_value_high;




--
--  The check_value subprogram check two results and output
--  a potential disagreement error. The disagreement
--  would then be sent to the CFDIU and potentially
--  reported as an ECAM message.
--

subprogram check_value
features
	value1  : in parameter icd::command_msg.impl;
	value2  : in parameter icd::command_msg.impl;
	error   : out parameter base_types::boolean;
end check_value;

subprogram implementation check_value.impl
annex behavior_specification {**
    states
		start 	: initial state;
		done	: final state;
	transitions
	    --
	    --  We log an error only if the braking value
	    --  are different.
	    --
	    
		t0 : start -[]-> done
		{
			if (value1.braking_mode = value2.braking_mode)
			{
				error := false
			}
			else
			{
				error := true
			}
			end if
		};
**};
end check_value.impl;

--
--  Synchronize with the other channels.
--

subprogram sync_channels
features
	sync_from_other 	: in parameter icd::sync_msg.impl;
	sync_to_other 		: out parameter icd::sync_msg.impl;
	error   			: out parameter icd::error.impl;
end sync_channels;

subprogram implementation sync_channels.impl
subcomponents
	disagreement_counter : data base_types::integer;
end sync_channels.impl;


end spgs;