Synchronous_reactive_systems/tests/automaton.node

23 lines
539 B
Plaintext
Raw Normal View History

node diagonal_int (i: int) returns (o1, o2 : int);
let
(o1, o2) = (i, i);
tel
node undiag_test (i: int) returns (o : bool);
var l1, l2: int; l3: int;
let
l3 = (pre (1)) -> 0;
(l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel
2022-12-13 11:45:40 +01:00
2022-12-13 15:02:54 +01:00
node auto (i: int) returns (o : int);
var x, y:int;
2022-12-13 15:02:54 +01:00
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
| Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
| Done -> do o = pre o; done
2022-12-13 15:02:54 +01:00
tel