CristalCaveGem » LustreC » Lustrec-Tests

node tawoa_automata(input : int) returns (ok: bool);

var x1,  x2 : int;

    y1, y2:int; 

let

  automaton aut1

  state A :

  let

     x1 = input;

     y1 = x2;

  tel

  until true restart B

  state B :

  let

    x1 = 1; --    x1 = x2;

    y1 = 1;

  tel

  until true restart A

  automaton aut2

  state C :

  let

    x2 = x1;

    y2 = 2;

  tel

  until true restart D

  state D :

  let

    x2 = input;

y2 = x2;   -- y2 = x1;

  tel

  until true restart C

  ok = y1 = input || y2 = input;

tel