diff --git a/Einstein/Makefile b/Einstein/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..32f38e3358e771dd774abb574834f78649770af6
--- /dev/null
+++ b/Einstein/Makefile
@@ -0,0 +1,20 @@
+PROBCLI=probcli
+
+VISBFILE=einstein_puzzle_als.json
+SPEC=einsteins_puzzle.als
+
+VISBFILE2=Einstein_tla.json
+SPEC2=Einstein.tla
+
+all: html/$(SPEC).html html/$(SPEC2).html
+ @echo "Generated VisB HTML files in html/"
+
+html/$(SPEC).html: $(SPEC) $(VISBFILE) Makefile
+ @echo "Running alloy command run for $(SPEC), generating html/$(SPEC).html"
+ $(PROBCLI) $(SPEC) -cbc-sequence run0 -visb_with_vars $(VISBFILE) html/$(SPEC).html
+
+
+
+html/$(SPEC2).html: $(SPEC2) $(VISBFILE2) Makefile
+ @echo "Performing symbolic invariant check on $(SPEC2), generating html/$(SPEC).html"
+ $(PROBCLI) $(SPEC2) -cbc all -visb_with_vars $(VISBFILE2) html/$(SPEC2).html -expecterr cbc
\ No newline at end of file
diff --git a/Einstein/html/Einstein.tla.html b/Einstein/html/Einstein.tla.html
new file mode 100644
index 0000000000000000000000000000000000000000..8892e712091b6e374f1456eb5d3832194464cf25
--- /dev/null
+++ b/Einstein/html/Einstein.tla.html
@@ -0,0 +1,309 @@
+<!DOCTYPE html>
+<html>
+<head>
+ <!-- html file generated by ProB from a VisB visualization -->
+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
+ <script>
+ function setAttr(id, attribute, value){
+ var 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 {
+ obj.setAttribute(attribute, value);
+ }
+ }
+ function sleep(ms) {
+ return new Promise(resolve => setTimeout(resolve, ms));
+ }
+ var lastSelectedRow = 0;
+ function highlightRow(id) {
+ if (lastSelectedRow>0) {setAttr("row"+lastSelectedRow,"bgcolor","")};
+ setAttr("row"+id,"bgcolor","yellow");
+ lastSelectedRow = id;
+ }
+ function backStep() {
+ if (lastSelectedRow>1) {
+ var prev = lastSelectedRow-1;
+ document.getElementById("row"+prev).click();
+ }
+ }
+ function forwardStep() {
+ if (lastSelectedRow>0) {
+ var nxt = lastSelectedRow+1;
+ var 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;
+ }
+ </style>
+
+
+
+ <script>
+ function visualise0(stepNr) {
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/2, State ID: 0");
+ highlightRow(stepNr);
+ }
+ function visualise1(stepNr) {
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/2, State ID: 1");
+ setAttr("house1","fill","yellow");
+ setAttr("house2","fill","blue");
+ setAttr("house3","fill","red");
+ setAttr("house4","fill","green");
+ setAttr("house5","fill","white");
+ setAttr("pet1","text","cat");
+ setAttr("pet2","text","horse");
+ setAttr("pet3","text","bird");
+ setAttr("pet4","text","fish");
+ setAttr("pet5","text","dog");
+ setAttr("cigar1","text","dh");
+ setAttr("cigar2","text","blend");
+ setAttr("cigar3","text","pm");
+ setAttr("cigar4","text","prince");
+ setAttr("cigar5","text","bm");
+ setAttr("drink1","text","water");
+ setAttr("drink2","text","tea");
+ setAttr("drink3","text","mylk");
+ setAttr("drink4","text","coffee");
+ setAttr("drink5","text","beer");
+ setAttr("nationality1","text","norwegian");
+ setAttr("nationality2","text","dane");
+ setAttr("nationality3","text","brit");
+ setAttr("nationality4","text","german");
+ setAttr("nationality5","text","swede");
+ setAttr("bVar_nationality","text","{(1|->\"norwegian\"),(2|->\"dane\"),(3|->\"brit\"),(4|->\"german\"),(5|->\"swede\")}");
+ setAttr("bVar_colors","text","{(1|->\"yellow\"),(2|->\"blue\"),(3|->\"red\"),(4|->\"green\"),(5|->\"white\")}");
+ setAttr("bVar_pets","text","{(1|->\"cat\"),(2|->\"horse\"),(3|->\"bird\"),(4|->\"fish\"),(5|->\"dog\")}");
+ setAttr("bVar_cigars","text","{(1|->\"dh\"),(2|->\"blend\"),(3|->\"pm\"),(4|->\"prince\"),(5|->\"bm\")}");
+ setAttr("bVar_drinks","text","{(1|->\"water\"),(2|->\"tea\"),(3|->\"mylk\"),(4|->\"coffee\"),(5|->\"beer\")}");
+ highlightRow(stepNr);
+ }
+ async function runAll(delay) {
+ visualise0(1);
+ setAttr("visb_debug_messages","text","Step: 1/2, State ID: 0, Event: constraint_based_check");
+ await sleep(delay);
+ visualise1(2);
+ setAttr("visb_debug_messages","text","Step: 2/2, State ID: 1, Event: INITIALISATION(nationality=\{(1\|-\>\"norwegian\"),(2\|-\>\"dane\"),(3\|-\>\"brit\"),(4\|-\>\"german\"),(5\|-\>\"swede\")\},colors=\{(1\|-\>\"yell...");
+ await sleep(delay);
+ }
+ </script>
+
+ <script> function registerHovers() {} </script>
+ </head>
+<body>
+ <button type="button" class="collapsible collapsible-style">SVG Visualisation</button>
+ <div text-align="left">
+
+
+<svg xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+xmlns:svg="http://www.w3.org/2000/svg"
+xmlns="http://www.w3.org/2000/svg"
+width="1024" height="512"
+version="1.1" id="svg2">
+<!-- Source of the House Logo: https://commons.wikimedia.org/wiki/File:Home_Icon.svg -->
+ <g transform="translate(0,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="red"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house1"
+ />
+ </g>
+ <g transform="translate(125,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="green"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house2"
+ />
+ </g>
+ <g transform="translate(250,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="blue"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house3"
+ />
+ </g>
+ <g transform="translate(375,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="white"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house4"
+ />
+ </g>
+ <g transform="translate(500,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="orange"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house5"
+ />
+ </g>
+
+
+ <text x="0" y="20" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="nationality1">nationality</tspan>
+ <tspan x="175" dy = "0.0em" id="nationality2">nationality</tspan>
+ <tspan x="300" dy = "0.0em" id="nationality3">nationality</tspan>
+ <tspan x="425" dy = "0.0em" id="nationality4">nationality</tspan>
+ <tspan x="550" dy = "0.0em" id="nationality5">nationality</tspan>
+ </text>
+ <text x="0" y="200" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="pet1">Pet</tspan>
+ <tspan x="175" dy = "0.0em" id="pet2">Pet</tspan>
+ <tspan x="300" dy = "0.0em" id="pet3">Pet</tspan>
+ <tspan x="425" dy = "0.0em" id="pet4">Pet</tspan>
+ <tspan x="550" dy = "0.0em" id="pet5">Pet</tspan>
+ </text>
+ <text x="0" y="220" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="cigarette1">cigarette</tspan>
+ <tspan x="175" dy = "0.0em" id="cigarette2">cigarette</tspan>
+ <tspan x="300" dy = "0.0em" id="cigarette3">cigarette</tspan>
+ <tspan x="425" dy = "0.0em" id="cigarette4">cigarette</tspan>
+ <tspan x="550" dy = "0.0em" id="cigarette5">cigarette</tspan>
+ </text>
+ <text x="0" y="180" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="drink1">drink</tspan>
+ <tspan x="175" dy = "0.0em" id="drink2">drink</tspan>
+ <tspan x="300" dy = "0.0em" id="drink3">drink</tspan>
+ <tspan x="425" dy = "0.0em" id="drink4">drink</tspan>
+ <tspan x="550" dy = "0.0em" id="drink5">drink</tspan>
+ </text>
+
+</svg>
+ </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>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Variables (5/5)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="var_rownationality"> <td>1</td> <td>nationality</td> <td id="bVar_nationality">?</td></tr>
+
+ <tr id="var_rowcolors"> <td>2</td> <td>colors</td> <td id="bVar_colors">?</td></tr>
+
+ <tr id="var_rowpets"> <td>3</td> <td>pets</td> <td id="bVar_pets">?</td></tr>
+
+ <tr id="var_rowcigars"> <td>4</td> <td>cigars</td> <td id="bVar_cigars">?</td></tr>
+
+ <tr id="var_rowdrinks"> <td>5</td> <td>drinks</td> <td id="bVar_drinks">?</td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Trace (length=2)</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">constraint_based_check</td><td>State 0</td></tr>
+
+ <tr id="row2" onclick="visualise1(2)"><td>2</td><td style="cursor:pointer">INITIALISATION(nationality={(1|->"norwegian"),(2|->"dane"),(3|->"brit"),(4|->"german"),(5|->"swede")},colors={(1|->"yell...</td><td><button onclick="visualise1(2);">State 1</button></td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis">
+Generated on 22/3/2021 at 8:19 using ProB version 1.11.0-nightly
+<br>Main specification file: Einstein.prob
+ </table>
+ </div>
+ <script> visualise1(2); </script>
+ </div>
+ <script> registerHovers() </script>
+
+<script>
+var collapsibles = document.getElementsByClassName("collapsible");
+var ii;
+
+for (ii = 0; ii < collapsibles.length; ii++) {
+ collapsibles[ii].addEventListener("click", function() {
+ this.classList.toggle("active");
+ var content = this.nextElementSibling;
+ if (content.style.display === "block") {
+ content.style.display = "none";
+ } else {
+ content.style.display = "block";
+ }
+ });
+}
+</script>
+
+</body>
+</html>
+
diff --git a/Einstein/html/einsteins_puzzle.als.html b/Einstein/html/einsteins_puzzle.als.html
new file mode 100644
index 0000000000000000000000000000000000000000..9107149041c87fe0cf3bfc58fa63a30cd659faa4
--- /dev/null
+++ b/Einstein/html/einsteins_puzzle.als.html
@@ -0,0 +1,326 @@
+<!DOCTYPE html>
+<html>
+<head>
+ <!-- html file generated by ProB from a VisB visualization -->
+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
+ <script>
+ function setAttr(id, attribute, value){
+ var 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 {
+ obj.setAttribute(attribute, value);
+ }
+ }
+ function sleep(ms) {
+ return new Promise(resolve => setTimeout(resolve, ms));
+ }
+ var lastSelectedRow = 0;
+ function highlightRow(id) {
+ if (lastSelectedRow>0) {setAttr("row"+lastSelectedRow,"bgcolor","")};
+ setAttr("row"+id,"bgcolor","yellow");
+ lastSelectedRow = id;
+ }
+ function backStep() {
+ if (lastSelectedRow>1) {
+ var prev = lastSelectedRow-1;
+ document.getElementById("row"+prev).click();
+ }
+ }
+ function forwardStep() {
+ if (lastSelectedRow>0) {
+ var nxt = lastSelectedRow+1;
+ var 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;
+ }
+ </style>
+
+
+
+ <script>
+ function visualise0(stepNr) {
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/3, State ID: 0");
+ highlightRow(stepNr);
+ }
+ function visualise1(stepNr) {
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/3, State ID: 1");
+ setAttr("house1","fill","yellow");
+ setAttr("house2","fill","blue");
+ setAttr("house3","fill","red");
+ setAttr("house4","fill","green");
+ setAttr("house5","fill","white");
+ setAttr("pet1","text","cat");
+ setAttr("nationality1","text","Norwegian");
+ setAttr("cigarette1","text","Dunhills");
+ setAttr("drink1","text","water");
+ setAttr("pet2","text","horse");
+ setAttr("nationality2","text","Dane");
+ setAttr("cigarette2","text","Blend");
+ setAttr("drink2","text","tea");
+ setAttr("pet3","text","bird");
+ setAttr("nationality3","text","Englishman");
+ setAttr("cigarette3","text","Pall_Mall");
+ setAttr("drink3","text","milk");
+ setAttr("pet4","text","dog");
+ setAttr("nationality4","text","German");
+ setAttr("cigarette4","text","Prince");
+ setAttr("drink4","text","coffee");
+ setAttr("pet5","text","dog");
+ setAttr("nationality5","text","Swede");
+ setAttr("cigarette5","text","Blue_Masters");
+ setAttr("drink5","text","beer");
+ highlightRow(stepNr);
+ }
+ async function runAll(delay) {
+ visualise0(1);
+ setAttr("visb_debug_messages","text","Step: 1/3, State ID: 0, Event: SETUP_CONSTANTS(House=\{0,1,2,3,4\},color_House=\{(0\|-\>yellow),(1\|-\>blue),(2\|-\>red),(3\|-\>green),(4\|-\>white)\},nationality_Ho...");
+ await sleep(delay);
+ visualise1(2);
+ setAttr("visb_debug_messages","text","Step: 2/3, State ID: 1, Event: INITIALISATION()");
+ await sleep(delay);
+ visualise1(3);
+ setAttr("visb_debug_messages","text","Step: 3/3, State ID: 1, Event: run0");
+ await sleep(delay);
+ }
+ </script>
+
+ <script> function registerHovers() {} </script>
+ </head>
+<body>
+ <button type="button" class="collapsible collapsible-style">SVG Visualisation</button>
+ <div text-align="left">
+
+
+<svg xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+xmlns:svg="http://www.w3.org/2000/svg"
+xmlns="http://www.w3.org/2000/svg"
+width="1024" height="512"
+version="1.1" id="svg2">
+<!-- Source of the House Logo: https://commons.wikimedia.org/wiki/File:Home_Icon.svg -->
+ <g transform="translate(0,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="red"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house1"
+ />
+ </g>
+ <g transform="translate(125,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="green"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house2"
+ />
+ </g>
+ <g transform="translate(250,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="blue"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house3"
+ />
+ </g>
+ <g transform="translate(375,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="white"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house4"
+ />
+ </g>
+ <g transform="translate(500,44) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="orange"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-44)"
+ id = "house5"
+ />
+ </g>
+
+
+ <text x="0" y="20" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="nationality1">nationality</tspan>
+ <tspan x="175" dy = "0.0em" id="nationality2">nationality</tspan>
+ <tspan x="300" dy = "0.0em" id="nationality3">nationality</tspan>
+ <tspan x="425" dy = "0.0em" id="nationality4">nationality</tspan>
+ <tspan x="550" dy = "0.0em" id="nationality5">nationality</tspan>
+ </text>
+ <text x="0" y="200" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="pet1">Pet</tspan>
+ <tspan x="175" dy = "0.0em" id="pet2">Pet</tspan>
+ <tspan x="300" dy = "0.0em" id="pet3">Pet</tspan>
+ <tspan x="425" dy = "0.0em" id="pet4">Pet</tspan>
+ <tspan x="550" dy = "0.0em" id="pet5">Pet</tspan>
+ </text>
+ <text x="0" y="220" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="cigarette1">cigarette</tspan>
+ <tspan x="175" dy = "0.0em" id="cigarette2">cigarette</tspan>
+ <tspan x="300" dy = "0.0em" id="cigarette3">cigarette</tspan>
+ <tspan x="425" dy = "0.0em" id="cigarette4">cigarette</tspan>
+ <tspan x="550" dy = "0.0em" id="cigarette5">cigarette</tspan>
+ </text>
+ <text x="0" y="180" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="drink1">drink</tspan>
+ <tspan x="175" dy = "0.0em" id="drink2">drink</tspan>
+ <tspan x="300" dy = "0.0em" id="drink3">drink</tspan>
+ <tspan x="425" dy = "0.0em" id="drink4">drink</tspan>
+ <tspan x="550" dy = "0.0em" id="drink5">drink</tspan>
+ </text>
+
+</svg>
+ </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>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Constants (6/6)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="var_rowHouse"> <td>1</td> <td>House</td> <td id="bVar_House">{0,1,2,3,4}</td></tr>
+
+ <tr id="var_rowcolor_House"> <td>2</td> <td>color_House</td> <td id="bVar_color_House">{(0|->yellow),(1|->blue),(2|->red),(3|->green),(4|->white)}</td></tr>
+
+ <tr id="var_rownationality_House"> <td>3</td> <td>nationality_House</td> <td id="bVar_nationality_House">{(0|->Norwegian),(1|->Dane),(2|->Englishman),(3|->German),(4|->Swede)}</td></tr>
+
+ <tr id="var_rowdrink_House"> <td>4</td> <td>drink_House</td> <td id="bVar_drink_House">{(0|->water),(1|->tea),(2|->milk),(3|->coffee),(4|->beer)}</td></tr>
+
+ <tr id="var_rowcigarette_House"> <td>5</td> <td>cigarette_House</td> <td id="bVar_cigarette_House">{(0|->Dunhills),(1|->Blend),(2|->Pall_Mall),(3|->Prince),(4|->Blue_Masters)}</td></tr>
+
+ <tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|->cat),(1|->horse),(2|->bird),(3|->dog),(4|->dog)}</td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Sets (5/5)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="var_rowColor"> <td>1</td> <td>Color</td> <td id="bVar_Color">{red,blue,green,white,yellow}</td></tr>
+
+ <tr id="var_rowNationality"> <td>2</td> <td>Nationality</td> <td id="bVar_Nationality">{Englishman,Dane,German,Norwegian,Swede}</td></tr>
+
+ <tr id="var_rowDrink"> <td>3</td> <td>Drink</td> <td id="bVar_Drink">{tea,beer,coffee,milk,water}</td></tr>
+
+ <tr id="var_rowCigarette"> <td>4</td> <td>Cigarette</td> <td id="bVar_Cigarette">{Pall_Mall,Blend,Blue_Masters,Dunhills,Prince}</td></tr>
+
+ <tr id="var_rowPet"> <td>5</td> <td>Pet</td> <td id="bVar_Pet">{dog,bird,cat,fish,horse}</td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Trace (length=3)</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(House={0,1,2,3,4},color_House={(0|->yellow),(1|->blue),(2|->red),(3|->green),(4|->white)},nationality_Ho...</td><td>State 0</td></tr>
+
+ <tr id="row2" onclick="visualise1(2)"><td>2</td><td style="cursor:pointer">INITIALISATION()</td><td><button onclick="visualise1(2);">State 1</button></td></tr>
+
+ <tr id="row3" onclick="visualise1(3)"><td>3</td><td style="cursor:pointer">run0</td><td><button onclick="visualise1(3);">State 1</button></td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis">
+Generated on 22/3/2021 at 8:19 using ProB version 1.11.0-nightly
+<br>Main specification file: einsteins_puzzle.als
+ </table>
+ </div>
+ <script> visualise1(3); </script>
+ </div>
+ <script> registerHovers() </script>
+
+<script>
+var collapsibles = document.getElementsByClassName("collapsible");
+var ii;
+
+for (ii = 0; ii < collapsibles.length; ii++) {
+ collapsibles[ii].addEventListener("click", function() {
+ this.classList.toggle("active");
+ var content = this.nextElementSibling;
+ if (content.style.display === "block") {
+ content.style.display = "none";
+ } else {
+ content.style.display = "block";
+ }
+ });
+}
+</script>
+
+</body>
+</html>
+