|
| 1 | +----------------------------- MODULE DieHardest ------------------------------ |
| 2 | +(***************************************************************************) |
| 3 | +(* This module compares two jug configurations by composing two instances *) |
| 4 | +(* of DieHarder into a single specification. The two instances share no *) |
| 5 | +(* variables and their next-state relations are conjoined, so they advance *) |
| 6 | +(* in lock-step: every step of the composed system is a step of both *) |
| 7 | +(* instances simultaneously. This is called parallel (or synchronous) *) |
| 8 | +(* composition. *) |
| 9 | +(* *) |
| 10 | +(* The property NotSolved (below) asks whether one configuration can reach *) |
| 11 | +(* the Goal while the other has not. This is a question about *pairs* of *) |
| 12 | +(* behaviors—one from each configuration—rather than about a single *) |
| 13 | +(* behavior. Properties that relate multiple behaviors of a system are *) |
| 14 | +(* called hyperproperties; NotSolved is a 2-hyperproperty because it *) |
| 15 | +(* relates two behaviors. Ordinary model checkers, including TLC, check *) |
| 16 | +(* trace properties (properties of individual behaviors), not *) |
| 17 | +(* hyperproperties. The standard workaround is self-composition: run two *) |
| 18 | +(* copies of the system side by side and reduce the hyperproperty to an *) |
| 19 | +(* ordinary invariant on the product system. That is exactly what this *) |
| 20 | +(* module does. *) |
| 21 | +(* *) |
| 22 | +(* Background: *) |
| 23 | +(* - Lamport, "Verifying Hyperproperties With TLA", 2021. *) |
| 24 | +(* (https://ieeexplore.ieee.org/document/9505222) *) |
| 25 | +(* - Wayne, "Hypermodeling Hyperproperties", 2020 *) |
| 26 | +(* (https://hillelwayne.com/post/hyperproperties/). *) |
| 27 | +(***************************************************************************) |
| 28 | +EXTENDS Naturals, Functions, FiniteSetsExt, TLCExt |
| 29 | + |
| 30 | +(***************************************************************************) |
| 31 | +(* The Die Hard problem has a solution if and only if two conditions are *) |
| 32 | +(* satisfied: (1) the Goal is at most the capacity of the largest jug, *) |
| 33 | +(* and (2) the Goal is divisible by the greatest common divisor (GCD) of *) |
| 34 | +(* all jug capacities. The first condition ensures the goal can fit in *) |
| 35 | +(* at least one jug. The second follows from Bézout's Identity and *) |
| 36 | +(* number theory: the set of quantities that can be measured with jugs of *) |
| 37 | +(* capacities c1, c2, ..., cn is precisely the set of natural number *) |
| 38 | +(* multiples of GCD(c1, c2, ..., cn). The definitions below are *) |
| 39 | +(* self-contained versions of the necessary mathematical operators to *) |
| 40 | +(* avoid naming conflicts. *) |
| 41 | +(* *) |
| 42 | +(* Note: Condition (1) could be changed to Goal <= sum of all jug *) |
| 43 | +(* capacities, reflecting different puzzle rules where the goal may be *) |
| 44 | +(* distributed across multiple jugs rather than contained in a single one. *) |
| 45 | +(***************************************************************************) |
| 46 | +HasSolution(capacity, goal) == |
| 47 | + LET DivDH(d, n) == \E k \in 0..n : n = d * k |
| 48 | + CDivDH(S) == {d \in 1..Min(S): \A n \in S: DivDH(d, n)} |
| 49 | + GCDDH(S) == IF S = {} THEN 0 ELSE Max(CDivDH(S)) |
| 50 | + IN /\ goal <= Max(Range(capacity)) |
| 51 | + /\ DivDH(GCDDH(Range(capacity)), goal) |
| 52 | + |
| 53 | +CONSTANT Capacities, |
| 54 | + Goal |
| 55 | + |
| 56 | +(***************************************************************************) |
| 57 | +(* The two configurations must differ; comparing a configuration with *) |
| 58 | +(* itself is uninteresting. *) |
| 59 | +(***************************************************************************) |
| 60 | +ASSUME Capacities[1] # Capacities[2] |
| 61 | + |
| 62 | +(***************************************************************************) |
| 63 | +(* Both configurations must have a solution. If either does not, TLC *) |
| 64 | +(* will never reach the Goal and will report no counterexample. *) |
| 65 | +(***************************************************************************) |
| 66 | +ASSUME /\ HasSolution(Capacities[1], Goal) |
| 67 | + /\ HasSolution(Capacities[2], Goal) |
| 68 | + |
| 69 | +VARIABLE c1, c2 |
| 70 | +vars == << c1, c2 >> |
| 71 | + |
| 72 | +D1 == INSTANCE DieHarder |
| 73 | + WITH Jug <- DOMAIN Capacities[1], |
| 74 | + Capacity <- Capacities[1], |
| 75 | + Goal <- Goal, |
| 76 | + contents <- c1 |
| 77 | + |
| 78 | +D2 == INSTANCE DieHarder |
| 79 | + WITH Jug <- DOMAIN Capacities[2], |
| 80 | + Capacity <- Capacities[2], |
| 81 | + Goal <- Goal, |
| 82 | + contents <- c2 |
| 83 | + |
| 84 | +Init == D1!Init /\ D2!Init |
| 85 | + |
| 86 | +Next == D1!Next /\ D2!Next |
| 87 | + |
| 88 | +Spec == Init /\ [][Next]_vars |
| 89 | +----------------------------------------------------------------------------- |
| 90 | + |
| 91 | +(***************************************************************************) |
| 92 | +(* NotSolved is the 2-hyperproperty reduced to an invariant of the *) |
| 93 | +(* composed system (see the module comment above). It holds as long as *) |
| 94 | +(* the two configurations have not both reached the Goal. A *) |
| 95 | +(* counterexample is a behavior in which both configurations solve the *) |
| 96 | +(* problem. *) |
| 97 | +(* *) |
| 98 | +(* - TLC reports no counterexample if either configuration cannot reach *) |
| 99 | +(* the Goal (prevented by the ASSUMEs above). *) |
| 100 | +(* *) |
| 101 | +(* - TLC reports a counterexample when both configurations reach the *) |
| 102 | +(* Goal in the same step. This is perhaps unexpected but harmless. *) |
| 103 | +(* *) |
| 104 | +(* - TLC reports a counterexample when one configuration reaches the *) |
| 105 | +(* Goal before the other. Because Next conjoins D1!Next and D2!Next, *) |
| 106 | +(* both configurations advance together in every non-stuttering step. *) |
| 107 | +(* The trace has the length of the slower configuration; in some steps *) |
| 108 | +(* the faster one makes no useful progress. *) |
| 109 | +(***************************************************************************) |
| 110 | +NotSolved == |
| 111 | + ~ (Goal \in Range(c1) /\ Goal \in Range(c2)) |
| 112 | + |
| 113 | +(***************************************************************************) |
| 114 | +(* The Alias below uses TLCGetAndSet to count non-stuttering steps in *) |
| 115 | +(* each instance (s1 and s2), i.e., steps in which the jug contents *) |
| 116 | +(* actually change. In a counterexample trace, s1 and s2 reveal which *) |
| 117 | +(* configuration reaches the Goal first and how many moves it takes. *) |
| 118 | +(* (In the TLA+ VS Code / Cursor extension, the modification markers in *) |
| 119 | +(* the model-checking view provide the same information visually.) *) |
| 120 | +(* *) |
| 121 | +(* An alternative would be to add s1 and s2 as specification variables *) |
| 122 | +(* and update them in the next-state relation, but that would pollute the *) |
| 123 | +(* spec with bookkeeping that is irrelevant to the problem being modeled. *) |
| 124 | +(***************************************************************************) |
| 125 | +Alias == |
| 126 | + [ |
| 127 | + c1 |-> c1, |
| 128 | + c2 |-> c2, |
| 129 | + s1 |-> TLCGetAndSet(0, +, IF UNCHANGED c1 THEN 0 ELSE 1, 1), |
| 130 | + s2 |-> TLCGetAndSet(1, +, IF UNCHANGED c2 THEN 0 ELSE 1, 1) |
| 131 | + ] |
| 132 | +============================================================================= |
0 commit comments