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

node auto (i: int) returns (o : int);
var x, y:int;
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
tel