module main
{
    const n : int; // capacity of the main

    type main_t : record {
        top : int; // index of the top element in the main
        elements : array [0, n-1] of int; // array to store elements of the main
    };

    var s : main_t; // main variable

    procedure push(v: int)
        requires s.top < n; // main is not full
        modifies s;
    {
        s.elements[s.top] := v;
        s.top := s.top + 1;
    }

    procedure pop()
        requires s.top > 0; // main is not empty
        modifies s;
    {
        s.top := s.top - 1;
    }

    function top() : int
        requires s.top > 0; // main is not empty
    {
        return s.elements[s.top - 1];
    }

    procedure init()
        modifies s;
    {
        s.top := 0; // initialize the main
    }

    procedure next()
        modifies s;
    {
        havoc s;
        if (s.top < n) {
            // non-deterministically decide whether to push or pop
            if (nondet()) {
                push(nondet());
            } else {
                pop();
            }
        } else {
            pop();
        }
    }

    procedure main()
    {
        init(); // initialize the main
        next(); // perform a transition
    }
}
