2022-12-07 21:56:38 +01:00
|
|
|
node diagonal_int (i: int) returns (o1, o2 : int);
|
2022-12-07 16:45:55 +01:00
|
|
|
let
|
2022-12-07 21:56:38 +01:00
|
|
|
(o1, o2) = (i, i);
|
|
|
|
|
tel
|
|
|
|
|
|
|
|
|
|
node undiag_test (i: int) returns (o : bool);
|
|
|
|
|
var l1, l2: int; l3: int;
|
|
|
|
|
let
|
2022-12-13 14:25:48 +01:00
|
|
|
l3 = (pre (1)) -> 0;
|
2022-12-07 21:56:38 +01:00
|
|
|
(l1, l2) = diagonal_int(i);
|
|
|
|
|
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
2022-12-07 16:45:55 +01:00
|
|
|
tel
|
2022-12-13 11:45:40 +01:00
|
|
|
|
2022-12-13 15:02:54 +01:00
|
|
|
node auto (i: int) returns (o : int);
|
|
|
|
|
let
|
|
|
|
|
automaton
|
|
|
|
|
| Incr -> do o = (pre o) + 1; done
|
|
|
|
|
| Decr -> do o = (pre o) - 1; done
|
|
|
|
|
tel
|
|
|
|
|
|
