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

add XTL button example 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent ed768b13
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Button/TLA/button.json
+ 3
− 2
View file @ 57999cdd
......@@ -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",
......
Button/XTL/button.P 0 → 100644
+ 12
− 0
View file @ 57999cdd
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
Button/XTL/button.html 0 → 100644
+ 257
− 0
View file @ 57999cdd
<!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()">&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>
<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>
Button/XTL/button.json 0 → 100644
+ 31
− 0
View file @ 57999cdd
{
"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"}]
}
]
}
Button/button.json
+ 1
− 1
View file @ 57999cdd
......@@ -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"
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment