add waterheater (Wasserkocher) example

VisB-Examples.prob2project

@@ -94,6 +94,7 @@
       "symbolicAnimationFormulas": [],
       "testCases": [],
       "traces": [
+        "traces/MovingParticles3.prob2trace",
         "traces/MovingParticles.prob2trace"
       ],
       "modelcheckingItems": [],
@@ -112,13 +113,27 @@
       "traces": [],
       "modelcheckingItems": [],
       "visBVisualisation": null
+    },
+    {
+      "name": "WasserkocherEinfach_mch",
+      "description": "",
+      "location": "Waterboiler/WasserkocherEinfach_mch.eventb",
+      "lastUsedPreferenceName": "default",
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "testCases": [],
+      "traces": [],
+      "modelcheckingItems": [],
+      "visBVisualisation": "Waterboiler/visb_wasserkocher.json"
     }
   ],
   "preferences": [],
   "metadata": {
     "fileType": "Project",
     "formatVersion": 9,
-    "savedAt": "2020-11-12T16:09:03.372063Z",
+    "savedAt": "2020-11-20T09:34:16.941580Z",
     "creator": "User",
     "proB2KernelVersion": "4.0.0-SNAPSHOT",
     "proBCliVersion": null,

Waterboiler/WasserkocherEinfach_mch.eventb

+package(load_event_b_project([event_b_model(none,'WasserkocherEinfach',[sees(none,[]),variables(none,[identifier(none,an),identifier(none,deckel_zu)]),invariant(none,[conjunct(rodinpos('WasserkocherEinfach',type,'_oTcjUb1TEeeOg4aHCVa6rA'),member(none,identifier(none,an),bool_set(none)),member(none,identifier(none,deckel_zu),bool_set(none))),implication(rodinpos('WasserkocherEinfach',safety,'_7UekQL1TEeeOg4aHCVa6rA'),equal(none,identifier(none,an),boolean_true(none)),equal(none,identifier(none,deckel_zu),boolean_true(none)))]),theorems(none,[]),events(none,[event(rodinpos('WasserkocherEinfach','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('WasserkocherEinfach',init,'_rabiYL1TEeeOg4aHCVa6rA'),[identifier(none,an),identifier(none,deckel_zu)],[boolean_false(none),boolean_false(none)])],[]),event(rodinpos('WasserkocherEinfach',deckel_zu,'_y4IDAL1TEeeOg4aHCVa6rA'),deckel_zu,ordinary(none),[],[],[equal(rodinpos('WasserkocherEinfach',g1,'_y4IqEL1TEeeOg4aHCVa6rA'),identifier(none,deckel_zu),boolean_false(none))],[],[assign(rodinpos('WasserkocherEinfach',a,'_y4IqEb1TEeeOg4aHCVa6rA'),[identifier(none,deckel_zu)],[boolean_true(none)])],[]),event(rodinpos('WasserkocherEinfach',deckel_auf,'_2SuhoL1TEeeOg4aHCVa6rA'),deckel_auf,ordinary(none),[],[],[conjunct(rodinpos('WasserkocherEinfach',g1,'_2Suhob1TEeeOg4aHCVa6rA'),equal(none,identifier(none,deckel_zu),boolean_true(none)),equal(none,identifier(none,an),boolean_false(none)))],[],[assign(rodinpos('WasserkocherEinfach',a,'_2Suhor1TEeeOg4aHCVa6rA'),[identifier(none,deckel_zu)],[boolean_false(none)])],[]),event(rodinpos('WasserkocherEinfach',an,'_5ZFOkL1TEeeOg4aHCVa6rA'),an,ordinary(none),[],[],[conjunct(rodinpos('WasserkocherEinfach',g1,'_5ZFOkb1TEeeOg4aHCVa6rA'),equal(none,identifier(none,deckel_zu),boolean_true(none)),equal(none,identifier(none,an),boolean_false(none)))],[],[assign(rodinpos('WasserkocherEinfach',a,'_5ZFOkr1TEeeOg4aHCVa6rA'),[identifier(none,an)],[boolean_true(none)])],[])])])],[],[exporter_version(3),po('WasserkocherEinfach','Invariant  establishment',[event('INITIALISATION'),invariant(type)],true),po('WasserkocherEinfach','Invariant  establishment',[event('INITIALISATION'),invariant(safety)],true),po('WasserkocherEinfach','Invariant  preservation',[event(deckel_zu),invariant(type)],true),po('WasserkocherEinfach','Invariant  preservation',[event(deckel_zu),invariant(safety)],true),po('WasserkocherEinfach','Invariant  preservation',[event(deckel_auf),invariant(type)],true),po('WasserkocherEinfach','Invariant  preservation',[event(deckel_auf),invariant(safety)],true),po('WasserkocherEinfach','Invariant  preservation',[event(an),invariant(type)],true),po('WasserkocherEinfach','Invariant  preservation',[event(an),invariant(safety)],true)],_Error)).
+

Waterboiler/visb_wasserkocher.json

+{
+  "svg": "waterheater.svg",
+  "items": [
+    {
+      "id": "cap_open",
+      "attr": "visibility",
+      "value": "IF deckel_zu=FALSE THEN \"visible\" ELSE \"hidden\" END"
+    },
+    {
+      "id": "cap_closed",
+      "attr": "visibility",
+      "value": "IF deckel_zu=TRUE & an=FALSE THEN \"visible\" ELSE \"hidden\" END"
+    },
+    {
+      "id": "cap_closed_on",
+      "attr": "visibility",
+      "value": "IF deckel_zu=TRUE & an=TRUE THEN \"visible\" ELSE \"hidden\" END"
+    },
+    {
+      "id": "turn_on",
+      "attr": "opacity",
+      "value": "IF deckel_zu=TRUE & an=FALSE THEN 1.0 ELSE 0.4 END"
+    },
+    {
+      "id": "turn_off",
+      "attr": "visibility",
+      "value": "IF an=TRUE THEN \"visible\" ELSE \"hidden\" END"
+    }
+  ],
+  "events": [
+    {
+      "id": "turn_on",
+      "event": "an",
+      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+                 { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+    },
+    {
+      "id": "cap_closed",
+      "event": "deckel_auf",
+      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+                 { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+    },
+    {
+      "id": "cap_open",
+      "event": "deckel_zu",
+      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+                 { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+    }
+  ]
+}