Skip to content

Commit

Permalink
Merge pull request #1178 from informalsystems/gabriela/ewd840-adaptat…
Browse files Browse the repository at this point in the history 
…ions

Fix and update ewd840 spec
  • Loading branch information
@bugarela
bugarela authored Nov 8, 2023
2 parents 3b0209c + b28084b commit 766b7de
Show file tree
Hide file tree
Showing 5 changed files with 100 additions and 118 deletions.
6 changes: 3 additions & 3 deletions examples/.scripts/run-example.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,7 @@ result () {
fi

# Print additional explanations
if [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" && ( "$cmd" != "parse" ) ]] ; then
printf "<sup>https://github.com/informalsystems/quint/issues/581</sup>"
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 "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
Expand All @@ -66,6 +64,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
Expand Down
2 changes: 1 addition & 1 deletion examples/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:<sup>https://github.com/informalsystems/quint/issues/581</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/581</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/581</sup> |
| [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:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
Expand Down
6 changes: 4 additions & 2 deletions examples/classic/distributed/ewd840/EWD840.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
199 changes: 91 additions & 108 deletions examples/classic/distributed/ewd840/ewd840.qnt
View file
Original file line number Diff line number Diff line change
@@ -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))))
Expand All @@ -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",
Expand All @@ -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 {
Expand All @@ -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)),
Expand All @@ -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),
Expand All @@ -115,109 +104,103 @@ 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,
}

// FIXME(#630): OrKeep takes an arbitrary type for now
val vars = (active, color, tpos, tcolor)

// temporal Spec = Init and always(Next.orKeep(vars) and System.weakFair(vars))
// 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))

//-----------------------------------------------------------------------------

/***************************************************************************)
(* 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 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)
// )) 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).*
}
5 changes: 1 addition & 4 deletions quint/cli-tests.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

<!-- test check EWD840 - Types & Effects -->
<!-- !test check EWD840 - Types & Effects -->
quint typecheck ../examples/classic/distributed/ewd840/ewd840.qnt

### OK on parse Tendermint
Expand Down

0 comments on commit 766b7de

Please sign in to comment.