module main {
    // Define the fixed capacity of the stack
    const n : int = 10;

    // The stack is modeled as an array with a fixed size
    var s : [int] int;
    // Top index to track the current top element in 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 s, top_index;
    {
        if (top_index < n - 1) {
            top_index = top_index + 1;
            s[top_index] = x;
        }
    }

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

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

    // Safety properties
    invariant capacity_limit : top_index < n;
    invariant non_negative_index : top_index >= -1;

    // Model checking control block
    control {
        v = unroll(5);
        check;
        print_results;
    }
}
