interface IConsole
{
    in void arm();
    in void disarm();

    out void detected();

  behaviour a
  {
    enum States {
        Disarmed,
        Armed,
        Triggered,
        Disarming
    };

    States state = States.Disarmed;

    [state.Disarmed]
    {
      on arm:
      {
        state = States.Armed;
      }
      on disarm:
        illegal;
    }

    [state.Armed]
    {
      on disarm:
      {
        state = States.Disarmed;
      }
      on optional:
      {
        detected;
        state = States.Triggered;
      }
      on arm:
        illegal;
    }

    [state.Triggered]
    {
      on disarm:
      {
        state = States.Disarmed;
      }
      on arm:
        illegal;
    }
  }
}

interface ISensor
{
  in void enable();
  in void disable();

  out void triggered();
  out void disabled();

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

    [state.Disabled]
    {
      on enable:
      {
        state = States.Enabled;
      }
      on disable:
        illegal;
    }
    [state.Enabled]
    {
      on enable:
        illegal;
      on disable:
      {
        state = States.Disabling;
      }
      on optional:
      {
        triggered;
        state = States.Triggered;
      }
    }
    [state.Disabling]
    {
      on enable, disable:
        illegal;
      on inevitable:
      {
        disabled;
        state = States.Disabled;
      }
    }
    [state.Triggered]
    {
      on enable:
        illegal;
      on disable:
      {
        state = States.Disabling;
      }
    }
  }
}

interface ISiren
{
  in void turnon();
  in void turnoff();

  behaviour c
  {
    enum States {
        Off,
        On
    };
    States state = States.Off;

    [state.Off]
    {
      on turnon:
      {
        state = States.On;
      }
      on turnoff:
        illegal;
    }
    [state.On]
    {
      on turnoff:
      {
        state = States.Off;
      }
      on turnon:
        illegal;
    }
  }
}

component AlarmBlock
{
    provides IConsole console;
    requires ISensor sensor;
    requires ISiren siren;

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

    [state.Disarmed]
    {
      on console.arm():
      {
        sensor.enable();
        state = States.Armed;
      }
      on console.disarm(), sensor.triggered(), sensor.disabled():
        illegal;
    }
    [state.Armed]
    {
      on console.arm():
        illegal;
      on console.disarm():
      blocking  	
      {
        sensor.disable();
        state = States.Disarming;
      }
      on sensor.triggered():
      {
        console.detected();
        siren.turnon();
        sounding = true;
        state = States.Triggered;
      }
      on sensor.disabled():
        illegal;
    }
    [state.Disarming]
    {
      on console.arm(), console.disarm():
        illegal;
      on sensor.triggered():
      {
        //illegal;
      }
      on sensor.disabled():
      {
        [sounding]
        {
          siren.turnoff();
          state = States.Disarmed;
	  console.reply();
          sounding = false;
        }
        [otherwise]
        {
          state = States.Disarmed;
 	  console.reply();
        }
      }
    }
    [state.Triggered]
    {
      on console.arm():
        illegal;

      on console.disarm():
      blocking
      {
        sensor.disable();
        siren.turnoff();
        sounding = false;
        state = States.Disarming;
      }
      on sensor.triggered(), sensor.disabled():
        illegal;
    }
  }
}