
module main {
    const n : int = 10;
    type stack_t = [int] int;

    var s : stack_t;
    var top_index : int;

    init {
        top_index := -1;
    }

    define is_empty(top_index : int) : boolean {
        return top_index == -1;
    }

    define is_full(top_index : int) : boolean {
        return top_index == n-1;
    }

    define top_val(s : stack_t, top_index : int) : (int) {
        if (is_empty(top_index)) {
            return 0;
        } else {
            return s[top_index];
        }
    }

    procedure push(new_elem : int) {
        if (!is_full(top_index)) {
            top_index := top_index + 1;
            s[top_index] := new_elem;
        }
    }

    procedure pop() {
        if (!is_empty(top_index)) {
            top_index := top_index - 1;
        }
    }

    next {
        if (*) {
            var new_elem : int;
            new_elem = choose v : int :: v >= 0;
            call push(new_elem);
        } else if (*) {
            call pop();
        } else {
            skip;
        }
    }

    invariant "top_index_within_bounds" {
        top_index >= -1 && top_index < n
    }

    control {
        liveness "can_push_if_not_full" {
            !is_full(top_index) => eventually (!is_full(top_index) && top_index' > top_index)
        }
    }
}