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

    // Stack is represented as an array of nonnegative integers
    var s : array[int, int];
    // Top index indicates the current top of the stack
    var top_index : int;

    // Initialize the stack
    init {
        top_index = -1;
    }

    // Procedure to push an element onto the stack
    procedure push(x : int)
        modifies top_index, s;
    {
        if (top_index < n - 1) {
            top_index = top_index + 1;
            s[top_index] = x;
        }
    }

    // Procedure to pop the top element from the stack
    procedure pop()
        modifies top_index;
    {
        if (top_index >= 0) {
            top_index = top_index - 1;
        }
    }

    // Function to return the top element of the stack
    function top() : int
    {
        if (top_index >= 0) {
            return s[top_index];
        } else {
            return -1; // Return -1 if the stack is empty
        }
    }

    // Next state transitions
    next {
        // Non-deterministically choose to push, pop, or do nothing
        if (*) {
            var elem : int;
            elem = *; // Non-deterministically choose an element to push
            call push(elem);
        } else if (*) {
            call pop();
        }
    }

    // Invariants to maintain the correctness of the stack
    invariant inv_nonnegative_top_index : top_index >= -1;
    invariant inv_within_capacity : top_index < n;
}
