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

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

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

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

    // Illegal paths (satisfy completeness):
    on arm: 
      [!state.Disarmed] illegal;
    on disarm: 
      [!state.Armed] 
      [!state.Triggered] illegal;
  }
}