diff --git a/Reals/WaterTankReals.tla b/Reals/WaterTankReals.tla
new file mode 100644
index 0000000000000000000000000000000000000000..7ef24def8e8633529bc290068d33f7d9d436e551
--- /dev/null
+++ b/Reals/WaterTankReals.tla
@@ -0,0 +1,49 @@
+---------------------- MODULE WaterTankReals ----------------------
+EXTENDS Naturals, Reals
+CONSTANTS
+ low_threshold,
+ high_threshold,
+ (*@ unit s *) step_size,
+ (*@ unit m**3 / s *) outflow,
+ inflow
+ASSUME
+ /\ low_threshold = 20.0
+ /\ high_threshold = 60.0
+ /\ outflow = 10.0
+ /\ inflow = 15.0
+ /\ step_size = 0.5
+VARIABLES
+ pump,
+ level
+Init == level \in {50.0} /\ pump=FALSE
+SwitchPump == pump' = IF level < low_threshold THEN TRUE ELSE IF level > high_threshold THEN FALSE ELSE pump
+UpdateLevel == level' = IF pump THEN level + inflow * step_size - outflow * step_size ELSE level - outflow * step_size
+Next == SwitchPump /\ UpdateLevel
+WaterTank == Init /\ [][Next]_{pump}
+
+
+lft == 10.0 \* left offset
+wid == 30.0 \* width of water tank
+bot == 120.0 \* bottom of water tank display
+maxw == high_threshold+inflow \* maximum capacity as shown
+Invariant == level > 0.0 /\ level <= maxw
+convy(lvl) == bot-lvl
+VISB_SVG_BOX == [width |-> wid+4.0*lft, height |-> bot+lft]
+VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level), height |-> level, width |-> wid,
+ fill |-> "lightsteelblue"]
+VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid,
+ fill |-> "none", stroke |-> "black", stroke_width|->1.0]
+VISB_SVG_OBJECTS2 == [svg_class |-> "line", x1|->lft-0.5, x2|->lft+wid+0.5,
+ y1|->convy(low_threshold), y2|->convy(low_threshold),
+ stroke |-> "red", stroke_width|->1.0] \* line for low_threshold
+VISB_SVG_OBJECTS3 == [svg_class |-> "line", x1|->lft-0.5, x2|->lft+wid+0.5,
+ y1|->convy(high_threshold), y2|->convy(high_threshold),
+ stroke |-> "red", stroke_width|->1.0] \* line for high_threshold
+VISB_SVG_OBJECTS4 == [svg_class |-> "rect", x|->lft, y |-> 2.0*lft, height |-> lft, width |-> wid, rx|->5,
+ fill |-> IF pump THEN "mediumseagreen" ELSE "palegoldenrod",
+ stroke |-> "black", stroke_width|->1.0]
+VISB_SVG_OBJECTS5 == [svg_class |-> "text", x|->lft+5.0, y |-> 2.0*lft-8.0, text|->"Pump:", font_size|->8.0]
+VISB_SVG_OBJECTS6 == [svg_class |-> "text", x|->lft+9.5, y |-> 2.0*lft+7.2, text|->IF pump THEN "on" ELSE "off", font_size|->8.0]
+--------------------------------------------------------------
+THEOREM WaterTank => []Init
+==============================================================
\ No newline at end of file
diff --git a/Reals/WaterTankRealsHistory.html b/Reals/WaterTankRealsHistory.html
new file mode 100644
index 0000000000000000000000000000000000000000..cb691200f5acd7532b7080c8206b6e617b43316d
--- /dev/null
+++ b/Reals/WaterTankRealsHistory.html
@@ -0,0 +1,755 @@
+<!DOCTYPE html>
+<html>
+<head>
+ <!-- html file generated by ProB from a VisB visualization -->
+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
+ <meta http-equiv="content-type" content="text/html; charset=utf-8">
+ <script>
+ function setAttr(id, attribute, value){
+ const obj = document.getElementById(id);
+ if (obj == null) {
+ if (id != "visb_debug_messages") {
+ console.error("Unknown SVG id " + id + " for attribute " + attribute);
+ }
+ } else if(attribute=="text") {
+ obj.textContent = value;
+ } else if(attribute=="class" && value != "") {
+ if(value[0]=="+") {
+ obj.classList.add(value.substring(1));
+ } else if(value[0]=="-") {
+ obj.classList.remove(value.substring(1));
+ } else {
+ obj.setAttribute(attribute, value);
+ }
+ } else {
+ obj.setAttribute(attribute, value);
+ }
+ }
+ function sleep(ms) {
+ return new Promise(resolve => setTimeout(resolve, ms));
+ }
+ let lastSelectedRow = 0;
+ function highlightRow(id) {
+ if (lastSelectedRow>0) {setAttr("row"+lastSelectedRow,"bgcolor","")}
+ setAttr("row"+id,"bgcolor","yellow");
+ lastSelectedRow = id;
+ }
+ function backStep() {
+ if (lastSelectedRow>1) {
+ const prev = lastSelectedRow - 1;
+ document.getElementById("row"+prev).click();
+ }
+ }
+ function forwardStep() {
+ if (lastSelectedRow>0) {
+ const nxt = lastSelectedRow + 1;
+ const row = document.getElementById("row" + (nxt));
+ if (row != null) { row.click() }
+ }
+ }
+ </script>
+
+ <style>
+ table {
+ font-family: arial, sans-serif;
+ font-size: 11px;
+ border-collapse: collapse;
+ width: 100%;
+ }
+ td, th {
+ border: 1px solid #dddddd;
+ text-align: left;
+ padding: 2px;
+ }
+/*
+ tr:nth-child(even) {
+ background-color: #dddddd;
+ }
+ */
+ </style>
+
+ <style>
+ .collapsible {
+ cursor: pointer;
+ }
+ .collapsible-style {
+ background-color: #777;
+ color: white;
+ padding: 6px;
+ width: 100%;
+ border: none;
+ text-align: left;
+ outline: none;
+ font-size: 12px;
+ }
+
+ .active, .collapsible:hover {
+ background-color: #555;
+ }
+
+ .collapsible:after {
+ content: '\002B';
+ color: white;
+ font-weight: bold;
+ float: right;
+ margin-left: 5px;
+ }
+
+ .active:after {
+ content: "\2212";
+ }
+
+ .coll-content-hid {
+ padding: 0 12px;
+ display: none;
+ overflow: hidden;
+ background-color: #f1f1f1;
+ }
+ .coll-content-vis {
+ padding: 0 12px;
+ display: block;
+ overflow: hidden;
+ background-color: #f1f1f1;
+ }
+ .visb-messages {
+ text-align: left;
+ outline: none;
+ font-size: 12px;
+ font-family: arial, sans-serif;
+ }
+ .svg-outer-container {
+ width: 100%;
+ height: 100%;
+ overflow: auto;
+ visibility: hidden;
+ resize: vertical;
+ }
+ .svg-inner-container {
+ width: 100%;
+ height: 100%;
+ display: flex;
+ transform-origin: left top;
+ /*cursor: grab;*/
+ }
+ .svg-inner-container:active {
+ cursor: grabbing;
+ }
+ svg {
+ width: 100%;
+ height: 100%;
+ }
+ </style>
+
+
+
+ <script>
+ const differences = [
+ [
+ {id: "trace_meter", attr: "value", val: "1"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 1/42, State ID: 0, Event: SETUP_CONSTANTS(low_threshold=20.0,high_threshold=60.0,step_size=0.5,outflow=10.0,inflow=15.0) "},
+ {id: "bOperation_Next", attr: "text", val: "⛔"},
+ {id: "row_bOperation_Next", attr: "bgcolor", val: "#f1f1f1"},
+ {id: "name_bOperation_Next", attr: "text", val: "Next"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "2"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 2/42, State ID: 1, Event: INITIALISATION(level=50.0,pump=FALSE) "},
+ {id: "svg_id__1", attr: "height", val: "50.0"},
+ {id: "svg_id__1", attr: "y", val: "70.0"},
+ {id: "svg_id__5", attr: "fill", val: "palegoldenrod"},
+ {id: "svg_id__7", attr: "text", val: "off"},
+ {id: "bVar_level", attr: "text", val: "50.0"},
+ {id: "row_bVar_level", attr: "bgcolor", val: "#fffacd"},
+ {id: "bVarPrev_level", attr: "text", val: "?"},
+ {id: "bVar_pump", attr: "text", val: "FALSE"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "#fffacd"},
+ {id: "bVarPrev_pump", attr: "text", val: "?"},
+ {id: "bOperation_Next", attr: "text", val: "✅"},
+ {id: "row_bOperation_Next", attr: "bgcolor", val: "white"},
+ {id: "name_bOperation_Next", attr: "text", val: "Next"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "3"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 3/42, State ID: 2, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "45.0"},
+ {id: "svg_id__1", attr: "y", val: "75.0"},
+ {id: "bVar_level", attr: "text", val: "45.0"},
+ {id: "bVarPrev_level", attr: "text", val: "50.0"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "white"},
+ {id: "bVarPrev_pump", attr: "text", val: "FALSE"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "4"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 4/42, State ID: 3, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "40.0"},
+ {id: "svg_id__1", attr: "y", val: "80.0"},
+ {id: "bVar_level", attr: "text", val: "40.0"},
+ {id: "bVarPrev_level", attr: "text", val: "45.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "5"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 5/42, State ID: 4, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "35.0"},
+ {id: "svg_id__1", attr: "y", val: "85.0"},
+ {id: "bVar_level", attr: "text", val: "35.0"},
+ {id: "bVarPrev_level", attr: "text", val: "40.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "6"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 6/42, State ID: 5, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "30.0"},
+ {id: "svg_id__1", attr: "y", val: "90.0"},
+ {id: "bVar_level", attr: "text", val: "30.0"},
+ {id: "bVarPrev_level", attr: "text", val: "35.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "7"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 7/42, State ID: 6, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "25.0"},
+ {id: "svg_id__1", attr: "y", val: "95.0"},
+ {id: "bVar_level", attr: "text", val: "25.0"},
+ {id: "bVarPrev_level", attr: "text", val: "30.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "8"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 8/42, State ID: 7, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "20.0"},
+ {id: "svg_id__1", attr: "y", val: "100.0"},
+ {id: "bVar_level", attr: "text", val: "20.0"},
+ {id: "bVarPrev_level", attr: "text", val: "25.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "9"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 9/42, State ID: 8, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "15.0"},
+ {id: "svg_id__1", attr: "y", val: "105.0"},
+ {id: "bVar_level", attr: "text", val: "15.0"},
+ {id: "bVarPrev_level", attr: "text", val: "20.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "10"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 10/42, State ID: 9, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "10.0"},
+ {id: "svg_id__1", attr: "y", val: "110.0"},
+ {id: "svg_id__5", attr: "fill", val: "mediumseagreen"},
+ {id: "svg_id__7", attr: "text", val: "on"},
+ {id: "bVar_level", attr: "text", val: "10.0"},
+ {id: "bVarPrev_level", attr: "text", val: "15.0"},
+ {id: "bVar_pump", attr: "text", val: "TRUE"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "#fffacd"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "11"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 11/42, State ID: 10, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "12.5"},
+ {id: "svg_id__1", attr: "y", val: "107.5"},
+ {id: "bVar_level", attr: "text", val: "12.5"},
+ {id: "bVarPrev_level", attr: "text", val: "10.0"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "white"},
+ {id: "bVarPrev_pump", attr: "text", val: "TRUE"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "12"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 12/42, State ID: 11, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "15.0"},
+ {id: "svg_id__1", attr: "y", val: "105.0"},
+ {id: "bVar_level", attr: "text", val: "15.0"},
+ {id: "bVarPrev_level", attr: "text", val: "12.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "13"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 13/42, State ID: 12, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "17.5"},
+ {id: "svg_id__1", attr: "y", val: "102.5"},
+ {id: "bVar_level", attr: "text", val: "17.5"},
+ {id: "bVarPrev_level", attr: "text", val: "15.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "14"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 14/42, State ID: 13, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "20.0"},
+ {id: "svg_id__1", attr: "y", val: "100.0"},
+ {id: "bVar_level", attr: "text", val: "20.0"},
+ {id: "bVarPrev_level", attr: "text", val: "17.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "15"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 15/42, State ID: 14, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "22.5"},
+ {id: "svg_id__1", attr: "y", val: "97.5"},
+ {id: "bVar_level", attr: "text", val: "22.5"},
+ {id: "bVarPrev_level", attr: "text", val: "20.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "16"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 16/42, State ID: 15, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "25.0"},
+ {id: "svg_id__1", attr: "y", val: "95.0"},
+ {id: "bVar_level", attr: "text", val: "25.0"},
+ {id: "bVarPrev_level", attr: "text", val: "22.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "17"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 17/42, State ID: 16, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "27.5"},
+ {id: "svg_id__1", attr: "y", val: "92.5"},
+ {id: "bVar_level", attr: "text", val: "27.5"},
+ {id: "bVarPrev_level", attr: "text", val: "25.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "18"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 18/42, State ID: 17, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "30.0"},
+ {id: "svg_id__1", attr: "y", val: "90.0"},
+ {id: "bVar_level", attr: "text", val: "30.0"},
+ {id: "bVarPrev_level", attr: "text", val: "27.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "19"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 19/42, State ID: 18, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "32.5"},
+ {id: "svg_id__1", attr: "y", val: "87.5"},
+ {id: "bVar_level", attr: "text", val: "32.5"},
+ {id: "bVarPrev_level", attr: "text", val: "30.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "20"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 20/42, State ID: 19, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "35.0"},
+ {id: "svg_id__1", attr: "y", val: "85.0"},
+ {id: "bVar_level", attr: "text", val: "35.0"},
+ {id: "bVarPrev_level", attr: "text", val: "32.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "21"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 21/42, State ID: 20, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "37.5"},
+ {id: "svg_id__1", attr: "y", val: "82.5"},
+ {id: "bVar_level", attr: "text", val: "37.5"},
+ {id: "bVarPrev_level", attr: "text", val: "35.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "22"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 22/42, State ID: 21, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "40.0"},
+ {id: "svg_id__1", attr: "y", val: "80.0"},
+ {id: "bVar_level", attr: "text", val: "40.0"},
+ {id: "bVarPrev_level", attr: "text", val: "37.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "23"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 23/42, State ID: 22, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "42.5"},
+ {id: "svg_id__1", attr: "y", val: "77.5"},
+ {id: "bVar_level", attr: "text", val: "42.5"},
+ {id: "bVarPrev_level", attr: "text", val: "40.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "24"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 24/42, State ID: 23, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "45.0"},
+ {id: "svg_id__1", attr: "y", val: "75.0"},
+ {id: "bVar_level", attr: "text", val: "45.0"},
+ {id: "bVarPrev_level", attr: "text", val: "42.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "25"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 25/42, State ID: 24, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "47.5"},
+ {id: "svg_id__1", attr: "y", val: "72.5"},
+ {id: "bVar_level", attr: "text", val: "47.5"},
+ {id: "bVarPrev_level", attr: "text", val: "45.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "26"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 26/42, State ID: 25, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "50.0"},
+ {id: "svg_id__1", attr: "y", val: "70.0"},
+ {id: "bVar_level", attr: "text", val: "50.0"},
+ {id: "bVarPrev_level", attr: "text", val: "47.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "27"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 27/42, State ID: 26, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "52.5"},
+ {id: "svg_id__1", attr: "y", val: "67.5"},
+ {id: "bVar_level", attr: "text", val: "52.5"},
+ {id: "bVarPrev_level", attr: "text", val: "50.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "28"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 28/42, State ID: 27, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "55.0"},
+ {id: "svg_id__1", attr: "y", val: "65.0"},
+ {id: "bVar_level", attr: "text", val: "55.0"},
+ {id: "bVarPrev_level", attr: "text", val: "52.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "29"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 29/42, State ID: 28, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "57.5"},
+ {id: "svg_id__1", attr: "y", val: "62.5"},
+ {id: "bVar_level", attr: "text", val: "57.5"},
+ {id: "bVarPrev_level", attr: "text", val: "55.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "30"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 30/42, State ID: 29, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "60.0"},
+ {id: "svg_id__1", attr: "y", val: "60.0"},
+ {id: "bVar_level", attr: "text", val: "60.0"},
+ {id: "bVarPrev_level", attr: "text", val: "57.5"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "31"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 31/42, State ID: 30, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "62.5"},
+ {id: "svg_id__1", attr: "y", val: "57.5"},
+ {id: "bVar_level", attr: "text", val: "62.5"},
+ {id: "bVarPrev_level", attr: "text", val: "60.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "32"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 32/42, State ID: 31, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "65.0"},
+ {id: "svg_id__1", attr: "y", val: "55.0"},
+ {id: "svg_id__5", attr: "fill", val: "palegoldenrod"},
+ {id: "svg_id__7", attr: "text", val: "off"},
+ {id: "bVar_level", attr: "text", val: "65.0"},
+ {id: "bVarPrev_level", attr: "text", val: "62.5"},
+ {id: "bVar_pump", attr: "text", val: "FALSE"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "#fffacd"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "33"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 33/42, State ID: 32, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "60.0"},
+ {id: "svg_id__1", attr: "y", val: "60.0"},
+ {id: "bVar_level", attr: "text", val: "60.0"},
+ {id: "bVarPrev_level", attr: "text", val: "65.0"},
+ {id: "row_bVar_pump", attr: "bgcolor", val: "white"},
+ {id: "bVarPrev_pump", attr: "text", val: "FALSE"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "34"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 34/42, State ID: 33, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "55.0"},
+ {id: "svg_id__1", attr: "y", val: "65.0"},
+ {id: "bVar_level", attr: "text", val: "55.0"},
+ {id: "bVarPrev_level", attr: "text", val: "60.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "35"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 35/42, State ID: 1, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "50.0"},
+ {id: "svg_id__1", attr: "y", val: "70.0"},
+ {id: "bVar_level", attr: "text", val: "50.0"},
+ {id: "bVarPrev_level", attr: "text", val: "55.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "36"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 36/42, State ID: 2, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "45.0"},
+ {id: "svg_id__1", attr: "y", val: "75.0"},
+ {id: "bVar_level", attr: "text", val: "45.0"},
+ {id: "bVarPrev_level", attr: "text", val: "50.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "37"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 37/42, State ID: 3, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "40.0"},
+ {id: "svg_id__1", attr: "y", val: "80.0"},
+ {id: "bVar_level", attr: "text", val: "40.0"},
+ {id: "bVarPrev_level", attr: "text", val: "45.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "38"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 38/42, State ID: 4, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "35.0"},
+ {id: "svg_id__1", attr: "y", val: "85.0"},
+ {id: "bVar_level", attr: "text", val: "35.0"},
+ {id: "bVarPrev_level", attr: "text", val: "40.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "39"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 39/42, State ID: 5, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "30.0"},
+ {id: "svg_id__1", attr: "y", val: "90.0"},
+ {id: "bVar_level", attr: "text", val: "30.0"},
+ {id: "bVarPrev_level", attr: "text", val: "35.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "40"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 40/42, State ID: 6, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "25.0"},
+ {id: "svg_id__1", attr: "y", val: "95.0"},
+ {id: "bVar_level", attr: "text", val: "25.0"},
+ {id: "bVarPrev_level", attr: "text", val: "30.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "41"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 41/42, State ID: 7, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "20.0"},
+ {id: "svg_id__1", attr: "y", val: "100.0"},
+ {id: "bVar_level", attr: "text", val: "20.0"},
+ {id: "bVarPrev_level", attr: "text", val: "25.0"},
+ ],
+ [
+ {id: "trace_meter", attr: "value", val: "42"},
+ {id: "visb_debug_messages", attr: "text", val: "Step 42/42, State ID: 8, Event: Next "},
+ {id: "svg_id__1", attr: "height", val: "15.0"},
+ {id: "svg_id__1", attr: "y", val: "105.0"},
+ {id: "bVar_level", attr: "text", val: "15.0"},
+ {id: "bVarPrev_level", attr: "text", val: "20.0"},
+ ]
+ ]
+
+ const transitions = new Map();
+ for (let j = 0; j < differences.length; j++) {
+ const transitionAttributeValues = new Map();
+ for (let i = 0; i <= j; i++) {
+ const transitionI = differences[i];
+ for (const attrValue of transitionI) {
+ const key = {id: attrValue.id, attr: attrValue.attr};
+ transitionAttributeValues.set(key, attrValue.val);
+ }
+ }
+ transitions.set(j+1, transitionAttributeValues);
+ }
+
+ function replayStep(stepNr) {
+ transitions.get(stepNr).forEach((value, key) => {
+ setAttr(key.id, key.attr, value);
+ });
+ highlightRow(stepNr);
+ }
+
+ async function runAll(delay) {
+ for (let i = 1; i <= transitions.size; i++) {
+ replayStep(i);
+ await sleep(delay);
+ }
+ }
+
+ </script>
+
+ <script> function registerHovers() {} </script>
+ </head>
+<body>
+
+
+ <button type="button" class="collapsible collapsible-style active">SVG Visualisation</button>
+ <div text-align="left" id="visb_svg_outer_container" class="svg-outer-container">
+ <div id="visb_svg_inner_container" class="svg-inner-container">
+<svg xmlns="http://www.w3.org/2000/svg"
+ width="70.0" height="130.0" viewBox="0 0 70.0 130.0" >
+ <rect id="svg_id__1" fill="lightsteelblue" width="30.0" x="10.0"></rect>
+ <rect id="svg_id__2" fill="none" height="75.0" stroke="black" stroke-width="1.0" width="30.0" x="10.0" y="45.0"></rect>
+ <line id="svg_id__3" stroke="red" stroke-width="1.0" x1="9.5" x2="40.5" y1="100.0" y2="100.0"></line>
+ <line id="svg_id__4" stroke="red" stroke-width="1.0" x1="9.5" x2="40.5" y1="60.0" y2="60.0"></line>
+ <rect id="svg_id__5" height="10.0" rx="5" stroke="black" stroke-width="1.0" width="30.0" x="10.0" y="20.0"></rect>
+ <text id="svg_id__6" font-size="8.0" x="15.0" y="12.0">Pump:</text>
+ <text id="svg_id__7" font-size="8.0" x="19.5" y="27.2"></text>
+</svg>
+ </div>
+ </div>
+ <button type="button" class="collapsible-style">Replay Trace</button>
+ <div class="coll-content-vis">
+ <button onclick="backStep()">« Back</button>
+ <button onclick="forwardStep()">Forward »</button>
+ <button onclick="runAll(10)">Run Trace (10 ms delay)</button>
+ <button onclick="runAll(500)">Run Trace (500 ms delay)</button>
+ <br><label id="visb_debug_messages" class="visb-messages"> </label>
+ </div>
+ <progress id="trace_meter" min="0" max="42" value="0"></progress>
+ <button type="button" class="collapsible collapsible-style">Variables (2)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> <th>Previous Value</th> </tr>
+
+ <tr id="row_bVar_level" title="Type: REAL"> <td>1</td> <td id="name_bVar_level">level</td> <td id="bVar_level">?</td> <td id="bVarPrev_level">?</td> </tr>
+
+ <tr id="row_bVar_pump" title="Type: BOOL"> <td>2</td> <td id="name_bVar_pump">pump</td> <td id="bVar_pump">?</td> <td id="bVarPrev_pump">?</td> </tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Constants (5)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="row_bConstant_low_threshold" title="Type: REAL"> <td>1</td> <td id="name_bConstant_low_threshold">low_threshold</td> <td id="bConstant_low_threshold">20.0</td> </tr>
+
+ <tr id="row_bConstant_high_threshold" title="Type: REAL"> <td>2</td> <td id="name_bConstant_high_threshold">high_threshold</td> <td id="bConstant_high_threshold">60.0</td> </tr>
+
+ <tr id="row_bConstant_step_size" title="Type: REAL"> <td>3</td> <td id="name_bConstant_step_size">step_size</td> <td id="bConstant_step_size">0.5</td> </tr>
+
+ <tr id="row_bConstant_outflow" title="Type: REAL"> <td>4</td> <td id="name_bConstant_outflow">outflow</td> <td id="bConstant_outflow">10.0</td> </tr>
+
+ <tr id="row_bConstant_inflow" title="Type: REAL"> <td>5</td> <td id="name_bConstant_inflow">inflow</td> <td id="bConstant_inflow">15.0</td> </tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Actions (1)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Enabled</th> </tr>
+
+ <tr id="row_bOperation_Next" title="Operation: Next()"> <td>1</td> <td id="name_bOperation_Next">Next</td> <td id="bOperation_Next">?</td> </tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible collapsible-style active">Trace (length=42)</button>
+<div class="coll-content-vis">
+ <table> <tr> <th>Nr</th> <th>Event</th> <th>Target State ID</th> </tr>
+
+ <tr id="row1"><td>1</td><td style="cursor:not-allowed">SETUP_CONSTANTS(low_threshold=20.0,high_threshold=60.0,step_size=0.5,outflow=10.0,inflow=15.0)</td><td>State 0</td></tr>
+
+ <tr id="row2" onclick="replayStep(2)"><td>2</td><td style="cursor:pointer">INITIALISATION(level=50.0,pump=FALSE)</td><td><button onclick="replayStep(2);">State 1</button></td></tr>
+
+ <tr id="row3" onclick="replayStep(3)"><td>3</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(3);">State 2</button></td></tr>
+
+ <tr id="row4" onclick="replayStep(4)"><td>4</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(4);">State 3</button></td></tr>
+
+ <tr id="row5" onclick="replayStep(5)"><td>5</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(5);">State 4</button></td></tr>
+
+ <tr id="row6" onclick="replayStep(6)"><td>6</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(6);">State 5</button></td></tr>
+
+ <tr id="row7" onclick="replayStep(7)"><td>7</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(7);">State 6</button></td></tr>
+
+ <tr id="row8" onclick="replayStep(8)"><td>8</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(8);">State 7</button></td></tr>
+
+ <tr id="row9" onclick="replayStep(9)"><td>9</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(9);">State 8</button></td></tr>
+
+ <tr id="row10" onclick="replayStep(10)"><td>10</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(10);">State 9</button></td></tr>
+
+ <tr id="row11" onclick="replayStep(11)"><td>11</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(11);">State 10</button></td></tr>
+
+ <tr id="row12" onclick="replayStep(12)"><td>12</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(12);">State 11</button></td></tr>
+
+ <tr id="row13" onclick="replayStep(13)"><td>13</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(13);">State 12</button></td></tr>
+
+ <tr id="row14" onclick="replayStep(14)"><td>14</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(14);">State 13</button></td></tr>
+
+ <tr id="row15" onclick="replayStep(15)"><td>15</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(15);">State 14</button></td></tr>
+
+ <tr id="row16" onclick="replayStep(16)"><td>16</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(16);">State 15</button></td></tr>
+
+ <tr id="row17" onclick="replayStep(17)"><td>17</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(17);">State 16</button></td></tr>
+
+ <tr id="row18" onclick="replayStep(18)"><td>18</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(18);">State 17</button></td></tr>
+
+ <tr id="row19" onclick="replayStep(19)"><td>19</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(19);">State 18</button></td></tr>
+
+ <tr id="row20" onclick="replayStep(20)"><td>20</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(20);">State 19</button></td></tr>
+
+ <tr id="row21" onclick="replayStep(21)"><td>21</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(21);">State 20</button></td></tr>
+
+ <tr id="row22" onclick="replayStep(22)"><td>22</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(22);">State 21</button></td></tr>
+
+ <tr id="row23" onclick="replayStep(23)"><td>23</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(23);">State 22</button></td></tr>
+
+ <tr id="row24" onclick="replayStep(24)"><td>24</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(24);">State 23</button></td></tr>
+
+ <tr id="row25" onclick="replayStep(25)"><td>25</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(25);">State 24</button></td></tr>
+
+ <tr id="row26" onclick="replayStep(26)"><td>26</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(26);">State 25</button></td></tr>
+
+ <tr id="row27" onclick="replayStep(27)"><td>27</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(27);">State 26</button></td></tr>
+
+ <tr id="row28" onclick="replayStep(28)"><td>28</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(28);">State 27</button></td></tr>
+
+ <tr id="row29" onclick="replayStep(29)"><td>29</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(29);">State 28</button></td></tr>
+
+ <tr id="row30" onclick="replayStep(30)"><td>30</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(30);">State 29</button></td></tr>
+
+ <tr id="row31" onclick="replayStep(31)"><td>31</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(31);">State 30</button></td></tr>
+
+ <tr id="row32" onclick="replayStep(32)"><td>32</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(32);">State 31</button></td></tr>
+
+ <tr id="row33" onclick="replayStep(33)"><td>33</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(33);">State 32</button></td></tr>
+
+ <tr id="row34" onclick="replayStep(34)"><td>34</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(34);">State 33</button></td></tr>
+
+ <tr id="row35" onclick="replayStep(35)"><td>35</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(35);">State 1</button></td></tr>
+
+ <tr id="row36" onclick="replayStep(36)"><td>36</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(36);">State 2</button></td></tr>
+
+ <tr id="row37" onclick="replayStep(37)"><td>37</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(37);">State 3</button></td></tr>
+
+ <tr id="row38" onclick="replayStep(38)"><td>38</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(38);">State 4</button></td></tr>
+
+ <tr id="row39" onclick="replayStep(39)"><td>39</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(39);">State 5</button></td></tr>
+
+ <tr id="row40" onclick="replayStep(40)"><td>40</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(40);">State 6</button></td></tr>
+
+ <tr id="row41" onclick="replayStep(41)"><td>41</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(41);">State 7</button></td></tr>
+
+ <tr id="row42" onclick="replayStep(42)"><td>42</td><td style="cursor:pointer">Next</td><td><button onclick="replayStep(42);">State 8</button></td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis visb-messages">
+Generated on 6/9/2024 at 17:03 using <a href="https://prob.hhu.de/">ProB</a> version 1.13.1-nightly
+<br>Main specification file: WaterTankReals.tla (modified on 6/9/2024 at 16:59)
+<br>Main specification name: WaterTankReals
+ <script> replayStep(42); </script>
+ </div>
+ <script>
+ registerHovers();
+
+ const collapsibles = document.getElementsByClassName("collapsible");
+ for (let ii = 0; ii < collapsibles.length; ii++) {
+ collapsibles[ii].onclick = function() {
+ this.classList.toggle("active");
+ this.nextElementSibling.style.display = this.classList.contains("active") ? "block" : "none";
+ };
+ }
+
+ const outerContainer = document.getElementById('visb_svg_outer_container');
+ const innerContainer = document.getElementById('visb_svg_inner_container');
+ let scale = 1;
+ let isDragging = false;
+ let startMouseX, startMouseY;
+
+ outerContainer.onwheel = (e) => {
+ e.preventDefault();
+ const oldScale = scale;
+ scale *= (e.deltaY < 0) ? 1.06 : 1 / 1.06;
+ scale = Math.max(scale, 0.5);
+
+ const rect = outerContainer.getBoundingClientRect();
+ const mouseX = e.clientX - rect.left + outerContainer.scrollLeft;
+ const mouseY = e.clientY - rect.top + outerContainer.scrollTop;
+ const scaleChange = scale / oldScale;
+
+ innerContainer.style.transform = `scale(${scale})`;
+ outerContainer.scrollBy({
+ left: mouseX * (scaleChange - 1),
+ top: mouseY * (scaleChange - 1),
+ behavior: 'instant'
+ });
+ };
+
+ outerContainer.onmousedown = (e) => {
+ isDragging = true;
+ startMouseX = e.clientX;
+ startMouseY = e.clientY;
+ };
+
+ document.onmousemove = (e) => {
+ if (!isDragging) return;
+ const dx = startMouseX - e.clientX;
+ const dy = startMouseY - e.clientY;
+ outerContainer.scrollBy(dx,dy);
+ startMouseX = e.clientX;
+ startMouseY = e.clientY;
+ };
+
+ document.onmouseup = () => isDragging = false;
+ outerContainer.onmouseleave = () => isDragging = false;
+
+ const outerContainerHeight = parseFloat(window.getComputedStyle(outerContainer).height);
+ if (outerContainerHeight > window.innerHeight * 0.7) {
+ outerContainer.style.height = '70vh';
+ }
+ outerContainer.style.visibility = 'visible';
+ </script>
+
+ </body>
+</html>
+