add step for distributed demon

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()

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()

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()