package System {
	private import Hierarchy::*;
	private import Contracts::*;
	private import ScalarValues::*;
	private import LogicFunctions::*;
	private import LTLSpec::*;
	private import LTLFunctions::*;

	enum def Enum_1 {
		enum ONE;
		enum TWO;
	}

	part def System {
		in attribute speed : Real;
		out attribute sensed_speed : Real;
		out attribute sensed_speed_is_present : Boolean;

		attribute sense : Contract {
			assert constraint :>> assumption {
				 ( speed == 0 ) and G ( { ( ( ( next ( {speed } ) - speed ) <= 1 ) and ( ( next ( {speed } ) - speed ) >= -1 ) ) } ) 
			}
			assert constraint :>> guarantee {
				 always ( { ( ( ( ( sensed_speed - speed ) <= 4 ) and ( ( sensed_speed - speed ) >= -4 ) ) and sensed_speed_is_present ) } ) 
			}
			:>> refinedBy = (monitor1.monitor, monitor2.monitor, selector.select, selector.switch, sensor1.sense, sensor2.sense);
		}
		part sensor1 : SpeedSensor;
		part sensor2 : SpeedSensor;
		part selector : Selector;
		part monitor1 : MonitorPresence;
		part monitor2 : MonitorPresence;
		bind speed = sensor1.speed;
		bind speed = sensor2.speed;
		connect sensor1.sensed_speed to selector.input1;
		connect sensor2.sensed_speed to selector.input2;
		connect sensor1.sensed_speed_is_present to selector.input1_is_present;
		connect sensor2.sensed_speed_is_present to selector.input2_is_present;
		connect sensor1.sensed_speed_is_present to monitor1.input_is_present;
		connect sensor2.sensed_speed_is_present to monitor2.input_is_present;
		bind selector.output = sensed_speed;
		bind selector.output_is_present = sensed_speed_is_present;
		:>> selector.switch_current_use =  ( monitor1.absence_alarm or monitor2.absence_alarm ) ;
		:>> monitor1.enabled =  (  ( selector.current_use == Enum_1::ONE )  ) ;
		:>> monitor2.enabled =  (  ( selector.current_use == Enum_1::TWO )  ) ;
	}

	part def SpeedSensor {
		in attribute speed : Real;
		out attribute sensed_speed : Real;
		out attribute sensed_speed_is_present : Boolean;

		attribute sense : Contract {
			assert constraint :>> assumption {
				 ( speed == 0 ) and G ( { ( ( ( next ( {speed } ) - speed ) <= 1 ) and ( ( next ( {speed } ) - speed ) >= -1 ) ) } ) 
			}
			assert constraint :>> guarantee {
				 always ( { ( ( ( ( sensed_speed - speed ) <= 1 ) and ( ( sensed_speed - speed ) >= -1 ) ) and sensed_speed_is_present ) } ) 
			}
		}
	}

	part def Selector {
		in attribute input1 : Real;
		in attribute input1_is_present : Boolean;
		in attribute input2 : Real;
		in attribute input2_is_present : Boolean;
		in attribute switch_current_use : Boolean;
		out attribute output : Real;
		out attribute output_is_present : Boolean;
		out attribute current_use : Enum_1;

		attribute select : Contract {
			assert constraint :>> assumption {
				true
			}
			assert constraint :>> guarantee {
				 ( ( output == 0 ) and ( output_is_present == true ) ) and always ( { ( ( next ( {current_use == Enum_1::ONE } ) implies ( ( next ( {output } ) == input1 ) and ( next ( {output_is_present } ) == input1_is_present ) ) ) and ( next ( {current_use == Enum_1::TWO } ) implies ( ( next ( {output } ) == input2 ) and ( next ( {output_is_present } ) == input2_is_present ) ) ) ) } ) 
			}
		}
		attribute switch : Contract {
			assert constraint :>> assumption {
				true
			}
			assert constraint :>> guarantee {
				 always ( { ( ( ( ( ( current_use == Enum_1::ONE ) and switch_current_use ) implies ( next ( {current_use } ) == Enum_1::TWO ) ) and ( ( ( current_use == Enum_1::TWO ) and switch_current_use ) implies ( next ( {current_use } ) == Enum_1::ONE ) ) ) and ( ( not switch_current_use ) implies not change ( {current_use } ) ) ) } ) 
			}
		}
	}

	part def MonitorPresence {
		in attribute input_is_present : Boolean;
		in attribute enabled : Boolean;
		out attribute absence_alarm : Boolean;

		attribute monitor : Contract {
			assert constraint :>> assumption {
				input_is_present == true
			}
			assert constraint :>> guarantee {
				 always ( { ( iff ( {absence_alarm}, { ( enabled and not ( input_is_present ) ) } ) ) } ) 
			}
		}
	}

	part system : System, SystemComponent {
	}
}