module main int)
{
  const capacity: int = n;
  type stack_t: record {
    size: int;
    elems: array [int] of int;
  };

  var s: stack_t;

  procedure push(e: int)
    requires s.size < capacity;
    modifies s;
  {
    s.size := s.size + 1;
    s.elems[s.size] := e;
  }

  procedure pop()
    requires s.size > 0;
    modifies s;
  {
    s.size := s.size - 1;
  }

  function top(): int
    requires s.size > 0;
  {
    return s.elems[s.size];
  }

  init {
    s.size := 0;
  }

  transition {
    if (s.size < capacity) {
      havoc e: int;
      push(e);
    } else {
      pop();
    }
  }
}
