From 24f17a8af81e257d18da4719506a70b234ffc0bd Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 21 Sep 2023 16:01:55 -0300 Subject: [PATCH 1/4] Fix and update ewd840 spec --- examples/.scripts/run-example.sh | 6 +- examples/README.md | 2 +- .../classic/distributed/ewd840/EWD840.tla | 6 +- .../classic/distributed/ewd840/ewd840.qnt | 194 ++++++++---------- quint/cli-tests.md | 5 +- 5 files changed, 96 insertions(+), 117 deletions(-) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index 2181b4e22..7d901d3fc 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -46,9 +46,7 @@ result () { fi # Print additional explanations - if [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" && ( "$cmd" != "parse" ) ]] ; then - printf "https://github.com/informalsystems/quint/issues/581" - elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then + if [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then printf "https://github.com/informalsystems/quint/issues/244" elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then printf "https://github.com/informalsystems/quint/issues/244" @@ -68,6 +66,8 @@ get_main () { main="--main=LamportMutex_3_10" elif [[ "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ]] ; then main="--main=ReadersWriters_5" + elif [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" ]] ; then + main="--main=ewd840_3" elif [[ "$file" == "classic/sequential/BinSearch/BinSearch.qnt" ]] ; then main="--main=BinSearch10" elif [[ "$file" == "cosmos/ics20/bank.qnt" ]] ; then diff --git a/examples/README.md b/examples/README.md index 776d23faa..41b0ad533 100644 --- a/examples/README.md +++ b/examples/README.md @@ -49,7 +49,7 @@ listed without any additional command line arguments. | Example | Syntax (`parse`) | Types (`typecheck`) | Unit tests (`test`) | Apalache (`verify`) | |---------|:----------------:|:-------------------:|:-------------------:|:-------------------:| | [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | -| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/581 | :x:https://github.com/informalsystems/quint/issues/581 | :x:https://github.com/informalsystems/quint/issues/581 | +| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/244 | :x:https://github.com/informalsystems/quint/issues/244 | | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/244 | :x:https://github.com/informalsystems/quint/issues/244 | diff --git a/examples/classic/distributed/ewd840/EWD840.tla b/examples/classic/distributed/ewd840/EWD840.tla index 018d7ec3a..7eaf5227b 100644 --- a/examples/classic/distributed/ewd840/EWD840.tla +++ b/examples/classic/distributed/ewd840/EWD840.tla @@ -150,11 +150,13 @@ AllNodesTerminateIfNoMessages == (***************************************************************************) (* Dijkstra's inductive invariant *) (***************************************************************************) -Inv == +Inv == \/ P0:: \A i \in Node : tpos < i => ~ active[i] - \/ P1:: \E j \in 0 .. tpos : color[j] = "black" + \/ P1:: \E j \in Node: (0 <= j /\ j <= tpos) => color[j] = "black" \/ P2:: tcolor = "black" + (*\/ P1:: \E j \in 0 .. tpos : color[j] = "black"*) + (***************************************************************************) (* Use the following specification to let TLC check that the predicate *) (* TypeOK /\ Inv is inductive for EWD 840: verify that it is an *) diff --git a/examples/classic/distributed/ewd840/ewd840.qnt b/examples/classic/distributed/ewd840/ewd840.qnt index 1279dd85e..6dbf574b8 100644 --- a/examples/classic/distributed/ewd840/ewd840.qnt +++ b/examples/classic/distributed/ewd840/ewd840.qnt @@ -1,12 +1,14 @@ // -*- mode: Bluespec; -*- -module EWD840 { -/***************************************************************************) -(* TLA+ specification of an algorithm for distributed termination *) -(* detection on a ring, due to Dijkstra, published as EWD 840: *) -(* Derivation of a termination detection algorithm for distributed *) -(* computations (with W.H.J.Feijen and A.J.M. van Gasteren). *) -(***************************************************************************/ +/** + * Quint spefication for EWD840: an algorithm for distributed termination + * detection on a ring, due to Dijkstra, published as EWD 840: Derivation + * of a termination detection algorithm for distributed computations (with + * W.H.J.Feijen and A.J.M. van Gasteren). + * + * Igor Konnov and Gabriela Moreira, Informal Systems, 2022-2023 + */ +module ewd840 { const N: int assume NAssumption = N.in((Nat.exclude(Set(0)))) @@ -18,35 +20,30 @@ var color: NODE -> str var tpos: NODE var tcolor: str -val Node = 0.to(N - 1) +val Nodes = 0.to(N - 1) val Color = Set("white", "black") val TypeOK = and { - active.in(setOfMaps(Node, Bool)), // status of nodes (active or passive) - color.in(setOfMaps(Node, Color)), // color of nodes - tpos.in(Node), // token position + active.in(setOfMaps(Nodes, Bool)), // status of nodes (active or passive) + color.in(setOfMaps(Nodes, Color)), // color of nodes + tpos.in(Nodes), // token position tcolor.in(Color) // token color } -/***************************************************************************) -(* Initially the token is black. The other variables may take any *) -(* "type-correct" values. *) -(***************************************************************************/ -action Init = all { - nondet a = setOfMaps(Node, Bool).oneOf() +/// Initially the token is black. The other variables may take any "type-correct" values. +action init = all { + nondet a = setOfMaps(Nodes, Bool).oneOf() active' = a, - nondet c = setOfMaps(Node, Color).oneOf() + nondet c = setOfMaps(Nodes, Color).oneOf() color' = c, - nondet n = Node.oneOf() + nondet n = Nodes.oneOf() tpos' = n, tcolor' = "black" } -/***************************************************************************) -(* Node 0 may initiate a probe when it has the token and when either it is *) -(* black or the token is black. It passes a white token to node N-1 and *) -(* paints itself white. *) -(***************************************************************************/ +/// Node 0 may initiate a probe when it has the token and when either it is +/// black or the token is black. It passes a white token to node N-1 and paints +/// itself white. action InitiateProbe = all { tpos == 0, tcolor == "black" or color.get(0) == "black", @@ -56,16 +53,14 @@ action InitiateProbe = all { active' = active, } -/***************************************************************************) -(* A node i different from 0 that possesses the token may pass it to node *) -(* i-1 under the following circumstances: *) -(* - node i is inactive or *) -(* - node i is colored black or *) -(* - the token is black. *) -(* Note that the last two conditions will result in an inconclusive round, *) -(* since the token will be black. The token will be stained if node i is *) -(* black, otherwise its color is unchanged. Node i will be made white. *) -(***************************************************************************/ +/// A node i different from 0 that possesses the token may pass it to node +/// i-1 under the following circumstances: +/// - node i is inactive or +/// - node i is colored black or +/// - the token is black. +/// Note that the last two conditions will result in an inconclusive round, +/// since the token will be black. The token will be stained if node i is +/// black, otherwise its color is unchanged. Node i will be made white. action PassToken(i) = all { tpos == i, or { @@ -79,23 +74,19 @@ action PassToken(i) = all { active' = active, } -/***************************************************************************) -(* token passing actions controlled by the termination detection algorithm *) -(***************************************************************************/ +/// Token passing actions controlled by the termination detection algorithm action System = any { InitiateProbe, - nondet i = Node.exclude(Set(0)).oneOf() + nondet i = Nodes.exclude(Set(0)).oneOf() PassToken(i), } -/***************************************************************************) -(* An active node i may activate another node j by sending it a message. *) -(* If j>i (hence activation goes against the direction of the token being *) -(* passed), then node i becomes black. *) -(***************************************************************************/ +/// An active node i may activate another node j by sending it a message. +/// If j>i (hence activation goes against the direction of the token being +/// passed), then node i becomes black. action SendMsg(i) = all { active.get(i), - nondet j = Node.exclude(Set(i)).oneOf() + nondet j = Nodes.exclude(Set(i)).oneOf() all { active' = active.set(j, true), color' = color.setBy(i, (old => if (j > i) "black" else old)), @@ -104,9 +95,7 @@ action SendMsg(i) = all { } } -/***************************************************************************) -(* Any active node may become inactive at any moment. *) -(***************************************************************************/ +/// Any active node may become inactive at any moment. action Deactivate(i) = all { active.get(i), active' = active.set(i, false), @@ -115,20 +104,16 @@ action Deactivate(i) = all { tcolor' = tcolor, } -/***************************************************************************) -(* actions performed by the underlying algorithm *) -(***************************************************************************/ +/// Actions performed by the underlying algorithm action Environment = - val i = oneOf(Node) + nondet i = oneOf(Nodes) any { SendMsg(i), Deactivate(i), } -/***************************************************************************) -(* next-state relation: disjunction of above actions *) -(***************************************************************************/ -action Next = any { +/// Next-state relation: disjunction of above actions +action step = any { System, Environment, } @@ -139,85 +124,80 @@ val vars = (active, color, tpos, tcolor) //----------------------------------------------------------------------------- -/***************************************************************************) -(* Non-properties, useful for validating the specification with TLC. *) -(***************************************************************************/ +/* Non-properties, useful for validating the specification with `run` and `verify`. */ + val TokenAlwaysBlack = tcolor == "black" temporal NeverChangeColor = always((color' = color).orKeep(vars)) -/***************************************************************************) -(* Main safety property: if there is a white token at node 0 then every *) -(* node is inactive. *) -(***************************************************************************/ +/// Main safety property: if there is a white token at node 0 then every node is +/// inactive. val terminationDetected = and { tpos == 0 and tcolor == "white", color.get(0) == "white" and not(active.get(0)) } val TerminationDetection = - terminationDetected implies Node.forall(i => not(active.get(i))) + terminationDetected implies Nodes.forall(i => not(active.get(i))) -/***************************************************************************) -(* Liveness property: termination is eventually detected. *) -(***************************************************************************/ +/// Liveness property: termination is eventually detected. temporal Liveness = - always(Node.forall(i => not(active.get(i))) implies eventually(terminationDetected)) + always(Nodes.forall(i => not(active.get(i))) implies eventually(terminationDetected)) -/***************************************************************************) -(* The following property asserts that when every process always *) -(* eventually terminates then eventually termination will be detected. *) -(* It does not hold since processes can wake up each other. *) -(***************************************************************************/ +/// The following property asserts that when every process always eventually +/// terminates then eventually termination will be detected. It does not hold +/// since processes can wake up each other. temporal FalseLiveness = - always(Node.forall(i => always(eventually(not(active.get(i))))) + always(Nodes.forall(i => always(eventually(not(active.get(i))))) implies eventually(terminationDetected)) -/***************************************************************************) -(* The following property says that eventually all nodes will terminate *) -(* assuming that from some point onwards no messages are sent. It is *) -(* not supposed to hold: any node may indefinitely perform local *) -(* computations. However, this property is verified if the fairness *) -(* condition WF_vars(Next) is used instead of only WF_vars(System) that *) -(* requires fairness of the actions controlled by termination detection. *) -(***************************************************************************/ -temporal SpecWFNext = Init and always(Next.orKeep(vars) and Next.weakFair(vars)) - -temporal AllNodesTerminateIfNoMessages = ( - eventually(always( - Node.forall(i => not(SendMsg(i))).orKeep(vars) - )) implies eventually(Node.forall(i => not(active.get(i)))) -) - -/***************************************************************************) -(* Dijkstra's inductive invariant *) -(***************************************************************************/ +/// The following property says that eventually all nodes will terminate +/// assuming that from some point onwards no messages are sent. It is not +/// supposed to hold: any node may indefinitely perform local computations. +/// However, this property is verified if the fairness condition WF_vars(Next) +/// is used instead of only WF_vars(System) that requires fairness of the +/// actions controlled by termination detection. +/// +/// Quint translation note: we cannot add `Init` to this property since, in quint, +/// it is an action - not a predicate +temporal SpecWFNext = always(step.orKeep(vars) and step.weakFair(vars)) // and Init + +// The following property is not expressible in quint (for now), as it negates an action +// temporal AllNodesTerminateIfNoMessages = ( +// eventually(always( +// Node.forall(i => not(SendMsg(i))).orKeep(vars) +// )) implies eventually(Node.forall(i => not(active.get(i)))) +// ) + +/// Dijkstra's inductive invariant val Inv = or { - Node.forall(i => tpos < i implies not(active.get(i))), - 0.to(tpos).exists(j => color.get(j) == "black"), + Nodes.forall(i => tpos < i implies not(active.get(i))), + Nodes.exists(j => (0 <= j and j <= tpos) implies color.get(j) == "black"), tcolor == "black" } -/***************************************************************************) -(* Use the following specification to let TLC check that the predicate *) -(* TypeOK /\ Inv is inductive for EWD 840: verify that it is an *) -(* (ordinary) invariant of a specification obtained by replacing the *) -(* initial condition by that conjunction. *) -(***************************************************************************/ +/// Use the following specification to check that the predicate TypeOK /\ Inv is +/// inductive for EWD 840: verify that it is an (ordinary) invariant of a +/// specification obtained by replacing the initial condition by that +/// conjunction. temporal CheckInductiveSpec = and { TypeOK, Inv, - always(Next.orKeep(vars)) + always(step.orKeep(vars)) } -/***************************************************************************) -(* The algorithm implements the high-level specification of termination *) -(* detection in a ring with synchronous communication between nodes. *) -(* Note that the parameters of the module SyncTerminationDetection are *) -(* instantiated by the symbols of the same name in the present module. *) -(***************************************************************************/ +// There is no refinment in quint, so we can't verify the following theorem. + +// The algorithm implements the high-level specification of termination +// detection in a ring with synchronous communication between nodes. Note that +// the parameters of the module SyncTerminationDetection are instantiated by +// the symbols of the same name in the present module. // module TD = SyncTerminationDetection(*) //THEOREM Spec => TD!Spec } + +module ewd840_3 { + import ewd840(N=3).* +} diff --git a/quint/cli-tests.md b/quint/cli-tests.md index d011569c4..5ef78b8c2 100644 --- a/quint/cli-tests.md +++ b/quint/cli-tests.md @@ -60,11 +60,8 @@ bash - ### OK on typecheck EWD840 This example was pointing to Paxos. Now it does not typecheck. -See [#581](https://github.com/informalsystems/quint/issues/581). -Temporarily disabled. - - + quint typecheck ../examples/classic/distributed/ewd840/ewd840.qnt ### OK on parse Tendermint From 7c51ff70c00bf5807e85cc545beb2f5b9966a9a9 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 21 Sep 2023 16:07:18 -0300 Subject: [PATCH 2/4] Rename references to Init and Next in comments --- examples/classic/distributed/ewd840/ewd840.qnt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/classic/distributed/ewd840/ewd840.qnt b/examples/classic/distributed/ewd840/ewd840.qnt index 6dbf574b8..6afe52dbc 100644 --- a/examples/classic/distributed/ewd840/ewd840.qnt +++ b/examples/classic/distributed/ewd840/ewd840.qnt @@ -120,7 +120,7 @@ action step = any { val vars = (active, color, tpos, tcolor) -// temporal Spec = Init and always(Next.orKeep(vars) and System.weakFair(vars)) +// temporal Spec = init and always(step.orKeep(vars) and System.weakFair(vars)) //----------------------------------------------------------------------------- @@ -154,13 +154,13 @@ temporal FalseLiveness = /// The following property says that eventually all nodes will terminate /// assuming that from some point onwards no messages are sent. It is not /// supposed to hold: any node may indefinitely perform local computations. -/// However, this property is verified if the fairness condition WF_vars(Next) +/// However, this property is verified if the fairness condition WF_vars(step) /// is used instead of only WF_vars(System) that requires fairness of the /// actions controlled by termination detection. /// -/// Quint translation note: we cannot add `Init` to this property since, in quint, +/// Quint translation note: we cannot add `init` to this property since, in quint, /// it is an action - not a predicate -temporal SpecWFNext = always(step.orKeep(vars) and step.weakFair(vars)) // and Init +temporal SpecWFstep = always(step.orKeep(vars) and step.weakFair(vars)) // and init // The following property is not expressible in quint (for now), as it negates an action // temporal AllNodesTerminateIfNoMessages = ( From c26c7a6a818f3411856b67bd6852394078264b1d Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 7 Nov 2023 09:39:36 -0300 Subject: [PATCH 3/4] Update comments and add issue reference --- .../classic/distributed/ewd840/ewd840.qnt | 26 ++++++++++--------- 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/examples/classic/distributed/ewd840/ewd840.qnt b/examples/classic/distributed/ewd840/ewd840.qnt index 6afe52dbc..69bfa9b60 100644 --- a/examples/classic/distributed/ewd840/ewd840.qnt +++ b/examples/classic/distributed/ewd840/ewd840.qnt @@ -120,6 +120,8 @@ action step = any { val vars = (active, color, tpos, tcolor) +// FIXME(#1236): we cannot add `init` to this property since, in quint, it is an +// action - not a predicate // temporal Spec = init and always(step.orKeep(vars) and System.weakFair(vars)) //----------------------------------------------------------------------------- @@ -151,18 +153,18 @@ temporal FalseLiveness = always(Nodes.forall(i => always(eventually(not(active.get(i))))) implies eventually(terminationDetected)) -/// The following property says that eventually all nodes will terminate -/// assuming that from some point onwards no messages are sent. It is not -/// supposed to hold: any node may indefinitely perform local computations. -/// However, this property is verified if the fairness condition WF_vars(step) -/// is used instead of only WF_vars(System) that requires fairness of the -/// actions controlled by termination detection. -/// -/// Quint translation note: we cannot add `init` to this property since, in quint, -/// it is an action - not a predicate -temporal SpecWFstep = always(step.orKeep(vars) and step.weakFair(vars)) // and init - -// The following property is not expressible in quint (for now), as it negates an action +// The property `AllNodesTerminateIfNoMessages` says that eventually all nodes +// will terminate assuming that from some point onwards no messages are sent. +// It is not supposed to hold: any node may indefinitely perform local +// computations. However, this property is verified if the fairness condition +// WF_vars(step) is used instead of only WF_vars(System) that requires fairness +// of the actions controlled by termination detection. +// +// FIXME(#1236): we cannot add `init` to this property since, in quint, it is an +// action - not a predicate +// temporal SpecWFstep = always(step.orKeep(vars) and step.weakFair(vars)) and init + +// Not expressible in quint (for now), as it negates an action // temporal AllNodesTerminateIfNoMessages = ( // eventually(always( // Node.forall(i => not(SendMsg(i))).orKeep(vars) From 831f0185ea06822ebfb47430a4243db01983ec0c Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 7 Nov 2023 09:42:43 -0300 Subject: [PATCH 4/4] Reference `orKeep` argument issue --- examples/classic/distributed/ewd840/ewd840.qnt | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/classic/distributed/ewd840/ewd840.qnt b/examples/classic/distributed/ewd840/ewd840.qnt index 69bfa9b60..5aa2b3686 100644 --- a/examples/classic/distributed/ewd840/ewd840.qnt +++ b/examples/classic/distributed/ewd840/ewd840.qnt @@ -118,6 +118,7 @@ action step = any { Environment, } +// FIXME(#630): OrKeep takes an arbitrary type for now val vars = (active, color, tpos, tcolor) // FIXME(#1236): we cannot add `init` to this property since, in quint, it is an