From 045af53ebd1ca66403b047b814ecacbe4d346f72 Mon Sep 17 00:00:00 2001 From: mahtab75 Date: Wed, 15 Jan 2025 01:37:36 -0500 Subject: [PATCH 1/9] Add Dijkstra's Stabilizing Token Ring example in Quint --- examples/classic/Dijkstra/Dijkstra.qnt | 156 +++++++++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 examples/classic/Dijkstra/Dijkstra.qnt diff --git a/examples/classic/Dijkstra/Dijkstra.qnt b/examples/classic/Dijkstra/Dijkstra.qnt new file mode 100644 index 000000000..1bfb0eb12 --- /dev/null +++ b/examples/classic/Dijkstra/Dijkstra.qnt @@ -0,0 +1,156 @@ +// -*- mode: Bluespec; -*- +/** + * Dijkstra's Stabilizing Token Ring (EWD426) + * This implementation ensures that exactly one token circulates in a ring of nodes, self-stabilizing to this state. + * + * Mahtab Norouzi, Informal Systems, 2024 + */ + +module token_ring { + // Number of nodes in the ring + const N: int + const K: int // K > N, ensures the state space is larger than the number of nodes + + // Variable: Mapping of node indices to their states + var nodes_to_states: int -> int + + // Pure function to check if a node has the token + pure def has_token(nodes: int -> int, index: int): bool = { + val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring + nodes.get(index) == (nodes.get(predecessor_index) + 1) % K + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + to(0, N - 1).filter(i => has_token(nodes, i)).size() + } + + // Pure function to update the state of a specific node + pure def update_node(nodes: int -> int, index: int): int -> int = { + val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring + val updated_state = (nodes.get(predecessor_index) + 1) % K + nodes.set(index, updated_state) + } + + /// Initialize all nodes with random states + action init = all { + // Step 1: Generate a nondeterministic mapping of indices to random states + nondet random = to(0, N - 1).setOfMaps(to(0, K - 1)).oneOf() + // Step 2: Map the random states to nodes + nodes_to_states' = to(0, N - 1).mapBy(i => random.get(i)) + } + + /// Update a single random node based on its predecessor + action update = { + nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node + nodes_to_states' = update_node(nodes_to_states, node_to_update) + } + + /// Step action to simulate the system + action step = any { + update + } + + // Invariants + /// Ensure exactly one token exists in the ring + val one_token_invariant = { + count_tokens(nodes_to_states) == 1 + } + + // Temporal properties + /// Convergence: The system eventually stabilizes with exactly one token + temporal convergence = eventually (count_tokens(nodes_to_states) == 1) + + /// Closure: Once stabilized, the system remains with one token + temporal closure = + always (count_tokens(nodes_to_states) == 1 + implies always (count_tokens(nodes_to_states) == 1)) + + /// Check whether the convergence witness holds + val convergence_witness = { + count_tokens(nodes_to_states) > 1 + } +} + +module token_ring_three_four_state { + + import token_ring as tr + + // Number of nodes in the ring + const N: int + + // Variable: Mapping of node indices to their states + var nodes_to_states: int -> int + + // --- Three-state machine solution --- + /** + * Each machine state is represented by an integer `S` such that 0 ≤ S < 3. + * The rules for transitions depend on the position (bottom, top, or other nodes). + */ + + // Transition function for the three-state machine + pure def three_state_transition(nodes: int -> int, index: int): int = { + val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring + val successor_state = (nodes.get(index) + 1) % 3 // Compute the next state modulo 3 + + if (index == 0) { + // Bottom node logic + if (successor_state == 2) (nodes.get(predecessor_index) + 2) % 3 else nodes.get(index) + } else if (index == N - 1) { + // Top node logic + if (nodes.get(predecessor_index) % 3 == 2) (nodes.get(predecessor_index) + 1) % 3 else nodes.get(index) + } else { + // Other nodes + if (nodes.get(predecessor_index) % 3 == 2) (nodes.get(predecessor_index) + 1) % 3 else nodes.get(index) + } + } + + /// Action for the three-state machine + action three_state_update = { + nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node + nodes_to_states' = nodes_to_states.set(node_to_update, three_state_transition(nodes_to_states, node_to_update)) + } + + // --- Four-state machine solution --- + /** + * Each machine state is represented by two booleans `xS` and `upS`. + * States are defined as (xS, upS) where: + * - For the bottom machine, upS = true by definition. + * - For the top machine, upS = false by definition. + */ + + // Pure function to handle the four-state transition + pure def four_state_transition(nodes: int -> int, index: int): (bool, bool) = { + val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring + val xS = nodes.get(index) // Current state (interpreted as a pair) + val upS = if (index == 0) true else if (index == N - 1) false else xS % 2 == 0 + + if (index == 0) { + // Bottom node + if (xS == 1 and upS) (0, true) else (xS, upS) + } else if (index == N - 1) { + // Top node + if (xS == 0 and not(upS)) (1, false) else (xS, upS) + } else { + // Other nodes + if (xS == 0 and not(upS)) (1, true) else (xS, upS) + } + } + + /// Action for the four-state machine + action four_state_update = { + nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node + val updated_state = four_state_transition(nodes_to_states, node_to_update) + nodes_to_states' = nodes_to_states.set(node_to_update, updated_state) + } + + /// Step action for both solutions + action step = any { + three_state_update, + four_state_update + } + + // Temporal properties for three-state and four-state machines + temporal convergence_three_state = eventually (tr.count_tokens(nodes_to_states) == 1) + temporal convergence_four_state = eventually (tr.count_tokens(nodes_to_states) == 1) +} From 0951661becadab5de318d64a50940399a8a1072b Mon Sep 17 00:00:00 2001 From: mahtab75 Date: Tue, 21 Jan 2025 08:19:07 -0500 Subject: [PATCH 2/9] Added 3state and 4state --- examples/classic/Dijkstra/Dijkstra.qnt | 108 +++-------------------- examples/classic/Dijkstra/Dijkstra_3.qnt | 38 ++++++++ examples/classic/Dijkstra/Dijkstra_4.qnt | 36 ++++++++ 3 files changed, 85 insertions(+), 97 deletions(-) create mode 100644 examples/classic/Dijkstra/Dijkstra_3.qnt create mode 100644 examples/classic/Dijkstra/Dijkstra_4.qnt diff --git a/examples/classic/Dijkstra/Dijkstra.qnt b/examples/classic/Dijkstra/Dijkstra.qnt index 1bfb0eb12..d977c72a8 100644 --- a/examples/classic/Dijkstra/Dijkstra.qnt +++ b/examples/classic/Dijkstra/Dijkstra.qnt @@ -34,123 +34,37 @@ module token_ring { /// Initialize all nodes with random states action init = all { - // Step 1: Generate a nondeterministic mapping of indices to random states nondet random = to(0, N - 1).setOfMaps(to(0, K - 1)).oneOf() - // Step 2: Map the random states to nodes nodes_to_states' = to(0, N - 1).mapBy(i => random.get(i)) } /// Update a single random node based on its predecessor action update = { - nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node + nondet node_to_update = to(0, N - 1).oneOf() nodes_to_states' = update_node(nodes_to_states, node_to_update) } - /// Step action to simulate the system action step = any { update } // Invariants - /// Ensure exactly one token exists in the ring - val one_token_invariant = { - count_tokens(nodes_to_states) == 1 - } + // val one_token_invariant = { + // count_tokens(nodes_to_states) == 1 + // } // Temporal properties - /// Convergence: The system eventually stabilizes with exactly one token temporal convergence = eventually (count_tokens(nodes_to_states) == 1) + temporal closure = always (count_tokens(nodes_to_states) == 1 implies always (count_tokens(nodes_to_states) == 1)) - /// Closure: Once stabilized, the system remains with one token - temporal closure = - always (count_tokens(nodes_to_states) == 1 - implies always (count_tokens(nodes_to_states) == 1)) - - /// Check whether the convergence witness holds + /// check whether witness is invariant. val convergence_witness = { count_tokens(nodes_to_states) > 1 } } +// write the command +//temporal properties are not verified -module token_ring_three_four_state { - - import token_ring as tr - - // Number of nodes in the ring - const N: int - - // Variable: Mapping of node indices to their states - var nodes_to_states: int -> int - - // --- Three-state machine solution --- - /** - * Each machine state is represented by an integer `S` such that 0 ≤ S < 3. - * The rules for transitions depend on the position (bottom, top, or other nodes). - */ - - // Transition function for the three-state machine - pure def three_state_transition(nodes: int -> int, index: int): int = { - val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring - val successor_state = (nodes.get(index) + 1) % 3 // Compute the next state modulo 3 - - if (index == 0) { - // Bottom node logic - if (successor_state == 2) (nodes.get(predecessor_index) + 2) % 3 else nodes.get(index) - } else if (index == N - 1) { - // Top node logic - if (nodes.get(predecessor_index) % 3 == 2) (nodes.get(predecessor_index) + 1) % 3 else nodes.get(index) - } else { - // Other nodes - if (nodes.get(predecessor_index) % 3 == 2) (nodes.get(predecessor_index) + 1) % 3 else nodes.get(index) - } - } - - /// Action for the three-state machine - action three_state_update = { - nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node - nodes_to_states' = nodes_to_states.set(node_to_update, three_state_transition(nodes_to_states, node_to_update)) - } - - // --- Four-state machine solution --- - /** - * Each machine state is represented by two booleans `xS` and `upS`. - * States are defined as (xS, upS) where: - * - For the bottom machine, upS = true by definition. - * - For the top machine, upS = false by definition. - */ - - // Pure function to handle the four-state transition - pure def four_state_transition(nodes: int -> int, index: int): (bool, bool) = { - val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring - val xS = nodes.get(index) // Current state (interpreted as a pair) - val upS = if (index == 0) true else if (index == N - 1) false else xS % 2 == 0 - - if (index == 0) { - // Bottom node - if (xS == 1 and upS) (0, true) else (xS, upS) - } else if (index == N - 1) { - // Top node - if (xS == 0 and not(upS)) (1, false) else (xS, upS) - } else { - // Other nodes - if (xS == 0 and not(upS)) (1, true) else (xS, upS) - } - } - - /// Action for the four-state machine - action four_state_update = { - nondet node_to_update = to(0, N - 1).oneOf() // Pick a random node - val updated_state = four_state_transition(nodes_to_states, node_to_update) - nodes_to_states' = nodes_to_states.set(node_to_update, updated_state) - } - - /// Step action for both solutions - action step = any { - three_state_update, - four_state_update - } - - // Temporal properties for three-state and four-state machines - temporal convergence_three_state = eventually (tr.count_tokens(nodes_to_states) == 1) - temporal convergence_four_state = eventually (tr.count_tokens(nodes_to_states) == 1) -} +module Dijkstra { + import token_ring(N = 5, K = 7).* +} \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_3.qnt b/examples/classic/Dijkstra/Dijkstra_3.qnt new file mode 100644 index 000000000..5ec0f1c42 --- /dev/null +++ b/examples/classic/Dijkstra/Dijkstra_3.qnt @@ -0,0 +1,38 @@ + + +module token_ring_three_state { + + // import token_ring as token_ring from "Dijkstra" + + import token_ring.* from "Dijkstra" + export token_ring.* + // Transition function for the three-state machine + pure def three_state_transition(nodes: int -> int, index: int): int = { + val predecessor_index = if (index == 0) N - 1 else index - 1 + val current_state = nodes.get(index) + val predecessor_state = nodes.get(predecessor_index) + + if (index == 0) { + // Bottom node logic + if (predecessor_state % 3 == 2) (predecessor_state + 2) % 3 else current_state + } else if (index == N - 1) { + // Top node logic + if (predecessor_state % 3 == 2) (predecessor_state + 1) % 3 else current_state + } else { + // Other nodes + if (predecessor_state % 3 == 2) (predecessor_state + 1) % 3 else current_state + } + } + + /// Action for the three-state machine + action three_state_update = { + nondet node_to_update = to(0, N - 1).oneOf() + nodes_to_states' = nodes_to_states.set(node_to_update, three_state_transition(nodes_to_states, node_to_update)) + } + + temporal convergence_three_state = eventually (count_tokens(nodes_to_states) == 1) +} + +module Dijkstra_3 { + import token_ring_three_state(N = 5, K = 7).* +} \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_4.qnt b/examples/classic/Dijkstra/Dijkstra_4.qnt new file mode 100644 index 000000000..bc8fb3819 --- /dev/null +++ b/examples/classic/Dijkstra/Dijkstra_4.qnt @@ -0,0 +1,36 @@ + +module token_ring_four_state { + + import token_ring.* from "Dijkstra" + export token_ring.* + + // Pure function to handle the four-state transition + pure def four_state_transition(nodes: int -> int, index: int): int = { + val predecessor_index = if (index == 0) N - 1 else index - 1 + val xS = nodes.get(index) + val predecessor_xS = nodes.get(predecessor_index) + + if (index == 0) { + // Bottom node + if (xS == 1) 0 else xS + } else if (index == N - 1) { + // Top node + if (xS == 0) 1 else xS + } else { + // Other nodes + if (xS == 0) 1 else xS + } + } + + /// Action for the four-state machine + action four_state_update = { + nondet node_to_update = to(0, N - 1).oneOf() + nodes_to_states' = nodes_to_states.set(node_to_update, four_state_transition(nodes_to_states, node_to_update)) + } + + temporal convergence_four_state = eventually (count_tokens(nodes_to_states) == 1) +} + +module Dijkstra_4 { + import token_ring_four_state(N = 5, K = 7).* +} \ No newline at end of file From ec6673e76eb6b482f14731d2cdd41cd0e3134a2d Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Fri, 24 Jan 2025 15:14:57 +0100 Subject: [PATCH 3/9] fixed and unfied encoding --- examples/classic/Dijkstra/Dijkstra.qnt | 88 +++++++++-------- examples/classic/Dijkstra/Dijkstra_3.qnt | 111 ++++++++++++++++----- examples/classic/Dijkstra/Dijkstra_4.qnt | 119 ++++++++++++++++++----- 3 files changed, 235 insertions(+), 83 deletions(-) diff --git a/examples/classic/Dijkstra/Dijkstra.qnt b/examples/classic/Dijkstra/Dijkstra.qnt index d977c72a8..eb2a9339a 100644 --- a/examples/classic/Dijkstra/Dijkstra.qnt +++ b/examples/classic/Dijkstra/Dijkstra.qnt @@ -1,70 +1,82 @@ // -*- mode: Bluespec; -*- /** * Dijkstra's Stabilizing Token Ring (EWD426) - * This implementation ensures that exactly one token circulates in a ring of nodes, self-stabilizing to this state. + * K state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a ring of nodes, * - * Mahtab Norouzi, Informal Systems, 2024 + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 */ module token_ring { // Number of nodes in the ring const N: int - const K: int // K > N, ensures the state space is larger than the number of nodes + const K: int // K >= N, ensures the state space is larger than the number of nodes + + val bottom = 0 + val top = N // Variable: Mapping of node indices to their states - var nodes_to_states: int -> int + var system: int -> int // Pure function to check if a node has the token - pure def has_token(nodes: int -> int, index: int): bool = { - val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring - nodes.get(index) == (nodes.get(predecessor_index) + 1) % K - } + pure def has_token(nodes: int -> int, index: int): bool = + if (index == bottom) + nodes.get(bottom) == nodes.get(top) + else + not(nodes.get(index) == nodes.get(index - 1)) - // Pure function to count how many tokens exist - pure def count_tokens(nodes: int -> int): int = { - to(0, N - 1).filter(i => has_token(nodes, i)).size() - } // Pure function to update the state of a specific node - pure def update_node(nodes: int -> int, index: int): int -> int = { - val predecessor_index = if (index == 0) N - 1 else index - 1 // Wrap-around for the ring - val updated_state = (nodes.get(predecessor_index) + 1) % K - nodes.set(index, updated_state) - } + pure def state_transition(nodes: int -> int, index: int): int = + if (not(has_token(nodes, index))) + nodes.get(index) + else + if (index == bottom) + (nodes.get(bottom) +1) % K + else + nodes.get(index - 1) + + /// Initialize all nodes with random states action init = all { - nondet random = to(0, N - 1).setOfMaps(to(0, K - 1)).oneOf() - nodes_to_states' = to(0, N - 1).mapBy(i => random.get(i)) + nondet random = to(0, N).setOfMaps(to(0, K - 1)).oneOf() + system' = to(0, N).mapBy(i => random.get(i)) } - /// Update a single random node based on its predecessor - action update = { - nondet node_to_update = to(0, N - 1).oneOf() - nodes_to_states' = update_node(nodes_to_states, node_to_update) + /// Update a single random active node + action step = { + nondet node = to(0, N) .filter(i => has_token(system, i)) + .oneOf() + system' = system.set(node, state_transition(system, node) ) } - action step = any { - update - } - // Invariants - // val one_token_invariant = { - // count_tokens(nodes_to_states) == 1 - // } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + to(0, N).filter(i => has_token(nodes, i)).size() + } // Temporal properties - temporal convergence = eventually (count_tokens(nodes_to_states) == 1) - temporal closure = always (count_tokens(nodes_to_states) == 1 implies always (count_tokens(nodes_to_states) == 1)) + temporal convergence = eventually (count_tokens(system) == 1) + temporal closure = always (count_tokens(system) == 1 implies always (count_tokens(system) == 1)) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> int): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) - /// check whether witness is invariant. - val convergence_witness = { - count_tokens(nodes_to_states) > 1 - } } -// write the command -//temporal properties are not verified + module Dijkstra { import token_ring(N = 5, K = 7).* +} + +module BrokenDijkstra { + import token_ring(N = 3, K = 2).* } \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_3.qnt b/examples/classic/Dijkstra/Dijkstra_3.qnt index 5ec0f1c42..8a8818155 100644 --- a/examples/classic/Dijkstra/Dijkstra_3.qnt +++ b/examples/classic/Dijkstra/Dijkstra_3.qnt @@ -1,38 +1,103 @@ +// -*- mode: Bluespec; -*- +/** + * Dijkstra's Stabilizing Token Ring (EWD426) + * 3 state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a ring of nodes, + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 + */ module token_ring_three_state { - // import token_ring as token_ring from "Dijkstra" + // Number of nodes in the ring + const N: int + + val bottom = 0 + val top = N + + // Variable: Mapping of node indices to their states + var system: int -> int + + pure def has_token(nodes: int -> int, index: int): bool = + val s = nodes.get(index) + if (index == bottom) + val r = nodes.get(1) + (s + 1) % 3 == r + else if (index == top) + val l = nodes.get(N-1) + val r = nodes.get(bottom) + l == r and not((l+1)%3 == s) + else + val l = nodes.get(index-1) + val r = nodes.get(index+1) + or { + (s+1)%3 == l, + (s+1)%3 == r + } - import token_ring.* from "Dijkstra" - export token_ring.* // Transition function for the three-state machine - pure def three_state_transition(nodes: int -> int, index: int): int = { - val predecessor_index = if (index == 0) N - 1 else index - 1 - val current_state = nodes.get(index) - val predecessor_state = nodes.get(predecessor_index) - - if (index == 0) { - // Bottom node logic - if (predecessor_state % 3 == 2) (predecessor_state + 2) % 3 else current_state - } else if (index == N - 1) { - // Top node logic - if (predecessor_state % 3 == 2) (predecessor_state + 1) % 3 else current_state - } else { - // Other nodes - if (predecessor_state % 3 == 2) (predecessor_state + 1) % 3 else current_state - } + pure def state_transition(nodes: int -> int, index: int): int = + val s = nodes.get(index) + if (not(has_token(nodes, index))) + s + else + if (index == bottom) + (s + 2) % 3 // (s - 1) % 3 + else if (index == top) + val l = nodes.get(N-1) + (l + 1) % 3 + else + val l = nodes.get(index-1) + val r = nodes.get(index+1) + if ((s+1)%3 == l) // not 100% sure what Dijkstra wants here. + // might be non-determinism between the + // two options. We make it deterministic + // here + if ((s+1)%3 == r) + r + else + l + else + if ((s+1)%3 == r) + r + else + s + + + /// Initialize all nodes with random states + action init = all { + nondet random = to(0, N).setOfMaps(to(0, 2)).oneOf() + system' = to(0, N).mapBy(i => random.get(i)) } /// Action for the three-state machine - action three_state_update = { - nondet node_to_update = to(0, N - 1).oneOf() - nodes_to_states' = nodes_to_states.set(node_to_update, three_state_transition(nodes_to_states, node_to_update)) + action step = { + nondet node = to(0, N).filter(i => has_token(system, i)).oneOf() + system' = system.set(node, state_transition(system, node)) + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + to(0, N).filter(i => has_token(nodes, i)).size() } - temporal convergence_three_state = eventually (count_tokens(nodes_to_states) == 1) + // Temporal properties + temporal convergence = eventually (count_tokens(system) == 1) + temporal closure = always (count_tokens(system) == 1 implies + always (count_tokens(system) == 1)) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> int): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) + + } module Dijkstra_3 { - import token_ring_three_state(N = 5, K = 7).* + import token_ring_three_state(N = 5).* } \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_4.qnt b/examples/classic/Dijkstra/Dijkstra_4.qnt index bc8fb3819..cb91eb093 100644 --- a/examples/classic/Dijkstra/Dijkstra_4.qnt +++ b/examples/classic/Dijkstra/Dijkstra_4.qnt @@ -1,36 +1,111 @@ +// -*- mode: Bluespec; -*- +/** + * Dijkstra's Stabilizing Token Ring (EWD426) + * 4 state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a ring of nodes, + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 + */ module token_ring_four_state { - import token_ring.* from "Dijkstra" - export token_ring.* + // import token_ring.* from "Dijkstra" + // export token_ring.* + + const N: int + + val bottom = 0 + val top = N + + type State = { + x : bool, + up: bool + } + + var system: int -> State + + pure def has_token(nodes: int -> State, index: int): bool = + val s = nodes.get(index) + if (index == bottom) + val r = nodes.get(1) + s.x == r.x and not(r.up) + else if (index == top) + val l = nodes.get(N-1) + not(s.x == l.x) + else + val l = nodes.get(index-1) + val r = nodes.get(index+1) + or { + not(s.x == l.x), + and { + s.x == r.x, + s.up, + not(r.up) + } + } + // Pure function to handle the four-state transition - pure def four_state_transition(nodes: int -> int, index: int): int = { - val predecessor_index = if (index == 0) N - 1 else index - 1 - val xS = nodes.get(index) - val predecessor_xS = nodes.get(predecessor_index) - - if (index == 0) { - // Bottom node - if (xS == 1) 0 else xS - } else if (index == N - 1) { - // Top node - if (xS == 0) 1 else xS - } else { - // Other nodes - if (xS == 0) 1 else xS - } + pure def state_transition(nodes: int -> State, index: int): State = + val s = nodes.get(index) + if (not(has_token(nodes, index))) + s + else + if (index == bottom) + { x: not(s.x), up: s.up } + else if (index == top) + { x: not(s.x), up: s.up } + else + val l = nodes.get(index-1) + val r = nodes.get(index+1) + if (not(s.x == l.x)) + {x: not(s.x), up: true} + else + // and {s.x == r.x, s.up, not(r.up)} + { x: s.x, up: false } + + + action init = all { + val allState = + Set( { x: false, up: false }, + { x: false, up: true }, + { x: true, up: false }, + { x: true, up: true }) + nondet random = to(0, N).setOfMaps(allState).oneOf() + val s = to(0, N).mapBy(i => random.get(i)) + system' = s .set(bottom, { up: true, x: s.get(bottom).x }) + .set(top, { up: false, x: s.get(bottom).x }) } /// Action for the four-state machine - action four_state_update = { - nondet node_to_update = to(0, N - 1).oneOf() - nodes_to_states' = nodes_to_states.set(node_to_update, four_state_transition(nodes_to_states, node_to_update)) + action step = { + nondet node = to(0, N) + .filter(i => has_token(system, i)) + .oneOf() + system' = system.set(node, state_transition(system, node)) } - temporal convergence_four_state = eventually (count_tokens(nodes_to_states) == 1) + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> State): int = { + to(0, N).filter(i => has_token(nodes, i)).size() + } + + // Temporal properties + temporal convergence = eventually (count_tokens(system) == 1) + temporal closure = always (count_tokens(system) == 1 implies + always (count_tokens(system) == 1)) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> State): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) + + } module Dijkstra_4 { - import token_ring_four_state(N = 5, K = 7).* + import token_ring_four_state(N = 5).* } \ No newline at end of file From a765cd8e89d91c90f9daf1644bc61e2492b3468f Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 27 Jan 2025 15:21:53 -0300 Subject: [PATCH 4/9] Rename, format and reorganize ewd426 example --- examples/classic/Dijkstra/Dijkstra.qnt | 82 ------------- examples/classic/Dijkstra/Dijkstra_3.qnt | 103 ---------------- examples/classic/Dijkstra/Dijkstra_4.qnt | 111 ------------------ .../classic/distributed/ewd426/ewd426.qnt | 74 ++++++++++++ .../classic/distributed/ewd426/ewd426_3.qnt | 94 +++++++++++++++ .../classic/distributed/ewd426/ewd426_4.qnt | 101 ++++++++++++++++ 6 files changed, 269 insertions(+), 296 deletions(-) delete mode 100644 examples/classic/Dijkstra/Dijkstra.qnt delete mode 100644 examples/classic/Dijkstra/Dijkstra_3.qnt delete mode 100644 examples/classic/Dijkstra/Dijkstra_4.qnt create mode 100644 examples/classic/distributed/ewd426/ewd426.qnt create mode 100644 examples/classic/distributed/ewd426/ewd426_3.qnt create mode 100644 examples/classic/distributed/ewd426/ewd426_4.qnt diff --git a/examples/classic/Dijkstra/Dijkstra.qnt b/examples/classic/Dijkstra/Dijkstra.qnt deleted file mode 100644 index eb2a9339a..000000000 --- a/examples/classic/Dijkstra/Dijkstra.qnt +++ /dev/null @@ -1,82 +0,0 @@ -// -*- mode: Bluespec; -*- -/** - * Dijkstra's Stabilizing Token Ring (EWD426) - * K state machine - * This implementation ensures that from some time on, - * exactly one token circulates in a ring of nodes, - * - * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 - */ - -module token_ring { - // Number of nodes in the ring - const N: int - const K: int // K >= N, ensures the state space is larger than the number of nodes - - val bottom = 0 - val top = N - - // Variable: Mapping of node indices to their states - var system: int -> int - - // Pure function to check if a node has the token - pure def has_token(nodes: int -> int, index: int): bool = - if (index == bottom) - nodes.get(bottom) == nodes.get(top) - else - not(nodes.get(index) == nodes.get(index - 1)) - - - // Pure function to update the state of a specific node - pure def state_transition(nodes: int -> int, index: int): int = - if (not(has_token(nodes, index))) - nodes.get(index) - else - if (index == bottom) - (nodes.get(bottom) +1) % K - else - nodes.get(index - 1) - - - - /// Initialize all nodes with random states - action init = all { - nondet random = to(0, N).setOfMaps(to(0, K - 1)).oneOf() - system' = to(0, N).mapBy(i => random.get(i)) - } - - /// Update a single random active node - action step = { - nondet node = to(0, N) .filter(i => has_token(system, i)) - .oneOf() - system' = system.set(node, state_transition(system, node) ) - } - - - - // Pure function to count how many tokens exist - pure def count_tokens(nodes: int -> int): int = { - to(0, N).filter(i => has_token(nodes, i)).size() - } - - // Temporal properties - temporal convergence = eventually (count_tokens(system) == 1) - temporal closure = always (count_tokens(system) == 1 implies always (count_tokens(system) == 1)) - - // Invariant - def tokenInv = count_tokens(system) > 0 - - /// to better see the token in the repl - pure def show_token(nodes: int -> int): int -> bool = - nodes.keys().mapBy(i => has_token(nodes, i)) - -} - - -module Dijkstra { - import token_ring(N = 5, K = 7).* -} - -module BrokenDijkstra { - import token_ring(N = 3, K = 2).* -} \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_3.qnt b/examples/classic/Dijkstra/Dijkstra_3.qnt deleted file mode 100644 index 8a8818155..000000000 --- a/examples/classic/Dijkstra/Dijkstra_3.qnt +++ /dev/null @@ -1,103 +0,0 @@ -// -*- mode: Bluespec; -*- -/** - * Dijkstra's Stabilizing Token Ring (EWD426) - * 3 state machine - * This implementation ensures that from some time on, - * exactly one token circulates in a ring of nodes, - * - * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 - */ - - -module token_ring_three_state { - - // Number of nodes in the ring - const N: int - - val bottom = 0 - val top = N - - // Variable: Mapping of node indices to their states - var system: int -> int - - pure def has_token(nodes: int -> int, index: int): bool = - val s = nodes.get(index) - if (index == bottom) - val r = nodes.get(1) - (s + 1) % 3 == r - else if (index == top) - val l = nodes.get(N-1) - val r = nodes.get(bottom) - l == r and not((l+1)%3 == s) - else - val l = nodes.get(index-1) - val r = nodes.get(index+1) - or { - (s+1)%3 == l, - (s+1)%3 == r - } - - // Transition function for the three-state machine - pure def state_transition(nodes: int -> int, index: int): int = - val s = nodes.get(index) - if (not(has_token(nodes, index))) - s - else - if (index == bottom) - (s + 2) % 3 // (s - 1) % 3 - else if (index == top) - val l = nodes.get(N-1) - (l + 1) % 3 - else - val l = nodes.get(index-1) - val r = nodes.get(index+1) - if ((s+1)%3 == l) // not 100% sure what Dijkstra wants here. - // might be non-determinism between the - // two options. We make it deterministic - // here - if ((s+1)%3 == r) - r - else - l - else - if ((s+1)%3 == r) - r - else - s - - - /// Initialize all nodes with random states - action init = all { - nondet random = to(0, N).setOfMaps(to(0, 2)).oneOf() - system' = to(0, N).mapBy(i => random.get(i)) - } - - /// Action for the three-state machine - action step = { - nondet node = to(0, N).filter(i => has_token(system, i)).oneOf() - system' = system.set(node, state_transition(system, node)) - } - - // Pure function to count how many tokens exist - pure def count_tokens(nodes: int -> int): int = { - to(0, N).filter(i => has_token(nodes, i)).size() - } - - // Temporal properties - temporal convergence = eventually (count_tokens(system) == 1) - temporal closure = always (count_tokens(system) == 1 implies - always (count_tokens(system) == 1)) - - // Invariant - def tokenInv = count_tokens(system) > 0 - - /// to better see the token in the repl - pure def show_token(nodes: int -> int): int -> bool = - nodes.keys().mapBy(i => has_token(nodes, i)) - - -} - -module Dijkstra_3 { - import token_ring_three_state(N = 5).* -} \ No newline at end of file diff --git a/examples/classic/Dijkstra/Dijkstra_4.qnt b/examples/classic/Dijkstra/Dijkstra_4.qnt deleted file mode 100644 index cb91eb093..000000000 --- a/examples/classic/Dijkstra/Dijkstra_4.qnt +++ /dev/null @@ -1,111 +0,0 @@ -// -*- mode: Bluespec; -*- -/** - * Dijkstra's Stabilizing Token Ring (EWD426) - * 4 state machine - * This implementation ensures that from some time on, - * exactly one token circulates in a ring of nodes, - * - * Mahtab Norouzi, Josef Widder, Informal Systems, 2024, 2025 - */ - -module token_ring_four_state { - - // import token_ring.* from "Dijkstra" - // export token_ring.* - - const N: int - - val bottom = 0 - val top = N - - type State = { - x : bool, - up: bool - } - - var system: int -> State - - pure def has_token(nodes: int -> State, index: int): bool = - val s = nodes.get(index) - if (index == bottom) - val r = nodes.get(1) - s.x == r.x and not(r.up) - else if (index == top) - val l = nodes.get(N-1) - not(s.x == l.x) - else - val l = nodes.get(index-1) - val r = nodes.get(index+1) - or { - not(s.x == l.x), - and { - s.x == r.x, - s.up, - not(r.up) - } - } - - - // Pure function to handle the four-state transition - pure def state_transition(nodes: int -> State, index: int): State = - val s = nodes.get(index) - if (not(has_token(nodes, index))) - s - else - if (index == bottom) - { x: not(s.x), up: s.up } - else if (index == top) - { x: not(s.x), up: s.up } - else - val l = nodes.get(index-1) - val r = nodes.get(index+1) - if (not(s.x == l.x)) - {x: not(s.x), up: true} - else - // and {s.x == r.x, s.up, not(r.up)} - { x: s.x, up: false } - - - action init = all { - val allState = - Set( { x: false, up: false }, - { x: false, up: true }, - { x: true, up: false }, - { x: true, up: true }) - nondet random = to(0, N).setOfMaps(allState).oneOf() - val s = to(0, N).mapBy(i => random.get(i)) - system' = s .set(bottom, { up: true, x: s.get(bottom).x }) - .set(top, { up: false, x: s.get(bottom).x }) - } - - /// Action for the four-state machine - action step = { - nondet node = to(0, N) - .filter(i => has_token(system, i)) - .oneOf() - system' = system.set(node, state_transition(system, node)) - } - - // Pure function to count how many tokens exist - pure def count_tokens(nodes: int -> State): int = { - to(0, N).filter(i => has_token(nodes, i)).size() - } - - // Temporal properties - temporal convergence = eventually (count_tokens(system) == 1) - temporal closure = always (count_tokens(system) == 1 implies - always (count_tokens(system) == 1)) - - // Invariant - def tokenInv = count_tokens(system) > 0 - - /// to better see the token in the repl - pure def show_token(nodes: int -> State): int -> bool = - nodes.keys().mapBy(i => has_token(nodes, i)) - - -} - -module Dijkstra_4 { - import token_ring_four_state(N = 5).* -} \ No newline at end of file diff --git a/examples/classic/distributed/ewd426/ewd426.qnt b/examples/classic/distributed/ewd426/ewd426.qnt new file mode 100644 index 000000000..64badbf7b --- /dev/null +++ b/examples/classic/distributed/ewd426/ewd426.qnt @@ -0,0 +1,74 @@ +// -*- mode: Bluespec; -*- +/** + * ewd426's Stabilizing Token Ring (EWD426) + * K state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a set of nodes, + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 + */ +module self_stabilization { + // Number of nodes in the ring + const N: int + const K: int // K >= N, ensures the state space is larger than the number of nodes + + val bottom = 0 + val top = N + + // Variable: Mapping of node indices to their states + var system: int -> int + + // Pure function to check if a node has the token + pure def has_token(nodes: int -> int, index: int): bool = + if (index == bottom) + nodes.get(bottom) == nodes.get(top) + else + not(nodes.get(index) == nodes.get(index - 1)) + + // Pure function to update the state of a specific node + pure def state_transition(nodes: int -> int, index: int): int = + if (not(has_token(nodes, index))) + nodes.get(index) + else if (index == bottom) + (nodes.get(bottom) + 1) % K + else + nodes.get(index - 1) + + /// Initialize all nodes with random states + action init = all { + nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf() + system' = initial + } + + /// Update a single random active node + action step = { + nondet node = 0.to(N).filter(i => has_token(system, i)) + .oneOf() + system' = system.set(node, state_transition(system, node)) + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + 0.to(N).filter(i => has_token(nodes, i)).size() + } + + // Temporal properties + temporal convergence = eventually(count_tokens(system) == 1) + temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1)) + + temporal persistance = eventually(always(count_tokens(system) == 1)) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> int): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) +} + +module ewd426 { + import self_stabilization(N = 5, K = 7).* +} + +module broken_ewd426 { + import self_stabilization(N = 3, K = 2).* +} diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt new file mode 100644 index 000000000..bc8f2fa8a --- /dev/null +++ b/examples/classic/distributed/ewd426/ewd426_3.qnt @@ -0,0 +1,94 @@ +// -*- mode: Bluespec; -*- +/** + * ewd426's Stabilizing Token Ring (EWD426) + * 3 state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a set of nodes. + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 + */ +module self_stabilization_three_states { + // Number of nodes in the ring + const N: int + + val bottom = 0 + val top = N + + // Variable: Mapping of node indices to their states + var system: int -> int + + pure def has_token(nodes: int -> int, index: int): bool = + val s = nodes.get(index) + if (index == bottom) + val r = nodes.get(1) + (s + 1) % 3 == r + else if (index == top) + val l = nodes.get(N - 1) + val r = nodes.get(bottom) + l == r and not((l + 1) % 3 == s) + else + val l = nodes.get(index - 1) + val r = nodes.get(index + 1) + or { + (s + 1) % 3 == l, + (s + 1) % 3 == r + } + + // Transition function for the three-state machine + pure def state_transition(nodes: int -> int, index: int): int = + val s = nodes.get(index) + if (not(has_token(nodes, index))) + s + else if (index == bottom) + (s + 2) % 3 // (s - 1) % 3 + else if (index == top) + val l = nodes.get(N - 1) + (l + 1) % 3 + else + val l = nodes.get(index - 1) + val r = nodes.get(index + 1) + if ((s + 1) % 3 == l) + // Not 100% sure what ewd426 wants here. Might be non-determinism + // between the two options. We make it deterministic here. + if ((s + 1) % 3 == r) + r + else + l + else if ((s + 1) % 3 == r) + r + else + s + + /// Initialize all nodes with random states + action init = all { + nondet initial = 0.to(N).setOfMaps(0.to(2)).oneOf() + system' = initial + } + + /// Action for the three-state machine + action step = { + nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() + system' = system.set(node, state_transition(system, node)) + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + to(0, N).filter(i => has_token(nodes, i)).size() + } + + // Temporal properties + temporal convergence = eventually(count_tokens(system) == 1) + temporal closure = always( + count_tokens(system) == 1 implies always(count_tokens(system) == 1) + ) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> int): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) +} + +module ewd426_3 { + import self_stabilization_three_states(N = 5).* +} diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt new file mode 100644 index 000000000..e1cb30102 --- /dev/null +++ b/examples/classic/distributed/ewd426/ewd426_4.qnt @@ -0,0 +1,101 @@ +// -*- mode: Bluespec; -*- +/** + * ewd426's Stabilizing Token Ring (EWD426) + * 4 state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a set of nodes, + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 + */ +module self_stabilization_four_states { + const N: int + + val bottom = 0 + val top = N + + type State = { + x: bool, + up: bool + } + + var system: int -> State + + pure def has_token(nodes: int -> State, index: int): bool = + val s = nodes.get(index) + if (index == bottom) + val r = nodes.get(1) + s.x == r.x and not(r.up) + else if (index == top) + val l = nodes.get(N - 1) + not(s.x == l.x) + else + val l = nodes.get(index - 1) + val r = nodes.get(index + 1) + or { + not(s.x == l.x), + and { + s.x == r.x, + s.up, + not(r.up) + } + } + + // Pure function to handle the four-state transition + pure def state_transition(nodes: int -> State, index: int): State = + val s = nodes.get(index) + if (not(has_token(nodes, index))) + s + else if (index == bottom) + { x: not(s.x), up: s.up } + else if (index == top) + { x: not(s.x), up: s.up } + else + val l = nodes.get(index - 1) + val r = nodes.get(index + 1) + if (not(s.x == l.x)) + { x: not(s.x), up: true } + else + // and {s.x == r.x, s.up, not(r.up)} + { x: s.x, up: false } + + action init = all { + val allState = Set( + { x: false, up: false }, + { x: false, up: true }, + { x: true, up: false }, + { x: true, up: true } + ) + nondet initial = 0.to(N).setOfMaps(allState).oneOf() + // "For the bottom machine upS = true by definition, for the top machine upS = false by definition" + system' = initial + .setBy(bottom, s => { ...s, up: true }) + .setBy(top, s => { ...s, up: false }) + } + + /// Action for the four-state machine + action step = { + nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() + system' = system.set(node, state_transition(system, node)) + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> State): int = { + 0.to(N).filter(i => has_token(nodes, i)).size() + } + + // Temporal properties + temporal convergence = eventually(count_tokens(system) == 1) + temporal closure = always( + count_tokens(system) == 1 implies always(count_tokens(system) == 1) + ) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> State): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) +} + +module ewd426_4 { + import self_stabilization_four_states(N = 5).* +} From ea74c7f38723b679e51bc33a9bcdea26f6de3f4b Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 27 Jan 2025 15:47:39 -0300 Subject: [PATCH 5/9] Add weak fairness to temporal properties --- .../classic/distributed/ewd426/ewd426.qnt | 27 ++++++++++--------- .../classic/distributed/ewd426/ewd426_3.qnt | 7 +++-- .../classic/distributed/ewd426/ewd426_4.qnt | 7 +++-- 3 files changed, 21 insertions(+), 20 deletions(-) diff --git a/examples/classic/distributed/ewd426/ewd426.qnt b/examples/classic/distributed/ewd426/ewd426.qnt index 64badbf7b..29dca5a06 100644 --- a/examples/classic/distributed/ewd426/ewd426.qnt +++ b/examples/classic/distributed/ewd426/ewd426.qnt @@ -10,22 +10,25 @@ module self_stabilization { // Number of nodes in the ring const N: int - const K: int // K >= N, ensures the state space is larger than the number of nodes + const K: int + + /// Ensures the state space is larger than the number of nodes + assume _ = K >= N val bottom = 0 val top = N - // Variable: Mapping of node indices to their states + /// Mapping of node indices to their states var system: int -> int - // Pure function to check if a node has the token + /// Check if a node has the token pure def has_token(nodes: int -> int, index: int): bool = if (index == bottom) nodes.get(bottom) == nodes.get(top) else not(nodes.get(index) == nodes.get(index - 1)) - // Pure function to update the state of a specific node + /// Update the state of a specific node pure def state_transition(nodes: int -> int, index: int): int = if (not(has_token(nodes, index))) nodes.get(index) @@ -34,16 +37,15 @@ module self_stabilization { else nodes.get(index - 1) - /// Initialize all nodes with random states + /// Initialize all nodes with non-deterministic states action init = all { nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf() system' = initial } - /// Update a single random active node + /// Update a single non-deterministic active node action step = { - nondet node = 0.to(N).filter(i => has_token(system, i)) - .oneOf() + nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() system' = system.set(node, state_transition(system, node)) } @@ -53,16 +55,16 @@ module self_stabilization { } // Temporal properties - temporal convergence = eventually(count_tokens(system) == 1) + temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1) temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1)) - - temporal persistance = eventually(always(count_tokens(system) == 1)) + temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1)) // Invariant def tokenInv = count_tokens(system) > 0 /// to better see the token in the repl - pure def show_token(nodes: int -> int): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) + pure def show_token(nodes: int -> int): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) } module ewd426 { @@ -70,5 +72,6 @@ module ewd426 { } module broken_ewd426 { + // This should break the assumption of K >= N. See #1182. import self_stabilization(N = 3, K = 2).* } diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt index bc8f2fa8a..997d303d3 100644 --- a/examples/classic/distributed/ewd426/ewd426_3.qnt +++ b/examples/classic/distributed/ewd426/ewd426_3.qnt @@ -77,10 +77,9 @@ module self_stabilization_three_states { } // Temporal properties - temporal convergence = eventually(count_tokens(system) == 1) - temporal closure = always( - count_tokens(system) == 1 implies always(count_tokens(system) == 1) - ) + temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1) + temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1)) + temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1)) // Invariant def tokenInv = count_tokens(system) > 0 diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt index e1cb30102..d759ab13b 100644 --- a/examples/classic/distributed/ewd426/ewd426_4.qnt +++ b/examples/classic/distributed/ewd426/ewd426_4.qnt @@ -84,10 +84,9 @@ module self_stabilization_four_states { } // Temporal properties - temporal convergence = eventually(count_tokens(system) == 1) - temporal closure = always( - count_tokens(system) == 1 implies always(count_tokens(system) == 1) - ) + temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1) + temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1)) + temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1)) // Invariant def tokenInv = count_tokens(system) > 0 From 8ed6389069aad62bcefab6de5c32c0c129aa1b5d Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 27 Jan 2025 16:18:44 -0300 Subject: [PATCH 6/9] Add script to check temporal properties with TLC --- .../distributed/ewd426/check_with_tlc.sh | 67 +++++++++++++++++++ .../classic/distributed/ewd426/ewd426_3.qnt | 3 +- .../classic/distributed/ewd426/ewd426_4.qnt | 3 +- 3 files changed, 71 insertions(+), 2 deletions(-) create mode 100644 examples/classic/distributed/ewd426/check_with_tlc.sh diff --git a/examples/classic/distributed/ewd426/check_with_tlc.sh b/examples/classic/distributed/ewd426/check_with_tlc.sh new file mode 100644 index 000000000..0314a81a2 --- /dev/null +++ b/examples/classic/distributed/ewd426/check_with_tlc.sh @@ -0,0 +1,67 @@ +#!/bin/bash + +# Files to process +FILES=("ewd426.qnt" "ewd426_3.qnt" "ewd426_4.qnt") + +# Apalache jar path +APALACHE_JAR="$HOME/.quint/apalache-dist-0.47.2/apalache/lib/apalache.jar" + +# Memory options for Java +JAVA_OPTS="-Xmx8G -Xss515m" + +for file in "${FILES[@]}"; do + base_name="${file%.qnt}" + tla_file="${base_name}.tla" + cfg_file="${base_name}.cfg" + + echo "Processing $file..." + + # Step 1: Compile the .qnt file to .tla + quint compile --target=tlaplus "$file" --temporal=convergence,closure,persistence --invariant=tokenInv > "$tla_file" + + if [[ $? -ne 0 ]]; then + echo "Error: Compilation failed for $file" + exit 1 + fi + + # Step 2: Fix init to be a predicate instead of an assignment + perl -0777 -i -pe "s/(.*)'\s+:= (.*_self_stabilization_.*?initial)/\1 = \2/s" "$tla_file" + + + if [[ $? -ne 0 ]]; then + echo "Error: Failed to edit $tla_file" + exit 1 + fi + + # Step 3: Create the .cfg file + cat < "$cfg_file" +INIT +q_init + +NEXT +q_step + +PROPERTY +q_temporalProps + +INVARIANT +q_inv +EOF + + # Step 4: Run TLC with the required Apalache lib files and check output + output=$(java $JAVA_OPTS -cp "$APALACHE_JAR" tlc2.TLC -deadlock "$tla_file" 2>&1) + + # Step 5: Delete the generated .tla and .cfg files + rm -f "$tla_file" "$cfg_file" + + if echo "$output" | grep -q "Model checking completed. No error has been found."; then + echo "Model checking succeeded for $tla_file" + else + echo "Error: Model checking failed for $tla_file" + echo "$output" + exit 1 + fi + +done + +echo "All files processed successfully." diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt index 997d303d3..8db7e4054 100644 --- a/examples/classic/distributed/ewd426/ewd426_3.qnt +++ b/examples/classic/distributed/ewd426/ewd426_3.qnt @@ -85,7 +85,8 @@ module self_stabilization_three_states { def tokenInv = count_tokens(system) > 0 /// to better see the token in the repl - pure def show_token(nodes: int -> int): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) + pure def show_token(nodes: int -> int): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) } module ewd426_3 { diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt index d759ab13b..8a73f86e4 100644 --- a/examples/classic/distributed/ewd426/ewd426_4.qnt +++ b/examples/classic/distributed/ewd426/ewd426_4.qnt @@ -92,7 +92,8 @@ module self_stabilization_four_states { def tokenInv = count_tokens(system) > 0 /// to better see the token in the repl - pure def show_token(nodes: int -> State): int -> bool = nodes.keys().mapBy(i => has_token(nodes, i)) + pure def show_token(nodes: int -> State): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) } module ewd426_4 { From b7605f73876a96f1a07bcfe4e56cf9f30e2b84bc Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 27 Jan 2025 16:29:25 -0300 Subject: [PATCH 7/9] Add a README file --- examples/classic/distributed/ewd426/README.md | 30 +++++++++++++++++++ .../classic/distributed/ewd426/ewd426_3.qnt | 4 +-- .../classic/distributed/ewd426/ewd426_4.qnt | 4 +-- 3 files changed, 34 insertions(+), 4 deletions(-) create mode 100644 examples/classic/distributed/ewd426/README.md diff --git a/examples/classic/distributed/ewd426/README.md b/examples/classic/distributed/ewd426/README.md new file mode 100644 index 000000000..1fec43c4e --- /dev/null +++ b/examples/classic/distributed/ewd426/README.md @@ -0,0 +1,30 @@ +# EWD426 + +This folder contains Quint specifications for the three different self-stabilization algorithms proposed by Dijkstra in [EWD426](https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD426.html). +1. A solution with K-state machines [ewd426.qnt](ewd426.qnt) +2. A solution with three-state machines [ewd426_3.qnt](ewd426_3.qnt) +3. A solution with four-state machines [ewd426_4.qnt](ewd426_4.qnt) + +Due to the presence of temporal properties and fairness, we need to use TLC to model check these specs. As the integration with TLC is not completed, we provide a script to automate running it for these specific specifications: [check_with_tlc.sh](check_with_tlc.sh). + +If you are trying to learn/understand these algorithms, we recommend playing with the Quint REPL. For that, pick one of the files (for example [ewd426.qnt](ewd426.qnt)) and run the following command in the terminal: +``` sh +quint -r ewd426.qnt::ewd426 +``` + +This will open the REPL with the `ewd426` machine loaded. You can now interact with the machine and explore its states and transitions: + +``` bluespec +Quint REPL 0.22.4 +Type ".exit" to exit, or ".help" for more information +>>> init +true +>>> step +true +>>> show_token(system) +Map(0 -> false, 1 -> true, 2 -> true, 3 -> false, 4 -> true, 5 -> false) +>>> 5.reps(_ => step) +true +>>> show_token(system) +Map(0 -> true, 1 -> false, 2 -> false, 3 -> false, 4 -> false, 5 -> false) +``` diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt index 8db7e4054..77b47b838 100644 --- a/examples/classic/distributed/ewd426/ewd426_3.qnt +++ b/examples/classic/distributed/ewd426/ewd426_3.qnt @@ -7,7 +7,7 @@ * * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 */ -module self_stabilization_three_states { +module self_stabilization_three_state { // Number of nodes in the ring const N: int @@ -90,5 +90,5 @@ module self_stabilization_three_states { } module ewd426_3 { - import self_stabilization_three_states(N = 5).* + import self_stabilization_three_state(N = 5).* } diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt index 8a73f86e4..9b0da36d5 100644 --- a/examples/classic/distributed/ewd426/ewd426_4.qnt +++ b/examples/classic/distributed/ewd426/ewd426_4.qnt @@ -7,7 +7,7 @@ * * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 */ -module self_stabilization_four_states { +module self_stabilization_four_state { const N: int val bottom = 0 @@ -97,5 +97,5 @@ module self_stabilization_four_states { } module ewd426_4 { - import self_stabilization_four_states(N = 5).* + import self_stabilization_four_state(N = 5).* } From fa99056fd57c0ffa8a90306d3801d75f7f6a3c9d Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 27 Jan 2025 16:32:35 -0300 Subject: [PATCH 8/9] Update examples dashboard --- examples/README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/examples/README.md b/examples/README.md index 7835502ad..0e8c954b0 100644 --- a/examples/README.md +++ b/examples/README.md @@ -49,6 +49,9 @@ 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/ewd426/ewd426.qnt](./classic/distributed/ewd426/ewd426.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | +| [classic/distributed/ewd426/ewd426_3.qnt](./classic/distributed/ewd426/ewd426_3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | +| [classic/distributed/ewd426/ewd426_4.qnt](./classic/distributed/ewd426/ewd426_4.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: | :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: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1284 | From 23d3c9a938659a1f90a6c7b9c2b6866cb5e3959f Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Tue, 28 Jan 2025 10:57:11 +0100 Subject: [PATCH 9/9] add step for distributed demon --- examples/classic/distributed/ewd426/ewd426.qnt | 10 +++++++++- examples/classic/distributed/ewd426/ewd426_3.qnt | 10 +++++++++- examples/classic/distributed/ewd426/ewd426_4.qnt | 10 +++++++++- 3 files changed, 27 insertions(+), 3 deletions(-) diff --git a/examples/classic/distributed/ewd426/ewd426.qnt b/examples/classic/distributed/ewd426/ewd426.qnt index 29dca5a06..9607c645d 100644 --- a/examples/classic/distributed/ewd426/ewd426.qnt +++ b/examples/classic/distributed/ewd426/ewd426.qnt @@ -43,12 +43,20 @@ module self_stabilization { system' = initial } - /// Update a single non-deterministic active node + /// Pick a single active node non-deterministically and update its state action step = { nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() system' = system.set(node, state_transition(system, node)) } + /// Pick several active nodes non-deterministically and update their state. + /// Closer to the distributed demon is discussed in EWD 391. We are not + /// considering interleaving in the execution of state_transition here + action distributed_step = { + nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf() + system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x))) + } + // Pure function to count how many tokens exist pure def count_tokens(nodes: int -> int): int = { 0.to(N).filter(i => has_token(nodes, i)).size() diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt index 77b47b838..a4d3b9fc9 100644 --- a/examples/classic/distributed/ewd426/ewd426_3.qnt +++ b/examples/classic/distributed/ewd426/ewd426_3.qnt @@ -65,12 +65,20 @@ module self_stabilization_three_state { system' = initial } - /// Action for the three-state machine + /// Pick a single active node non-deterministically and update its state action step = { nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() system' = system.set(node, state_transition(system, node)) } + /// Pick several active nodes non-deterministically and update their state. + /// Closer to the distributed demon is discussed in EWD 391. We are not + /// considering interleaving in the execution of state_transition here + action distributed_step = { + nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf() + system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x))) + } + // Pure function to count how many tokens exist pure def count_tokens(nodes: int -> int): int = { to(0, N).filter(i => has_token(nodes, i)).size() diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt index 9b0da36d5..962bfabd6 100644 --- a/examples/classic/distributed/ewd426/ewd426_4.qnt +++ b/examples/classic/distributed/ewd426/ewd426_4.qnt @@ -72,12 +72,20 @@ module self_stabilization_four_state { .setBy(top, s => { ...s, up: false }) } - /// Action for the four-state machine + /// Pick a single active node non-deterministically and update its state action step = { nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() system' = system.set(node, state_transition(system, node)) } + /// Pick several active nodes non-deterministically and update their state. + /// Closer to the distributed demon is discussed in EWD 391. We are not + /// considering interleaving in the execution of state_transition here + action distributed_step = { + nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf() + system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x))) + } + // Pure function to count how many tokens exist pure def count_tokens(nodes: int -> State): int = { 0.to(N).filter(i => has_token(nodes, i)).size()