From d9ee8a3b89000a488270b2522d921ebc31d7dcb0 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 25 Nov 2024 14:03:44 +0100
Subject: [PATCH] fix width of svg box
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
BRP/brp_1_prob_mch.html | 602 ++++++++++++++++++++++++++++++++++++++++
BRP/visb_brp.def | 2 +-
2 files changed, 603 insertions(+), 1 deletion(-)
create mode 100644 BRP/brp_1_prob_mch.html
diff --git a/BRP/brp_1_prob_mch.html b/BRP/brp_1_prob_mch.html
new file mode 100644
index 0000000..dbe79b1
--- /dev/null
+++ b/BRP/brp_1_prob_mch.html
@@ -0,0 +1,602 @@
+<!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()">« 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>
+ <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<->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<->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<->D)"> <td>1</td> <td id="name_bConstant_f">f</td> <td id="bConstant_f">{(1|->data1),(2|->data2),(3|->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↦data1),(2↦data2),(3↦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=∅,h=∅,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↦data1),(2↦data2),(3↦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>
+
diff --git a/BRP/visb_brp.def b/BRP/visb_brp.def
index 363491c..2f56d94 100644
--- a/BRP/visb_brp.def
+++ b/BRP/visb_brp.def
@@ -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)}
--
GitLab