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