DieHardest: compare jug configurations via self-composition

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)
+   ]
+=============================================================================

specifications/DieHard/MCDieHardest.cfg

@@ -0,0 +1,9 @@
+SPECIFICATION
+    Spec
+CONSTANT 
+    Goal <- MCGoal
+    Capacities <- MCCapacities
+INVARIANT
+    NotSolved
+ALIAS
+    Alias

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
+=============================================================================

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"
+        }
+      ]
     }
   ]
 }