diff --git a/Jars/Jars.json b/Jars/Jars.json new file mode 100644 index 0000000000000000000000000000000000000000..7d426ff08cd9bd61814349a1f834bf9924243c41 --- /dev/null +++ b/Jars/Jars.json @@ -0,0 +1,86 @@ +{ + "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" + } + ] +} + diff --git a/Jars/Jars.mch b/Jars/Jars.mch index d1106cfc1b5cdb19245b10caaee884b5d0f46f02..e1bca3dc2cb372702811d0e827934a3101321634 100644 --- a/Jars/Jars.mch +++ b/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 diff --git a/Jars/Jars.prob2project b/Jars/Jars.prob2project new file mode 100644 index 0000000000000000000000000000000000000000..62c08f71f6487207f4513413ddb106289f145eb3 --- /dev/null +++ b/Jars/Jars.prob2project @@ -0,0 +1,34 @@ +{ + "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 diff --git a/Jars/Jars.svg b/Jars/Jars.svg new file mode 100644 index 0000000000000000000000000000000000000000..5a6cc18970ca21d8c6713ee0822437137144b071 --- /dev/null +++ b/Jars/Jars.svg @@ -0,0 +1,28 @@ +<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"/>