//purpose: The garage door example with a series of illustrative errors
/* ******************************************************************************************* */
/* This example models the behaviour of the automatic "up and over" garage door I have at home.*/
/* See the associated specification document that describes the observed behaviour of the door.*/
/* Note that this model has been built to simply show how certain basic features of Dezyne     */
/* work and how they might be used. If this were a real system I would have implemented        */
/* certain things differently, e.g. the timer on the switch press. Note that I'm also sure that*/
/* the purists will argue that the whole thing could have been done differently. But my        */
/* purpose here is to illustrate how a simple minded ex-programmer like me might go about      */
/* solving this problem. Note that for illustrative purposes I have left a simple error in the */
/* models.                                                                                     */
/*                                                                                             */
/* Robert Howe                                                                                 */
/* ******************************************************************************************* */

// The Limit Switch detects when the door has reached either the open or the closed end of the
// track. This component only knows when the door is at the open position or the closed position
// anywhere other position is 'unknown'

interface LimitSwitchIF
{
       enum Position { Opened, Closed, Unknown };
       in void doorOpening();
       in void doorClosing();
       in void doorStopped();
       out void doorOpened();
       out void doorClosed();
       out void proximityWarning();
       in Position queryPosition();
       in void initialise();

       behaviour
       {
             enum DoorState { Uninitialized, Opening, Closing, Idle };
             DoorState door = DoorState.Uninitialized;
             Position state = Position.Unknown;

             // I have assumed that we might want to initialise the limit switch component, i.e. the door state
             // in particular.

             [door.Uninitialized]
             {
                    on initialise:
                          [door.Uninitialized]door = DoorState.Idle;
                    on doorOpening, doorClosing, doorStopped, queryPosition: illegal;
             }
             [!door.Uninitialized]
             {
                    on initialise: illegal;

                    // Return the position of the door
                    on queryPosition: reply ( state );
             }

             [door.Idle]
             {
                    on doorOpening:     door = DoorState.Opening;
                    on doorClosing: door = DoorState.Closing;
                    on doorStopped: illegal;
             }

             // If the door is in the Closed position and then told to open
             // the track will firstly report that the door position is unknown as the
             // door transits from one end of the track to the other. Then it will
             // report that it has reached the Opened position. But equally the door might
             // start in an unknown position or stop in an unknown position.

             [door.Opening]
             {
                    // An internal event leads to the door being in the Opened state

                    on inevitable: { doorOpened; state = Position.Opened; door = DoorState.Idle; }

                    // An internal event leads to the door being in the Unknown state

                    [state.Closed] on inevitable: { state = Position.Unknown; }

                    on doorClosing, doorOpening: illegal;
                    on doorStopped: door = DoorState.Idle;
             }

             // Same thing applies here, but then for the Opened to Closed transition. Additionally
             // if the door hits something while closing it will report a proximity problem

             [door.Closing]
             {
                    on inevitable: { doorClosed; state = Position.Closed; door = DoorState.Idle; }
                    [state.Opened] on inevitable: { state = Position.Unknown; }
                    on optional: { proximityWarning; }
                    on doorOpening, doorClosing: illegal;
                    on doorStopped: door = DoorState.Idle;
             }

       }
}

// The motor control is pretty dumb. With the motor off, we can select either the open or close direction
// Then we can turn it on. If the motor is working too hard - for instance if the counter balance spring
// on the door has weakened, then the motor will report a "power warning". If the motor hits a hard stop,
// for instance if a limit switch fails, then it will immediately shutoff and send a drive fault message

interface MotorControlIF
{
	in void initialise();
	in void start();
	in void stop();
	in void setOpen();
	in void setClose();
	out void driveFault();
	out void powerWarning();

	behaviour
	{
		enum State { NotReady, Ready };
		enum OnOff { MotorOn, MotorOff };
		enum Direction { DoorOpen, DoorClose };

		OnOff motor = OnOff.MotorOff;
		Direction dir = Direction.DoorOpen;
		State state = State.NotReady;

		[state.Ready]
		{
			[motor.MotorOff]
			{
				on start: motor = OnOff.MotorOn;
				on setOpen: dir = Direction.DoorOpen;
				on setClose: dir = Direction.DoorClose;
				on stop: illegal;
			}
			[motor.MotorOn]
			{
				on stop: motor = OnOff.MotorOff;
				on start, setOpen, setClose: illegal;
				on optional: { driveFault; motor = OnOff.MotorOff; }
				on optional: powerWarning;
			}
			on initialise: illegal;
		}
		[state.NotReady]
		{
			on initialise:
			{
				state = State.Ready;
				motor = OnOff.MotorOff;
			}
			on start, stop, setOpen, setClose: illegal;
		}
	}
}

// In this case I have only modelled a single 'press button' wall switch controller
// for opening and closing the door. My door also has a remote control, which essentially
// behaves the same way as the wall switch. When the door is closed, pressing the wall
// switch once starts it opening. When it is open, pressing the wall switch starts it
// closing. When in transition another press of the switch will reverse its direction.
// But also when in transition two quick presses of the switch will stop the door.

interface SwitchPressIF
{
	out void switchPressed();
	in void acknowledge();

	behaviour
	{
		enum State { Ready, NotReady };
		State state = State.Ready;

		[state.Ready]
		{
			on inevitable: { switchPressed; state = State.NotReady; }
			on acknowledge: illegal;
		}
		[state.NotReady]
		{
			on acknowledge: state = State.Ready;
		}
	}
}

// Interface to an one shot timer
// The Timer can be started via CreateTimer, CreateTimerEx, or via CreateTimerMSec
// The Timer is stopped via CancelTimer
// The Timer reports expiration via Timeout

interface ITimer
{
  extern double $double$;
  extern long $long$;
  in void CreateTimer(double t);
  in void CreateTimerEx(long tsec, long tnsec);
  in void CreateTimerMSec(long tmsec);
  in void CancelTimer();
  out void Timeout();

  behaviour
  {
    enum States {Inactive, Active};
    States state = States.Inactive;

    on CancelTimer: state = States.Inactive;

    [state.Inactive]
    {
      on CreateTimer, CreateTimerEx, CreateTimerMSec:
        state = States.Active;
    }
    [state.Active]
    {
      on inevitable:
      {
        Timeout;
        state = States.Inactive;
      }
      on CreateTimer, CreateTimerEx, CreateTimerMSec:
        illegal;
    }
  }
}

// This is the interface to the door control component. My idea is that when the system
// powers up it is the not-ready state. The main() code will firstly initialise the controller.
// After that it will only display warnings or errors (by LEDs on the outside of the box?) and
// respond to someone pressing the reset button.

interface DoorControlIF
{
	in void initialise();
	in void reset();
	out void warning();
	out void error();

	behaviour
	{
		enum State { NotReady, Ready, Error };
		State state = State.NotReady;

		[state.NotReady]
		{
			on initialise: state = State.Ready;
			on reset: illegal;
		}
		[state.Ready]
		{
			on initialise: illegal;
			on reset: illegal;
			on inevitable: warning;
			on inevitable: { error; state = State.Error; }
		}
		[state.Error]
		{
			on reset: state = State.Ready;
			on initialise: illegal;
		}
	}
}

// This component implements all the control for the door controller. I have deliberately put
// all of the control in a single component just for illustrative purposes.

component GarageDoorControlErr
{
	provides DoorControlIF doorControl;
	requires SwitchPressIF switchPress;
	requires MotorControlIF motorControl;
	requires LimitSwitchIF limitSw;
	requires ITimer timer;

	behaviour
	{
		enum State { NotReady, Ready, Opening, Closing, Error };
		State state = State.NotReady;
		bool secondSwitchPress = false;
		LimitSwitchIF.Position position = LimitSwitchIF.Position.Unknown;

		// This function deals with the consequences of two quick presses of the wall switch
		// when the door is opening or closing. It creates a timer with (say) a short trigger
		// period, e.g. 500msec and then stops the door. If a second press comes before the
		// timer expires, the door will stay stopped. If the timer expires, the door direction
		// will be reversed (later in the model).

		void switchPressCheck()
		{
			if ( ! secondSwitchPress )
			{
				timer.CreateTimerMSec( $500$ );
				motorControl.stop();
				limitSw.doorStopped();
				secondSwitchPress = true;
			}
			else
			{
				timer.CancelTimer();
				state = State.Ready;
				secondSwitchPress = false;
			}
		}

		// In the not ready state, initialise the various components that need it. If the wall switch is pressed
		// during initialisation, just ignore it.

		[state.NotReady]
		{
			on doorControl.initialise(): { limitSw.initialise(); motorControl.initialise(); state = State.Ready; }
			on switchPress.switchPressed(): { switchPress.acknowledge(); }
		}

		// In the ready state wait for the wall switch to be pressed. Figure out where the door
		// is and then transit the door accordingly. Nothing else should happen.

		[state.Ready]
		{
			on switchPress.switchPressed():
			{
				switchPress.acknowledge();
				secondSwitchPress = false;

				position = limitSw.queryPosition();

				// If the door is opened, close it

				if ( position == LimitSwitchIF.Position.Opened )
				{
					motorControl.setClose();
					motorControl.start();
					limitSw.doorClosing();
					state = State.Closing;
				}

				// If it's closed or the position is unknown, open it.

				else if ( position == LimitSwitchIF.Position.Closed ||
					      position == LimitSwitchIF.Position.Unknown )
				{
					motorControl.setOpen();
					motorControl.start();
					limitSw.doorOpening();
					state = State.Opening;
				}
			}
		}

		// When the door is opening, if the wall switch is pressed once, reverse it. It if it is pressed
		// twice quickly, then stop it. When opening the proximity warning and door closed events are illegal.

		[state.Opening]
		{
			on switchPress.switchPressed():
			{
				switchPressCheck();
			}
			on timer.Timeout():
			{
				secondSwitchPress = false;
				motorControl.setOpen();
				motorControl.start();
				limitSw.doorClosing();
				state = State.Closing;
			}
			on limitSw.doorOpened():
			{
				motorControl.stop();
				state = State.Ready;
				timer.CancelTimer();
			}
		}

		// When the door is closing, if the wall switch is pressed once, reverse it. It if it is pressed
		// twice quickly, then stop it. When closing door opened events are illegal.

		[state.Closing]
		{
			on switchPress.switchPressed():
			{
				switchPressCheck();
			}
			on timer.Timeout():
			{
				secondSwitchPress = false;
				motorControl.setOpen();
				motorControl.start();
				limitSw.doorOpening();
				state = State.Opening;
			}
			on limitSw.doorClosed():
			{
				motorControl.stop();
				state = State.Ready;
			}

			// If the door collides with something, stop & reverse it.

			on limitSw.proximityWarning():
			{
				motorControl.stop();
				limitSw.doorStopped();
				motorControl.setOpen();
				motorControl.start();
				limitSw.doorOpening();
				state = State.Opening;
			}
		}

		// If there's an error, the only thing that can happen is a reset.

		[state.Error]
		{
			on doorControl.reset(): state = State.Ready;
			on limitSw.doorClosed(), limitSw.doorOpened(), limitSw.proximityWarning(): {}
			on switchPress.switchPressed(): { switchPress.acknowledge(); }
		}

		on motorControl.powerWarning(): doorControl.warning();
		on motorControl.driveFault():
		{
			motorControl.stop();
			limitSw.doorStopped();
			timer.CancelTimer();
			doorControl.error();
			state = State.Error;
		}
	}
}