From bd2594fe626a8239698e79bebba6fb428fe9dc46 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 3 Sep 2024 15:32:37 +0200
Subject: [PATCH] add TLA+ version of Jars puzzle
---
Jars/DieHard.tla | 141 ++++++++++++++++++++++++++++++++++
Jars/DieHard_tla.json | 172 ++++++++++++++++++++++++++++++++++++++++++
2 files changed, 313 insertions(+)
create mode 100644 Jars/DieHard.tla
create mode 100644 Jars/DieHard_tla.json
diff --git a/Jars/DieHard.tla b/Jars/DieHard.tla
new file mode 100644
index 0000000..bedfe7d
--- /dev/null
+++ b/Jars/DieHard.tla
@@ -0,0 +1,141 @@
+------------------------------ MODULE DieHard -------------------------------
+(* File from TLC distribution; minor change for ProB and VisB *)
+(***************************************************************************)
+(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
+(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
+(* goal: to get TLC to solve the problem for us. *)
+(* *)
+(* First, we write a spec that describes all allowable behaviors of our *)
+(* heros. *)
+(***************************************************************************)
+EXTENDS Integers
+ (*************************************************************************)
+ (* This statement imports the definitions of the ordinary operators on *)
+ (* natural numbers, such as +. *)
+ (*************************************************************************)
+
+
+(***************************************************************************)
+(* We next declare the specification's variables. *)
+(***************************************************************************)
+VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
+ small \* The number of gallons of water in the 3 gallon jug.
+
+
+VISB_JSON_FILE == "DieHard_tla.json" \* addition for ProB-VisB
+GOAL == (big=4) \* for ProB; not really required; config file has invariant
+
+(***************************************************************************)
+(* We now define TypeOK to be the type invariant, asserting that the value *)
+(* of each variable is an element of the appropriate set. A type *)
+(* invariant like this is not part of the specification, but it's *)
+(* generally a good idea to include it because it helps the reader *)
+(* understand the spec. Moreover, having TLC check that it is an *)
+(* invariant of the spec catches errors that, in a typed language, are *)
+(* caught by type checking. *)
+(* *)
+(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
+(* or \/ denotes the conjunction or disjunction of those formulas. *)
+(* Indentation of subitems is significant, allowing one to eliminate lots *)
+(* of parentheses. This makes a large formula much easier to read. *)
+(* However, it does mean that you have to be careful with your indentation.*)
+(***************************************************************************)
+TypeOK == /\ small \in 0..3
+ /\ big \in 0..5
+
+
+(***************************************************************************)
+(* Now we define of the initial predicate, that specifies the initial *)
+(* values of the variables. I like to name this predicate Init, but the *)
+(* name doesn't matter. *)
+(***************************************************************************)
+Init == /\ big = 0
+ /\ small = 0
+
+(***************************************************************************)
+(* Now we define the actions that our hero can perform. There are three *)
+(* things they can do: *)
+(* *)
+(* - Pour water from the faucet into a jug. *)
+(* *)
+(* - Pour water from a jug onto the ground. *)
+(* *)
+(* - Pour water from one jug into another *)
+(* *)
+(* We now consider the first two. Since the jugs are not calibrated, *)
+(* partially filling or partially emptying a jug accomplishes nothing. *)
+(* So, the first two possibilities yield the following four possible *)
+(* actions. *)
+(***************************************************************************)
+FillSmallJug == /\ small' = 3
+ /\ big' = big
+
+FillBigJug == /\ big' = 5
+ /\ small' = small
+
+EmptySmallJug == /\ small' = 0
+ /\ big' = big
+
+EmptyBigJug == /\ big' = 0
+ /\ small' = small
+
+(***************************************************************************)
+(* We now consider pouring water from one jug into another. Again, since *)
+(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
+(* makes sense only to either fill B or empty A. And there's no point in *)
+(* emptying A if this will cause B to overflow, since that could be *)
+(* accomplished by the two actions of first filling B and then emptying A. *)
+(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
+(* contained in both jugs and (ii) the volume of B. To express this *)
+(* mathematically, we first define Min(m,n) to equal the minimum of the *)
+(* numbers m and n. *)
+(***************************************************************************)
+Min(m,n) == IF m < n THEN m ELSE n
+
+(***************************************************************************)
+(* Now we define the last two pouring actions. From the observation *)
+(* above, these definitions should be clear. *)
+(***************************************************************************)
+SmallToBig == /\ big' = Min(big + small, 5)
+ /\ small' = small - (big' - big)
+
+BigToSmall == /\ small' = Min(big + small, 3)
+ /\ big' = big - (small' - small)
+
+(***************************************************************************)
+(* We define the next-state relation, which I like to call Next. A Next *)
+(* step is a step of one of the six actions defined above. Hence, Next is *)
+(* the disjunction of those actions. *)
+(***************************************************************************)
+Next == \/ FillSmallJug
+ \/ FillBigJug
+ \/ EmptySmallJug
+ \/ EmptyBigJug
+ \/ SmallToBig
+ \/ BigToSmall
+
+(***************************************************************************)
+(* We define the formula Spec to be the complete specification, asserting *)
+(* of a behavior that it begins in a state satisfying Init, and that every *)
+(* step either satisfies Next or else leaves the pair <<big, small>> *)
+(* unchanged. *)
+(***************************************************************************)
+Spec == Init /\ [][Next]_<<big, small>>
+-----------------------------------------------------------------------------
+
+(***************************************************************************)
+(* Remember that our heros must measure out 4 gallons of water. *)
+(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
+(* solved their problem when they reach a state with big = 4. So, we *)
+(* define NotSolved to be the predicate asserting that big # 4. *)
+(***************************************************************************)
+NotSolved == big # 4
+
+(***************************************************************************)
+(* We find a solution by having TLC check if NotSolved is an invariant, *)
+(* which will cause it to print out an "error trace" consisting of a *)
+(* behavior ending in a states where NotSolved is false. Such a *)
+(* behavior is the desired solution. (Because TLC uses a breadth-first *)
+(* search, it will find the shortest solution.) *)
+(***************************************************************************)
+=============================================================================
diff --git a/Jars/DieHard_tla.json b/Jars/DieHard_tla.json
new file mode 100644
index 0000000..7671df9
--- /dev/null
+++ b/Jars/DieHard_tla.json
@@ -0,0 +1,172 @@
+{
+ "svg":"Jars.svg",
+ "comment": "VisB Visualization for Jars by Jonas Erdmann",
+ "definitions":[
+ {"name":"level",
+ "value": "{3|->small, 5|->big}",
+ "comment":"simulating the level variable from the classical B model"
+ },
+ {"name":"maxf",
+ "value": "{3|->3, 5|->5}",
+ "comment":"simulating the level variable from the classical B model"
+ }
+ ],
+ "items": [
+ {
+ "id": "jar_%0_full",
+ "attr": "height",
+ "value": "level(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_text",
+ "attr": "text",
+ "value": "level(%0)",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_svg",
+ "attr": "height",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_svg",
+ "attr": "y",
+ "value": "0 -(max({maxf(3), maxf(5)}) * 20 - 100)",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_empty",
+ "attr": "height",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "left_%0",
+ "attr": "y2",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "right_%0",
+ "attr": "y2",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "goal_achieved",
+ "attr": "opacity",
+ "value": "IF max({level(3), level(5)}) = max({maxf(3), maxf(5)}) -1 THEN 1 ELSE 0 END"
+ },
+ {
+ "id": "transfer_left",
+ "attr": "opacity",
+ "value": "IF level(3) = maxf(3) THEN 0 ELSE IF level(5) = 0 THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "transfer_right",
+ "attr": "opacity",
+ "value": "IF level(5) = maxf(5) THEN 0 ELSE IF level(3) = 0 THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "transfer_sym3",
+ "attr": "opacity",
+ "value": "IF level(3) = 0 & level(5) = 0 THEN 0 ELSE IF level(3) = maxf(3) & level(5) = maxf(5) THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "goal",
+ "attr": "x1",
+ "value": "IF maxf(3) > maxf(5) THEN 2 ELSE 107 END"
+ },
+ {
+ "id": "goal",
+ "attr": "x2",
+ "value": "IF maxf(3) > maxf(5) THEN 48 ELSE 153 END"
+ }
+
+],
+ "events": [
+ {
+ "id": "fill_3",
+ "event": "FillSmallJug",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "fill_5",
+ "event": "FillBigJug",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "fill_3_sym",
+ "event": "FillSmallJug"
+ },
+ {
+ "id": "fill_5_sym",
+ "event": "FillBigJug"
+ },
+ {
+ "id": "empty_3",
+ "event": "EmptySmallJug",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "empty_5",
+ "event": "EmptyBigJug",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "empty_3_sym",
+ "event": "EmptySmallJug"
+ },
+ {
+ "id": "empty_5_sym",
+ "event": "EmptyBigJug"
+ },
+ {
+ "id": "transfer",
+ "event": "BigToSmall",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "transfer",
+ "event": "SmallToBig"
+ },
+ {
+ "id": "transfer_left",
+ "event": "BigToSmall"
+ },
+ {
+ "id": "transfer_right",
+ "event": "SmallToBig"
+ },
+ {
+ "id": "transfer_sym3",
+ "event": "BigToSmall"
+ },
+ {
+ "id": "transfer_sym3",
+ "event": "SmallToBig"
+ }
+ ]
+}
+
--
GitLab