|
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
|
|
|