
@requires discrete-time
COMPONENT System system
INTERFACE
INPUT speed : real ;
OUTPUT sensed_speed : real ;
OUTPUT sensed_speed_is_present : boolean ;
CONTRACT sense
assume : ( ( speed = 0 ) & G ( ( ( ( ( next ( speed ) - speed ) ) <= 1 ) & ( ( ( next ( speed ) - speed ) ) >= -1 ) ) ) ) ;
guarantee :  always ( ( ( ( ( ( sensed_speed - speed ) <= 4 ) ) & ( ( ( sensed_speed - speed ) >= -4 ) ) ) & sensed_speed_is_present ) ) ;
REFINEMENT
SUB sensor1 : SpeedSensor ;
SUB sensor2 : SpeedSensor ;
SUB selector : Selector ;
SUB monitor1 : MonitorPresence ;
SUB monitor2 : MonitorPresence ;
CONNECTION sensor1.speed := speed ;
CONNECTION sensor2.speed := speed ;
CONNECTION selector.input1 := sensor1.sensed_speed ;
CONNECTION selector.input2 := sensor2.sensed_speed ;
CONNECTION selector.input1_is_present := sensor1.sensed_speed_is_present ;
CONNECTION selector.input2_is_present := sensor2.sensed_speed_is_present ;
CONNECTION monitor1.input_is_present := sensor1.sensed_speed_is_present ;
CONNECTION monitor2.input_is_present := sensor2.sensed_speed_is_present ;
CONNECTION sensed_speed := selector.output ;
CONNECTION sensed_speed_is_present := selector.output_is_present ;
CONNECTION selector.switch_current_use := ( monitor1.absence_alarm | monitor2.absence_alarm ) ;
CONNECTION monitor1.enabled := ( ( selector.current_use = ONE ) ) ;
CONNECTION monitor2.enabled := ( ( selector.current_use = TWO ) ) ;
CONTRACT sense REFINEDBY monitor1.monitor , monitor2.monitor , selector.select , selector.switch , sensor1.sense , sensor2.sense ;
COMPONENT SpeedSensor
INTERFACE
INPUT speed : real ;
OUTPUT sensed_speed : real ;
OUTPUT sensed_speed_is_present : boolean ;
CONTRACT sense
assume : ( ( speed = 0 ) & G ( ( ( ( ( next ( speed ) - speed ) ) <= 1 ) & ( ( ( next ( speed ) - speed ) ) >= -1 ) ) ) ) ;
guarantee :  always ( ( ( ( ( ( sensed_speed - speed ) <= 1 ) ) & ( ( ( sensed_speed - speed ) >= -1 ) ) ) & sensed_speed_is_present ) ) ;
COMPONENT Selector
INTERFACE
INPUT input1 : real ;
INPUT input1_is_present : boolean ;
INPUT input2 : real ;
INPUT input2_is_present : boolean ;
INPUT switch_current_use : boolean ;
OUTPUT output : real ;
OUTPUT output_is_present : boolean ;
OUTPUT current_use : { ONE , TWO } ;
CONTRACT select
assume : TRUE ;
guarantee : ( ( ( ( output = 0 ) & ( output_is_present = TRUE ) ) ) &  always ( ( ( ( next ( ( current_use = ONE ) ) implies ( ( ( next ( output ) = input1 ) & ( next ( output_is_present ) = input1_is_present ) ) ) ) ) & ( ( next ( ( current_use = TWO ) ) implies ( ( ( next ( output ) = input2 ) & ( next ( output_is_present ) = input2_is_present ) ) ) ) ) ) ) ) ;
CONTRACT switch
assume : TRUE ;
guarantee :  always ( ( ( ( ( ( ( ( current_use = ONE ) & switch_current_use ) ) implies ( next ( current_use ) = TWO ) ) ) & ( ( ( ( ( current_use = TWO ) & switch_current_use ) ) implies ( next ( current_use ) = ONE ) ) ) ) & ( ( ( !switch_current_use ) implies !change ( current_use ) ) ) ) ) ;
COMPONENT MonitorPresence
INTERFACE
INPUT input_is_present : boolean ;
INPUT enabled : boolean ;
OUTPUT absence_alarm : boolean ;
CONTRACT monitor
assume : ( ( input_is_present = TRUE ) ) ;
guarantee :  always ( ( absence_alarm iff ( enabled & ! ( input_is_present ) ) ) ) ;