Skip to content
Snippets Groups Projects
Commit 1b415c80 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add Makefile for Einstein puzzles

parent e402f3ba
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Einstein/Makefile 0 → 100644
+ 20
− 0
View file @ 1b415c80
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
Einstein/html/Einstein.tla.html 0 → 100644
+ 309
− 0
View file @ 1b415c80
<!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()">&laquo; Back</button>
<button onclick="forwardStep()">Forward &raquo;</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>
Einstein/html/einsteins_puzzle.als.html 0 → 100644
+ 326
− 0
View file @ 1b415c80
<!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()">&laquo; Back</button>
<button onclick="forwardStep()">Forward &raquo;</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|-&gt;yellow),(1|-&gt;blue),(2|-&gt;red),(3|-&gt;green),(4|-&gt;white)}</td></tr>
<tr id="var_rownationality_House"> <td>3</td> <td>nationality_House</td> <td id="bVar_nationality_House">{(0|-&gt;Norwegian),(1|-&gt;Dane),(2|-&gt;Englishman),(3|-&gt;German),(4|-&gt;Swede)}</td></tr>
<tr id="var_rowdrink_House"> <td>4</td> <td>drink_House</td> <td id="bVar_drink_House">{(0|-&gt;water),(1|-&gt;tea),(2|-&gt;milk),(3|-&gt;coffee),(4|-&gt;beer)}</td></tr>
<tr id="var_rowcigarette_House"> <td>5</td> <td>cigarette_House</td> <td id="bVar_cigarette_House">{(0|-&gt;Dunhills),(1|-&gt;Blend),(2|-&gt;Pall_Mall),(3|-&gt;Prince),(4|-&gt;Blue_Masters)}</td></tr>
<tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|-&gt;cat),(1|-&gt;horse),(2|-&gt;bird),(3|-&gt;dog),(4|-&gt;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>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment