interface NonDetHiddenTransition
{
  in void c();
  out void na();
  out void ns();

  behaviour
  {
    enum State {A, B};
    State s = State.A;
    bool b = false;

    [s.A]
    {
      on c: illegal;
      on inevitable: {b = true; s = State.B;}
      on inevitable: {b = false; s = State.B;}
    }
    [s.B]
    {
      on c: {[b] {ns;} [otherwise] illegal;}
      on inevitable: {[b] na; [!b] {}}
    }
  }
}