diff --git a/Button/TLA/button.json b/Button/TLA/button.json
index 30b88867da067380a44d1511af4342f9fb36f2c2..5bf60bcb54924328f56fe3a47c65bdea85e5da0b 100644
--- a/Button/TLA/button.json
+++ b/Button/TLA/button.json
@@ -9,8 +9,9 @@
{
"id": "button",
"attr": "stroke-width",
- "value": "IF ENABLED(\"press_button\") THEN 6 ELSE 1 END",
- "ignore": "is now used in hover below"
+ "value": "IF GET_IS_ENABLED(\"press_button\")=TRUE THEN 6 ELSE 1 END",
+ "ignore": "true",
+ "comment": "is now used in hover below"
},
{
"id": "button_%0",
diff --git a/Button/XTL/button.P b/Button/XTL/button.P
new file mode 100644
index 0000000000000000000000000000000000000000..800b0c777d975efac8bbee3886e87db87603ff0c
--- /dev/null
+++ b/Button/XTL/button.P
@@ -0,0 +1,12 @@
+start(button(on)).
+
+trans(press_button,button(off),button(on)).
+trans(toggle_button,button(X),button(Y)) :- toggle(X,Y).
+trans(set_button(V),_,button(V)) :- toggle(V,_).
+
+prop(button(X),'='(button,X)).
+
+toggle(on,off).
+toggle(off,on).
+
+prob_pragma_string('VISB_JSON_FILE','button.json').
\ No newline at end of file
diff --git a/Button/XTL/button.html b/Button/XTL/button.html
new file mode 100644
index 0000000000000000000000000000000000000000..72a62a9d708bc75c2abeb958c260f1c26514e242
--- /dev/null
+++ b/Button/XTL/button.html
@@ -0,0 +1,257 @@
+<!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 if(attribute=="class" && value != "") {
+ if(value[0]=="+") {
+ obj.classList.add(value.substr(1));
+ } else if(value[0]=="-") {
+ obj.classList.remove(value.substr(1));
+ } else {
+ obj.setAttribute(attribute, 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("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/9, State ID: 0");
+ setAttr("button","fill","green");
+ setAttr("button_TRUE","visibility","hidden");
+ setAttr("button_FALSE","visibility","hidden");
+ highlightRow(stepNr);
+ }
+ function visualise1(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/9, State ID: 1");
+ setAttr("button","fill","red");
+ setAttr("button_TRUE","visibility","hidden");
+ setAttr("button_FALSE","visibility","hidden");
+ highlightRow(stepNr);
+ }
+ async function runAll(delay) {
+ visualise0(1);
+ setAttr("visb_debug_messages","text","Step: 1/9, State ID: 0, Event: start_xtl_system");
+ await sleep(delay);
+ visualise1(2);
+ setAttr("visb_debug_messages","text","Step: 2/9, State ID: 1, Event: set_button(off)");
+ await sleep(delay);
+ visualise0(3);
+ setAttr("visb_debug_messages","text","Step: 3/9, State ID: 0, Event: set_button(on)");
+ await sleep(delay);
+ visualise1(4);
+ setAttr("visb_debug_messages","text","Step: 4/9, State ID: 1, Event: toggle_button");
+ await sleep(delay);
+ visualise0(5);
+ setAttr("visb_debug_messages","text","Step: 5/9, State ID: 0, Event: press_button");
+ await sleep(delay);
+ visualise1(6);
+ setAttr("visb_debug_messages","text","Step: 6/9, State ID: 1, Event: toggle_button");
+ await sleep(delay);
+ visualise0(7);
+ setAttr("visb_debug_messages","text","Step: 7/9, State ID: 0, Event: press_button");
+ await sleep(delay);
+ visualise1(8);
+ setAttr("visb_debug_messages","text","Step: 8/9, State ID: 1, Event: toggle_button");
+ await sleep(delay);
+ visualise0(9);
+ setAttr("visb_debug_messages","text","Step: 9/9, State ID: 0, Event: toggle_button");
+ await sleep(delay);
+ }
+ </script>
+
+ <script>
+ function registerHovers() {
+ button.onmouseover = function(ev){
+ setAttr("button","stroke-width","6")
+ setAttr("button","opacity","0.8")
+ };
+ button.onmouseout = function(){
+ setAttr("button","stroke-width","1")
+ setAttr("button","opacity","1.0")
+ };
+ }
+ </script>
+ </head>
+<body>
+ <button type="button" class="collapsible collapsible-style">SVG Visualisation</button>
+ <div text-align="left">
+
+
+<svg height="240" width="200">
+ <circle id="button" cx="100" cy="100" r="80"
+ stroke="black" stroke-width="3" fill="green" />
+ <text text-align="left" x="50" y="190"
+ font-family="sans-serif">
+ <tspan dx="0" dy = "0.6em" id="visb_debug_messages">1.</tspan>
+ </text>
+ <circle id="button_TRUE" cx="10" cy="200" r="8"
+ stroke="black" stroke-width="3" fill="green" />
+ <circle id="button_FALSE" cx="30" cy="200" r="8"
+ stroke="black" stroke-width="3" fill="red" />
+</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>
+ <progress id="trace_meter" min="0" max="9" value="0"></progress>
+ <button type="button" class="collapsible-style">Trace (length=9)</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">start_xtl_system</td><td>State 0</td></tr>
+
+ <tr id="row2"><td>2</td><td style="cursor:not-allowed">set_button(off)</td><td>State 1</td></tr>
+
+ <tr id="row3"><td>3</td><td style="cursor:not-allowed">set_button(on)</td><td>State 0</td></tr>
+
+ <tr id="row4"><td>4</td><td style="cursor:not-allowed">toggle_button</td><td>State 1</td></tr>
+
+ <tr id="row5"><td>5</td><td style="cursor:not-allowed">press_button</td><td>State 0</td></tr>
+
+ <tr id="row6"><td>6</td><td style="cursor:not-allowed">toggle_button</td><td>State 1</td></tr>
+
+ <tr id="row7"><td>7</td><td style="cursor:not-allowed">press_button</td><td>State 0</td></tr>
+
+ <tr id="row8"><td>8</td><td style="cursor:not-allowed">toggle_button</td><td>State 1</td></tr>
+
+ <tr id="row9"><td>9</td><td style="cursor:not-allowed">toggle_button</td><td>State 0</td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis">
+Generated on 16/6/2022 at 9:36 using ProB version 1.12.0-nightly
+<br>Main specification file: button.P (modified on 16/6/2022 at 9:25)
+<br>Main VisB JSON file: button.json (modified on 16/6/2022 at 9:31)
+ </table>
+ </div>
+ <script> visualise0(9); </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/Button/XTL/button.json b/Button/XTL/button.json
new file mode 100644
index 0000000000000000000000000000000000000000..e010c48c77562e8a3a7624e128e2e1a30eb759f2
--- /dev/null
+++ b/Button/XTL/button.json
@@ -0,0 +1,31 @@
+{
+ "svg": "../button.svg",
+ "items": [
+ {
+ "id": "button",
+ "attr": "fill",
+ "value": "IF STATE_PROPERTY(\"button\")=\"on\" THEN \"green\" ELSE \"red\" END"
+ },
+ {
+ "id": "button",
+ "attr": "stroke-width",
+ "value": "IF GET_IS_ENABLED(\"press_button\")=TRUE THEN 6 ELSE 1 END",
+ "ignore": "true",
+ "comment": "is now used in hover below"
+ },
+ {
+ "id": "button_%0",
+ "attr": "visibility",
+ "value": "\"hidden\"",
+ "repeat": [ "TRUE", "FALSE" ]
+ }
+ ],
+ "events": [
+ {
+ "id": "button",
+ "event": "toggle_button",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ }
+ ]
+}
diff --git a/Button/button.json b/Button/button.json
index e723b293672215f1bd9f3801e452aa0553dc1417..3cd871d10ad6240b002e370661de29f988778c3f 100644
--- a/Button/button.json
+++ b/Button/button.json
@@ -10,7 +10,7 @@
{
"id": "button",
"attr": "stroke-width",
- "value": "IF ENABLED(\"press_button\") THEN 6 ELSE 1 END",
+ "value": "IF GET_IS_ENABLED(\"press_button\")=TRUE THEN 6 ELSE 1 END",
"ignore": "true",
"comment": "stroke-width is now used in hover below"
}