queue [ID: TYPE, ID1: ID]: THEORY

BEGIN

  IMPORTING event[ID]

  null_event: EVENT =  (#id:=ID1,act:=NIL,adr:=0,val:=0#)

  IMPORTING special_list[EVENT,null_event]

  Q: TYPE = list

  q:  VAR Q
  id: VAR ID
  adr: VAR ADDRESS
  val: VAR VALUE

  % the projection of q on id
  project(q: Q): [ID -> Q] =
    (LAMBDA (id: ID):
       projection(of_id(id),q))

  % adds a non-transactional read transaction to q
  add_ntread(id,adr,val,q): Q =
    LET new_e1 = (#id := id, act := OPEN,   adr := 0,   val := 0#)   IN
    LET new_e2 = (#id := id, act := READ,   adr := adr, val := val#) IN
    LET new_e3 = (#id := id, act := COMMIT, adr := 0,   val := 0#)   IN
        add(new_e3,add(new_e2,add(new_e1,q)))

  % adds a non-transactional write transaction to q
  add_ntwrite(id,adr,val,q): Q =
    LET new_e1 = (#id := id, act := OPEN,   adr := 0,   val := 0#)   IN
    LET new_e2 = (#id := id, act := WRITE,  adr := adr, val := val#) IN
    LET new_e3 = (#id := id, act := COMMIT, adr := 0,   val := 0#)   IN
        add(new_e3,add(new_e2,add(new_e1,q)))

  % adds an open event of id to q
  add_open(id,q): Q =
    LET new_e = (#id := id, act := OPEN, adr := 0, val := 0#)
    IN add(new_e,q)

  % adds a write event of id to q
  add_write(id,adr,val,q): Q =
    LET new_e = (#id := id, act := WRITE, adr := adr, val := val#)
    IN add(new_e,q)

  % adds a read event of id to q
  add_read(id,adr,val,q): Q =
    LET new_e = (#id := id, act := READ, adr := adr, val := val#)
    IN add(new_e,q)

  % adds a commit event of id to q
  add_commit(id,q): Q =
    LET new_e = (#id := id, act := COMMIT, adr := 0, val := 0#)
    IN add(new_e,q)

  % adds an abort event of id to q
  add_abort(id,q): Q =
    LET new_e = (#id := id, act := ABORT, adr := 0, val := 0#)
    IN add(new_e,q)

  % adds a mark of id to q -- might not needed for "big" steps
  add_mark(id,q): Q =
    LET new_e = (#id := id, act := MARK, adr := 0, val := 0#)
    IN add(new_e,q)

  % Axiom of adding an event to projection
  add_to_projection: AXIOM
    FORALL q,(e: EVENT),id: 
      IF of_id(id)(e)
        THEN project(add(e,q))(id) = add(e,project(q)(id))
        ELSE project(add(e,q))(id) = project(q)(id)
      ENDIF    

  indices_of_projection: AXIOM %LEMMA
    FORALL q,(e: EVENT),(i: posnat):
      IF i = project(q)(e`id)`size + 1
        THEN project(add(e,q))(e`id)`entry(i) = e
        ELSE project(add(e,q))(e`id)`entry(i) = project(q)(e`id)`entry(i)
      ENDIF  


  some_of_empty_proj: AXIOM
    FORALL q,(id: ID):
      empty(project(q)(id)) IMPLIES
        some(of_id(id),q) = FALSE  

  some_of_empty_p_projection: AXIOM
    FORALL q,(p: [EVENT -> bool]):
      empty(projection(p,q)) IMPLIES
        some(of_id(id),q) = FALSE 

  some_write_of_id_of_empty_proj: AXIOM
    FORALL q,(id: ID):
      empty(project(q)(id)) IMPLIES
        some(is_write_of_id(id),q) = FALSE  


  not_some_list_not_some_proj: AXIOM
    FORALL q,(p: [EVENT -> bool]),(id: ID):
      NOT some(p,q) IMPLIES
        NOT some(p,project(q)(id))

%% needs to prove the following axioms: !!!!!!
  eql_queues_eql_some: LEMMA
    FORALL (q1,q2: Q),(p: [EVENT -> bool]):
      eql(q1,q2) IMPLIES
        some(p,q1) <=> some(p,q2) 

  some_write_id_q_imp_some_write_proj_id: AXIOM
    FORALL q,id:
      some(is_write_of_id(id),q) IFF
        some(is_write_of_id(id),project(q)(id))

  
  proj_of_id_of_proj_of_not_id: AXIOM
    FORALL q,id:
      empty(project(projection(not_of_id(id),q))(id))

  proj_of_id_of_proj_of_not_another_id: AXIOM
    FORALL q,(id1,id2: ID):
      (NOT (id1 = id2)) IMPLIES
        project(projection(not_of_id(id2),q))(id1) =
          project(q)(id1)

   % get the latest value that id wrote to adr
   % -> assuming q is in reversed order
   % -> should be used only after ensuring that there exists write(id)
   get_latest_write(id,adr,q): RECURSIVE VALUE =
     IF empty(q)
       THEN 0
       ELSE
         IF(car(q)`id  = id    AND
            car(q)`act = WRITE AND
            car(q)`adr = adr)
           THEN car(q)`val
           ELSE get_latest_write(id,adr,cdr(q))
         ENDIF
      ENDIF
      MEASURE q`size

  % when the q is empty the id of the car is undefined       
  id_of_car_null: AXIOM
    FORALL q: 
      FORALL (id: ID): 
        q`size = 0 IMPLIES
          car(q)`id /= id

  is_active(q, id): bool =
    some(of_id(id),q)

END queue