actor.maude

***(
	TODO:
	constants in PRED should be "true" and "false" for rltool to do auto matching
	rename to BOOL module name as well

	untested ops/require more testing
	newActor
	spawn
	releaseRecv
	ack_release first second final
	create snapshot
	del onack


	is onack/whatever ever set to false?
)

set include BOOL off .

--- load util.maude
load reference.maude

view TrivAsReferenceList from TRIV to REFERENCE is
	sort Elt to ReferenceListUnion .
endv

view TrivAsReferenceList2 from TRIV to REFERENCE is
	sort Elt to ReferenceList .
endv

view TrivAsiNat from TRIV to INAT is
	sort Elt to iNat .
endv

fmod ACTOR is 
	protecting PRED .
	protecting INAT .
	protecting REFERENCE .
	protecting MAP{TrivAsiNat, TrivAsReferenceList} .
	protecting MAP{TrivAsiNat, TrivAsReferenceList2} .
	
	--- ########## SORTS ##########
	sorts Actor NeActorList ActorList .
	
	--- ########## SUBSORTS ##########
	subsorts Actor < NeActorList < ActorList .

	--- ########## OPS ##########
	--- identities
	--- op mtActor : -> Actor [ctor] .
	op mtActorList : -> ActorList [ctor] .

	--- i = id, sn = seqnum, sid: snapshot id, r = refs, dr = deactivated_refs, o = owners, ro = released_owners, 
	--- m = memory, tr = target_releasing, owr = owner_releasing, owa: owner_ack, ta: target_ack, oa = onack, snap: snapshot map
	op < i: _ | sn: _ | sid: _ | r: _ | dr: _ | o: _ | ro: _ | m: _ | tr: _ | owr: _ | owa: _ | ta: _ | oa: _ | snap: _ > : 
		iNat iNat iNat ReferenceList ReferenceList ReferenceList ReferenceList ReferenceList 
			ReferenceList ReferenceList ReferenceList ReferenceList Map{TrivAsiNat, TrivAsReferenceList} Map{TrivAsiNat, TrivAsReferenceList2} ->  Actor [ctor] .
	--- TODO: Should this check for uniqueness (set) for i?
	op _;_ : ActorList ActorList -> ActorList [ctor assoc id: mtActorList] .
	op _;_ : NeActorList ActorList -> ActorList [ctor ditto] .
	op _;_ : ActorList NeActorList -> ActorList [ctor ditto] .

	--- Methods Declarations an Actor has
	--- Actor Constructor: ActorID1 to be created, ActorID2 of first reference, next unique refID
	--- NOTE: refID :: ActorID1 -> ActorID2
	op newActor(_,_,_) : iNat iNat iNat -> Actor [ctor] .
	--- Spawn: Allows an actor A to spawn a child, this is just a renaming of newActor
	--- NOTE: this only updates A's references, a rule will actually call newActor
	op spawn(_,_,_) : Actor iNat iNat -> ActorList .
	--- createRef: Creates a reference C -> B if given A -> B and A -> C
	op createRef(_,_,_) : iNat Reference Reference -> Reference .
	--- receive: Allows an actor A to recieve a new reference
	op receive(_,_) : Actor Reference -> Actor .
	--- release: Allows an actor to release an input reference, this only edits deactivated_refs
	--- updateInfo will be called alongside release in the relese rule which will also do error checking to see if
	--- the input reference is actually in the Actor.refs
	op release(_,_) : Actor Reference -> Actor .
	--- updateInfo: Called by actor A release an actor B to update local variables
	--- the actual release message will be created and sent via the rule into the soup
	op updateInfo(_,_) : Actor iNat -> Actor .
	--- This calls both release for an input reference list given from a releaseReq message, this also calls update info
	op releaseReferenceList(_,_) : Actor ReferenceList -> Actor .
	--- releaseRecv: Called by an actor B which received a recieve request from A
	--- this will release references in B and send an ack to A
	--- NOTE: the ackRelease message will be generated by a rule
	op releaseRecvReleasing(_,_) : Actor ReferenceList -> Actor .
	op releaseRecvCreated(_,_) : Actor ReferenceList -> Actor .
	op releaseRecv(_,_) : Actor iNat -> Actor .
	--- ackRelease: This is sent by actor B to A as an ack, we set map[N] to mtRefList
	--- NOTE : this only edits the actor A
	--- this implements the first for loop
	--- Actor, onack[n], seq num
	op ackReleaseFirst(_,_,_) : Actor ReferenceList iNat -> Actor .
	--- this implements the second for loop
	--- Actor, seq num, origin of message
	op ackReleaseSecond(_,_,_) : Actor ReferenceList iNat -> Actor .
	--- this operator creates a snapshot for an actor for sn N
	--- Actor to operate on, seqnum, snap id
	op createSnapshot(_,_,_) : Actor iNat iNat -> Actor .
	--- this operator deletes (resets) onack for a specific sequence number
	op delOnAck(_,_) : Actor iNat -> Actor .
	--- this calls both for loops one after another
	--- Actor to operate on, the onAck list, the origin actor, seq id, snapid
	op ackRelease(_,_,_,_,_) : Actor ReferenceList iNat iNat iNat -> Actor .

	--- ########## HELPER OPS ##########
	--- releasingEquiv(B, x : A -> B) = tt, releasingEquiv(B, x : A -> C) = ff
	op releasingEquiv(_,_) : iNat Reference -> Pred .
	--- releasingRefList(B, (x : A -> B), (y : C -> B), (z : D -> E)) returns x, y
	--- b: B, deactivatedRefs
	--- op releasingRefList(_,_) : iNat ReferenceList -> ReferenceList .
	op releasingRefList(_,_) : iNat ReferenceList -> ReferenceList .
	--- createdRefList(B, (x : A -> B), (y : C -> B), (z : D -> B), (y : C -> B)) returns z : D -> B
	--- b : B, Memory, TargetReleasing
	op createdRefList(_,_,_) : iNat ReferenceList ReferenceList -> ReferenceList .
	--- sentRefList(B, (x : A -> B), (y : E -> C), (z : B -> D), (y : C -> B)) returns z : B -> D
	op sentRefList(_,_,_) : iNat ReferenceList ReferenceList -> ReferenceList .
	--- getReleasing
	op getReleasing(_) : ReferenceListUnion -> ReferenceList .
	--- getCreated
	op getCreated(_) : ReferenceListUnion -> ReferenceList .
	--- getSent
	op getSent(_) : ReferenceListUnion -> ReferenceList .
	--- lenAL
	op lenAL(_) : ActorList -> iNat .

	--- ########## VARS ##########
	vars S N X Y A B C D E F G : iNat .
	vars AcA : Actor .
	vars AcLiA AcLiB AcLiC AcLiD : ActorList .
	vars RefA RefB : Reference .
	vars RefLiA RefLiB RefLiC RefLiD RefLiE RefLiF RefLiG RefLiH RefLiI RefLiJ RefLiK RefLiL RefLiM RefLiN RefLiO RefLiP RefLiQ RefLiR relLi creLi onAckLi : ReferenceList . 
	vars MapNatRefLiA MapNatRefLiC : Map{TrivAsiNat, TrivAsReferenceList} .
	vars MapNatRefLiB MapNatRefLiD : Map{TrivAsiNat, TrivAsReferenceList2} .

	--- ########## EQS ##########
	--- Uniqueness
	--- eq mtActor ; mtActor = mtActor .
	--- eq mtActor ; AcLiA = AcLiA .
	--- eq AcLiA ; mtActor = AcLiA .
	eq (AcLiA ; (< i: A | sn: B | sid: X | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiO | ta: RefLiP | oa: MapNatRefLiA | snap: MapNatRefLiB >) ; AcLiB)
		; (AcLiC ; (< i: A | sn: C | sid: Y | r: RefLiH | dr: RefLiI | o: RefLiJ | ro: RefLiK | m: RefLiL | tr: RefLiM | owr: RefLiN | owa: RefLiQ | ta: RefLiR | oa: MapNatRefLiC | snap: MapNatRefLiD >) ; AcLiD)
			= AcLiA ; (< i: A | sn: B | sid: X | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiO | ta: RefLiP | oa: MapNatRefLiA | snap: MapNatRefLiB >) ; AcLiB ; AcLiC ; AcLiD .
	--- implementations for Actor
	eq newActor(A, B, X) = < i: A | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: (X :: B -> A) | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: mtRefList | oa: empty | snap: empty > .
	--- implementations for Spawn
	eq spawn(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, B, X) = 
		< i: A | sn: B | sid: C | r: (X :: A -> B), RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- implementations for createRef
	eq createRef(A , B :: C -> D , E :: F -> G) = A :: G -> D .
	--- implementation of receive
	eq receive(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, RefA) =
		< i: A | sn: B | sid: C | r: RefA , RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- implementation of release
	eq release(< i: A | sn: B | sid: C | r: RefA, RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, RefA) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefA, RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- implementation of update info
	eq updateInfo(< i: A | sn: C | sid: X | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, B) =
		< i: A | sn: s C | sid: X | r: RefLiA | dr: remList(releasingRefList(B, RefLiB), RefLiB) 
		| o: RefLiC | ro: RefLiD | m: RefLiE | tr: createdRefList(B, RefLiE, RefLiF), RefLiF | owr: sentRefList(B, RefLiE, RefLiG),RefLiG | owa: RefLiH | ta: RefLiI  
		| oa: insert(s C, (releasingRefList(B, RefLiB) U sentRefList(B, RefLiE, RefLiG) U createdRefList(B, RefLiE, RefLiF)),MapNatRefLiA) | snap: MapNatRefLiB > .
	--- implementation of releaseReferenceList
	eq releaseReferenceList(AcA, mtRefList) = AcA .
	eq releaseReferenceList(AcA, ((X :: A -> B), RefLiA)) = releaseReferenceList(updateInfo(release(AcA, (X :: A -> B)), B), RefLiA) .
	--- implementation of releaseRecv
	--- remove released (first for loop)
	--- termination when releasing list is empty
	eq releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, mtRefList) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- x in releasing and x in owners
	eq releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefA, RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, relLi)) = 
		releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, relLi) .
	--- x in releasing and x not in owners
	eq releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, relLi)) = 
		releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefA, RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, relLi) .
	--- termination when created is empty
	eq releaseRecvCreated(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, mtRefList) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- x in releasing and x in owners
	eq releaseRecvCreated(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefA, RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, creLi)) = 
		releaseRecvCreated(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, creLi) .
	--- x in releasing and x not in owners
	eq releaseRecvCreated(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, creLi)) = 
		releaseRecvCreated(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefA, RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, creLi) .

	eq releaseRecv(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, N) =
		releaseRecvCreated(releaseRecvReleasing(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, getReleasing(MapNatRefLiA[N])), getCreated(MapNatRefLiA[N])) .

	--- implementation on ackRelease
	--- termination
	eq ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- X : C -> A and C =/= A if x in owa
	eq ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: (D :: E -> F), RefLiE | tr: RefLiF | owr: RefLiG | owa: (D :: E -> F), RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, ((D :: E -> F), onAckLi), F) = 
		ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: (D :: E -> F), RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F) .
	--- X : C -> A 
	eq ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, onAckLi), F) = 
		ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefA, RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F) .

	--- termination
	eq ackReleaseSecond(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, mtRefList, F) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > .
	--- x : B -> C in on ack and x in target ack
	eq ackReleaseSecond(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: (D :: F -> E), RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: (D :: F -> E), RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, ((D :: F -> E), onAckLi), F) = 
		ackReleaseSecond(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: (D :: F -> E), RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F) .
	--- x : B -> C in on ack and x not in target ack
	eq ackReleaseSecond(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, (RefA, onAckLi), F) = 
		ackReleaseSecond(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefA, RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F) .
	--- implementation of createSnapshot
	--- if snapid < in snapid
	ceq createSnapshot(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, N, S) = 
		< i: A | sn: B | sid: S | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: insert(S, ((RefLiA, (RefLiC, (RefLiE, (getReleasing(MapNatRefLiA[N]), (getCreated(MapNatRefLiA[N]), getSent(MapNatRefLiA[N])))))) ), MapNatRefLiB) > if !((S - C) ~iN 0) = tt .
	--- if snapid >= insnapid
	eq createSnapshot(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, N, S) =
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB > [owise] .
	--- implementation of delOnAck
	eq delOnAck(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, N) = 
		< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: insert(N, mtRefListUnion, MapNatRefLiA) | snap: MapNatRefLiB > .
	
	eq ackRelease(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F, N, S) = 
		createSnapshot(ackReleaseSecond(ackReleaseFirst(< i: A | sn: B | sid: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | owa: RefLiH | ta: RefLiI | oa: MapNatRefLiA | snap: MapNatRefLiB >, onAckLi, F), onAckLi, F), N, S) .
	
	--- eq ackRelease(< i: A | sn: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | oa: MapNatRefLiA >, N) =
	--- 	< i: A | sn: C | r: RefLiA | dr: RefLiB | o: RefLiC | ro: RefLiD | m: RefLiE | tr: RefLiF | owr: RefLiG | oa: insert(N, mtRefListUnion, MapNatRefLiA) > .


	--- ########## HELPER EQS ##########
	--- implementation of releasingEquiv
	eq releasingEquiv(B, C :: D -> E) = B ~iN E .
	
	--- implementation of releasingRefList
	eq releasingRefList(B, mtRefList) = mtRefList . --- termination
	eq releasingRefList(B, ((A :: C -> B), RefLiA)) = (A :: C -> B), releasingRefList(B, RefLiA). --- ref matches in dr
	eq releasingRefList(B, ((A :: C -> D), RefLiA)) = releasingRefList(B, RefLiA) . --- ref does not match in dr
	
	--- implmentation of createdRefList
	eq createdRefList(B, mtRefList, RefLiB) = mtRefList . --- termination
	--- ref in mem and tr 
	eq createdRefList(B, ((A :: C -> B), RefLiA), (RefLiB, (A :: C -> B), RefLiC)) = createdRefList(B, RefLiA, (RefLiB, RefLiC)) .
	--- ref in mem and not in tr
	--- this is the case where tr is empty
	eq createdRefList(B, ((A :: C -> B), RefLiA), mtRefList) = (A :: C -> B), createdRefList(B, RefLiA, mtRefList) .
	--- NOTE: Due to unique reference IDs, A :: C -> B and A :: D -> B cannot occur
	--- this is the case where tr is not empty
	eq createdRefList(B, ((A :: C -> B), RefLiA), (RefLiB, (D :: E -> F), RefLiC)) = (A :: C -> B), createdRefList(B, RefLiA, (RefLiB, (D :: E -> F), RefLiC)) .
	--- ref is not in mem
	eq createdRefList(B, ((A :: C -> D), RefLiA), RefLiB) = createdRefList(B, RefLiA, RefLiB) .

	--- implementation of sentRefList
	eq sentRefList(B, mtRefList, RefLiB) = mtRefList . --- termination
	--- ref in mem and owr
	eq sentRefList(B, ((A :: B -> C), RefLiA), (RefLiB, (A :: B -> C), RefLiC)) = sentRefList(B, RefLiA, (RefLiB, RefLiC)) .
	--- ref in mem and not in owr
	--- this is the case where owr is empty
	eq sentRefList(B, ((A :: B -> C), RefLiA), mtRefList) = (A :: B -> C), sentRefList(B, RefLiA, mtRefList) .
	--- NOTE: Due to unique reference IDs, A :: C -> B and A :: D -> B cannot occur
	--- this is the case where tr is not empty
	eq sentRefList(B, ((A :: B -> C), RefLiA), (RefLiB, (D :: E -> F), RefLiC)) = (A :: B -> C), sentRefList(B, RefLiA, (RefLiB, (D :: E -> F), RefLiC)) .
	--- ref is not in mem
	eq sentRefList(B, ((A :: C -> D), RefLiA), RefLiB) = sentRefList(B, RefLiA, RefLiB) .
	
	--- getReleasing implementation
	eq getReleasing(RefLiA U RefLiB U RefLiC) = RefLiA .
	--- getCreated
	eq getCreated(RefLiA U RefLiB U RefLiC) = RefLiB .
	--- getSent
	eq getSent(RefLiA U RefLiB U RefLiC) = RefLiC .

	--- implementation of lenAL
	eq lenAL(mtActorList) = 0 .
	eq lenAL(AcA ; AcLiA) = s lenAL(AcLiA) .
endfm

--- --- unchanged
--- red release(< i: 0 | sn: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, mtRefList) .
--- red release(< i: 0 | sn: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red release(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- --- add 0 :: 0 -> 0 to dr
--- red release(< i: 0 | sn: 0 | r: (0 :: 0 -> 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red release(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (0 :: 0 -> 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red release(< i: 0 | sn: 0 | r: ((0 :: 0 -> 0), (s s 0 :: s s 0 -> s s 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .

--- --- unchanced
--- red releaseReferenceList(< i: 0 | sn: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, mtRefList) .
--- red releaseReferenceList(< i: 0 | sn: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red releaseReferenceList(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- --- add 0 :: 0 -> 0 to dr
--- red releaseReferenceList(< i: 0 | sn: 0 | r: (0 :: 0 -> 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red releaseReferenceList(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (0 :: 0 -> 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- red releaseReferenceList(< i: 0 | sn: 0 | r: ((0 :: 0 -> 0), (s s 0 :: s s 0 -> s s 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, (0 :: 0 -> 0) ) .
--- --- only adds 0 :: 0 -> 0
--- red releaseReferenceList(< i: 0 | sn: 0 | r: (0 :: 0 -> 0) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0)) ) .
--- red releaseReferenceList(< i: 0 | sn: 0 | r: ((0 :: 0 -> 0), (s s 0 :: s s 0 -> s s 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0)) ) .
--- --- add 0 :: 0 -> 0 and s 0 :: s 0 -> s 0 to dr
--- red releaseReferenceList(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (0 :: 0 -> 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0)) ) .


--- --- removes nothing
--- red ackRelease(releaseReferenceList(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (0 :: 0 -> 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0)) ), 0) .
--- --- sets s 0 in map to mtRefList
--- red ackRelease(releaseReferenceList(< i: 0 | sn: 0 | r: ((s 0 :: s 0 -> s 0), (0 :: 0 -> 0)) | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0)) ), s 0) .

--- --- returns only releasing
--- red getReleasing(insert(0, ((0 :: 0 -> s 0),s 0 :: s 0 -> s 0) U s s s s s 0 :: s 0 -> s s s 0 U (s s s 0 :: s s s 0 -> s 0),s s s s 0 :: s s s s 0 -> s 0, empty)[0]) .
--- --- returns only created
--- red getCreated(insert(0, ((0 :: 0 -> s 0),s 0 :: s 0 -> s 0) U s s s s s 0 :: s 0 -> s s s 0 U (s s s 0 :: s s s 0 -> s 0),s s s s 0 :: s s s s 0 -> s 0, empty)[0]) .
--- --- returns only sent
--- red getSent(insert(0, ((0 :: 0 -> s 0),s 0 :: s 0 -> s 0) U s s s s s 0 :: s 0 -> s s s 0 U (s s s 0 :: s s s 0 -> s 0),s s s s 0 :: s s s s 0 -> s 0, empty)[0]) .


--- red releaseRecvReleasing(< i: 0 | sn: 0 | sid: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s s 0 :: s s s 0 -> s s s 0) | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: mtRefList | oa: insert(0, ((0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0) U mtRefList U mtRefList), empty) | snap: empty >, getReleasing(insert(0, ((0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0) U mtRefList U mtRefList), empty)[0]), 0) .
--- red getReleasing(insert(0, ((0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0) U mtRefList U mtRefList), empty)[0]) .

--- red releaseRecvCreated(< i: 0 | sn: 0 | sid: 0 | r: (s 0 :: s 0 -> s 0) | dr: mtRefList | o: (s 0 :: s 0 -> s 0), (s s s 0 :: s s s 0 -> s s s 0) | ro: (0 :: 0 -> 0) | m: mtRefList | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: mtRefList | oa: insert(0, ((0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0) U mtRefList U mtRefList), empty) | snap: empty >, getReleasing(insert(0, ((0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0) U mtRefList U mtRefList), empty)[0]), 0) .

--- red releaseRecv(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: (0 :: 0 -> 0), (s s 0 :: s s 0 -> s s 0) | ro: (s 0 :: s 0 -> s 0) | m: mtRefList | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: mtRefList | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, 0) .

--- red ackReleaseFirst(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: (0 :: 0 -> 0) | ta: mtRefList | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, ((0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)), 0) .

--- red ackReleaseSecond(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: (0 :: 0 -> 0) | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, ((0 :: 0 -> 0), (s s 0 :: s s s 0 -> s s 0), (s s s 0 :: s s s 0 -> s s s 0)), 0) .

--- red createSnapshot(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: (0 :: 0 -> 0) | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, 0, 0) .

--- red createSnapshot(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: (0 :: 0 -> 0) | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, 0, s 0) .

--- red delOnAck(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: (0 :: 0 -> 0) | oa: insert(0, ((0 :: 0 -> 0) U (s 0 :: s 0 -> s 0) U mtRefList), empty) | snap: empty >, 0) .

--- red delOnAck(< i: 0 | sn: 0 | sid: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (0 :: 0 -> 0) | tr: mtRefList | owr: mtRefList | owa: mtRefList | ta: (0 :: 0 -> 0) | oa: empty | snap: empty >, 0) .

--- red mtActorList .
--- red mtActorList ; mtActorList .
--- red mtActorList ; A:Actor .
--- red A:Actor ; mtActorList .
--- red < i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > ; mtActorList .
--- red mtActorList ; < i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > .
--- red < i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > ; < i: 0 | sn: s 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > .
--- red < i: 0 | sn: s 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > ; < i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > .
--- red < i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > ; < i: s 0 | sn: s 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > ; < i: s 0 | sn: 0 | r: RefLiA | dr: mtRefList | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty > .

--- red insert(0, mtRefList, insert(0, ((0 :: 0 -> 0),s 0 :: s 0 -> s 0), empty)) .