add TLA+ version of Jars puzzle

Jars/DieHard.tla

+------------------------------ 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.)                            *)
+(***************************************************************************)
+=============================================================================

Jars/DieHard_tla.json

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