Select Git revision
Einstein.tla.html
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
Einstein.tla.html 10.78 KiB
<!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="300"
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:20 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>