Create VisB visualization for Jars (by Jonas Erdmann)

Jars/Jars.json

+{
+  "svg":"Jars.svg",
+  "items": [
+  {
+  	"id": "rect_3",
+  	"attr": "height",
+
+  	"value": "level(j3) * 20"
+  },
+  {
+  	"id": "rect_5",
+  	"attr": "height",
+
+  	"value": "level(j5) * 20"
+  }
+],
+  "events": [
+   {
+  	"id": "fill_3",
+  	"event": "FillJar",
+  	"predicates": ["j=j3"],
+        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+         { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+  },
+  {
+  	"id": "fill_3_sym",
+  	"event": "FillJar",
+  	"predicates": ["j=j3"]
+  },
+  {
+  	"id": "fill_5",
+  	"event": "FillJar",
+  	"predicates": ["j=j5"],
+        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+         { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+  },
+  {
+  	"id": "fill_5_sym",
+  	"event": "FillJar",
+  	"predicates": ["j=j5"]
+  },
+  {
+  	"id": "empty_3",
+  	"event": "EmptyJar",
+  	"predicates": ["j=j3"],
+        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+         { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+  },
+  {
+  	"id": "empty_3_sym",
+  	"event": "EmptyJar",
+  	"predicates": ["j=j3"]
+  },
+  {
+  	"id": "empty_5",
+  	"event": "EmptyJar",
+  	"predicates": ["j=j5"],
+        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+         { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+  },
+  {
+  	"id": "empty_5_sym",
+  	"event": "EmptyJar",
+  	"predicates": ["j=j5"]
+  },
+  {
+  	"id": "transfer",
+  	"event": "Transfer",
+        "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+         { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+  },
+  {
+  	"id": "transfer_sym1",
+  	"event": "Transfer"
+  },
+  {
+  	"id": "transfer_sym2",
+  	"event": "Transfer"
+  },
+  {
+  	"id": "transfer_sym3",
+  	"event": "Transfer"
+  }
+  ]
+}
+

Jars/Jars.mch

@@ -7,7 +7,20 @@ Input: one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gal
 */
 DEFINITIONS
   GOAL == (4:ran(level));
-  gmax == max(ran(maxf))
+  ANIMATION_IMG1 == "images/Filled.gif";
+  ANIMATION_IMG2 == "images/Empty.gif";
+  ANIMATION_IMG3 == "images/Void.gif";
+  gmax == max(ran(maxf));
+  ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
+  ri == (gmax+1-r);
+  ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
+                                 (ri<=level(c) => i=1 ) & (ri>level(c) => i=2)};
+  ANIMATION_RIGHT_CLICK(J,Fill) ==
+               ANY J2,Amount WHERE J2:Jars & Amount:1..gmax THEN
+                CHOICE EmptyJar({1|->j3,2|->j5}(J)) OR FillJar({1|->j3,2|->j5}(J)) OR
+                       Transfer(J2,Amount,{1|->j3,2|->j5}(J))
+                END
+               END;
 SETS
  Jars = {j3,j5}
 CONSTANTS maxf

Jars/Jars.prob2project

+{
+  "name": "Jars",
+  "description": "(Projekt wurde automatisch aus Datei /home/gastentwickler/Downloads/Jars/Jars.mch erstellt)",
+  "machines": [
+    {
+      "name": "Jars",
+      "description": "",
+      "location": "Jars.mch",
+      "lastUsedPreferenceName": "default",
+      "requirements": [],
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "simulationItems": [],
+      "testCases": [],
+      "traces": [],
+      "modelcheckingItems": [],
+      "simulation": null,
+      "visBVisualisation": "Jars.json",
+      "historyChartItems": []
+    }
+  ],
+  "preferences": [],
+  "metadata": {
+    "fileType": "Project",
+    "formatVersion": 20,
+    "savedAt": "2022-01-27T10:21:05.310877Z",
+    "creator": "User",
+    "proB2KernelVersion": "4.0.0-SNAPSHOT",
+    "proBCliVersion": null,
+    "modelName": null
+  }
+}
\ No newline at end of file

Jars/Jars.svg

+<svg width="360" height="360"
+  xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="jar_3" transform="rotate(180 25 100)">
+	<svg width="50" height="60" X="0" y="100"> 
+	<g id="leer_3" opacity="1">
+	<rect x="0" y="0" width="50" height="60" style="fill:#DDEEFF"/>
+	<rect id="rect_3" x="0" y="0" width="50" height="60" style="fill:#0000FF"/>
+	</svg>
+</g>
+<g id="jar_5" transform="rotate(180 130 100)">
+	<svg width="50" height="100" X="105" y="100">
+	<g id="leer_5" opacity="1">
+	<rect x="0" y="0" width="50" height="100" style="fill:#DDEEFF"/>
+	<rect id ="rect_5" x="0" y="0" width="50" height="100" style="fill:#0000FF"/>
+	</svg>
+</g>
+<circle id="fill_3" cx="25" cy="125" r="15" fill="#7799FF"/>
+<rect id="fill_3_sym" x="20" y="120" width="10" height="12" style="fill:#0000FF"/>
+<circle id="fill_5" cx="130" cy="125" r="15" fill="#7799FF"/>
+<rect id="fill_5_sym"x="125" y="120" width="10" height="12" style="fill:#0000FF"/>
+<circle id="empty_3" cx="25" cy="165" r="15" fill="#7799FF"/>
+<rect id="empty_3_sym" x="20" y="160" width="10" height="12" style="fill:#DDDDFF"/>
+<circle id="empty_5" cx="130" cy="165" r="15" fill="#7799FF"/>
+<rect id="empty_5_sym" x="125" y="160" width="10" height="12" style="fill:#DDDDFF"/>
+<circle id="transfer" cx="77.5" cy="145" r="15" fill="#7799FF"/>
+<polyline id="transfer_sym1" points="70,145 76,141 76,149" fill="#00000"/>  
+<polyline id="transfer_sym2" points="85,145 79,141 79,149" fill="#00000"/>
+<rect id="transfer_sym3" x="76" y="143.5" height="3" width="3"/>