interface NonDet2
{
  in void stop();
  in void recover();
  out void ok();
  out void error();
  out void stopped();
  out void recovered();

  behaviour
  {
    enum States {Ready, Stopping, Error, Recovering};
    States mainState = States.Ready;

    {
      [mainState.Ready]
      {
        {
          [true]
            on stop:
            mainState = States.Stopping;
          [true]
            on stop:
            mainState = States.Error;
        }

        on recover:
        illegal;
      }

      [mainState.Stopping]
      {
        on inevitable:
        {
          {ok; mainState = States.Ready;}
        }

        // on stop:
        // illegal;

        on stop, recover:
        illegal;
      }

      [mainState.Recovering]
      {
        on inevitable:
        {
          {ok; mainState = States.Ready;}
        }

        // on stop:
        // illegal;

        on stop, recover:
        illegal;
      }

      [mainState.Error]
      {
        on inevitable: error;
        on recover:
        {
          [true]{mainState = States.Recovering;}
          [true]{}
        }

        on stop: ok;
      }
    }
  }
}