/*
make && { set -o pipefail; rm -f my.aut; { echo "eqn  I'allow_dillegals = true; C'allow_dillegals = true; I'allow_dillegals = true; init C'Implementation();"; ./pre-inst-env gdzn code -l mcrl2 -o - my.dzn; } | tee /dev/stderr | mcrl22lps -b | lps2lts /dev/stdin my.aut; cat my.aut | ltsconvert --tau=tau -edpweak-bisim my.aut my.aut; cat my.aut 1>&2; } && ltsgraph my.aut
*/

interface ihello {
  in void a ();
  in void b ();
  behaviour {
    bool open = true;
    on a: open = !open;
    [open] on b: {}
    [!open] on b: illegal;
  }
}

component hello_multiple_provides {
  provides ihello p1;
  provides ihello p2;
  behaviour {
    bool p1_open = true;
    bool p2_open = true;

    on p1.a (): p1_open = !p1_open;
    [p1_open] on p1.b (): {}
    [!p1_open] on p1.b (): illegal;

    on p2.a(): p2_open = !p2_open;
    [p2_open] on p2.b (): {}
    [!p2_open] on p2.b (): illegal;
  }
}