const bound: int = 7;

node updown() returns(probe x, probe y, probe z: int)
var last_x, last_y: int;
let
    last_x = 0 -> pre x;
    automaton
        initial state UP
        let x = last_x + 1; tel
        until if x >= bound resume DOWN;

        state DOWN
        let x = last_x - 1; tel
        until if x <= -bound resume UP;

    returns x;
    guarantee x_bounded: x >= -bound and x <= bound;

    last_y = 0 -> pre y;
    automaton
        initial state DOWN
        let y = last_y - 1; tel
        until if y <= -bound resume UP;

        state UP
        let y = last_y + 1; tel
        until if y >= bound resume DOWN;

    returns y;
    guarantee y_bounded: y >= -bound and y <= bound;

    z = x + y;
    guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
tel

node test(i: int) returns(a, b, c: int; exit: bool)
let
    exit = i >= 30;
    a, b, c = updown2();
tel