From 4af357d62f47b3a972110500c8762acd81c44281 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 12 Feb 2026 19:26:38 -0800 Subject: [PATCH] DieHardest: compare jug configurations via self-composition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add DieHardest.tla, which composes two instances of DieHarder in parallel (synchronous composition) so that TLC can check a 2-hyperproperty as an ordinary invariant. The invariant NotSolved holds as long as both configurations have not yet reached the Goal; a counterexample is a behavior in which both solve the problem, revealing which configuration is slower. The module also defines HasSolution, a GCD-based predicate (via Bézout's identity) used in ASSUME to reject unsolvable configurations before model checking begins. MCDieHardest instantiates the spec with Goal = 4, comparing a 2-jug (5, 3) setup against a 3-jug (5, 3, 4) setup. Co-authored-by: Dmitry Kulagin Signed-off-by: Markus Alexander Kuppe --- specifications/DieHard/DieHardest.tla | 132 ++++++++++++++++++++++++ specifications/DieHard/MCDieHardest.cfg | 9 ++ specifications/DieHard/MCDieHardest.tla | 16 +++ specifications/DieHard/manifest.json | 17 +++ 4 files changed, 174 insertions(+) create mode 100644 specifications/DieHard/DieHardest.tla create mode 100644 specifications/DieHard/MCDieHardest.cfg create mode 100644 specifications/DieHard/MCDieHardest.tla diff --git a/specifications/DieHard/DieHardest.tla b/specifications/DieHard/DieHardest.tla new file mode 100644 index 00000000..f738b464 --- /dev/null +++ b/specifications/DieHard/DieHardest.tla @@ -0,0 +1,132 @@ +----------------------------- MODULE DieHardest ------------------------------ +(***************************************************************************) +(* This module compares two jug configurations by composing two instances *) +(* of DieHarder into a single specification. The two instances share no *) +(* variables and their next-state relations are conjoined, so they advance *) +(* in lock-step: every step of the composed system is a step of both *) +(* instances simultaneously. This is called parallel (or synchronous) *) +(* composition. *) +(* *) +(* The property NotSolved (below) asks whether one configuration can reach *) +(* the Goal while the other has not. This is a question about *pairs* of *) +(* behaviors—one from each configuration—rather than about a single *) +(* behavior. Properties that relate multiple behaviors of a system are *) +(* called hyperproperties; NotSolved is a 2-hyperproperty because it *) +(* relates two behaviors. Ordinary model checkers, including TLC, check *) +(* trace properties (properties of individual behaviors), not *) +(* hyperproperties. The standard workaround is self-composition: run two *) +(* copies of the system side by side and reduce the hyperproperty to an *) +(* ordinary invariant on the product system. That is exactly what this *) +(* module does. *) +(* *) +(* Background: *) +(* - Lamport, "Verifying Hyperproperties With TLA", 2021. *) +(* (https://ieeexplore.ieee.org/document/9505222) *) +(* - Wayne, "Hypermodeling Hyperproperties", 2020 *) +(* (https://hillelwayne.com/post/hyperproperties/). *) +(***************************************************************************) +EXTENDS Naturals, Functions, FiniteSetsExt, TLCExt + +(***************************************************************************) +(* The Die Hard problem has a solution if and only if two conditions are *) +(* satisfied: (1) the Goal is at most the capacity of the largest jug, *) +(* and (2) the Goal is divisible by the greatest common divisor (GCD) of *) +(* all jug capacities. The first condition ensures the goal can fit in *) +(* at least one jug. The second follows from Bézout's Identity and *) +(* number theory: the set of quantities that can be measured with jugs of *) +(* capacities c1, c2, ..., cn is precisely the set of natural number *) +(* multiples of GCD(c1, c2, ..., cn). The definitions below are *) +(* self-contained versions of the necessary mathematical operators to *) +(* avoid naming conflicts. *) +(* *) +(* Note: Condition (1) could be changed to Goal <= sum of all jug *) +(* capacities, reflecting different puzzle rules where the goal may be *) +(* distributed across multiple jugs rather than contained in a single one. *) +(***************************************************************************) +HasSolution(capacity, goal) == + LET DivDH(d, n) == \E k \in 0..n : n = d * k + CDivDH(S) == {d \in 1..Min(S): \A n \in S: DivDH(d, n)} + GCDDH(S) == IF S = {} THEN 0 ELSE Max(CDivDH(S)) + IN /\ goal <= Max(Range(capacity)) + /\ DivDH(GCDDH(Range(capacity)), goal) + +CONSTANT Capacities, + Goal + +(***************************************************************************) +(* The two configurations must differ; comparing a configuration with *) +(* itself is uninteresting. *) +(***************************************************************************) +ASSUME Capacities[1] # Capacities[2] + +(***************************************************************************) +(* Both configurations must have a solution. If either does not, TLC *) +(* will never reach the Goal and will report no counterexample. *) +(***************************************************************************) +ASSUME /\ HasSolution(Capacities[1], Goal) + /\ HasSolution(Capacities[2], Goal) + +VARIABLE c1, c2 +vars == << c1, c2 >> + +D1 == INSTANCE DieHarder + WITH Jug <- DOMAIN Capacities[1], + Capacity <- Capacities[1], + Goal <- Goal, + contents <- c1 + +D2 == INSTANCE DieHarder + WITH Jug <- DOMAIN Capacities[2], + Capacity <- Capacities[2], + Goal <- Goal, + contents <- c2 + +Init == D1!Init /\ D2!Init + +Next == D1!Next /\ D2!Next + +Spec == Init /\ [][Next]_vars +----------------------------------------------------------------------------- + +(***************************************************************************) +(* NotSolved is the 2-hyperproperty reduced to an invariant of the *) +(* composed system (see the module comment above). It holds as long as *) +(* the two configurations have not both reached the Goal. A *) +(* counterexample is a behavior in which both configurations solve the *) +(* problem. *) +(* *) +(* - TLC reports no counterexample if either configuration cannot reach *) +(* the Goal (prevented by the ASSUMEs above). *) +(* *) +(* - TLC reports a counterexample when both configurations reach the *) +(* Goal in the same step. This is perhaps unexpected but harmless. *) +(* *) +(* - TLC reports a counterexample when one configuration reaches the *) +(* Goal before the other. Because Next conjoins D1!Next and D2!Next, *) +(* both configurations advance together in every non-stuttering step. *) +(* The trace has the length of the slower configuration; in some steps *) +(* the faster one makes no useful progress. *) +(***************************************************************************) +NotSolved == + ~ (Goal \in Range(c1) /\ Goal \in Range(c2)) + +(***************************************************************************) +(* The Alias below uses TLCGetAndSet to count non-stuttering steps in *) +(* each instance (s1 and s2), i.e., steps in which the jug contents *) +(* actually change. In a counterexample trace, s1 and s2 reveal which *) +(* configuration reaches the Goal first and how many moves it takes. *) +(* (In the TLA+ VS Code / Cursor extension, the modification markers in *) +(* the model-checking view provide the same information visually.) *) +(* *) +(* An alternative would be to add s1 and s2 as specification variables *) +(* and update them in the next-state relation, but that would pollute the *) +(* spec with bookkeeping that is irrelevant to the problem being modeled. *) +(***************************************************************************) +Alias == + [ + c1 |-> c1, + c2 |-> c2, + s1 |-> TLCGetAndSet(0, +, IF UNCHANGED c1 THEN 0 ELSE 1, 1), + s2 |-> TLCGetAndSet(1, +, IF UNCHANGED c2 THEN 0 ELSE 1, 1) + ] +============================================================================= diff --git a/specifications/DieHard/MCDieHardest.cfg b/specifications/DieHard/MCDieHardest.cfg new file mode 100644 index 00000000..d07cf8d7 --- /dev/null +++ b/specifications/DieHard/MCDieHardest.cfg @@ -0,0 +1,9 @@ +SPECIFICATION + Spec +CONSTANT + Goal <- MCGoal + Capacities <- MCCapacities +INVARIANT + NotSolved +ALIAS + Alias \ No newline at end of file diff --git a/specifications/DieHard/MCDieHardest.tla b/specifications/DieHard/MCDieHardest.tla new file mode 100644 index 00000000..6a3dd7d3 --- /dev/null +++ b/specifications/DieHard/MCDieHardest.tla @@ -0,0 +1,16 @@ +----------------------------- MODULE MCDieHardest ------------------------------ +EXTENDS TLC, DieHardest + +MCGoal == 4 + +MCCapacity1 == "j1" :> 5 @@ "j2" :> 3 + +MCCapacity2 == "j1" :> 5 @@ "j2" :> 3 @@ "j3" :> 4 + +MCCapacities == + << + MCCapacity1, + MCCapacity2 + >> +MCJugs == DOMAIN MCCapacities +============================================================================= diff --git a/specifications/DieHard/manifest.json b/specifications/DieHard/manifest.json index 1f335f53..50e08b87 100644 --- a/specifications/DieHard/manifest.json +++ b/specifications/DieHard/manifest.json @@ -35,6 +35,23 @@ "result": "safety failure" } ] + }, + { + "path": "specifications/DieHard/DieHardest.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/DieHard/MCDieHardest.tla", + "features": [], + "models": [ + { + "path": "specifications/DieHard/MCDieHardest.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "safety failure" + } + ] } ] } \ No newline at end of file