From 448d36ef3e380795c56e781d5565e23450e93593 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 24 Apr 2023 11:47:08 -0700 Subject: [PATCH] Refactor (shorten) EWD998ChanTrace by reusing existing sub-actions of EWD998Chan where possible. --- specifications/ewd998/EWD998ChanTrace.tla | 90 +++++++---------------- 1 file changed, 26 insertions(+), 64 deletions(-) diff --git a/specifications/ewd998/EWD998ChanTrace.tla b/specifications/ewd998/EWD998ChanTrace.tla index c5461b53..ca3ba7aa 100644 --- a/specifications/ewd998/EWD998ChanTrace.tla +++ b/specifications/ewd998/EWD998ChanTrace.tla @@ -37,6 +37,7 @@ TraceLog == TraceInit == /\ Init!1 /\ Init!2 + \* We happen to know that in the implementation all nodes are initially empty and white. /\ active \in [Node -> {TRUE}] /\ color \in [Node -> {"white"}] @@ -61,45 +62,27 @@ PayloadPred(msg) == IsInitiateToken(l) == \* Log statement was printed by the sender (initiator). /\ l.event = ">" - /\ LET msg == l.pkt.msg - snd == l.pkt.snd - rcv == l.pkt.rcv IN - \* Log statement is about a token message. - /\ msg.type = "tok" - \* Log statement show N-1 to be receiver and 0 to be the sender. - /\ rcv = N - 1 - /\ snd = 0 - \* The senders's inbox contains a tok message in the current state. - /\ \E idx \in DOMAIN inbox[snd]: - inbox[snd][idx].type = "tok" - \* The senders's inbox contains no longer the token in the next state. - /\ snd # rcv => \A idx \in DOMAIN inbox'[snd]: - inbox'[snd][idx].type # "tok" - \* Sender has *not* to be inactive to initiate the token! - /\ UNCHANGED <> + \* Log statement is about a token message. + /\ l.pkt.msg.type = "tok" + \* Log statement show N-1 to be receiver and 0 to be the sender. + /\ l.pkt.rcv = N - 1 + /\ l.pkt.snd = 0 + /\ <>_vars IsPassToken(l) == \* Log statement was printed by the sender. /\ l.event = ">" - /\ LET msg == l.pkt.msg - snd == l.pkt.snd - rcv == l.pkt.rcv IN - \* Log statement is about a token message. - /\ msg.type = "tok" - \* The sender's inbox contains a tok message in the current state. - /\ \E idx \in DOMAIN inbox[snd]: - /\ inbox[snd][idx].type = "tok" - /\ inbox[snd][idx].q + counter[snd] = msg.q - /\ msg.color = IF color[snd] = "black" - THEN "black" - ELSE inbox[snd][idx].color - \* The sender's inbox contains no tok message in the next state. - /\ \A idx \in DOMAIN inbox'[snd]: - inbox'[snd][idx].type # "tok" - \* Sender has to be inactive to pass the token, i.e., - /\ ~active[snd] - /\ UNCHANGED <> + \* Log statement is about a token message. + /\ l.pkt.msg.type = "tok" + /\ LET snd == l.pkt.snd IN + \* The high-level spec precludes the initiator from passing the token in the + \* the System formula by remove the initiator from the set of all nodes. Here, + \* we model this by requiring that the sender is not the initiator. + /\ l.pkt.snd > 0 + /\ <>_vars +\* Note that there is no corresponding sub-action in the high-level spec! This constraint + \* is true of any sub-action that appends a tok message to the receiver's inbox. IsRecvToken(l) == \* Log statement was printed by the receiver. /\ l.event = "<" @@ -120,47 +103,26 @@ IsRecvToken(l) == IsSendMsg(l) == \* Log statement was printed by the sender. /\ l.event = ">" - /\ LET msg == l.pkt.msg - rcv == l.pkt.rcv - snd == l.pkt.snd IN - \* Log statement is about a payload message. - /\ msg.type = "pl" - \* Sender has to be active to send a message. - /\ active[snd] - \* Sender increments its counter. - /\ counter'[snd] = counter[snd] + 1 - \* The sender's inbox remains unchanged, bu the receivers's inbox contains one more + \* Log statement is about a payload message. + /\ l.pkt.msg.type = "pl" + /\ <>_vars + /\ LET rcv == l.pkt.rcv IN + \* The sender's inbox remains unchanged, but the receivers's inbox contains one more \* pl message. In the implementation, the message is obviously in flight, i.e. it \* is send via the wire to the receiver. However, the SendMsg action models it \* such that the message is atomically appended to the receiver's inbox. - /\ Len(SelectSeq(inbox[rcv], PayloadPred)) < Len(SelectSeq(inbox'[rcv], PayloadPred)) - /\ UNCHANGED <> + Len(SelectSeq(inbox[rcv], PayloadPred)) < Len(SelectSeq(inbox'[rcv], PayloadPred)) IsRecvMsg(l) == \* Log statement was printed by the receiver. /\ l.event = "<" - /\ LET msg == l.pkt.msg - rcv == l.pkt.rcv IN - \* Log statement is about a payload message. - /\ msg.type = "pl" - \* Receiving a message activates, decrements the counter, and changes the color of the - \* receiver. - /\ active' = [active EXCEPT ![rcv] = TRUE] - /\ counter' = [counter EXCEPT ![rcv] = @ - 1] - /\ color' = [ color EXCEPT ![rcv] = "black" ] - \* Even though the name of the action suggests that there is one *more* pl message in - \* the receiver's inbox, the action RecvMsg removes the pl message from the node's - \* inbox. Thus, thee receiver's inbox contains one less pl message in the next state. - /\ Len(SelectSeq(inbox[rcv], PayloadPred)) > Len(SelectSeq(inbox'[rcv], PayloadPred)) + /\ l.pkt.msg .type = "pl" + /\ <>_vars IsDeactivate(l) == \* Log statement was printed by the receiver. /\ l.event = "d" - /\ LET node == l.node IN - \* The receiver and only the receiver transitions to inactive. - /\ active[node] - /\ active' = [active EXCEPT ![node] = FALSE] - /\ UNCHANGED <> + /\ <>_vars IsTrm(l) == \* "trm" messages are not part of EWD998, and, thus, not modeled in EWD998Chan. We map