
-- ===============================================================================

-- ===============================================================================
MODULE main
    VAR
        System : System(speed);
    VAR
        speed : real;

    DEFINE
        sensed_speed := System.sensed_speed;
        sensed_speed_is_present := System.sensed_speed_is_present;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE System(speed)
    VAR
        sensor1 : SpeedSensor(speed);
        sensor2 : SpeedSensor(speed);
        selector : Selector(sensor1.sensed_speed, sensor1.sensed_speed_is_present, sensor2.sensed_speed, sensor2.sensed_speed_is_present, (monitor1.absence_alarm | monitor2.absence_alarm));
        monitor1 : MonitorPresence(sensor1.sensed_speed_is_present, selector.current_use = ONE);
        monitor2 : MonitorPresence(sensor2.sensed_speed_is_present, selector.current_use = TWO);
    DEFINE
        sensed_speed := selector.output;
        sensed_speed_is_present := selector.output_is_present;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE SpeedSensor(speed)
    VAR
        State : {primary, t};
        sensed_speed : real;
        sensed_speed_is_present : boolean;

    IVAR
        Transition : {primary-primary};

    FROZENVAR
        InitTransition : {_speedSensorStates_to_primary_};

    ASSIGN
        init(sensed_speed) := case
InitTransition = _speedSensorStates_to_primary_ : 0;
esac;
        init(sensed_speed_is_present) := case
InitTransition = _speedSensorStates_to_primary_ : TRUE;
esac;
        next(sensed_speed) := case
Transition = primary-primary : speed;
TRUE : sensed_speed;
esac;

        next(sensed_speed_is_present) := case
Transition = primary-primary : TRUE;
TRUE : sensed_speed_is_present;
esac;

    INIT (InitTransition = _speedSensorStates_to_primary_ -> State = primary);

    TRANS (Transition = primary-primary -> ((TRUE & State = primary) & next(State) = primary));


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Selector(input1, input1_is_present, input2, input2_is_present, switch_current_use)
    VAR
        State : {input_1, input_2, t};
        output : real;
        output_is_present : boolean;
        current_use : {ONE, TWO};

    IVAR
        Transition : {input_1-input_1, input_1-input_2, input_2-input_2, input_2-input_1};

    FROZENVAR
        InitTransition : {_selectorStates_to_input_1_};

    ASSIGN
        init(output) := case
InitTransition = _selectorStates_to_input_1_ : 0;
esac;
        init(output_is_present) := case
InitTransition = _selectorStates_to_input_1_ : TRUE;
esac;
        init(current_use) := case
InitTransition = _selectorStates_to_input_1_ : ONE;
esac;
        next(output) := case
Transition = input_1-input_1 : input1;
Transition = input_1-input_2 : input2;
Transition = input_2-input_2 : input2;
Transition = input_2-input_1 : input1;
TRUE : output;
esac;

        next(output_is_present) := case
Transition = input_1-input_1 : input1_is_present;
Transition = input_1-input_2 : input2_is_present;
Transition = input_2-input_2 : input2_is_present;
Transition = input_2-input_1 : input1_is_present;
TRUE : output_is_present;
esac;

        next(current_use) := case
Transition = input_1-input_2 : TWO;
Transition = input_2-input_1 : ONE;
TRUE : current_use;
esac;

    INIT (InitTransition = _selectorStates_to_input_1_ -> State = input_1);

    TRANS (Transition = input_1-input_1 -> ((!switch_current_use & State = input_1) & next(State) = input_1));

    TRANS (Transition = input_1-input_2 -> ((switch_current_use = TRUE & State = input_1) & next(State) = input_2));

    TRANS (Transition = input_2-input_2 -> ((!switch_current_use & State = input_2) & next(State) = input_2));

    TRANS (Transition = input_2-input_1 -> ((switch_current_use = TRUE & State = input_2) & next(State) = input_1));


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE MonitorPresence(input_is_present, enabled)
    VAR
        State : {primary, t};
        absence_alarm : boolean;

    IVAR
        Transition : {primary-primary};

    FROZENVAR
        InitTransition : {_monitorPresenceStates_to_primary_};

    ASSIGN
        init(absence_alarm) := case
InitTransition = _monitorPresenceStates_to_primary_ : FALSE;
esac;
        next(absence_alarm) := case
Transition = primary-primary : (!input_is_present & enabled = TRUE);
TRUE : absence_alarm;
esac;

    INIT (InitTransition = _monitorPresenceStates_to_primary_ -> State = primary);

    TRANS (Transition = primary-primary -> ((TRUE & State = primary) & next(State) = primary));


-- ===============================================================================
--                               End of module
-- ===============================================================================
