constants
  size = 4;

sets
  value = {a,b,c,d,null};
  pos = [0,size-1];
  
fluents
  data: pos -> value;
  first: pos+{size};
  top: value;
  
actions
  push: value;
  pop: event;
  
vars
  I : pos;
  V : value;

rules
  first:=prev(first)+1 if pertinent(push);
  data(prev(first)):=push if prev(first)!=size;
  first:=prev(first)-1 if pop;  
  top:=data(first-1) if first>0;
  top:=null if first=0;

initially
  first:=0,data(I):=null,top:=null;
do {
  push:=a; push:=c; push:=b; push:=d;
}
query
  top=V?