.gitignore

@@ -4,3 +4,4 @@
 *.fuzz
 *.log
 *_tla.txt
+*.dot

Jars/DieHard.tla

@@ -69,15 +69,19 @@ Init == /\ big = 0
 (***************************************************************************)
 FillSmallJug  == /\ small' = 3 
                  /\ big' = big
+                 /\ small < 3     \* added for VisB
 
 FillBigJug    == /\ big' = 5 
                  /\ small' = small
+                 /\ big < 5     \* added for VisB
 
 EmptySmallJug == /\ small' = 0 
                  /\ big' = big
+                 /\ small > 0     \* added for VisB
 
 EmptyBigJug   == /\ big' = 0 
                  /\ small' = small
+                 /\ big > 0     \* added for VisB
 
 (***************************************************************************)
 (* We now consider pouring water from one jug into another.  Again, since  *)
@@ -98,9 +102,13 @@ Min(m,n) == IF m < n THEN m ELSE n
 (***************************************************************************)
 SmallToBig == /\ big'   = Min(big + small, 5)
               /\ small' = small - (big' - big)
+              /\ small > 0     \* added for VisB
+              /\ big < 5       \* added for VisB
 
 BigToSmall == /\ small' = Min(big + small, 3) 
               /\ big'   = big - (small' - small)
+              /\ big > 0     \* added for VisB
+              /\ small < 3   \* added for VisB
 
 (***************************************************************************)
 (* We define the next-state relation, which I like to call Next.  A Next   *)

Jars/DieHard_tla.json

@@ -97,6 +97,22 @@
     "id": "goal",
     "attr": "x2",
     "value": "IF maxf(3) > maxf(5) THEN 48 ELSE 153 END"
+  },
+  {
+  	"id": "fill_%0",
+    "attr": "stroke",
+    "value": "IF level(%0) = %0 THEN \"white\" ELSE \"black\" END",
+	"repeat": [
+        ["3"], ["5"]
+        ]
+  },
+  {
+  	"id": "empty_%0",
+    "attr": "stroke",
+    "value": "IF level(%0) = 0 THEN \"white\" ELSE \"black\" END",
+	"repeat": [
+        ["3"], ["5"]
+        ]
   }
   
 ],
@@ -104,13 +120,13 @@
    {
   	"id": "fill_3",
   	"event": "FillSmallJug",
-        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+        "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
          { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
   },
    {
   	"id": "fill_5",
   	"event": "FillBigJug",
-    "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+    "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
      { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
   },
   {
@@ -124,13 +140,13 @@
   {
   	"id": "empty_3",
   	"event": "EmptySmallJug",
-    "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+    "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
      { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
   },
   {
   	"id": "empty_5",
   	"event": "EmptyBigJug",
-        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+        "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
          { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
   },
   {

Jars/Jars.svg

@@ -27,13 +27,13 @@
 <text id="jar_5_text" opacity="1" x="125" y="95">0</text>
 <line id="goal" x1="107" y1="120" x2="153" y2="120" stroke-width="2" stroke="#FF7777"/>
 
-<circle id="fill_3" cx="25" cy="25" r="15" fill="#BBBBBB"/>
+<circle id="fill_3" cx="25" cy="25" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
 <rect id="fill_3_sym" x="20" y="20" width="10" height="12" style="fill:#267CEB"/>
-<circle id="fill_5" cx="130" cy="25" r="15" fill="#BBBBBB"/>
+<circle id="fill_5" cx="130" cy="25" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
 <rect id="fill_5_sym" x="125" y="20" width="10" height="12" style="fill:#267CEB"/>
-<circle id="empty_3" cx="25" cy="65" r="15" fill="#BBBBBB"/>
+<circle id="empty_3" cx="25" cy="65" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
 <rect id="empty_3_sym" x="20" y="60" width="10" height="12" style="fill:#DDEEFF"/>
-<circle id="empty_5" cx="130" cy="65" r="15" fill="#BBBBBB"/>
+<circle id="empty_5" cx="130" cy="65" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
 <rect id="empty_5_sym" x="125" y="60" width="10" height="12" style="fill:#DDEEFF"/>
 <circle id="transfer" cx="77.5" cy="45" r="15" fill="#BBBBBB"/>
 <polyline id="transfer_left" points="70,45 76,41 76,49" fill="#00000"/>