loop init . (omod DATA is protecting MACHINE-INT . sort OidSet . subsort Oid < OidSet . *** sorts for pairs/triple *** first parameter is the source node identity sort Status . sort IdStatusPair . sort IdIdPair . sort IdIntPair . sort IdIdStatusTriple . *** sorts for partial functions *** all class attributes are realized as partial functions sort IdStatusPFun . subsort IdStatusPair < IdStatusPFun . sort IdIdPFun . subsort IdIdPair < IdIdPFun . sort IdIntPFun . subsort IdIntPair < IdIntPFun . sort IdIdStatusPFun . subsort IdIdStatusTriple < IdIdStatusPFun . *** operations for class attributes op active : -> Status . op passive : -> Status . op state : Oid Status -> IdStatusPair . op parent : Oid Oid -> IdIdPair . op seqNo : Oid MachineInt -> IdIntPair . op nbState : Oid Oid Status -> IdIdStatusTriple . *** operations for partial functions op mtstates : -> IdStatusPFun . op inIdStatusPFun : Oid IdStatusPFun -> Bool . op states : IdStatusPFun IdStatusPFun -> IdStatusPFun [assoc comm id: mtstates] . op assignIdStatusPFun : IdStatusPFun Oid Status -> IdStatusPFun . op assignIdStatusPFunNoOverriding : IdStatusPFun Oid Status -> IdStatusPFun . op mtparents : -> IdIdPFun . op inIdIdPFun : Oid IdIdPFun -> Bool . op inIdIdPFunAsParentForSource : Oid Oid IdIdPFun -> Bool . op parents : IdIdPFun IdIdPFun -> IdIdPFun [assoc comm id: mtparents] . op assignIdIdPFun : IdIdPFun Oid Oid -> IdIdPFun . op deleteIdIdPFunAsParentForSource : IdIdPFun Oid Oid -> IdIdPFun . op mtseqNos : -> IdIntPFun . op inIdIntPFun : Oid IdIntPFun -> Bool . op forSourceSmallerOrNoSeqnoInIdIntPFun : Oid MachineInt IdIntPFun -> Bool . op seqNos : IdIntPFun IdIntPFun -> IdIntPFun [assoc comm id: mtseqNos] . op assignIdIntPFun : IdIntPFun Oid MachineInt -> IdIntPFun . op assignIdIntPFunNoOverriding : IdIntPFun Oid MachineInt -> IdIntPFun . op deleteIdIntPFun : IdIntPFun Oid -> IdIntPFun . op dom : IdIntPFun -> OidSet . op mtnbsStates : -> IdIdStatusPFun . op inIdIdStatusPFun : Oid Oid IdIdStatusPFun -> Bool . op inIdIdStatusPFunAsNeighborForSource : Oid Oid IdIdStatusPFun -> Bool . op nbsStates : IdIdStatusPFun IdIdStatusPFun -> IdIdStatusPFun [assoc comm id: mtnbsStates] . op assignIdIdStatusPFun : IdIdStatusPFun Oid Oid Status -> IdIdStatusPFun . op assignIdIdStatusPFunNoOverriding : IdIdStatusPFun Oid Oid Status -> IdIdStatusPFun . op deleteIdIdStatusPFunAsNeighborForSource : IdIdStatusPFun Oid Oid -> IdIdStatusPFun . op assignAllIdIdStatusPFun : IdIdStatusPFun Oid OidSet Status -> IdIdStatusPFun . op assignAllIdIdStatusPFunNoOverriding : IdIdStatusPFun Oid OidSet Status -> IdIdStatusPFun . *** this operation looks up whether all neighbors (except parent node) *** are passive wrt to the given source node (second parameter) op allNbsPassiveWRTSrcUnlessParent : IdIdStatusPFun Oid Oid -> Bool . op allNbsPassiveWRTSrc : IdIdStatusPFun Oid -> Bool . *** Set constructors: op mtnbs : -> OidSet . op nbs : OidSet OidSet -> OidSet [assoc comm id: mtnbs] . op inSet : Oid OidSet -> Bool . op deleteFromSet : Oid OidSet -> OidSet . *** Variable declarations: var STAT1 STAT2 : Status . var IDSTATUSPFUN : IdStatusPFun . var IDIDPFUN : IdIdPFun . var IDINTPFUN : IdIntPFun . var IDIDSTATUSPFUN : IdIdStatusPFun . var I J M : MachineInt . vars A B C D X : Oid . var OIDSET : OidSet . *** *** EQUATIONS FOR DATATYPES (partial functions etc) *** *** Equations for IdStatusPFun: eq inIdStatusPFun(A, states(state(B,STAT1), IDSTATUSPFUN)) = if A == B then true else inIdStatusPFun(A, IDSTATUSPFUN) fi . eq inIdStatusPFun(A, mtstates) = false . eq assignIdStatusPFun(states(state(A,STAT1), IDSTATUSPFUN), A, STAT2) = states(state(A,STAT2), IDSTATUSPFUN) . ceq assignIdStatusPFun(IDSTATUSPFUN, A, STAT1) = states(state(A,STAT1), IDSTATUSPFUN) if not(inIdStatusPFun(A,IDSTATUSPFUN)) . eq assignIdStatusPFunNoOverriding(states(state(A,STAT1), IDSTATUSPFUN), A, STAT2) = states(state(A,STAT1), IDSTATUSPFUN) . ceq assignIdStatusPFunNoOverriding(IDSTATUSPFUN, A, STAT1) = states(state(A,STAT1), IDSTATUSPFUN) if not(inIdStatusPFun(A,IDSTATUSPFUN)) . *** Equations for IdIdPFun: eq inIdIdPFun(A, parents(parent(B,C), IDIDPFUN)) = if A == B then true else inIdIdPFun(A, IDIDPFUN) fi . eq inIdIdPFun(A, mtparents) = false . eq inIdIdPFunAsParentForSource(A, D, parents(parent(B,C), IDIDPFUN)) = if (A == C) and (D == B) then true else inIdIdPFunAsParentForSource(A, D, IDIDPFUN) fi . eq inIdIdPFunAsParentForSource(A, D, mtparents) = false . eq assignIdIdPFun(parents(parent(A,B), IDIDPFUN), A, C) = parents(parent(A,C), IDIDPFUN) . ceq assignIdIdPFun(IDIDPFUN, A, B) = parents(parent(A,B), IDIDPFUN) if not(inIdIdPFun(A,IDIDPFUN)) . eq deleteIdIdPFunAsParentForSource(parents(parent(A,B), IDIDPFUN), B, A) = IDIDPFUN . ceq deleteIdIdPFunAsParentForSource(IDIDPFUN, B, A) = IDIDPFUN if not(inIdIdPFunAsParentForSource(B,A,IDIDPFUN)) . *** Equations for IdIntPFun: eq dom(mtseqNos) = mtnbs . eq dom(seqNos(seqNo(A,I), IDINTPFUN)) = nbs(A, dom(IDINTPFUN)) . eq inIdIntPFun(A, seqNos(seqNo(B,I), IDINTPFUN)) = if A == B then true else inIdIntPFun(A, IDINTPFUN) fi . eq inIdIntPFun(A, mtseqNos) = false . ceq forSourceSmallerOrNoSeqnoInIdIntPFun(A, J, IDINTPFUN) = true if not(inIdIntPFun(A, IDINTPFUN)) . eq forSourceSmallerOrNoSeqnoInIdIntPFun(A, J, seqNos(seqNo(B,I), IDINTPFUN)) = if A == B then if J > I then true else false fi else forSourceSmallerOrNoSeqnoInIdIntPFun(A, J, IDINTPFUN) fi . eq forSourceSmallerOrNoSeqnoInIdIntPFun(A, J, mtseqNos) = true . eq assignIdIntPFun(seqNos(seqNo(A,I), IDINTPFUN), A, J) = seqNos(seqNo(A,J), IDINTPFUN) . ceq assignIdIntPFun(IDINTPFUN, A, I) = seqNos(seqNo(A,I), IDINTPFUN) if not(inIdIntPFun(A,IDINTPFUN)) . eq assignIdIntPFunNoOverriding(seqNos(seqNo(A,I), IDINTPFUN), A, J) = seqNos(seqNo(A,I), IDINTPFUN) . ceq assignIdIntPFunNoOverriding(IDINTPFUN, A, I) = seqNos(seqNo(A,I), IDINTPFUN) if not(inIdIntPFun(A,IDINTPFUN)) . eq deleteIdIntPFun(seqNos(seqNo(A,I), IDINTPFUN), A) = IDINTPFUN . ceq deleteIdIntPFun(IDINTPFUN, A) = IDINTPFUN if not(inIdIntPFun(A,IDINTPFUN)) . *** Equations for IdIdStatusPFun: eq inIdIdStatusPFun(A, B, nbsStates(nbState(C,D,STAT1), IDIDSTATUSPFUN)) = if (A == C) and (B == D) then true else inIdIdStatusPFun(A, B, IDIDSTATUSPFUN) fi . eq inIdIdStatusPFun(A, B, mtnbsStates) = false . eq inIdIdStatusPFunAsNeighborForSource(B,A, nbsStates(nbState(C,D,STAT1), IDIDSTATUSPFUN)) = if (A == C) and (B == D) then true else inIdIdStatusPFunAsNeighborForSource(B, A, IDIDSTATUSPFUN) fi . eq inIdIdStatusPFunAsNeighborForSource(B, A, mtnbsStates) = false . eq assignIdIdStatusPFun(nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN), A, B, STAT2) = nbsStates(nbState(A,B,STAT2), IDIDSTATUSPFUN) . ceq assignIdIdStatusPFun(IDIDSTATUSPFUN, A, B, STAT1) = nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN) if not(inIdIdStatusPFun(A,B,IDIDSTATUSPFUN)) . eq assignIdIdStatusPFunNoOverriding(nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN), A, B, STAT2) = nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN) . ceq assignIdIdStatusPFunNoOverriding(IDIDSTATUSPFUN, A, B, STAT1) = nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN) if not(inIdIdStatusPFun(A,B,IDIDSTATUSPFUN)) . eq deleteIdIdStatusPFunAsNeighborForSource(nbsStates(nbState(A,B,STAT1), IDIDSTATUSPFUN), B, A) = IDIDSTATUSPFUN . ceq deleteIdIdStatusPFunAsNeighborForSource(IDIDSTATUSPFUN, B, A) = IDIDSTATUSPFUN if not(inIdIdStatusPFun(B,A,IDIDSTATUSPFUN)) . *** assign the same status to a set of neighbors (for a given source node) eq assignAllIdIdStatusPFun(IDIDSTATUSPFUN, A, nbs(B,OIDSET), STAT1) = assignAllIdIdStatusPFun( assignIdIdStatusPFun(IDIDSTATUSPFUN, A, B, STAT1), A, OIDSET, STAT1) . eq assignAllIdIdStatusPFun(IDIDSTATUSPFUN, A, mtnbs, STAT1) = IDIDSTATUSPFUN . *** assign the same status to a set of neighbors (for a given source *** node) but only if there is no entry for this source yet eq assignAllIdIdStatusPFunNoOverriding(IDIDSTATUSPFUN, A, nbs(B,OIDSET), STAT1) = assignAllIdIdStatusPFun( assignIdIdStatusPFunNoOverriding(IDIDSTATUSPFUN, A, B, STAT1), A, OIDSET, STAT1) . eq assignAllIdIdStatusPFunNoOverriding(IDIDSTATUSPFUN, A, mtnbs, STAT1) = IDIDSTATUSPFUN . eq allNbsPassiveWRTSrcUnlessParent(nbsStates(nbState(B,C,STAT1), IDIDSTATUSPFUN), A, X) = if A == B then if C == X then allNbsPassiveWRTSrcUnlessParent(IDIDSTATUSPFUN, A, X) else if STAT1 == passive then allNbsPassiveWRTSrcUnlessParent(IDIDSTATUSPFUN, A, X) else false fi fi else allNbsPassiveWRTSrcUnlessParent(IDIDSTATUSPFUN, A, X) fi . eq allNbsPassiveWRTSrcUnlessParent(mtnbsStates, A, X) = true . eq allNbsPassiveWRTSrc(nbsStates(nbState(B,C,STAT1),IDIDSTATUSPFUN), A) = if A == B then if STAT1 == passive then allNbsPassiveWRTSrc(IDIDSTATUSPFUN, A) else false fi else allNbsPassiveWRTSrc(IDIDSTATUSPFUN, A) fi . eq allNbsPassiveWRTSrc(mtnbsStates, A) = true . *** Equations for sets: eq nbs(A,A) = A . eq inSet(A, nbs(B,OIDSET)) = if A == B then true else inSet(A, OIDSET) fi . eq inSet(A, mtnbs) = false . eq deleteFromSet(A, nbs(B,OIDSET)) = if A == B then OIDSET else nbs(B,deleteFromSet(A, OIDSET)) fi . eq deleteFromSet(A, mtnbs) = mtnbs . endom) (omod RBP is protecting MACHINE-INT . protecting DATA . *** *** NETWORK NODES *** class Node | nbs : OidSet, states : IdStatusPFun, parents : IdIdPFun, seqNos : IdIntPFun, nbsStates : IdIdStatusPFun . *** messages: msg msg_To_From_Src_ : MachineInt Oid Oid Oid -> Msg . msg ack_To_From_Src_ : MachineInt Oid Oid Oid -> Msg . msg newlink : Oid Oid -> Msg . msg linkUpFrom_To_ : Oid Oid -> Msg . msg forSrc_LinkUp__ : Oid Oid Oid -> Msg . msg failure : Oid Oid -> Msg . msg linkDownFrom_To_ : Oid Oid -> Msg . msg forSrc_LinkDown__ : Oid Oid Oid -> Msg . *** multimessage-declarations: msg multimsg_To_From_Src_ : MachineInt OidSet Oid Oid -> Configuration . msg multiLinkUp_From_To_ : OidSet Oid Oid -> Configuration . msg multiLinkDown_From_To_ : OidSet Oid Oid -> Configuration . ops a b c d e f : -> Oid . *** Topology with up to six objects *** Initial configurations for testing ops test1 test2 test3 : -> Configuration . *** Variable declarations: var STAT1 STAT2 : Status . var IDSTATUSPFUN : IdStatusPFun . var IDIDPFUN : IdIdPFun . var IDINTPFUN : IdIntPFun . var IDIDSTATUSPFUN : IdIdStatusPFun . var I J M : MachineInt . vars A B C D X : Oid . var OIDSET : OidSet . var BOOL : Bool . var CONF : Configuration . *** multimessage definition: eq multimsg I To A From B Src C = msg I To A From B Src C . eq multimsg I To mtnbs From B Src C = none . eq multimsg I To nbs(A,OIDSET) From B Src C = (msg I To A From B Src C) (multimsg I To OIDSET From B Src C) . eq multiLinkUp X From A To B = forSrc X LinkUp A B . eq multiLinkUp mtnbs From A To B = none . eq multiLinkUp nbs(X,OIDSET) From A To B = (forSrc X LinkUp A B) (multiLinkUp OIDSET From A To B) . eq multiLinkDown X From A To B = forSrc X LinkDown A B . eq multiLinkDown mtnbs From A To B = none . eq multiLinkDown nbs(X,OIDSET) From A To B = (forSrc X LinkDown A B) (multiLinkDown OIDSET From A To B) . *** Some initial configurations for testing: eq test1 = < a : Node | nbs : nbs(b,c), states : states(state(a,passive), state(b,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0), seqNo(c,0)), nbsStates : nbsStates(nbState(a,b,passive), nbState(a,c,passive), nbState(b,b,passive), nbState(b,c,passive), nbState(c,b,passive), nbState(c,c,passive)) > < b : Node | nbs : nbs(a,c), states : states(state(a,passive), state(b,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0), seqNo(c,0)), nbsStates : nbsStates(nbState(a,a,passive), nbState(a,c,passive), nbState(b,a,passive), nbState(b,c,passive), nbState(c,a,passive), nbState(c,c,passive)) > < c : Node | nbs : nbs(b,a), states : states(state(a,passive), state(b,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0), seqNo(c,0)), nbsStates : nbsStates(nbState(a,a,passive), nbState(a,b,passive), nbState(b,a,passive), nbState(b,b,passive), nbState(c,a,passive), nbState(c,a,passive)) > . *** Test for New Link eq test2 = < b : Node | nbs : a, states : states(state(a,passive), state(b,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0)), nbsStates : nbsStates(nbState(a,a,passive), nbState(b,a,passive)) > < c : Node | nbs : a, states : states(state(a,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(c,0)), nbsStates : nbsStates(nbState(a,a,passive), nbState(c,a,passive)) > newlink(b,c) . *** Test for Failure of Link eq test3 = < b : Node | nbs : nbs(a,c), states : states(state(a,passive), state(b,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0), seqNo(c,0)), nbsStates : nbsStates(nbState(b,a,passive), nbState(b,c,passive), nbState(a,a,passive), nbState(a,c,passive), nbState(c,a,passive), nbState(c,c,passive)) > < a : Node | nbs : b, states : states(state(a,passive), state(b,passive)), parents : mtparents, seqNos : seqNos(seqNo(a,0), seqNo(b,0)), nbsStates : nbsStates(nbState(a,b,passive), nbState(b,b,passive)) > < c : Node | nbs : b, states : states(state(b,passive), state(c,passive)), parents : mtparents, seqNos : seqNos(seqNo(b,0), seqNo(c,0)), nbsStates : nbsStates(nbState(c,b,passive), nbState(b,b,passive)) > failure(b,a) . *** Start broadcasting a message: *** RESTRICTED VERSION FOR MODELCHECKING: *** only node 'a' sends exactly one message (a,1) crl [Send] : < a : Node | nbs : OIDSET, states : states(state(a,passive),IDSTATUSPFUN), parents : IDIDPFUN, seqNos : seqNos(seqNo(a,0),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > => < a : Node | states : assignIdStatusPFun(IDSTATUSPFUN, a, active), parents : assignIdIdPFun(IDIDPFUN, a, a), seqNos : assignIdIntPFun(IDINTPFUN, a, 1), nbsStates : assignAllIdIdStatusPFun( IDIDSTATUSPFUN, a, OIDSET, active) > (multimsg 1 To OIDSET From a Src a) if OIDSET =/= mtnbs . *** Receiver (active or passive) receives current message -> ack rl [RepeatRecCurrentMsg] : < A : Node | nbs : nbs(B,OIDSET), states : IDSTATUSPFUN, parents : IDIDPFUN, seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > (msg M To A From B Src C) => < A : Node | nbs : nbs(B,OIDSET) > (ack M To B From A Src C) . *** NONLEAFCASE *** Receiver (active or passive) receives newer message than his *** current one (wrt to a source) -> forget old message, forward newest *** message to all neighbors crl [RecNewMsg] : < A : Node | nbs : nbs(B,OIDSET), states : IDSTATUSPFUN, parents : IDIDPFUN, seqNos : IDINTPFUN, nbsStates : IDIDSTATUSPFUN > (msg M To A From B Src C) => < A : Node | states : assignIdStatusPFun(IDSTATUSPFUN, C, active), parents : assignIdIdPFun(IDIDPFUN, C, B), seqNos : assignIdIntPFun(IDINTPFUN, C, M), nbsStates : assignAllIdIdStatusPFun( assignIdIdStatusPFun( IDIDSTATUSPFUN, C, B, passive), C, OIDSET, active) > (multimsg M To OIDSET From A Src C) if (OIDSET =/= mtnbs) and forSourceSmallerOrNoSeqnoInIdIntPFun(C,M,IDINTPFUN) . *** LEAFCASE *** Receiver (active or passive) receives newer message than his *** current one (wrt to a source) -> forget old message, *** Receiver is leaf node, i.e., besides the object from which it got *** the message, there are no more neighbors -> acknowledge sender crl [RecNewMsgLeaf] : < A : Node | nbs : B, states : IDSTATUSPFUN, parents : IDIDPFUN, seqNos : IDINTPFUN, nbsStates : IDIDSTATUSPFUN > (msg M To A From B Src C) => < A : Node | states : assignIdStatusPFun(IDSTATUSPFUN, C, passive), parents : assignIdIdPFun(IDIDPFUN, C, B), seqNos : assignIdIntPFun(IDINTPFUN, C, M), nbsStates : assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, passive) > (ack M To B From A Src C) if forSourceSmallerOrNoSeqnoInIdIntPFun(C,M,IDINTPFUN) . *** Receiver (active) receives older message than his *** current one (wrt to a source) -> he sends the newest message to *** the sender and sets the sender active crl [ActiveRecOldMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,active),IDSTATUSPFUN), seqNos : seqNos(seqNo(C,I),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > (msg M To A From B Src C) => < A : Node | nbsStates : assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, active) > (msg I To B From A Src C) if I > M . *** Receiver (passive) receives older message than his *** current one (wrt to a source) -> he sends the newest message to *** the sender and sets the sender active, and sets himself to be *** active and to be the source of this LOCAL DIFFUSION COMPETITION crl [PassiveRecOldMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,passive),IDSTATUSPFUN), parents : IDIDPFUN, seqNos : seqNos(seqNo(C,I),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > (msg M To A From B Src C) => < A : Node | states : assignIdStatusPFun(IDSTATUSPFUN, C, active), parents : assignIdIdPFun(IDIDPFUN, C, A), nbsStates : assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, active) > (msg I To B From A Src C) if I > M . *** Message cannot be received since sender is not neighbor *** -> delete message crl [MsgNotReceivable] : < A : Node | nbs : OIDSET > (msg M To A From B Src C) => < A : Node | nbs : OIDSET > if not(inSet(B,OIDSET)) . *** receive ack for newer message -> ack current/old message crl [RecAckNewerMsg] : < A : Node | nbs : nbs(B,OIDSET), seqNos : seqNos(seqNo(C,I),IDINTPFUN) > (ack M To A From B Src C) => < A : Node | nbs : nbs(B,OIDSET) > (ack I To B From A Src C) if M > I . *** Receiver (passive) receives acknowledgment for current message *** -> do nothing, consume message rl [PassiveRecAckCurrentMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,passive),IDSTATUSPFUN), seqNos : seqNos(seqNo(C,M),IDINTPFUN) > (ack M To A From B Src C) => < A : Node | nbs : nbs(B,OIDSET) > . *** Receiver (active) receives acknowledgment for current message *** -> set the sender to passive (wrt to the source), if all neighbors *** already acknowledged this message, i.e., they are set to passive *** wrt to the source, then the receiver sets itself to passive and *** if the receiver is not the source, then also acknowledge the *** source rl [ActiveRecAckCurrentMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,active),IDSTATUSPFUN), parents : parents(parent(C,X),IDIDPFUN), seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : nbsStates(nbState(C,B,STAT1), IDIDSTATUSPFUN) > (ack M To A From B Src C) => if allNbsPassiveWRTSrcUnlessParent(IDIDSTATUSPFUN, C, X) == true then if X =/= A then < A : Node | states : states(state(C,passive), IDSTATUSPFUN), nbsStates : nbsStates(nbState(C,B,passive), IDIDSTATUSPFUN) > (ack M To X From A Src C) else < A : Node | states : states(state(C,passive), IDSTATUSPFUN), nbsStates : nbsStates(nbState(C,B,passive), IDIDSTATUSPFUN) > fi else < A : Node | nbsStates : nbsStates(nbState(C,B,passive), IDIDSTATUSPFUN) > fi . *** THIS CASE SHOULD NOT OCCUR -> TO BE PROVEN FORMALLY *** SUPERFLUOUS RULE? *** Receiver (active) receives acknowledgment for current message *** BUT it does not have a parent for that source *** -> if all neighbor states are passive wrt to *** that source, node sets itself to passive and the neighbor state *** of the neighbor from which it just got the ack to passive *** if there are still neighbors active, then it only sets the *** state of the neighbor from which it got the ack to passive crl [ActiveRecAckCurrentMsgNoParent] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,active),IDSTATUSPFUN), parents : IDIDPFUN, seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : nbsStates(nbState(C,B,STAT1), IDIDSTATUSPFUN) > (ack M To A From B Src C) => if allNbsPassiveWRTSrc(IDIDSTATUSPFUN, C) == true then < A : Node | states : states(state(C,passive),IDSTATUSPFUN), nbsStates : nbsStates(nbState(C,B,passive), IDIDSTATUSPFUN) > else < A : Node | nbsStates : nbsStates(nbState(C,B,passive), IDIDSTATUSPFUN) > fi if not(inIdIdPFun(C,IDIDPFUN)) . *** THIS CASE SHOULD NOT OCCUR -> TO BE PROVEN FORMALLY *** SUPERFLUOUS RULE? *** Receiver which has not defined status for source *** node C receives an ack for that source *** Solution here: consume ack, do nothing in response crl [UndefRecAckCurrentMsg] : < A : Node | nbs : nbs(B,OIDSET), states : IDSTATUSPFUN, seqNos : seqNos(seqNo(C,M),IDINTPFUN) > (ack M To A From B Src C) => < A : Node | nbs : nbs(B,OIDSET) > if not(inIdStatusPFun(C,IDSTATUSPFUN)) . *** Receiver (active) receives acknowledgment for older *** message -> send newer/current message to the sender and sets the *** sender to be active wrt to the source. crl [ActiveRecAckOldMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,active),IDSTATUSPFUN), seqNos : seqNos(seqNo(C,I),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > (ack M To A From B Src C) => < A : Node | nbsStates : assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, active) > (msg I To B From A Src C) if I > M . *** Receiver (passive) receives acknowledgement for older message *** than his current messages (wrt to a source) -> he sends the newest *** message to the sender and sets the sender active, sets himself to be *** active and to be the source of this LOCAL DIFFUSION COMPETITION crl [PassiveRecAckOldMsg] : < A : Node | nbs : nbs(B,OIDSET), states : states(state(C,passive),IDSTATUSPFUN), parents : IDIDPFUN, seqNos : seqNos(seqNo(C,I),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > (ack M To A From B Src C) => < A : Node | states : assignIdStatusPFun(IDSTATUSPFUN, C, active), parents : assignIdIdPFun(IDIDPFUN, C, A), nbsStates : assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, active) > (msg I To B From A Src C) if I > M . *** Receiver (active or passive) receives acknowledgement for *** source but does not have a sequence number for that source *** -> the source is added to the node's set of destinations nodes *** and node sends an ack with sequence number 0 back, *** all other fields are initialized for that node crl [RecAckForNewSource] : < A : Node | nbs : nbs(B,OIDSET), states : IDSTATUSPFUN, seqNos : IDINTPFUN, nbsStates : IDIDSTATUSPFUN > (ack M To A From B Src C) => < A : Node | states : assignIdStatusPFun(IDSTATUSPFUN, C, passive), seqNos : seqNos(seqNo(C,0),IDINTPFUN), nbsStates : assignAllIdIdStatusPFun(IDIDSTATUSPFUN, C, nbs(B,OIDSET), passive) > (ack 0 To B From A Src C) if not(inIdIntPFun(C,IDINTPFUN)) . *** Ack cannot be received since sender is not neighbor *** -> delete ack crl [AckNotReceivable] : < A : Node | nbs : OIDSET > (ack M To A From B Src C) => < A : Node | nbs : OIDSET > if not(inSet(B,OIDSET)) . *** NEW LINK rl [Link] : newlink(A,B) => (linkUpFrom A To B) (linkUpFrom B To A) . rl [MultiLinkUp] : (linkUpFrom A To B) < A : Node | seqNos : IDINTPFUN > => (multiLinkUp dom(IDINTPFUN) From A To B) < A : Node | seqNos : IDINTPFUN > . *** new link from A -> B for source C; A is active for C. Thus, send *** the latest message to B and set B to be active wrt source C crl [ActiveLink] : (forSrc C LinkUp A B) < A : Node | nbs : OIDSET, states : states(state(C,active),IDSTATUSPFUN), seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > => < A : Node | nbs : nbs(B,OIDSET), states : assignIdStatusPFunNoOverriding( states(state(C,active),IDSTATUSPFUN), B, passive), seqNos : assignIdIntPFunNoOverriding( seqNos(seqNo(C,M),IDINTPFUN), B, 0), nbsStates : assignAllIdIdStatusPFunNoOverriding( assignIdIdStatusPFun(IDIDSTATUSPFUN, C, B, active), B, nbs(B,OIDSET), passive) > (msg M To B From A Src C) if M > 0 . *** PassiveLink is similar to ActiveLink, but *** LOCAL DIFFUSION COMPETITION (PassiveLink) *** vs FORWARD (ActiveLink) *** Therefore, additionally A sets *** itself to active and to the parent of this LOCAL DIFFUSION *** COMPETITION (if there is a message to be sent) rl [PassiveLink] : (forSrc C LinkUp A B) < A : Node | nbs : OIDSET, states : states(state(C,passive),IDSTATUSPFUN), parents : IDIDPFUN, seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > => if M > 0 *** heard at least one msg from source C then < A : Node | nbs : nbs(B,OIDSET), states : assignIdStatusPFunNoOverriding( states(state(C,active),IDSTATUSPFUN), B, passive), parents : assignIdIdPFun(IDIDPFUN, C, A), seqNos : assignIdIntPFunNoOverriding( seqNos(seqNo(C,M),IDINTPFUN), B, 0), nbsStates : assignAllIdIdStatusPFunNoOverriding( assignIdIdStatusPFun( IDIDSTATUSPFUN, C, B, active), B, nbs(B,OIDSET), passive) > (msg M To B From A Src C) else < A : Node | nbs : nbs(B,OIDSET), states : assignIdStatusPFunNoOverriding( states(state(C,passive),IDSTATUSPFUN), B, passive), seqNos : assignIdIntPFunNoOverriding( seqNos(seqNo(C,M),IDINTPFUN), B, 0), nbsStates : assignAllIdIdStatusPFunNoOverriding( assignIdIdStatusPFun( IDIDSTATUSPFUN, C, B, passive), B, nbs(B,OIDSET), passive) > fi . *** FAILURE OF A LINK rl [Failure] : failure(A,B) => (linkDownFrom A To B) (linkDownFrom B To A) . rl [MultiLinkDown] : (linkDownFrom A To B) < A : Node | seqNos : IDINTPFUN > => (multiLinkDown dom(IDINTPFUN) From A To B) < A : Node | seqNos : IDINTPFUN > . *** link down from A -> B for source C; A is active for C *** delete neighbor B from neighbor set and from neighborstate set *** moreover, if all other neighbors acknowledged the latest message, then *** if A is not the parent for source C, A will acknowledge the *** message and set himself to passive wrt to C *** otherwise A only sets himself to passive wrt to C (no ack needed) crl [ActiveFailure] : (forSrc C LinkDown A B) < A : Node | nbs : OIDSET, states : states(state(C,active),IDSTATUSPFUN), parents : parents(parent(C,X), IDIDPFUN), seqNos : seqNos(seqNo(C,M),IDINTPFUN), nbsStates : IDIDSTATUSPFUN > => if allNbsPassiveWRTSrcUnlessParent( deleteIdIdStatusPFunAsNeighborForSource(IDIDSTATUSPFUN, B, C), C, X) == true then (if X =/= A then < A : Node | nbs : deleteFromSet(B,OIDSET), states : states(state(C,passive), IDSTATUSPFUN), parents : deleteIdIdPFunAsParentForSource( IDIDPFUN, B, C), nbsStates : deleteIdIdStatusPFunAsNeighborForSource( IDIDSTATUSPFUN, B, C) > (ack M To X From A Src C) else < A : Node | nbs : deleteFromSet(B,OIDSET), states : states(state(C,passive),IDSTATUSPFUN), parents : deleteIdIdPFunAsParentForSource( IDIDPFUN, B, C), nbsStates : deleteIdIdStatusPFunAsNeighborForSource( IDIDSTATUSPFUN, B, C) > fi) else < A : Node | nbs : deleteFromSet(B,OIDSET), parents : deleteIdIdPFunAsParentForSource( IDIDPFUN, B, C), nbsStates : deleteIdIdStatusPFunAsNeighborForSource( IDIDSTATUSPFUN, B, C) > fi if M > 0 . *** THIS CASE SHOULD NOT OCCUR -> TO BE PROVEN FORMALLY *** SUPERFLUOUS RULE? *** Rule for link down from A -> B for source C; A is active for C *** BUT parent for source C is not defined *** Solution here: consume LinkDown, do nothing in response crl [UndefActiveFailure] : (forSrc C LinkDown A B) < A : Node | nbs : OIDSET, states : states(state(C,active),IDSTATUSPFUN), parents : IDIDPFUN > => < A : Node | nbs : OIDSET > if not(inIdIdPFun(C,IDIDPFUN)) . *** FAILURE OF Link *** node is passive for the corresponding source rl [PassiveFailure] : (forSrc C LinkDown A B) < A : Node | nbs : OIDSET, states : states(state(C,passive),IDSTATUSPFUN), parents : IDIDPFUN, nbsStates : IDIDSTATUSPFUN > => < A : Node | nbs : deleteFromSet(B,OIDSET), parents : deleteIdIdPFunAsParentForSource(IDIDPFUN, B, C), nbsStates : deleteIdIdStatusPFunAsNeighborForSource( IDIDSTATUSPFUN, B, C) > . *** node has no entry for the corresponding source, i.e., no *** information whether it is active or passive for this source crl [FailureNoSrc] : (forSrc C LinkDown A B) < A : Node | nbs : OIDSET, states : IDSTATUSPFUN, parents : IDIDPFUN, nbsStates : IDIDSTATUSPFUN > => < A : Node | nbs : deleteFromSet(B,OIDSET), parents : deleteIdIdPFunAsParentForSource(IDIDPFUN, B, C), nbsStates : deleteIdIdStatusPFunAsNeighborForSource(IDIDSTATUSPFUN, B, C) > if not(inIdStatusPFun(C,IDSTATUSPFUN)) . endom)