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

fix width of svg box

parent 18dc4b26
No related branches found
No related tags found
No related merge requests found
<!DOCTYPE html>
<html>
<head>
<!-- html file generated by ProB from a VisB visualization -->
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<script>
function setAttr(id, attribute, value){
const 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") {
if (obj.closest('foreignObject')) {
obj.innerHTML = value;
} else {
obj.textContent = value;
}
} else if(attribute==="class" && value !== "") {
if(value[0]==="+") {
obj.classList.add(value.substring(1));
} else if(value[0]==="-") {
obj.classList.remove(value.substring(1));
} else {
obj.setAttribute(attribute, value);
}
} else {
obj.setAttribute(attribute, value);
}
}
function sleep(ms) {
return new Promise(resolve => setTimeout(resolve, ms));
}
let lastSelectedRow = 0;
function highlightRow(id) {
if (lastSelectedRow>0) {setAttr("row"+lastSelectedRow,"bgcolor","")}
if (document.getElementById("row"+id) != null) {
setAttr("row"+id,"bgcolor","yellow");
lastSelectedRow = id;
}
}
function backStep() {
if (lastSelectedRow>1) {
const prev = lastSelectedRow - 1;
document.getElementById("row"+prev).click();
}
}
function forwardStep() {
if (lastSelectedRow>0) {
const nxt = lastSelectedRow + 1;
const 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;
max-height: 30vh;
display: none;
overflow: auto;
background-color: #f1f1f1;
}
.coll-content-vis {
padding: 0 12px;
max-height: 30vh;
display: block;
overflow: auto;
background-color: #f1f1f1;
}
.visb-messages {
text-align: left;
outline: none;
font-size: 12px;
font-family: arial, sans-serif;
}
.svg-outer-container {
width: 100%;
height: 100%;
overflow: auto;
visibility: hidden;
resize: vertical;
}
.svg-inner-container {
width: 100%;
height: 100%;
display: flex;
transform-origin: left top;
/*cursor: grab;*/
}
.svg-inner-container:active {
cursor: grabbing;
}
svg {
width: 100%;
height: 100%;
}
.seq-chart-container {
width: 100%;
height: 100%;
overflow: auto;
resize: vertical;
}
</style>
<script>
const differences = [
[
{id: "trace_meter", attr: "value", val: "1"},
{id: "visb_debug_messages", attr: "text", val: "Step 1/7, State ID: 0, Event: SETUP_CONSTANTS(f={(1↦data1),(2↦data2),(3↦data3)},n=3) "},
{id: "bOperation_brp", attr: "text", val: ""},
{id: "row_bOperation_brp", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_brp", attr: "text", val: "brp"},
{id: "bOperation_RCV_current_data", attr: "text", val: ""},
{id: "row_bOperation_RCV_current_data", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_RCV_current_data", attr: "text", val: "RCV_current_data"},
{id: "bOperation_RCV_success", attr: "text", val: ""},
{id: "row_bOperation_RCV_success", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_RCV_success", attr: "text", val: "RCV_success"},
{id: "bOperation_RCV_failure", attr: "text", val: ""},
{id: "row_bOperation_RCV_failure", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_RCV_failure", attr: "text", val: "RCV_failure"},
{id: "bOperation_SND_success", attr: "text", val: ""},
{id: "row_bOperation_SND_success", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_SND_success", attr: "text", val: "SND_success"},
{id: "bOperation_SND_failure", attr: "text", val: ""},
{id: "row_bOperation_SND_failure", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_SND_failure", attr: "text", val: "SND_failure"},
],
[
{id: "trace_meter", attr: "value", val: "2"},
{id: "visb_debug_messages", attr: "text", val: "Step 2/7, State ID: 1, Event: INITIALISATION(g=∅,h=∅,i=0,r=0,r_st=working,s_st=working) "},
{id: "dcf903643b0cad1b752d514f0e0272cc59db95d8", attr: "fill", val: "brown"},
{id: "visb_title__1", attr: "text", val: "Packet at position 2"},
{id: "dcf903643b0cad1b752d514f0e0272cc59db95d8", attr: "y", val: "40.0"},
{id: "c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4", attr: "fill", val: "olive"},
{id: "visb_title__2", attr: "text", val: "Packet at position 3"},
{id: "c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4", attr: "y", val: "60.0"},
{id: "99852a08e4430cc11bbc4024aecda23e07d97369", attr: "fill", val: "white"},
{id: "visb_title__3", attr: "text", val: "Packet at position 4"},
{id: "99852a08e4430cc11bbc4024aecda23e07d97369", attr: "y", val: "80.0"},
{id: "0dc8c8a9d3ccd4dac8bfba08183049141d24a1db", attr: "fill", val: "white"},
{id: "visb_title__4", attr: "text", val: "Packet at position 5"},
{id: "0dc8c8a9d3ccd4dac8bfba08183049141d24a1db", attr: "y", val: "100.0"},
{id: "8f7d96168b21c39adae40a6b891ffc38476ec068", attr: "fill", val: "green"},
{id: "visb_title__5", attr: "text", val: "Packet at position 1"},
{id: "8f7d96168b21c39adae40a6b891ffc38476ec068", attr: "y", val: "20.0"},
{id: "5fbaf8471f17137d0b5a04be74f971ac446a3b9d", attr: "fill", val: "white"},
{id: "visb_title__6", attr: "text", val: "Packet at position 1"},
{id: "5fbaf8471f17137d0b5a04be74f971ac446a3b9d", attr: "y", val: "20.0"},
{id: "0cb90f31a4b31af152b607c414d1d702bb4ad956", attr: "fill", val: "white"},
{id: "visb_title__7", attr: "text", val: "Packet at position 5"},
{id: "0cb90f31a4b31af152b607c414d1d702bb4ad956", attr: "y", val: "100.0"},
{id: "ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0", attr: "fill", val: "white"},
{id: "visb_title__8", attr: "text", val: "Packet at position 4"},
{id: "ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0", attr: "y", val: "80.0"},
{id: "7673a90e80cf71cc35e50c60c96ceee720e509c3", attr: "fill", val: "white"},
{id: "visb_title__9", attr: "text", val: "Packet at position 3"},
{id: "7673a90e80cf71cc35e50c60c96ceee720e509c3", attr: "y", val: "60.0"},
{id: "b189f6518dc79b567372d086468aa87b56ec1555", attr: "fill", val: "white"},
{id: "visb_title__10", attr: "text", val: "Packet at position 2"},
{id: "b189f6518dc79b567372d086468aa87b56ec1555", attr: "y", val: "40.0"},
{id: "a0028c9b03d87aa039426030a5e3f308bab1d912", attr: "fill", val: "white"},
{id: "visb_title__11", attr: "text", val: "Packet at position 4"},
{id: "a0028c9b03d87aa039426030a5e3f308bab1d912", attr: "y", val: "80.0"},
{id: "f403521da54e936b4c5ac6d1cffa8045c4536ffb", attr: "fill", val: "white"},
{id: "visb_title__12", attr: "text", val: "Packet at position 3"},
{id: "f403521da54e936b4c5ac6d1cffa8045c4536ffb", attr: "y", val: "60.0"},
{id: "6875f825d52a8aa516485ca8edfcaf8e3b4ad35b", attr: "fill", val: "white"},
{id: "visb_title__13", attr: "text", val: "Packet at position 2"},
{id: "6875f825d52a8aa516485ca8edfcaf8e3b4ad35b", attr: "y", val: "40.0"},
{id: "e4c40e27c9cf272e335810e609461f6d5c56773d", attr: "fill", val: "white"},
{id: "visb_title__14", attr: "text", val: "Packet at position 5"},
{id: "e4c40e27c9cf272e335810e609461f6d5c56773d", attr: "y", val: "100.0"},
{id: "b767cf0b58fa58dc23f9f36be265982e806dec52", attr: "fill", val: "white"},
{id: "visb_title__15", attr: "text", val: "Packet at position 1"},
{id: "b767cf0b58fa58dc23f9f36be265982e806dec52", attr: "y", val: "20.0"},
{id: "bVar_g", attr: "text", val: "{}"},
{id: "row_bVar_g", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_g", attr: "text", val: "?"},
{id: "bVar_h", attr: "text", val: "{}"},
{id: "row_bVar_h", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_h", attr: "text", val: "?"},
{id: "bVar_i", attr: "text", val: "0"},
{id: "row_bVar_i", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_i", attr: "text", val: "?"},
{id: "bVar_r", attr: "text", val: "0"},
{id: "row_bVar_r", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_r", attr: "text", val: "?"},
{id: "bVar_r_st", attr: "text", val: "working"},
{id: "row_bVar_r_st", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_r_st", attr: "text", val: "?"},
{id: "bVar_s_st", attr: "text", val: "working"},
{id: "row_bVar_s_st", attr: "bgcolor", val: "#fffacd"},
{id: "bVarPrev_s_st", attr: "text", val: "?"},
{id: "bOperation_RCV_current_data", attr: "text", val: ""},
{id: "row_bOperation_RCV_current_data", attr: "bgcolor", val: "white"},
{id: "name_bOperation_RCV_current_data", attr: "text", val: "RCV_current_data"},
{id: "bOperation_SND_failure", attr: "text", val: ""},
{id: "row_bOperation_SND_failure", attr: "bgcolor", val: "white"},
{id: "name_bOperation_SND_failure", attr: "text", val: "SND_failure"},
],
[
{id: "trace_meter", attr: "value", val: "3"},
{id: "visb_debug_messages", attr: "text", val: "Step 3/7, State ID: 2, Event: RCV_current_data the receiver receives packet nr. 1 : data1"},
{id: "b767cf0b58fa58dc23f9f36be265982e806dec52", attr: "fill", val: "green"},
{id: "row_bVar_g", attr: "bgcolor", val: "white"},
{id: "bVarPrev_g", attr: "text", val: "{}"},
{id: "bVar_h", attr: "text", val: "{(1|->data1)}"},
{id: "bVarPrev_h", attr: "text", val: "{}"},
{id: "row_bVar_i", attr: "bgcolor", val: "white"},
{id: "bVarPrev_i", attr: "text", val: "0"},
{id: "bVar_r", attr: "text", val: "1"},
{id: "bVarPrev_r", attr: "text", val: "0"},
{id: "row_bVar_r_st", attr: "bgcolor", val: "white"},
{id: "bVarPrev_r_st", attr: "text", val: "working"},
{id: "row_bVar_s_st", attr: "bgcolor", val: "white"},
{id: "bVarPrev_s_st", attr: "text", val: "working"},
],
[
{id: "trace_meter", attr: "value", val: "4"},
{id: "visb_debug_messages", attr: "text", val: "Step 4/7, State ID: 4, Event: RCV_current_data the receiver receives packet nr. 2 : data2"},
{id: "6875f825d52a8aa516485ca8edfcaf8e3b4ad35b", attr: "fill", val: "brown"},
{id: "bVar_h", attr: "text", val: "{(1|->data1),(2|->data2)}"},
{id: "bVarPrev_h", attr: "text", val: "{(1|->data1)}"},
{id: "bVar_r", attr: "text", val: "2"},
{id: "bVarPrev_r", attr: "text", val: "1"},
{id: "bOperation_RCV_current_data", attr: "text", val: ""},
{id: "row_bOperation_RCV_current_data", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_RCV_current_data", attr: "text", val: "RCV_current_data"},
{id: "bOperation_RCV_success", attr: "text", val: ""},
{id: "row_bOperation_RCV_success", attr: "bgcolor", val: "white"},
{id: "name_bOperation_RCV_success", attr: "text", val: "RCV_success"},
],
[
{id: "trace_meter", attr: "value", val: "5"},
{id: "visb_debug_messages", attr: "text", val: "Step 5/7, State ID: 6, Event: RCV_success the receiver receives last packet nr. 3 : data3"},
{id: "f403521da54e936b4c5ac6d1cffa8045c4536ffb", attr: "fill", val: "olive"},
{id: "bVar_h", attr: "text", val: "{(1|->data1),(2|->data2),(3|->data3)}"},
{id: "bVarPrev_h", attr: "text", val: "{(1|->data1),(2|->data2)}"},
{id: "bVar_r", attr: "text", val: "3"},
{id: "bVarPrev_r", attr: "text", val: "2"},
{id: "bVar_r_st", attr: "text", val: "success"},
{id: "row_bVar_r_st", attr: "bgcolor", val: "#fffacd"},
{id: "bOperation_RCV_success", attr: "text", val: ""},
{id: "row_bOperation_RCV_success", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_RCV_success", attr: "text", val: "RCV_success"},
{id: "bOperation_SND_success", attr: "text", val: ""},
{id: "row_bOperation_SND_success", attr: "bgcolor", val: "white"},
{id: "name_bOperation_SND_success", attr: "text", val: "SND_success"},
],
[
{id: "trace_meter", attr: "value", val: "6"},
{id: "visb_debug_messages", attr: "text", val: "Step 6/7, State ID: 8, Event: SND_success the sender detectcs successful completion"},
{id: "row_bVar_h", attr: "bgcolor", val: "white"},
{id: "bVarPrev_h", attr: "text", val: "{(1|->data1),(2|->data2),(3|->data3)}"},
{id: "row_bVar_r", attr: "bgcolor", val: "white"},
{id: "bVarPrev_r", attr: "text", val: "3"},
{id: "row_bVar_r_st", attr: "bgcolor", val: "white"},
{id: "bVarPrev_r_st", attr: "text", val: "success"},
{id: "bVar_s_st", attr: "text", val: "success"},
{id: "row_bVar_s_st", attr: "bgcolor", val: "#fffacd"},
{id: "bOperation_brp", attr: "text", val: ""},
{id: "row_bOperation_brp", attr: "bgcolor", val: "white"},
{id: "name_bOperation_brp", attr: "text", val: "brp(g={(1|->data1),(2|->data2),(3|->data3)},i=3)"},
{id: "bOperation_SND_success", attr: "text", val: ""},
{id: "row_bOperation_SND_success", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_SND_success", attr: "text", val: "SND_success"},
{id: "bOperation_SND_failure", attr: "text", val: ""},
{id: "row_bOperation_SND_failure", attr: "bgcolor", val: "#f1f1f1"},
{id: "name_bOperation_SND_failure", attr: "text", val: "SND_failure"},
],
[
{id: "trace_meter", attr: "value", val: "7"},
{id: "visb_debug_messages", attr: "text", val: "Step 7/7, State ID: 10, Event: brp(g={(1↦data1),(2↦data2),(3↦data3)},i=3) the protocol terminates on the sender side with 3 packets sent"},
{id: "5fbaf8471f17137d0b5a04be74f971ac446a3b9d", attr: "fill", val: "green"},
{id: "7673a90e80cf71cc35e50c60c96ceee720e509c3", attr: "fill", val: "olive"},
{id: "b189f6518dc79b567372d086468aa87b56ec1555", attr: "fill", val: "brown"},
{id: "bVar_g", attr: "text", val: "{(1|->data1),(2|->data2),(3|->data3)}"},
{id: "row_bVar_g", attr: "bgcolor", val: "#fffacd"},
{id: "bVar_i", attr: "text", val: "3"},
{id: "row_bVar_i", attr: "bgcolor", val: "#fffacd"},
{id: "row_bVar_s_st", attr: "bgcolor", val: "white"},
{id: "bVarPrev_s_st", attr: "text", val: "success"},
]
]
const transitions = new Map();
for (let j = 0; j < differences.length; j++) {
const transitionAttributeValues = new Map();
for (let i = 0; i <= j; i++) {
const transitionI = differences[i];
for (const attrValue of transitionI) {
const key = {id: attrValue.id, attr: attrValue.attr};
transitionAttributeValues.set(key, attrValue.val);
}
}
transitions.set(j+1, transitionAttributeValues);
}
function replayStep(stepNr) {
transitions.get(stepNr).forEach((value, key) => {
setAttr(key.id, key.attr, value);
});
highlightRow(stepNr);
}
async function runAll(delay) {
for (let i = 1; i <= transitions.size; i++) {
replayStep(i);
await sleep(delay);
}
}
</script>
<script> function registerHovers() {} </script>
</head>
<body>
<button type="button" class="collapsible collapsible-style active">SVG Visualisation</button>
<div>
<div text-align="left" id="visb_svg_outer_container" class="svg-outer-container">
<div id="visb_svg_inner_container" class="svg-inner-container">
<svg xmlns="http://www.w3.org/2000/svg"
width="60.0" height="125.0" viewBox="0 0 60.0 125.0" >
<script>let visb_vars = {};</script>
<text id="185c017c3519945db675741b005ddd058ee0e5ea" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
<rect id="dcf903643b0cad1b752d514f0e0272cc59db95d8" height="20.0" stroke="black" width="20.0" x="10.0">
<title id="visb_title__1">-title-not-set-</title>
</rect>
<text id="21fbf8bea61dfc7508d1536d7e49aee85f7aa6bc" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
<rect id="c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4" height="20.0" stroke="black" width="20.0" x="10.0">
<title id="visb_title__2">-title-not-set-</title>
</rect>
<text id="668b03895b45f81c53cd13e6a8ce2be6ad1e9b61" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
<rect id="99852a08e4430cc11bbc4024aecda23e07d97369" height="20.0" stroke="black" width="20.0" x="10.0">
<title id="visb_title__3">-title-not-set-</title>
</rect>
<text id="9e57278e1d7bf120da2d1bef7864d939a65c197b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
<rect id="0dc8c8a9d3ccd4dac8bfba08183049141d24a1db" height="20.0" stroke="black" width="20.0" x="10.0">
<title id="visb_title__4">-title-not-set-</title>
</rect>
<text id="acfc5e145aae9a6a80390a9c27f172053824ca63" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
<rect id="8f7d96168b21c39adae40a6b891ffc38476ec068" height="20.0" stroke="black" width="20.0" x="10.0">
<title id="visb_title__5">-title-not-set-</title>
</rect>
<text id="3c145d8704ce2d495bcf484ef6030e0f6361e477" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
<rect id="5fbaf8471f17137d0b5a04be74f971ac446a3b9d" height="20.0" stroke="black" width="20.0" x="40.0">
<title id="visb_title__6">-title-not-set-</title>
</rect>
<text id="66f9ec9c178d2c9393636aff340877e90ad52e20" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
<rect id="0cb90f31a4b31af152b607c414d1d702bb4ad956" height="20.0" stroke="black" width="20.0" x="40.0">
<title id="visb_title__7">-title-not-set-</title>
</rect>
<text id="6c577c7b9481f803c18ae3297a56415a093d067b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
<rect id="ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0" height="20.0" stroke="black" width="20.0" x="40.0">
<title id="visb_title__8">-title-not-set-</title>
</rect>
<text id="7e83e68e85ae62405e98a47bbc8b96b3bfda30ee" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
<rect id="7673a90e80cf71cc35e50c60c96ceee720e509c3" height="20.0" stroke="black" width="20.0" x="40.0">
<title id="visb_title__9">-title-not-set-</title>
</rect>
<text id="e36cfd8dc56c5b35e489917b7427e221de9c5d26" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
<rect id="b189f6518dc79b567372d086468aa87b56ec1555" height="20.0" stroke="black" width="20.0" x="40.0">
<title id="visb_title__10">-title-not-set-</title>
</rect>
<text id="0a6a56bb334abae4f7e4338b2e753441d4438030" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
<rect id="a0028c9b03d87aa039426030a5e3f308bab1d912" height="20.0" stroke="black" width="20.0" x="70.0">
<title id="visb_title__11">-title-not-set-</title>
</rect>
<text id="3aee0fe6e417da9d537d27629417ae588e9d9b6b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
<rect id="f403521da54e936b4c5ac6d1cffa8045c4536ffb" height="20.0" stroke="black" width="20.0" x="70.0">
<title id="visb_title__12">-title-not-set-</title>
</rect>
<text id="4ebfbc87d748752c9e96d6d2d36883d1be653a67" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
<rect id="6875f825d52a8aa516485ca8edfcaf8e3b4ad35b" height="20.0" stroke="black" width="20.0" x="70.0">
<title id="visb_title__13">-title-not-set-</title>
</rect>
<text id="6fbff960756ae2f6a255f05ea36f74dfe76b28d3" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
<rect id="e4c40e27c9cf272e335810e609461f6d5c56773d" height="20.0" stroke="black" width="20.0" x="70.0">
<title id="visb_title__14">-title-not-set-</title>
</rect>
<text id="ce5ae6be0a3b304d088edf9f6c02bdf6f04330d9" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
<rect id="b767cf0b58fa58dc23f9f36be265982e806dec52" height="20.0" stroke="black" width="20.0" x="70.0">
<title id="visb_title__15">-title-not-set-</title>
</rect>
</svg>
</div>
</div>
</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>
<br><label id="visb_debug_messages" class="visb-messages"> </label>
</div>
<progress id="trace_meter" min="0" max="7" value="0"></progress>
<button type="button" class="collapsible collapsible-style">Variables (6)</button>
<div class="coll-content-hid">
<table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> <th>Previous Value</th> </tr>
<tr id="row_bVar_g" title="Type: (INT&lt;-&gt;D)"> <td>1</td> <td id="name_bVar_g">g</td> <td id="bVar_g">?</td> <td id="bVarPrev_g">?</td> </tr>
<tr id="row_bVar_h" title="Type: (INT&lt;-&gt;D)"> <td>2</td> <td id="name_bVar_h">h</td> <td id="bVar_h">?</td> <td id="bVarPrev_h">?</td> </tr>
<tr id="row_bVar_i" title="Type: INT"> <td>3</td> <td id="name_bVar_i">i</td> <td id="bVar_i">?</td> <td id="bVarPrev_i">?</td> </tr>
<tr id="row_bVar_r" title="Type: INT"> <td>4</td> <td id="name_bVar_r">r</td> <td id="bVar_r">?</td> <td id="bVarPrev_r">?</td> </tr>
<tr id="row_bVar_r_st" title="Type: STATUS"> <td>5</td> <td id="name_bVar_r_st">r_st</td> <td id="bVar_r_st">?</td> <td id="bVarPrev_r_st">?</td> </tr>
<tr id="row_bVar_s_st" title="Type: STATUS"> <td>6</td> <td id="name_bVar_s_st">s_st</td> <td id="bVar_s_st">?</td> <td id="bVarPrev_s_st">?</td> </tr>
</table>
</div>
<button type="button" class="collapsible collapsible-style">Constants (2)</button>
<div class="coll-content-hid">
<table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
<tr id="row_bConstant_f" title="Type: (INT&lt;-&gt;D)"> <td>1</td> <td id="name_bConstant_f">f</td> <td id="bConstant_f">{(1|-&gt;data1),(2|-&gt;data2),(3|-&gt;data3)}</td> </tr>
<tr id="row_bConstant_n" title="Type: INT"> <td>2</td> <td id="name_bConstant_n">n</td> <td id="bConstant_n">3</td> </tr>
</table>
</div>
<button type="button" class="collapsible collapsible-style">Sets (2)</button>
<div class="coll-content-hid">
<table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
<tr id="row_bSet_D" title="Type: POW(D)
Desc: block contents of files"> <td>1</td> <td id="name_bSet_D">D</td> <td id="bSet_D">{data1,data2,data3}</td> </tr>
<tr id="row_bSet_STATUS" title="Type: POW(STATUS)"> <td>2</td> <td id="name_bSet_STATUS">STATUS</td> <td id="bSet_STATUS">{working,success,failure}</td> </tr>
</table>
</div>
<button type="button" class="collapsible collapsible-style">Events (6)</button>
<div class="coll-content-hid">
<table> <tr> <th>Nr</th> <th>Name</th> <th>Enabled</th> </tr>
<tr id="row_bOperation_brp" title="Operation: brp()"> <td>1</td> <td id="name_bOperation_brp">brp</td> <td id="bOperation_brp">?</td> </tr>
<tr id="row_bOperation_RCV_current_data" title="Operation: RCV_current_data()"> <td>2</td> <td id="name_bOperation_RCV_current_data">RCV_current_data</td> <td id="bOperation_RCV_current_data">?</td> </tr>
<tr id="row_bOperation_RCV_success" title="Operation: RCV_success()"> <td>3</td> <td id="name_bOperation_RCV_success">RCV_success</td> <td id="bOperation_RCV_success">?</td> </tr>
<tr id="row_bOperation_RCV_failure" title="Operation: RCV_failure()"> <td>4</td> <td id="name_bOperation_RCV_failure">RCV_failure</td> <td id="bOperation_RCV_failure">?</td> </tr>
<tr id="row_bOperation_SND_success" title="Operation: SND_success()"> <td>5</td> <td id="name_bOperation_SND_success">SND_success</td> <td id="bOperation_SND_success">?</td> </tr>
<tr id="row_bOperation_SND_failure" title="Operation: SND_failure()"> <td>6</td> <td id="name_bOperation_SND_failure">SND_failure</td> <td id="bOperation_SND_failure">?</td> </tr>
</table>
</div>
<button type="button" class="collapsible collapsible-style active">Trace (length=7)</button>
<div class="coll-content-vis">
<table> <tr> <th>Nr</th> <th>Event</th> <th>Description</th> <th>Target State ID</th> </tr>
<tr id="row1"><td>1</td><td style="cursor:not-allowed">SETUP_CONSTANTS(f={(1&#8614;data1),(2&#8614;data2),(3&#8614;data3)},n=3)</td><td></td><td>State 0</td></tr>
<tr id="row2" onclick="replayStep(2)"><td>2</td><td style="cursor:pointer">INITIALISATION(g=&empty;,h=&empty;,i=0,r=0,r_st=working,s_st=working)</td><td></td><td><button onclick="replayStep(2);">State 1</button></td></tr>
<tr id="row3" onclick="replayStep(3)"><td>3</td><td style="cursor:pointer">RCV_current_data</td><td>the receiver receives packet nr. 1 : data1</td><td><button onclick="replayStep(3);">State 2</button></td></tr>
<tr id="row4" onclick="replayStep(4)"><td>4</td><td style="cursor:pointer">RCV_current_data</td><td>the receiver receives packet nr. 2 : data2</td><td><button onclick="replayStep(4);">State 4</button></td></tr>
<tr id="row5" onclick="replayStep(5)"><td>5</td><td style="cursor:pointer">RCV_success</td><td>the receiver receives last packet nr. 3 : data3</td><td><button onclick="replayStep(5);">State 6</button></td></tr>
<tr id="row6" onclick="replayStep(6)"><td>6</td><td style="cursor:pointer">SND_success</td><td>the sender detectcs successful completion</td><td><button onclick="replayStep(6);">State 8</button></td></tr>
<tr id="row7" onclick="replayStep(7)"><td>7</td><td style="cursor:pointer">brp(g={(1&#8614;data1),(2&#8614;data2),(3&#8614;data3)},i=3)</td><td>the protocol terminates on the sender side with 3 packets sent</td><td><button onclick="replayStep(7);">State 10</button></td></tr>
</table>
</div>
<button type="button" class="collapsible-style">Info</button>
<div class="coll-content-vis visb-messages">
Generated on 25/11/2024 at 13:53 using <a href="https://prob.hhu.de/">ProB</a> version 1.13.1-nightly
<br>Main specification file: brp_1_prob_mch.eventb (modified on 25/11/2024 at 12:48)
<br>Main specification name: brp_1_prob
<br>Main VisB JSON file: ../../../../JAVAPROB/visb-visualisation-examples/BRP/visb_brp.def (modified on 25/11/2024 at 13:51)
<script> replayStep(7); </script>
</div>
<script>
registerHovers();
const collapsibles = document.getElementsByClassName("collapsible");
for (let ii = 0; ii < collapsibles.length; ii++) {
collapsibles[ii].onclick = function() {
this.classList.toggle("active");
this.nextElementSibling.style.display = this.classList.contains("active") ? "block" : "none";
};
}
const outerContainer = document.getElementById('visb_svg_outer_container');
const innerContainer = document.getElementById('visb_svg_inner_container');
let scale = 1;
let isDragging = false;
let startMouseX, startMouseY;
let scrollSpeed = 1.03;
let minScale = 0.5;
let maxScale = 100.0;
outerContainer.onwheel = (e) => {
e.preventDefault();
const oldScale = scale;
scale *= (e.deltaY < 0) ? scrollSpeed : 1 / scrollSpeed;
scale = Math.max(scale, minScale);
scale = Math.min(scale, maxScale);
const rect = outerContainer.getBoundingClientRect();
const mouseX = e.clientX - rect.left + outerContainer.scrollLeft;
const mouseY = e.clientY - rect.top + outerContainer.scrollTop;
const scaleChange = scale / oldScale;
innerContainer.style.transform = `scale(${scale})`;
outerContainer.scrollBy({
left: mouseX * (scaleChange - 1),
top: mouseY * (scaleChange - 1),
behavior: 'instant'
});
};
outerContainer.onmousedown = (e) => {
isDragging = true;
startMouseX = e.clientX;
startMouseY = e.clientY;
};
document.onmousemove = (e) => {
if (!isDragging) return;
const dx = startMouseX - e.clientX;
const dy = startMouseY - e.clientY;
outerContainer.scrollBy(dx,dy);
startMouseX = e.clientX;
startMouseY = e.clientY;
};
document.onmouseup = () => isDragging = false;
outerContainer.onmouseleave = () => isDragging = false;
const outerContainerHeight = parseFloat(window.getComputedStyle(outerContainer).height);
if (outerContainerHeight > window.innerHeight * 0.7) {
outerContainer.style.height = '70vh';
}
outerContainer.style.visibility = 'visible';
</script>
</body>
</html>
......@@ -12,7 +12,7 @@ DEFINITIONS
stroke:"black", title:```Packet at position ${pos}```));
VISB_SVG_BOX == rec(height:DPWID*(1.25+real(max(DOM))),
width:DPWID*3.0);
width:DPWID*4.6);
VISB_SVG_OBJECTS1 == {(i).i:DOM|DataPacket("f",f,i,0.5*DPWID)};
VISB_SVG_OBJECTS2 == {(i).i:DOM|DataPacket("g",g,i,2.0*DPWID)};
VISB_SVG_OBJECTS3 == {(i).i:DOM|DataPacket("h",h,i,3.5*DPWID)}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment