Merge pull request #1583 from informalsystems/add-Dijkstra-example

Add Dijkstra's Stabilizing Token Ring example in Quint

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:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |

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)
+```

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 <<EOF > "$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."

examples/classic/distributed/ewd426/ewd426.qnt

@@ -0,0 +1,85 @@
+// -*- 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
+
+  /// Ensures the state space is larger than the number of nodes
+  assume _ = K >= N
+
+  val bottom = 0
+  val top = N
+
+  /// Mapping of node indices to their states
+  var system: int -> int
+
+  /// 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))
+
+  /// 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 non-deterministic states
+  action init = all {
+    nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf()
+    system' = initial
+  }
+
+  /// 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()
+  }
+
+  // Temporal properties
+  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
+
+  /// 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 {
+  // This should break the assumption of K >= N. See #1182.
+  import self_stabilization(N = 3, K = 2).*
+}

examples/classic/distributed/ewd426/ewd426_3.qnt

@@ -0,0 +1,102 @@
+// -*- 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_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 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
+  }
+
+  /// 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()
+  }
+
+  // Temporal properties
+  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
+
+  /// 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_state(N = 5).*
+}