// Dezyne --- Dezyne command line tools
//
// Copyright © 2022 Jan (janneke) Nieuwenhuizen <janneke@gnu.org>
//
// This file is part of Dezyne.
//
// Dezyne is free software: you can redistribute it and/or modify it
// under the terms of the GNU Affero General Public License as
// published by the Free Software Foundation, either version 3 of the
// License, or (at your option) any later version.
//
// Dezyne is distributed in the hope that it will be useful, but
// WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
// Affero General Public License for more details.
//
// You should have received a copy of the GNU Affero General Public
// License along with Dezyne.  If not, see <http://www.gnu.org/licenses/>.
//
// Commentary:
//  * v2.15 is OK
//  * state1 and state2 must be enums with overlapping
//    field names
//  * state2 can be of same enum type status too
//  * the unreachable enum value must overlap ("BUSY"),
//    using "NEVER" yields OK
//
// Code:

interface ihello
{
  in void hello ();
  out void world ();

  behaviour
  {
    bool idle = true;
    [idle] on hello: idle = false;
    [!idle] on inevitable: {world; idle = true;}
  }
}

component bug_nondet
{
  provides ihello h;
  requires ihello w;

  behaviour {
    enum status {IDLE, BUSY};
    enum status2 {ALWAYS, NEVER, BUSY};
    status state1 = status.IDLE;
    //status state2 = status.IDLE; // also non-deterministic
    status2 state2 = status2.ALWAYS;

    [state1.IDLE] on h.hello(): {w.hello(); state1 = status.BUSY;}
    [state1.BUSY] on w.world(): {h.world(); state1 = status.IDLE;}

    // [state2.NEVER] on w.world(): {} // OK
    [state2.BUSY] on w.world(): {}     // non-deterministic
  }
}