From 69722809b094ab80545d593c5de412490d10b5e8 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 18 Oct 2023 09:56:49 +0200
Subject: [PATCH] add Event-B version of DieHard (Jars)
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
Jars/DieHard.html | 505 ++++++++++++++++++++++++++++++++++++++++
Jars/DieHard.json | 172 ++++++++++++++
Jars/DieHard_mch.eventb | 2 +
3 files changed, 679 insertions(+)
create mode 100644 Jars/DieHard.html
create mode 100644 Jars/DieHard.json
create mode 100644 Jars/DieHard_mch.eventb
diff --git a/Jars/DieHard.html b/Jars/DieHard.html
new file mode 100644
index 0000000..9d47336
--- /dev/null
+++ b/Jars/DieHard.html
@@ -0,0 +1,505 @@
+<!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){
+ 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;
+ }
+ .visb-messages {
+ text-align: left;
+ outline: none;
+ font-size: 12px;
+ font-family: arial, sans-serif;
+ }
+ </style>
+
+
+
+ <script>
+ function visualise0(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 0");
+ setAttr("jar_3_full","height","0");
+ setAttr("jar_5_full","height","0");
+ setAttr("jar_3_text","text","0");
+ setAttr("jar_5_text","text","0");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","0");
+ setAttr("transfer_right","opacity","0");
+ setAttr("transfer_sym3","opacity","0");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","0");
+ setAttr("bVar_small","text","0");
+ highlightRow(stepNr);
+ }
+ function visualise2(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 2");
+ setAttr("jar_3_full","height","0");
+ setAttr("jar_5_full","height","100");
+ setAttr("jar_3_text","text","0");
+ setAttr("jar_5_text","text","5");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","1");
+ setAttr("transfer_right","opacity","0");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","5");
+ setAttr("bVar_small","text","0");
+ highlightRow(stepNr);
+ }
+ function visualise7(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 7");
+ setAttr("jar_3_full","height","60");
+ setAttr("jar_5_full","height","40");
+ setAttr("jar_3_text","text","3");
+ setAttr("jar_5_text","text","2");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","0");
+ setAttr("transfer_right","opacity","1");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","2");
+ setAttr("bVar_small","text","3");
+ highlightRow(stepNr);
+ }
+ function visualise8(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 8");
+ setAttr("jar_3_full","height","0");
+ setAttr("jar_5_full","height","40");
+ setAttr("jar_3_text","text","0");
+ setAttr("jar_5_text","text","2");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","1");
+ setAttr("transfer_right","opacity","0");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","2");
+ setAttr("bVar_small","text","0");
+ highlightRow(stepNr);
+ }
+ function visualise9(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 9");
+ setAttr("jar_3_full","height","40");
+ setAttr("jar_5_full","height","0");
+ setAttr("jar_3_text","text","2");
+ setAttr("jar_5_text","text","0");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","0");
+ setAttr("transfer_right","opacity","1");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","0");
+ setAttr("bVar_small","text","2");
+ highlightRow(stepNr);
+ }
+ function visualise10(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 10");
+ setAttr("jar_3_full","height","40");
+ setAttr("jar_5_full","height","100");
+ setAttr("jar_3_text","text","2");
+ setAttr("jar_5_text","text","5");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","0");
+ setAttr("transfer_left","opacity","1");
+ setAttr("transfer_right","opacity","0");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","5");
+ setAttr("bVar_small","text","2");
+ highlightRow(stepNr);
+ }
+ function visualise11(stepNr) {
+ setAttr("trace_meter","value",stepNr);
+ setAttr("visb_debug_messages","text","Step "+stepNr+"/7, State ID: 11");
+ setAttr("jar_3_full","height","60");
+ setAttr("jar_5_full","height","80");
+ setAttr("jar_3_text","text","3");
+ setAttr("jar_5_text","text","4");
+ setAttr("jar_3_svg","height","60");
+ setAttr("jar_5_svg","height","100");
+ setAttr("jar_3_svg","y","0");
+ setAttr("jar_5_svg","y","0");
+ setAttr("jar_3_empty","height","60");
+ setAttr("jar_5_empty","height","100");
+ setAttr("left_3","y2","60");
+ setAttr("left_5","y2","100");
+ setAttr("right_3","y2","60");
+ setAttr("right_5","y2","100");
+ setAttr("goal_achieved","opacity","1");
+ setAttr("transfer_left","opacity","0");
+ setAttr("transfer_right","opacity","1");
+ setAttr("transfer_sym3","opacity","1");
+ setAttr("goal","x1","107");
+ setAttr("goal","x2","153");
+ setAttr("bVar_big","text","4");
+ setAttr("bVar_small","text","3");
+ highlightRow(stepNr);
+ }
+ async function runAll(delay) {
+ visualise0(1);
+ setAttr("visb_debug_messages","text","Step: 1/7, State ID: 0, Event: INITIALISATION(big=0,small=0)");
+ await sleep(delay);
+ visualise2(2);
+ setAttr("visb_debug_messages","text","Step: 2/7, State ID: 2, Event: fill_big");
+ await sleep(delay);
+ visualise7(3);
+ setAttr("visb_debug_messages","text","Step: 3/7, State ID: 7, Event: transfer_big_to_small(3)");
+ await sleep(delay);
+ visualise8(4);
+ setAttr("visb_debug_messages","text","Step: 4/7, State ID: 8, Event: empty_small");
+ await sleep(delay);
+ visualise9(5);
+ setAttr("visb_debug_messages","text","Step: 5/7, State ID: 9, Event: transfer_big_to_small(2)");
+ await sleep(delay);
+ visualise10(6);
+ setAttr("visb_debug_messages","text","Step: 6/7, State ID: 10, Event: fill_big");
+ await sleep(delay);
+ visualise11(7);
+ setAttr("visb_debug_messages","text","Step: 7/7, State ID: 11, Event: transfer_big_to_small(1)");
+ await sleep(delay);
+ }
+ </script>
+
+ <script>
+ function registerHovers() {
+ var obj;
+ obj = document.getElementById("fill_3");
+ obj.onmouseover = function(ev){
+ setAttr("fill_3","stroke-width","6")
+ setAttr("fill_3","opacity","0.8")
+ };
+ obj.onmouseout = function(){
+ setAttr("fill_3","stroke-width","1")
+ setAttr("fill_3","opacity","1.0")
+ };
+ obj = document.getElementById("fill_5");
+ obj.onmouseover = function(ev){
+ setAttr("fill_5","stroke-width","6")
+ setAttr("fill_5","opacity","0.8")
+ };
+ obj.onmouseout = function(){
+ setAttr("fill_5","stroke-width","1")
+ setAttr("fill_5","opacity","1.0")
+ };
+ obj = document.getElementById("empty_3");
+ obj.onmouseover = function(ev){
+ setAttr("empty_3","stroke-width","6")
+ setAttr("empty_3","opacity","0.8")
+ };
+ obj.onmouseout = function(){
+ setAttr("empty_3","stroke-width","1")
+ setAttr("empty_3","opacity","1.0")
+ };
+ obj = document.getElementById("empty_5");
+ obj.onmouseover = function(ev){
+ setAttr("empty_5","stroke-width","6")
+ setAttr("empty_5","opacity","0.8")
+ };
+ obj.onmouseout = function(){
+ setAttr("empty_5","stroke-width","1")
+ setAttr("empty_5","opacity","1.0")
+ };
+ obj = document.getElementById("transfer");
+ obj.onmouseover = function(ev){
+ setAttr("transfer","stroke-width","6")
+ setAttr("transfer","opacity","0.8")
+ };
+ obj.onmouseout = function(){
+ setAttr("transfer","stroke-width","1")
+ setAttr("transfer","opacity","1.0")
+ };
+ }
+ </script>
+ </head>
+<body>
+
+
+ <button type="button" class="collapsible collapsible-style">SVG Visualisation</button>
+ <div text-align="left">
+<!--svg for Jars by Jonas Erdmann-->
+<svg width="360" height="360"
+ xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<g id="jar_3" transform="rotate(180 25 100)">
+ <svg id ="jar_3_svg" width="50" height="60" X="0" y="00">
+ <g id="leer_3" opacity="1">
+ <rect id="jar_3_empty" x="0" y="0" width="50" height="60" style="fill:#DDEEFF"/>
+ <rect id="jar_3_full" x="0" y="0" width="50" height="60" style="fill:#267CEB"/>
+ <line id="left_3" x1="50" y1="0" x2="50" y2="60" style="stroke:#000000;stroke-width:4"/>
+ <line id="right_3" x1="0" y1="0" x2="0" y2="60" style="stroke:#000000;stroke-width:4"/>
+ <line x1="50" y1="0" x2="0" y2="0" style="stroke:#000000;stroke-width:4"/>
+ </svg>
+</g>
+<text id="jar_3_text" opacity="1" x="20" y="95">0</text>
+
+<g id="jar_5" transform="rotate(180 130 100)">
+ <svg id="jar_5_svg" width="50" height="100" x="105" y="0">
+ <g id="leer_5" opacity="1" >
+ <rect id="jar_5_empty" x="0" y="0" width="50" height="100" style="fill:#DDEEFF"/>
+ <rect id ="jar_5_full" x="0" y="0" width="50" height="100" style="fill:#267CEB"/>
+ <line id="left_5" x1="50" y1="0" x2="50" y2="100" style="stroke:#000000;stroke-width:4"/>
+ <line id="right_5" x1="0" y1="0" x2="0" y2="100" style="stroke:#000000;stroke-width:4"/>
+ <line x1="50" y1="0" x2="0" y2="0" style="stroke:#000000;stroke-width:4"/>
+ </svg>
+</g>
+<text id="jar_5_text" opacity="1" x="125" y="95">0</text>
+<line id="goal" x1="107" y1="120" x2="153" y2="120" stroke-width="2" stroke="#FF7777"/>
+
+<circle id="fill_3" cx="25" cy="25" r="15" fill="#BBBBBB"/>
+<rect id="fill_3_sym" x="20" y="20" width="10" height="12" style="fill:#267CEB"/>
+<circle id="fill_5" cx="130" cy="25" r="15" fill="#BBBBBB"/>
+<rect id="fill_5_sym" x="125" y="20" width="10" height="12" style="fill:#267CEB"/>
+<circle id="empty_3" cx="25" cy="65" r="15" fill="#BBBBBB"/>
+<rect id="empty_3_sym" x="20" y="60" width="10" height="12" style="fill:#DDEEFF"/>
+<circle id="empty_5" cx="130" cy="65" r="15" fill="#BBBBBB"/>
+<rect id="empty_5_sym" x="125" y="60" width="10" height="12" style="fill:#DDEEFF"/>
+<circle id="transfer" cx="77.5" cy="45" r="15" fill="#BBBBBB"/>
+<polyline id="transfer_left" points="70,45 76,41 76,49" fill="#00000"/>
+<polyline id="transfer_right" points="85,45 79,41 79,49" fill="#00000"/>
+<rect id="transfer_sym3" x="76" y="43.5" height="3" width="3"/>
+<text id="goal_achieved" opacity="0" x="160" y="125" fill="#FF4444" font-weight="bold">Goal achieved!</text>
+ </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><text id="visb_debug_messages" class="visb-messages"> </text>
+ </div>
+ <progress id="trace_meter" min="0" max="7" value="0"></progress>
+ <button type="button" class="collapsible collapsible-style">Variables (2/2)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="var_rowbig"> <td>1</td> <td>big</td> <td id="bVar_big">?</td></tr>
+
+ <tr id="var_rowsmall"> <td>2</td> <td>small</td> <td id="bVar_small">?</td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Trace (length=7)</button>
+<div class="coll-content-vis">
+ <table> <tr> <th>Nr</th> <th>Event</th> <th>Target State ID</th> </tr>
+
+ <tr id="row1" onclick="visualise0(1)"><td>1</td><td style="cursor:pointer">INITIALISATION(big=0,small=0)</td><td><button onclick="visualise0(1);">State 0</button></td></tr>
+
+ <tr id="row2" onclick="visualise2(2)"><td>2</td><td style="cursor:pointer">fill_big</td><td><button onclick="visualise2(2);">State 2</button></td></tr>
+
+ <tr id="row3" onclick="visualise7(3)"><td>3</td><td style="cursor:pointer">transfer_big_to_small(3)</td><td><button onclick="visualise7(3);">State 7</button></td></tr>
+
+ <tr id="row4" onclick="visualise8(4)"><td>4</td><td style="cursor:pointer">empty_small</td><td><button onclick="visualise8(4);">State 8</button></td></tr>
+
+ <tr id="row5" onclick="visualise9(5)"><td>5</td><td style="cursor:pointer">transfer_big_to_small(2)</td><td><button onclick="visualise9(5);">State 9</button></td></tr>
+
+ <tr id="row6" onclick="visualise10(6)"><td>6</td><td style="cursor:pointer">fill_big</td><td><button onclick="visualise10(6);">State 10</button></td></tr>
+
+ <tr id="row7" onclick="visualise11(7)"><td>7</td><td style="cursor:pointer">transfer_big_to_small(1)</td><td><button onclick="visualise11(7);">State 11</button></td></tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis visb-messages">
+Generated on 18/10/2023 at 9:55 using ProB version 1.12.3-nightly
+<br>Main specification package: event_b_project
+<br>Main specification name: DieHard
+<br>Main VisB JSON file: DieHard.json (modified on 18/10/2023 at 9:54)
+<br>VisB SVG file: Jars.svg (modified on 8/2/2022 at 15:17)
+ <script> visualise11(7); </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/Jars/DieHard.json b/Jars/DieHard.json
new file mode 100644
index 0000000..721e183
--- /dev/null
+++ b/Jars/DieHard.json
@@ -0,0 +1,172 @@
+{
+ "svg":"Jars.svg",
+ "comment": "VisB Visualization for Jars by Jonas Erdmann",
+ "definitions":[
+ {"name":"level",
+ "value": "{3|->small, 5|->big}",
+ "comment":"simulating the level variable from the classical B model"
+ },
+ {"name":"maxf",
+ "value": "{3|->3, 5|->5}",
+ "comment":"simulating the level variable from the classical B model"
+ }
+ ],
+ "items": [
+ {
+ "id": "jar_%0_full",
+ "attr": "height",
+ "value": "level(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_text",
+ "attr": "text",
+ "value": "level(%0)",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_svg",
+ "attr": "height",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_svg",
+ "attr": "y",
+ "value": "0 -(max({maxf(3), maxf(5)}) * 20 - 100)",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "jar_%0_empty",
+ "attr": "height",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "left_%0",
+ "attr": "y2",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "right_%0",
+ "attr": "y2",
+ "value": "maxf(%0) * 20",
+ "repeat": [
+ ["3"], ["5"]
+ ]
+ },
+ {
+ "id": "goal_achieved",
+ "attr": "opacity",
+ "value": "IF max({level(3), level(5)}) = max({maxf(3), maxf(5)}) -1 THEN 1 ELSE 0 END"
+ },
+ {
+ "id": "transfer_left",
+ "attr": "opacity",
+ "value": "IF level(3) = maxf(3) THEN 0 ELSE IF level(5) = 0 THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "transfer_right",
+ "attr": "opacity",
+ "value": "IF level(5) = maxf(5) THEN 0 ELSE IF level(3) = 0 THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "transfer_sym3",
+ "attr": "opacity",
+ "value": "IF level(3) = 0 & level(5) = 0 THEN 0 ELSE IF level(3) = maxf(3) & level(5) = maxf(5) THEN 0 ELSE 1 END END"
+ },
+ {
+ "id": "goal",
+ "attr": "x1",
+ "value": "IF maxf(3) > maxf(5) THEN 2 ELSE 107 END"
+ },
+ {
+ "id": "goal",
+ "attr": "x2",
+ "value": "IF maxf(3) > maxf(5) THEN 48 ELSE 153 END"
+ }
+
+],
+ "events": [
+ {
+ "id": "fill_3",
+ "event": "fill_small",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "fill_5",
+ "event": "fill_big",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "fill_3_sym",
+ "event": "fill_small"
+ },
+ {
+ "id": "fill_5_sym",
+ "event": "fill_big"
+ },
+ {
+ "id": "empty_3",
+ "event": "empty_small",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "empty_5",
+ "event": "empty_big",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "empty_3_sym",
+ "event": "empty_small"
+ },
+ {
+ "id": "empty_5_sym",
+ "event": "empty_big"
+ },
+ {
+ "id": "transfer",
+ "event": "transfer_big_to_small",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ },
+ {
+ "id": "transfer",
+ "event": "transfer_small_to_big"
+ },
+ {
+ "id": "transfer_left",
+ "event": "transfer_big_to_small"
+ },
+ {
+ "id": "transfer_right",
+ "event": "transfer_small_to_big"
+ },
+ {
+ "id": "transfer_sym3",
+ "event": "transfer_big_to_small"
+ },
+ {
+ "id": "transfer_sym3",
+ "event": "transfer_small_to_big"
+ }
+ ]
+}
+
diff --git a/Jars/DieHard_mch.eventb b/Jars/DieHard_mch.eventb
new file mode 100644
index 0000000..4dca5ab
--- /dev/null
+++ b/Jars/DieHard_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,'DieHard',[sees(none,[]),variables(none,[identifier(none,small),identifier(none,big)]),invariant(none,[conjunct(rodinpos('DieHard',typeok,'_eixRoP95EeeWE5wFp1eW8Q'),[member(none,identifier(none,big),interval(none,integer(none,0),integer(none,5))),member(none,identifier(none,small),interval(none,integer(none,0),integer(none,3)))]),negation(rodinpos('DieHard',goal,'_2KU8UP96EeeWE5wFp1eW8Q'),equal(none,identifier(none,big),integer(none,4)))]),theorems(none,[]),events(none,[event(rodinpos('DieHard','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('DieHard',init,'_g5-ZkP95EeeWE5wFp1eW8Q'),[identifier(none,big),identifier(none,small)],[integer(none,0),integer(none,0)])],[]),event(rodinpos('DieHard',fill_small,'_rnly0P95EeeWE5wFp1eW8Q'),fill_small,ordinary(none),[],[],[less(rodinpos('DieHard',g,'_rnly0f95EeeWE5wFp1eW8Q'),identifier(none,small),integer(none,3))],[],[assign(rodinpos('DieHard',act,'_rnly0v95EeeWE5wFp1eW8Q'),[identifier(none,small)],[integer(none,3)])],[]),event(rodinpos('DieHard',fill_big,'_ttg9gP95EeeWE5wFp1eW8Q'),fill_big,ordinary(none),[],[],[less(rodinpos('DieHard',g,'_tthkkP95EeeWE5wFp1eW8Q'),identifier(none,big),integer(none,5))],[],[assign(rodinpos('DieHard',act,'_tthkkf95EeeWE5wFp1eW8Q'),[identifier(none,big)],[integer(none,5)])],[]),event(rodinpos('DieHard',empty_small,'_xRYs4P95EeeWE5wFp1eW8Q'),empty_small,ordinary(none),[],[],[greater(rodinpos('DieHard',g,'_xRZT8P95EeeWE5wFp1eW8Q'),identifier(none,small),integer(none,0))],[],[assign(rodinpos('DieHard',act,'_xRZT8f95EeeWE5wFp1eW8Q'),[identifier(none,small)],[integer(none,0)])],[]),event(rodinpos('DieHard',empty_big,'_xRZT8v95EeeWE5wFp1eW8Q'),empty_big,ordinary(none),[],[],[greater(rodinpos('DieHard',g,'_xRZT8_95EeeWE5wFp1eW8Q'),identifier(none,big),integer(none,0))],[],[assign(rodinpos('DieHard',act,'_xRZT9P95EeeWE5wFp1eW8Q'),[identifier(none,big)],[integer(none,0)])],[]),event(rodinpos('DieHard',transfer_big_to_small,'_KG_UgP96EeeWE5wFp1eW8Q'),transfer_big_to_small,ordinary(none),[],[identifier(rodinpos('DieHard',[],'_KG_Ugf96EeeWE5wFp1eW8Q'),amount)],[greater(rodinpos('DieHard',g,'_KG_Ugv96EeeWE5wFp1eW8Q'),identifier(none,amount),integer(none,0)),equal(rodinpos('DieHard',g2,'_KG_Ug_96EeeWE5wFp1eW8Q'),identifier(none,amount),min(none,set_extension(none,[minus(none,integer(none,3),identifier(none,small)),identifier(none,big)]))),less_equal(rodinpos('DieHard',g3,'_KG_UhP96EeeWE5wFp1eW8Q'),identifier(none,amount),identifier(none,big))],[],[assign(rodinpos('DieHard',act,'_KG_Uhf96EeeWE5wFp1eW8Q'),[identifier(none,big),identifier(none,small)],[minus(none,identifier(none,big),identifier(none,amount)),add(none,identifier(none,small),identifier(none,amount))])],[]),event(rodinpos('DieHard',transfer_small_to_big,'_yQlqoP96EeeWE5wFp1eW8Q'),transfer_small_to_big,ordinary(none),[],[identifier(rodinpos('DieHard',[],'_yQlqof96EeeWE5wFp1eW8Q'),amount)],[greater(rodinpos('DieHard',g,'_yQlqov96EeeWE5wFp1eW8Q'),identifier(none,amount),integer(none,0)),equal(rodinpos('DieHard',g2,'_yQlqo_96EeeWE5wFp1eW8Q'),identifier(none,amount),min(none,set_extension(none,[minus(none,integer(none,5),identifier(none,big)),identifier(none,small)]))),less_equal(rodinpos('DieHard',g3,'_yQlqpP96EeeWE5wFp1eW8Q'),identifier(none,amount),identifier(none,small))],[],[assign(rodinpos('DieHard',act,'_yQlqpf96EeeWE5wFp1eW8Q'),[identifier(none,big),identifier(none,small)],[add(none,identifier(none,big),identifier(none,amount)),minus(none,identifier(none,small),identifier(none,amount))])],[])])])],[],[exporter_version(3),po('DieHard','Invariant establishment',[event('INITIALISATION'),invariant(typeok)],true),po('DieHard','Invariant establishment',[event('INITIALISATION'),invariant(goal)],true),po('DieHard','Invariant preservation',[event(fill_small),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(fill_big),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(fill_big),invariant(goal)],true),po('DieHard','Invariant preservation',[event(empty_small),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(empty_big),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(empty_big),invariant(goal)],true),po('DieHard','Well-definedness of Guard',[guard(g2),event(transfer_big_to_small)],true),po('DieHard','Invariant preservation',[event(transfer_big_to_small),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(transfer_big_to_small),invariant(goal)],false),po('DieHard','Well-definedness of Guard',[guard(g2),event(transfer_small_to_big)],true),po('DieHard','Invariant preservation',[event(transfer_small_to_big),invariant(typeok)],true),po('DieHard','Invariant preservation',[event(transfer_small_to_big),invariant(goal)],false)],_Error)).
+
--
GitLab