interface NonDet3
{
  in void init();
  in void work();
  in void stop();
  in void recover();
  out void ok();
  out void error();
  out void stopped();
  out void recovered();

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

    // on stop:
    // {
    //   [!mainState.Powered]
    //     mainState = States.Stopping;
    //   [otherwise]
    //     illegal;
    // }

    {
    [mainState.Powered]
    {
      on init:
      {
        [true] {ok; mainState = States.Ready;}
        [true] {error; mainState = States.Error;}
      }

      on work, recover:
        illegal;

      on stop:
        illegal;
    }

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

      on init, recover:
        illegal;
    }

    [mainState.Working]
    {
      on inevitable:
      {
        [true]{ok; mainState = States.Ready;}
        [true]{error; mainState = States.Error;}
      }

      // on inevitable:
      // {
      //   {error; mainState = States.Error;}
      // }
        
      on stop:
        mainState = States.Stopping;

      // on stop:
      //   mainState = States.Error;

      on init, work, recover:
        illegal;
    }

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

      on stop:
        mainState = States.Stopping;

      on init, work, recover:
        illegal;
    }

    [mainState.Error]
    {
      on recover:
      {
        [true]{ok; mainState = States.Ready;}
        [true]{error; mainState = States.Error;}
      }

      on stop:
        ok;

      on init, work:
        illegal;
    }
    }
  }
}