node abro(a, b, r: bool) returns(o: bool)
var
  ha, hb: bool;
let
  automaton initial state G let
    automaton
      initial state N ha = false; until if a resume M;
      state M ha = true;
    returns ha;

    automaton
      initial state N hb = false; until if b resume M;
      state M hb = true;
    returns hb;

  tel until if r restart G;
  returns ha, hb;
  o = ha and hb and (false -> not pre(ha and hb));
tel

node test(i: int) returns(a, b, c: int; exit: bool)
var xa, xb, xr: bool;
let
  xa = (i mod 3 = 2);
  xb = (i mod 5 = 3);
  xr = (i mod 9 = 4);
  a = if xa then 1 else 0;
  b = if xb then 1 else 0;
  c = (if abro(xa, xb, xr) then 1 else 0) + (if xr then 2 else 0);
  exit = (i >= 128);
tel