interface IConsole
{
    in void _i();
    in void _i1();

    out void detected();
    out void deactivated();

  behaviour
  {
    enum State { Disarmed, Armed, Triggered, Disarming };
    State state = State.Disarmed;

    [state.Disarmed]
    {
      on _i:           state = State.Armed;
      on _i1:        illegal;
    }
    [state.Armed]
    {
      on _i1:        state = State.Disarming;
      on optional:    { detected; state = State.Triggered; }
      on _i:           illegal;
    }
    [state.Triggered]
    {
      on _i1:        state = State.Disarming;
      on _i:           illegal;
    }
    [state.Disarming]
    {
      on inevitable:  { deactivated; state = State.Disarmed; }
      on _i,
         _i1:        illegal;
    }
  }
}

// This is the interface to a (movement) sensor used in the Alarm system.
// The Sensor can be enabled and disabled, and the status of the Sensor after enabling
// is reported via the triggered and disabled events. 
interface ISensor
{
  in void i_1();
  in void disable();

  out void i_();
  out void disabled();

  behaviour
  {
    enum State { Disabled, Enabled, Disabling, Triggered };
    State state = State.Disabled;

    [state.Disabled]
    {
      on i_1:        state = State.Enabled;
      on disable:       illegal;
    }
    [state.Enabled]
    {
      on i_1:        illegal;
      on disable:       state = State.Disabling;
      on optional:    { i_; state = State.Triggered; }
    }
    [state.Disabling]
    {
      on i_1,
         disable:       illegal;
      on inevitable:  { disabled; state = State.Disabled; }
    }
    [state.Triggered]
    {
      on i_1:        illegal;
      on disable:       state = State.Disabling;
    }
  }
}

// This is the interface to a siren used in the Alarm system.
// The Siren can be turned on and can be turned off.
interface ISiren
{
  in void _i_();
  in void turnoff();

  behaviour
  {
    enum State { Off, On };
    State state = State.Off;

    [state.Off]
    {
      on _i_:        state = State.On;
      on turnoff:       illegal;
    }
    [state.On]
    {
      on turnoff:       state = State.Off;
      on _i_:        illegal;
    }
  }
}

// Component specification for an Alarm system which implements a Console, and
// uses a (movement) Sensor and a Siren
component Alarm_mangle
{
    provides IConsole console;
    requires ISensor sensor;
    requires ISiren siren;

  behaviour
  {
    enum State { Disarmed, Armed, Triggered, Disarming };
    State state = State.Disarmed;
    bool sounding = false;

    [state.Disarmed]
    {
      on console._i():         { sensor.i_1(); state = State.Armed; }
      on console._i1(),
         sensor.i_(),
         sensor.disabled():       illegal;
    }
    [state.Armed]
    {
      on console._i():           illegal;
      on console._i1():      { sensor.disable(); state = State.Disarming; }
      on sensor.i_():    { console.detected();
                                  siren._i_();
                                  sounding = true;
                                  state = State.Triggered;
                                }
      on sensor.disabled():       illegal;
    }
    [state.Disarming]
    {
      on console._i(),
         console._i1():        illegal;
      on sensor.i_():      illegal;
      on sensor.disabled():
          { [sounding]          { console.deactivated();
                                  sounding = false;
                                  state = State.Disarmed;
                                }
            [otherwise]         { console.deactivated();
                                  state = State.Disarmed;
                                }
          }
    }
    [state.Triggered]
    {
      on console._i():           illegal;
      on console._i1():      { sensor.disable();
                                  siren.turnoff();
                                  sounding = false;
                                  state = State.Disarming;
                                }
      on sensor.i_(),
         sensor.disabled():       illegal;
    }
  }
}