types
  SmallInt = int [0..3];
  Stack = autocons system
  |[
  var
        my_stack : list [10] of SmallInt = [0]
  actions
        obs top (a : SmallInt) = requires (a = hd my_stack) :
                skip
                end ;
        obs pop = requires (len my_stack > 0) :
                my_stack := tl my_stack
                end;
        obs push (a : SmallInt) = requires len my_stack < 10 :
                my_stack := [a] ^ my_stack
                end

  do
        var A : SmallInt : push(A) []  pop() [] var B : SmallInt : top(B)
  od
  ]|
system
  Stack