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

-- ===============================================================================
MODULE main
    VAR
        FoldableDrill : FoldableDrill(command);
    VAR
        command : {OPEN, CLOSE};


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

-- ===============================================================================
MODULE FoldableDrill(command)
    VAR
        drill : Drill(controller.drill_operation);
        cavity : DrillCavity(controller.door_operation);
        controller : Controller(command, drill.sensed_value, cavity.sensed_value);

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

-- ===============================================================================
MODULE Drill(operation)
    VAR
        hinge : DrillFoldHinge(drill_motor.torque);
        drill_motor : ElectricMotor(operation);
        drill_angle_sensor : AngleSensor(hinge.percentage);
    DEFINE
        sensed_value := drill_angle_sensor.sensed_value;


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

-- ===============================================================================
MODULE DrillFoldHinge(torque)
    VAR
        State : {primary, t};
        percentage : integer;

    IVAR
        Transition : {idle, increment, decrement};

    FROZENVAR
        InitTransition : {_DrillFoldHingeStates_to_primary_};

    ASSIGN
        init(percentage) := case
InitTransition = _DrillFoldHingeStates_to_primary_ : 100;
esac;
        next(percentage) := case
Transition = idle : percentage;
Transition = increment :  (100 < percentage + 10 ? 100 : percentage + 10) ;
Transition = decrement :  (0 < percentage - 10 ? percentage - 10 : 0) ;
TRUE : percentage;
esac;

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

    TRANS (Transition = idle -> ((torque = 0 & State = primary) & next(State) = primary));

    TRANS (Transition = increment -> ((torque > 0 & State = primary) & next(State) = primary));

    TRANS (Transition = decrement -> ((torque < 0 & State = primary) & next(State) = primary));


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

-- ===============================================================================
MODULE ElectricMotor(operation)
    VAR
        State : {idle, opening, closing, t};
        torque : integer;

    IVAR
        Transition : {idle-opening, opening-idle, idle-closing, closing-idle, closing-opening, opening-closing, opening-opening, closing-closing, idle-idle};

    FROZENVAR
        InitTransition : {_ElectricMotorStates_to_idle_};

    ASSIGN
        init(torque) := case
InitTransition = _ElectricMotorStates_to_idle_ : 0;
esac;
        next(torque) := case
Transition = idle-opening : 10;
Transition = opening-idle : 0;
Transition = idle-closing : -10;
Transition = closing-idle : 0;
Transition = closing-opening : 10;
Transition = opening-closing : -10;
Transition = opening-opening : 10;
Transition = closing-closing : -10;
Transition = idle-idle : 0;
TRUE : torque;
esac;

    INIT (InitTransition = _ElectricMotorStates_to_idle_ -> State = idle);

    TRANS (Transition = idle-opening -> ((operation = OPEN & State = idle) & next(State) = opening));

    TRANS (Transition = opening-idle -> ((operation = IDLE & State = opening) & next(State) = idle));

    TRANS (Transition = idle-closing -> ((operation = CLOSE & State = idle) & next(State) = closing));

    TRANS (Transition = closing-idle -> ((operation = IDLE & State = closing) & next(State) = idle));

    TRANS (Transition = closing-opening -> ((operation = OPEN & State = closing) & next(State) = opening));

    TRANS (Transition = opening-closing -> ((operation = CLOSE & State = opening) & next(State) = closing));

    TRANS (Transition = opening-opening -> ((operation = OPEN & State = opening) & next(State) = opening));

    TRANS (Transition = closing-closing -> ((operation = CLOSE & State = closing) & next(State) = closing));

    TRANS (Transition = idle-idle -> ((operation = IDLE & State = idle) & next(State) = idle));


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

-- ===============================================================================
MODULE AngleSensor(value)
    VAR
        State : {primary, t};
        sensed_value : integer;

    IVAR
        Transition : {primary-primary};

    FROZENVAR
        InitTransition : {_AngleSensorStates_to_primary_};

    ASSIGN
        init(sensed_value) := case
InitTransition = _AngleSensorStates_to_primary_ : value;
esac;
        next(sensed_value) := case
Transition = primary-primary : value;
TRUE : sensed_value;
esac;

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

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


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

-- ===============================================================================
MODULE DrillCavity(operation)
    VAR
        door : DrillCavityDoor(door_motor.torque);
        door_motor : ElectricMotor(operation);
        door_angle_sensor : AngleSensor(door.percentage);
    DEFINE
        sensed_value := door_angle_sensor.sensed_value;


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

-- ===============================================================================
MODULE DrillCavityDoor(torque)
    VAR
        State : {primary, t};
        percentage : integer;

    IVAR
        Transition : {increment, decrement, idle};

    FROZENVAR
        InitTransition : {_DrillCavityDoorStates_to_primary_};

    ASSIGN
        init(percentage) := case
InitTransition = _DrillCavityDoorStates_to_primary_ : 0;
esac;
        next(percentage) := case
Transition = increment :  (100 < percentage + 10 ? 100 : percentage + 10) ;
Transition = decrement :  (0 < percentage - 10 ? percentage - 10 : 0) ;
Transition = idle : percentage;
TRUE : percentage;
esac;

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

    TRANS (Transition = increment -> ((torque > 0 & State = primary) & next(State) = primary));

    TRANS (Transition = decrement -> ((torque < 0 & State = primary) & next(State) = primary));

    TRANS (Transition = idle -> ((torque = 0 & State = primary) & next(State) = primary));


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

-- ===============================================================================
MODULE Controller(command, drill_sensed_value, door_sensed_value)
    VAR
        State : {drill_open, door_opening_when_open, drill_closing, door_closing_when_open, drill_closed, door_opening_when_closed, drill_opening, door_closing_when_closed, t};
        drill_operation : {OPEN, CLOSE, IDLE};
        door_operation : {OPEN, CLOSE, IDLE};

    IVAR
        Transition : {drill_open_self, drill_open-door_opening_when_open, door_opening_when_open-self, door_opening_when_open-drill_closing, drill_closing-self, drill_closing-door_closing_when_open, door_closing_when_open-self1, door_closing_when_open-self2, door_closing_when_open-drill_closed, drill_closed-self, drill_closed-door_opening_when_closed, door_opening_when_closed_self, door_opening_when_closed-drill_opening, drill_opening_self, drill_opening-door_closing_when_closed, door_closing_when_closed-self1, door_closing_when_closed-self2, door_closing_when_closed-drill_open, door_opening_when_open-door_closing_when_closed, drill_closing-door_closing_when_closed, door_closing_when_open-door_opening_when_closed, door_opening_when_closed-door_closing_when_open, drill_opening-door_closing_when_open, door_closing_when_closed-door_opening_when_open};

    FROZENVAR
        InitTransition : {_ControllerStates_to_drill_closed_};

    ASSIGN
        init(drill_operation) := case
InitTransition = _ControllerStates_to_drill_closed_ : IDLE;
esac;
        init(door_operation) := case
InitTransition = _ControllerStates_to_drill_closed_ : IDLE;
esac;
        next(drill_operation) := case
Transition = drill_open_self : IDLE;
Transition = drill_open-door_opening_when_open : IDLE;
Transition = door_opening_when_open-self : IDLE;
Transition = door_opening_when_open-drill_closing : CLOSE;
Transition = drill_closing-self : CLOSE;
Transition = drill_closing-door_closing_when_open : CLOSE;
Transition = door_closing_when_open-self1 : CLOSE;
Transition = door_closing_when_open-self2 : IDLE;
Transition = door_closing_when_open-drill_closed : IDLE;
Transition = drill_closed-self : IDLE;
Transition = drill_closed-door_opening_when_closed : IDLE;
Transition = door_opening_when_closed_self : IDLE;
Transition = door_opening_when_closed-drill_opening : OPEN;
Transition = drill_opening_self : OPEN;
Transition = drill_opening-door_closing_when_closed : OPEN;
Transition = door_closing_when_closed-self1 : OPEN;
Transition = door_closing_when_closed-self2 : IDLE;
Transition = door_closing_when_closed-drill_open : IDLE;
Transition = door_opening_when_open-door_closing_when_closed : IDLE;
Transition = drill_closing-door_closing_when_closed : OPEN;
Transition = door_closing_when_open-door_opening_when_closed : IDLE;
Transition = door_opening_when_closed-door_closing_when_open : IDLE;
Transition = drill_opening-door_closing_when_open : CLOSE;
Transition = door_closing_when_closed-door_opening_when_open : IDLE;
TRUE : drill_operation;
esac;

        next(door_operation) := case
Transition = drill_open_self : IDLE;
Transition = drill_open-door_opening_when_open : OPEN;
Transition = door_opening_when_open-self : OPEN;
Transition = door_opening_when_open-drill_closing : OPEN;
Transition = drill_closing-self : IDLE;
Transition = drill_closing-door_closing_when_open : CLOSE;
Transition = door_closing_when_open-self1 : CLOSE;
Transition = door_closing_when_open-self2 : CLOSE;
Transition = door_closing_when_open-drill_closed : IDLE;
Transition = drill_closed-self : IDLE;
Transition = drill_closed-door_opening_when_closed : OPEN;
Transition = door_opening_when_closed_self : OPEN;
Transition = door_opening_when_closed-drill_opening : OPEN;
Transition = drill_opening_self : IDLE;
Transition = drill_opening-door_closing_when_closed : CLOSE;
Transition = door_closing_when_closed-self1 : CLOSE;
Transition = door_closing_when_closed-self2 : CLOSE;
Transition = door_closing_when_closed-drill_open : IDLE;
Transition = door_opening_when_open-door_closing_when_closed : IDLE;
Transition = drill_closing-door_closing_when_closed : IDLE;
Transition = door_closing_when_open-door_opening_when_closed : OPEN;
Transition = door_opening_when_closed-door_closing_when_open : CLOSE;
Transition = drill_opening-door_closing_when_open : CLOSE;
Transition = door_closing_when_closed-door_opening_when_open : IDLE;
TRUE : door_operation;
esac;

    INIT (InitTransition = _ControllerStates_to_drill_closed_ -> State = drill_closed);

    TRANS (Transition = drill_open_self -> ((command = OPEN & State = drill_open) & next(State) = drill_open));

    TRANS (Transition = drill_open-door_opening_when_open -> ((command = CLOSE & State = drill_open) & next(State) = door_opening_when_open));

    TRANS (Transition = door_opening_when_open-self -> (((command = CLOSE & door_sensed_value < 40) & State = door_opening_when_open) & next(State) = door_opening_when_open));

    TRANS (Transition = door_opening_when_open-drill_closing -> (((command = CLOSE & door_sensed_value >= 40) & State = door_opening_when_open) & next(State) = drill_closing));

    TRANS (Transition = drill_closing-self -> (((command = CLOSE & drill_sensed_value > 40) & State = drill_closing) & next(State) = drill_closing));

    TRANS (Transition = drill_closing-door_closing_when_open -> (((command = CLOSE & drill_sensed_value <= 40) & State = drill_closing) & next(State) = door_closing_when_open));

    TRANS (Transition = door_closing_when_open-self1 -> ((((command = CLOSE & door_sensed_value > 0) & drill_sensed_value > 0) & State = door_closing_when_open) & next(State) = door_closing_when_open));

    TRANS (Transition = door_closing_when_open-self2 -> ((((command = CLOSE & door_sensed_value > 0) & drill_sensed_value = 0) & State = door_closing_when_open) & next(State) = door_closing_when_open));

    TRANS (Transition = door_closing_when_open-drill_closed -> (((command = CLOSE & door_sensed_value = 0) & State = door_closing_when_open) & next(State) = drill_closed));

    TRANS (Transition = drill_closed-self -> ((command = CLOSE & State = drill_closed) & next(State) = drill_closed));

    TRANS (Transition = drill_closed-door_opening_when_closed -> ((command = OPEN & State = drill_closed) & next(State) = door_opening_when_closed));

    TRANS (Transition = door_opening_when_closed_self -> (((command = OPEN & door_sensed_value < 40) & State = door_opening_when_closed) & next(State) = door_opening_when_closed));

    TRANS (Transition = door_opening_when_closed-drill_opening -> (((command = OPEN & door_sensed_value >= 40) & State = door_opening_when_closed) & next(State) = drill_opening));

    TRANS (Transition = drill_opening_self -> (((command = OPEN & drill_sensed_value < 40) & State = drill_opening) & next(State) = drill_opening));

    TRANS (Transition = drill_opening-door_closing_when_closed -> (((command = OPEN & drill_sensed_value >= 40) & State = drill_opening) & next(State) = door_closing_when_closed));

    TRANS (Transition = door_closing_when_closed-self1 -> ((((command = OPEN & door_sensed_value > 0) & drill_sensed_value < 100) & State = door_closing_when_closed) & next(State) = door_closing_when_closed));

    TRANS (Transition = door_closing_when_closed-self2 -> ((((command = OPEN & door_sensed_value > 0) & drill_sensed_value = 100) & State = door_closing_when_closed) & next(State) = door_closing_when_closed));

    TRANS (Transition = door_closing_when_closed-drill_open -> (((command = CLOSE & door_sensed_value = 0) & State = door_closing_when_closed) & next(State) = drill_open));

    TRANS (Transition = door_opening_when_open-door_closing_when_closed -> ((command = OPEN & State = door_opening_when_open) & next(State) = door_closing_when_closed));

    TRANS (Transition = drill_closing-door_closing_when_closed -> ((command = OPEN & State = drill_closing) & next(State) = door_closing_when_closed));

    TRANS (Transition = door_closing_when_open-door_opening_when_closed -> ((command = OPEN & State = door_closing_when_open) & next(State) = door_opening_when_closed));

    TRANS (Transition = door_opening_when_closed-door_closing_when_open -> ((command = CLOSE & State = door_opening_when_closed) & next(State) = door_closing_when_open));

    TRANS (Transition = drill_opening-door_closing_when_open -> ((command = CLOSE & State = drill_opening) & next(State) = door_closing_when_open));

    TRANS (Transition = door_closing_when_closed-door_opening_when_open -> ((command = CLOSE & State = door_closing_when_closed) & next(State) = door_opening_when_open));


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