|
| 1 | +----------------------------- MODULE DieHardest ------------------------------ |
| 2 | +(***************************************************************************) |
| 3 | +(* Given two jug configurations that can each solve the Die Hard problem, *) |
| 4 | +(* which one reaches the Goal in fewer steps? *) |
| 5 | +(* *) |
| 6 | +(* This is a question about pairs of behaviors — one from each *) |
| 7 | +(* configuration — rather than about a single behavior. Such properties *) |
| 8 | +(* are called hyperproperties; ours is a 2-hyperproperty because it *) |
| 9 | +(* relates two behaviors. Ordinary model checkers like TLC check trace *) |
| 10 | +(* properties (properties of individual behaviors), not hyperproperties. *) |
| 11 | +(* The standard workaround is self-composition: run two copies of the *) |
| 12 | +(* system side by side and reduce the hyperproperty to an ordinary *) |
| 13 | +(* invariant of the product system. This module does exactly that by *) |
| 14 | +(* composing two instances of DieHarder. *) |
| 15 | +(* *) |
| 16 | +(* The choice of how the two copies advance matters. Sections 1–3 show *) |
| 17 | +(* that the natural choice — parallel (lock-step) composition — has a *) |
| 18 | +(* subtle flaw: TLC's BFS finds the shortest trace for the slower *) |
| 19 | +(* configuration but not necessarily for the faster one. Two fixes are *) |
| 20 | +(* explored; one works but departs from the logic of TLA+. Section 4 *) |
| 21 | +(* gives a clean solution: interleaved composition, where each instance *) |
| 22 | +(* steps independently. *) |
| 23 | +(* *) |
| 24 | +(* Primary use case: show that adding a redundant jug (e.g. comparing *) |
| 25 | +(* <<5, 3>> against <<5, 3, 3>> for Goal = 4) can shorten the solution. *) |
| 26 | +(* *) |
| 27 | +(* References: *) |
| 28 | +(* - Lamport, "Verifying Hyperproperties With TLA", 2021. *) |
| 29 | +(* (https://ieeexplore.ieee.org/document/9505222) *) |
| 30 | +(* - Wayne, "Hypermodeling Hyperproperties", 2020 *) |
| 31 | +(* (https://hillelwayne.com/post/hyperproperties/). *) |
| 32 | +(***************************************************************************) |
| 33 | +EXTENDS Naturals, Functions, FiniteSetsExt, TLC, TLCExt |
| 34 | + |
| 35 | +(***************************************************************************) |
| 36 | +(* TLC only guarantees strict BFS with a single worker. Strict BFS is *) |
| 37 | +(* required so that counterexamples are shortest paths, and Section 3 *) |
| 38 | +(* additionally depends on TLCSet/TLCGet registers that assume *) |
| 39 | +(* single-threaded exploration. *) |
| 40 | +(***************************************************************************) |
| 41 | +ASSUME /\ TLCGet("config").mode = "bfs" |
| 42 | + /\ TLCGet("config").worker = 1 |
| 43 | + |
| 44 | +(***************************************************************************) |
| 45 | +(* The Die Hard problem has a solution iff: (1) the Goal fits in the *) |
| 46 | +(* largest jug, and (2) the Goal is divisible by the GCD of all jug *) |
| 47 | +(* capacities. Condition (2) follows from Bézout's identity: the *) |
| 48 | +(* measurable quantities with jugs of capacities c1, …, cn are exactly *) |
| 49 | +(* the multiples of GCD(c1, …, cn). The LET definitions use distinct *) |
| 50 | +(* names to avoid clashes with operators in DieHarder. *) |
| 51 | +(***************************************************************************) |
| 52 | +HasSolution(capacity, goal) == |
| 53 | + LET Div(d, n) == \E k \in 0..n : n = d * k |
| 54 | + CDivisors(S) == {d \in 1..Min(S) : \A n \in S : Div(d, n)} |
| 55 | + GCD(S) == IF S = {} THEN 0 ELSE Max(CDivisors(S)) |
| 56 | + IN /\ goal <= Max(Range(capacity)) |
| 57 | + /\ Div(GCD(Range(capacity) \ {0}), goal) |
| 58 | + |
| 59 | +CONSTANT Capacities, \* <<Cap1, Cap2>>: a tuple of two jug-capacity functions. |
| 60 | + Goal \* The target quantity of water. |
| 61 | + |
| 62 | +(***************************************************************************) |
| 63 | +(* TLC only guarantees strict BFS with a single worker. Strict BFS is *) |
| 64 | +(* required so that counterexamples are shortest paths, and Section 3 *) |
| 65 | +(* additionally depends on TLCSet/TLCGet registers that assume *) |
| 66 | +(* single-threaded exploration. *) |
| 67 | +(***************************************************************************) |
| 68 | +ASSUME /\ TLCGet("config").mode = "bfs" |
| 69 | + /\ TLCGet("config").worker = 1 |
| 70 | + |
| 71 | +ASSUME Capacities[1] # Capacities[2] |
| 72 | + |
| 73 | +ASSUME /\ HasSolution(Capacities[1], Goal) |
| 74 | + /\ HasSolution(Capacities[2], Goal) |
| 75 | + |
| 76 | +VARIABLE c1, \* Jug contents for configuration 1. |
| 77 | + c2, \* Jug contents for configuration 2. |
| 78 | + s1, \* Number of transitions taken by configuration 1. |
| 79 | + s2 \* Number of transitions taken by configuration 2. |
| 80 | +vars == <<c1, c2, s1, s2>> |
| 81 | + |
| 82 | +D1 == INSTANCE DieHarder WITH Jug <- DOMAIN Capacities[1], |
| 83 | + Capacity <- Capacities[1], |
| 84 | + Goal <- Goal, |
| 85 | + contents <- c1 |
| 86 | + |
| 87 | +D2 == INSTANCE DieHarder WITH Jug <- DOMAIN Capacities[2], |
| 88 | + Capacity <- Capacities[2], |
| 89 | + Goal <- Goal, |
| 90 | + contents <- c2 |
| 91 | + |
| 92 | +Init == |
| 93 | + /\ D1!Init |
| 94 | + /\ D2!Init |
| 95 | + /\ s1 = 0 |
| 96 | + /\ s2 = 0 |
| 97 | +----------------------------------------------------------------------------- |
| 98 | +(***************************************************************************) |
| 99 | +(* SECTION 1. Parallel composition *) |
| 100 | +(* *) |
| 101 | +(* Both instances step in lock-step: every transition advances both. *) |
| 102 | +(* *) |
| 103 | +(* Flaw: TLC's BFS guarantees the shortest trace to the state where the *) |
| 104 | +(* last instance reaches the Goal. The first instance's path in *) |
| 105 | +(* that trace may contain unnecessary detours and need not be its own *) |
| 106 | +(* shortest path. *) |
| 107 | +(* *) |
| 108 | +(* Running example (used throughout Sections 1–3): *) |
| 109 | +(* Goal = 2, Cap1 = {j1:9, j2:10}, Cap2 = {j1:1, j2:3} *) |
| 110 | +(* Cap1's shortest solution: 6 steps. Cap2's: 2 steps. *) |
| 111 | +(* *) |
| 112 | +(* With NextParallel, TLC produces the 6-step trace below. Cap1's path *) |
| 113 | +(* is its shortest (6 non-stuttering steps), but Cap2's path has 4 non- *) |
| 114 | +(* stuttering steps — not its shortest 2 (fill j2, pour j2→j1). *) |
| 115 | +(* *) |
| 116 | +(* c1 c2 *) |
| 117 | +(* [j1=0, j2=0] [j1=0, j2=0] initial *) |
| 118 | +(* [j1=0, j2=10] [j1=1, j2=0] *) |
| 119 | +(* [j1=9, j2=1] [j1=1, j2=0] c2 stutters *) |
| 120 | +(* [j1=0, j2=1] [j1=1, j2=0] c2 stutters *) |
| 121 | +(* [j1=1, j2=0] [j1=0, j2=0] c2 goes backwards (empties j1) *) |
| 122 | +(* [j1=1, j2=10] [j1=0, j2=3] *) |
| 123 | +(* [j1=9, j2=2] [j1=1, j2=2] both reach Goal = 2 *) |
| 124 | +(***************************************************************************) |
| 125 | +NextParallel == |
| 126 | + /\ D1!Next |
| 127 | + /\ D2!Next |
| 128 | + /\ UNCHANGED <<s1, s2>> |
| 129 | + |
| 130 | +(***************************************************************************) |
| 131 | +(* SECTION 2. Parallel with per-behavior freeze *) |
| 132 | +(* *) |
| 133 | +(* Once a behavior of an instance reaches the Goal, take no more steps. *) |
| 134 | +(* This is a per-behavior constraint, but TLC's BFS still generates all *) |
| 135 | +(* behaviors, including those in which the faster instance takes detours *) |
| 136 | +(* to keep pace with the slower one. Constraining each behavior *) |
| 137 | +(* individually does not eliminate suboptimal paths to the Goal. (TLC *) |
| 138 | +(* produces the same suboptimal path for Cap2 as in Section 1.) *) |
| 139 | +(***************************************************************************) |
| 140 | +NextParallelFreeze == |
| 141 | + /\ IF Goal \in Range(c1) THEN UNCHANGED c1 ELSE D1!Next |
| 142 | + /\ IF Goal \in Range(c2) THEN UNCHANGED c2 ELSE D2!Next |
| 143 | + /\ UNCHANGED <<s1, s2>> |
| 144 | + |
| 145 | +(***************************************************************************) |
| 146 | +(* SECTION 3. Parallel with global BFS-level freeze *) |
| 147 | +(* *) |
| 148 | +(* Use TLC's (global) registers to record the BFS depth at which each *) |
| 149 | +(* instance first reaches the Goal, then freeze the instance once the *) |
| 150 | +(* current depth exceeds that bound. This correctly finds the globally *) |
| 151 | +(* shortest path for both instances: the freeze threshold is set by *) |
| 152 | +(* the global BFS exploration (which discovers the minimum depth), not *) |
| 153 | +(* by the particular behavior being explored. *) |
| 154 | +(* *) |
| 155 | +(* For the running example, TLC now produces: *) |
| 156 | +(* c1 c2 *) |
| 157 | +(* [j1=0, j2=0] [j1=0, j2=0] initial *) |
| 158 | +(* [j1=0, j2=10] [j1=0, j2=3] *) |
| 159 | +(* [j1=9, j2=1] [j1=1, j2=2] c2 reaches Goal (2 steps) ← *) |
| 160 | +(* [j1=0, j2=1] [j1=1, j2=2] c2 frozen *) |
| 161 | +(* [j1=1, j2=0] [j1=1, j2=2] c2 frozen *) |
| 162 | +(* [j1=1, j2=10] [j1=1, j2=2] c2 frozen *) |
| 163 | +(* [j1=9, j2=2] [j1=1, j2=2] c1 reaches Goal (6 steps) ← *) |
| 164 | +(* *) |
| 165 | +(* Both paths are individually shortest. However, TLCSet and TLCGet *) |
| 166 | +(* are TLC-specific operators outside the logic of TLA+, making this *) |
| 167 | +(* approach incompatible with other TLA+ tools (e.g. Apalache). *) |
| 168 | +(***************************************************************************) |
| 169 | +ASSUME TLCSet(2, 999) /\ TLCSet(3, 999) |
| 170 | + |
| 171 | +NextParallelGlobalFreeze == |
| 172 | + /\ IF TLCGet("level") >= TLCGet(2) THEN UNCHANGED c1 ELSE D1!Next |
| 173 | + /\ IF TLCGet("level") >= TLCGet(3) THEN UNCHANGED c2 ELSE D2!Next |
| 174 | + /\ Goal \in Range(c1') /\ TLCGet(2) = 999 => TLCSet(2, TLCGet("level") + 1) |
| 175 | + /\ Goal \in Range(c2') /\ TLCGet(3) = 999 => TLCSet(3, TLCGet("level") + 1) |
| 176 | + /\ UNCHANGED <<s1, s2>> |
| 177 | + |
| 178 | +(***************************************************************************) |
| 179 | +(* SECTION 4. Interleaved (sequential) composition *) |
| 180 | +(* *) |
| 181 | +(* Each instance steps independently: every transition advances exactly *) |
| 182 | +(* one instance. TLC's BFS explores all interleavings and finds the *) |
| 183 | +(* shortest combined trace, whose length equals the sum of the two *) |
| 184 | +(* individual shortest paths. In the counterexample, s1 and s2 give *) |
| 185 | +(* each configuration's step count. *) |
| 186 | +(* *) |
| 187 | +(* This works because the two instances share no state: any path for one *) |
| 188 | +(* can be freely combined with any path for the other. BFS therefore *) |
| 189 | +(* individually minimizes both s1 and s2. *) |
| 190 | +(***************************************************************************) |
| 191 | +NextInterleaved == |
| 192 | + \/ D1!Next /\ UNCHANGED <<c2, s2>> /\ s1' = s1 + 1 |
| 193 | + \/ D2!Next /\ UNCHANGED <<c1, s1>> /\ s2' = s2 + 1 |
| 194 | + |
| 195 | +Spec == Init /\ [][NextInterleaved]_vars |
| 196 | +----------------------------------------------------------------------------- |
| 197 | +(***************************************************************************) |
| 198 | +(* NotSolved holds as long as the two configurations have not both *) |
| 199 | +(* reached the Goal. A counterexample — a behavior in which both *) |
| 200 | +(* configurations solve the problem — reveals the answer: the final *) |
| 201 | +(* state's s1 and s2 values show each configuration's step count. *) |
| 202 | +(* *) |
| 203 | +(* The ASSUMEs above guarantee that TLC will find a shortest *) |
| 204 | +(* counterexample. *) |
| 205 | +(***************************************************************************) |
| 206 | +NotSolved == |
| 207 | + ~ (Goal \in Range(c1) /\ Goal \in Range(c2)) |
| 208 | +============================================================================= |
0 commit comments