% RollBackQueue.lsl - implementation model
%
% The 'head' of the rollback queue is really an event in the
% center of a list of events.  If an event is added that 
% should be the new head, any events that are in between the 
% current head and the new head should be back in the queue.  
% The events that are before the head will be modeled as a stack, 
% head and after will be a signed priroity queue, where opposite 
% events will cancel out.

RollbackQueue(E,Time,EQueue): trait

assumes BasicEventTrait(E,Time)

includes int,
  % an EQueue will be both a stack and a queue
  Stack(E,EQueue,emptyhistory for empty:->C, 
        isEmptyhistory for isEmpty, \instack for \in),
  SignedPriorityQueue(E,EQueue,emptyqueue for empty:->EventQueue,
                     isEmptyqueue for isEmpty) 

introduces
  empty: -> EQueue
  add: E, EQueue, State -> EQueue
  __ \in __: E, EQueue -> Bool
  rollback: EQueue,State -> EQueue
  go: EQueue -> EQueue

asserts
  EQueue generated by empty, add 
  \forall e:E, q:EQueue, s:State

  % define add operation - state dependent
  % if e before top of history then rollback

  head(add(e,q,s)) ==
   if inbefore(e,top(q),s) then head(add(e,rollback(q,s),s))
    else head(append(e,q,s));

  tail(add(e,q,s)) ==
    if inbefore(e,top(q),s) then tail(add(e,rollback(q,s),s))
    else tail(append(e,q,s)); 

  top(add(e,q,s)) == 
    if inbefore(e,top(q),s) then top(add(e,rollback(q,s),s))
    else top(q);

  pop(add(e,q,s)) == 
    if inbefore(e,top(q),s) then pop(add(e,rollback(q,s),s)) 
    else pop(q);

  % define rollback - move top of stack into queue
  head(rollback(q,s)) == head(append(top(q),q,s));
  tail(rollback(q,s)) == tail(append(top(q),q,s));
  top(rollback(q,s)) == top(pop(q));
  pop(rollback(q,s)) == pop(pop(q));
  
  % define go - push head of queue
  head(go(q)) == head(tail(q));
  tail(go(q)) == tail(tail(q));
  top(go(q)) == head(q);
  pop(go(q)) == push(top(q),pop(q));

  e \in q == e \inq q \/ e \instack q;

implies
  \forall q: EQueue, e1,e2:E, s:State
  
  % current queue events cannot be before history events
  e1 \instack q /\ e2 \inq q => ~(inbefore(e2,e1,s));
  
  % the history is in order - ? base case ?
  inbefore(top(pop(q)),top(q),s);
  

%  len(q) >= 0;
%  converts count, \in, head, tail, len, isEmpty
%  exempting head(empty), tail(empty)

[Index]