From d8d19306bcaf47b18f53a54aa0ed75aa733b3e00 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 25 Nov 2020 15:34:04 +0100
Subject: [PATCH] =?UTF-8?q?add=20first=20version=20of=20Abrial=E2=80=99s?=
=?UTF-8?q?=20bridge=20model?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
Bridge/bridge_island_visualization.svg | 50 +++++++++++++++++++++
Bridge/m0_island_bridge_3cars_mch.eventb | 2 +
Bridge/m1_bridge_mch.eventb | 2 +
Bridge/visb_m0.json | 55 ++++++++++++++++++++++++
Bridge/visb_m1.json | 55 ++++++++++++++++++++++++
5 files changed, 164 insertions(+)
create mode 100644 Bridge/bridge_island_visualization.svg
create mode 100644 Bridge/m0_island_bridge_3cars_mch.eventb
create mode 100644 Bridge/m1_bridge_mch.eventb
create mode 100644 Bridge/visb_m0.json
create mode 100644 Bridge/visb_m1.json
diff --git a/Bridge/bridge_island_visualization.svg b/Bridge/bridge_island_visualization.svg
new file mode 100644
index 0000000..4147b84
--- /dev/null
+++ b/Bridge/bridge_island_visualization.svg
@@ -0,0 +1,50 @@
+<svg width="765.0000000000001" height="555" xmlns="http://www.w3.org/2000/svg" id="carsonbridge" xmlns:xlink="http://www.w3.org/1999/xlink">
+ <metadata id="metadata3426">image/svg+xml</metadata>
+ <defs>
+ <linearGradient id="linearGradient5682">
+ <stop offset="0" id="stop5684" stop-color="#4887d0"/>
+ <stop offset="1" id="stop5686" stop-opacity="0" stop-color="#4887d0"/>
+ </linearGradient>
+ <linearGradient xlink:href="#linearGradient5682" id="linearGradient5688" x1="-0.00079" y1="0.5" x2="1.00079" y2="0.5"/>
+ </defs>
+ <g id="g3402">
+ <title>background</title>
+ <rect id="canvas_background" x="-1" y="-1" fill="none" width="767" height="557"/>
+ </g>
+ <g>
+ <title>Layer 3</title>
+ <rect id="rect3428" width="630.12891" height="590.09137" x="-3.69577" y="-15.67732" stroke-width="1px" stroke="#2397c0" fill-rule="evenodd" fill="url(#linearGradient5688)"/>
+ </g>
+ <g id="g3411">
+ <title>Layer 2</title>
+ <rect stroke-dasharray="2,2" fill="#fff" stroke="#000" stroke-width="1.5" x="311.5" y="202.5" width="279" height="68" id="bridge"/>
+
+ <ellipse stroke="#000" fill="#e2ffc6" stroke-width="1.5" cx="682.50001" cy="274.00002" id="ML" rx="166.00001" ry="326.49999"/>
+
+ <ellipse fill="#fffcd3" stroke-width="1.5" cx="183.5" cy="235.50001" id="IL" rx="164.00001" ry="146.00001" stroke="#000"/>
+
+ <text xml:space="preserve" text-anchor="left" font-family="Helvetica, Arial, sans-serif" font-size="24" id="value_n" y="39.5" x="27" fill-opacity="null" stroke-opacity="null" stroke-dasharray="2,2" stroke-width="0" stroke="#000" fill="#000000">
+ <tspan id="nr_cars_on_island_and_bridge">%n</tspan></text>
+
+ <text xml:space="preserve" text-anchor="left" font-family="Helvetica, Arial, sans-serif" font-size="24" id="value_b" y="237.5" x="40" fill-opacity="null" stroke-opacity="null" stroke-dasharray="2,2" stroke-width="0" stroke="#000" fill="#000000">
+ <tspan id="nr_cars_on_island">%b</tspan>
+ </text>
+
+ <text xml:space="preserve" text-anchor="left" font-family="Helvetica, Arial, sans-serif" font-size="24" id="value_a" y="181.5" x="471" fill-opacity="null" stroke-opacity="null" stroke-dasharray="2,2" stroke-width="0" stroke="#000" fill="#000000"><tspan id="nr_cars_on_bridge_a">%a</tspan>
+ </text>
+
+ <text xml:space="preserve" text-anchor="left" font-family="Helvetica, Arial, sans-serif" font-size="24" id="value_c" y="304.5" x="356" fill-opacity="null" stroke-opacity="null" stroke-dasharray="2,2" stroke-width="0" stroke="#000" fill="#000000"><tspan id="nr_cars_on_bridge_c">%c</tspan></text>
+
+ <ellipse id="ml_tl" ry="14.5" rx="14.5" cy="139.5" cx="490" stroke-width="1.5" stroke="#000" fill="#fff"/>
+
+ <ellipse id="il_tl" ry="14.5" rx="14.5" cy="329.5" cx="371" stroke-width="1.5" stroke="#000" fill="#fff"/>
+
+ <rect id="il_in_sr" height="10" width="28.66667" y="210.66667" x="323.33333" stroke-opacity="null" stroke-width="0" stroke="#000" fill="#DDDDDD"/>
+
+ <rect id="il_out_sr" height="10" width="28.66667" y="244" x="341.33333" stroke-opacity="null" stroke-width="0" stroke="#000" fill="#DDDDDD"/>
+
+ <rect id="ml_in_sr" height="10" width="28.66667" y="244" x="511.66667" stroke-opacity="null" stroke-width="0" stroke="#000" fill="#DDDDDD"/>
+
+ <rect id="ml_out_sr" height="10" width="28.66667" y="210.66667" x="497.00001" stroke-opacity="null" stroke-width="0" stroke="#000" fill="#dddddd"/>
+ </g>
+</svg>
\ No newline at end of file
diff --git a/Bridge/m0_island_bridge_3cars_mch.eventb b/Bridge/m0_island_bridge_3cars_mch.eventb
new file mode 100644
index 0000000..91dc06f
--- /dev/null
+++ b/Bridge/m0_island_bridge_3cars_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,m0_island_bridge_3cars,[sees(none,[context0,context0_3cars]),refines(none,m0_island_bridge),variables(none,[identifier(none,n)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos(m0_island_bridge_3cars,'INITIALISATION',internal_sees2),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m0_island_bridge_3cars,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge_3cars,'ML_out',internal_sees3),'ML_out',ordinary(none),['ML_out'],[],[less(rodinpos(m0_island_bridge_3cars,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge_3cars,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge_3cars,'ML_in',internal_sees4),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m0_island_bridge_3cars,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge_3cars,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])]),event_b_model(none,m0_island_bridge,[sees(none,[context0]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(m0_island_bridge,inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(m0_island_bridge,inv2,internal_inv3I),identifier(none,n),identifier(none,d)),disjunct(rodinpos(m0_island_bridge,'DLF','_MLohYJHeEeWRGJ9JkSwucQ'),less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0)))]),theorems(none,[]),events(none,[event(rodinpos(m0_island_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),[],[],[less(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,context0,[extends(none,[]),constants(none,[identifier(none,d),identifier(none,green),identifier(none,red)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(context0,axm1,internal_axm1A),identifier(none,d),natural_set(none)),equal(rodinpos(context0,axm2,internal_axm2A),identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(context0,axm3,internal_axm3A),identifier(none,green),identifier(none,red))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT')])]),event_b_context(none,context0_3cars,[extends(none,[context0]),constants(none,[]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(context0_3cars,probn,'_5zHScLLNEeW75IcRipcYDg'),identifier(none,d),integer(none,3))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(m0_island_bridge,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(m0_island_bridge,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(m0_island_bridge,'Invariant establishment',[event('INITIALISATION'),invariant('DLF')],false),po(m0_island_bridge,'Invariant preservation',[event('ML_out'),invariant(inv1)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_out'),invariant(inv2)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_out'),invariant('DLF')],true),po(m0_island_bridge,'Invariant preservation',[event('ML_in'),invariant(inv1)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_in'),invariant(inv2)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_in'),invariant('DLF')],true)],_Error)).
+
diff --git a/Bridge/m1_bridge_mch.eventb b/Bridge/m1_bridge_mch.eventb
new file mode 100644
index 0000000..2f7f7b9
--- /dev/null
+++ b/Bridge/m1_bridge_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,m1_bridge,[sees(none,[context0]),refines(none,m0_island_bridge),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),invariant(none,[member(rodinpos(m1_bridge,inv1,internal_inv1I),identifier(none,a),natural_set(none)),member(rodinpos(m1_bridge,inv2,internal_inv2I),identifier(none,b),natural_set(none)),member(rodinpos(m1_bridge,inv3,internal_inv3I),identifier(none,c),natural_set(none)),equal(rodinpos(m1_bridge,inv4,internal_inv4I),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,n)),disjunct(rodinpos(m1_bridge,inv5,internal_inv5I),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,c),integer(none,0)))]),theorems(none,[]),variant(none,add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b))),events(none,[event(rodinpos(m1_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a),identifier(none,b),identifier(none,c)],[integer(none,0),integer(none,0),integer(none,0)])],[]),event(rodinpos(m1_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),['ML_out'],[],[less(rodinpos(m1_bridge,grd1,internal_grd1),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d)),equal(rodinpos(m1_bridge,grd2,internal_grd2),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[]),event(rodinpos(m1_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_in',internal_evt4),'IL_in',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m1_bridge,act2,'_QsLTsFBaEeOH8cnegPmrEg'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_out',internal_evt5),'IL_out',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,b),integer(none,0)),equal(rodinpos(m1_bridge,grd2,internal_grd2),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m1_bridge,act2,internal_act3),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[])])]),event_b_model(none,m0_island_bridge,[sees(none,[context0]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(m0_island_bridge,inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(m0_island_bridge,inv2,internal_inv3I),identifier(none,n),identifier(none,d))]),theorems(none,[]),events(none,[event(rodinpos(m0_island_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),[],[],[less(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,context0,[extends(none,[]),constants(none,[identifier(none,d),identifier(none,green),identifier(none,red)]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos(context0,axm1,internal_axm1A),member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))),equal(rodinpos(context0,axm2,internal_axm2A),identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(context0,axm3,internal_axm3A),identifier(none,green),identifier(none,red))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT')])])],[exporter_version(3),po(m1_bridge,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(m1_bridge,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(m1_bridge,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(m1_bridge,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(m1_bridge,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m1_bridge,'Invariant preservation',[event('ML_out'),event('ML_out'),invariant(inv1)],true),po(m1_bridge,'Invariant preservation',[event('ML_out'),event('ML_out'),invariant(inv4)],true),po(m1_bridge,'Invariant preservation',[event('ML_out'),event('ML_out'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out')],true),po(m1_bridge,'Invariant preservation',[event('ML_in'),event('ML_in'),invariant(inv3)],true),po(m1_bridge,'Invariant preservation',[event('ML_in'),event('ML_in'),invariant(inv4)],true),po(m1_bridge,'Invariant preservation',[event('ML_in'),event('ML_in'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_in'),guard(grd1),event('ML_in'),event('ML_in')],true),po(m1_bridge,'Invariant preservation',[event('IL_in'),invariant(inv1)],true),po(m1_bridge,'Invariant preservation',[event('IL_in'),invariant(inv2)],true),po(m1_bridge,'Invariant preservation',[event('IL_in'),invariant(inv4)],true),po(m1_bridge,'Invariant preservation',[event('IL_in'),invariant(inv5)],true),po(m1_bridge,'Variant of event',[variant(m1_bridge),event('IL_in')],true),po(m1_bridge,'Natural number variant of event',[variant(m1_bridge),event('IL_in')],true),po(m1_bridge,'Invariant preservation',[event('IL_out'),invariant(inv2)],true),po(m1_bridge,'Invariant preservation',[event('IL_out'),invariant(inv3)],true),po(m1_bridge,'Invariant preservation',[event('IL_out'),invariant(inv4)],true),po(m1_bridge,'Invariant preservation',[event('IL_out'),invariant(inv5)],true),po(m1_bridge,'Variant of event',[variant(m1_bridge),event('IL_out')],true),po(m1_bridge,'Natural number variant of event',[variant(m1_bridge),event('IL_out')],true)],_Error)).
+
diff --git a/Bridge/visb_m0.json b/Bridge/visb_m0.json
new file mode 100644
index 0000000..d7e3dca
--- /dev/null
+++ b/Bridge/visb_m0.json
@@ -0,0 +1,55 @@
+{
+ "svg": "bridge_island_visualization.svg",
+ "items": [
+ {
+ "id": "nr_cars_on_island",
+ "attr": "text",
+ "value": "\"-\""
+ },
+ {
+ "id": "nr_cars_on_bridge_a",
+ "attr": "text",
+ "value": "\"-\""
+ },
+ {
+ "id": "nr_cars_on_bridge_c",
+ "attr": "text",
+ "value": "\"-\""
+ },
+ {
+ "id": "nr_cars_on_island_and_bridge",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"~w/~w\",[n,d])"
+ },
+ {
+ "id": "IL",
+ "attr": "stroke-width",
+ "value": "1+(10*n)/d",
+ "not-working-yet-value": "1.0 + 2.0*real(n)/real(d)"
+ },
+ {
+ "id": "ml_tl",
+ "attr": "fill",
+ "value": "IF ENABLED(\"ML_out\")=TRUE THEN \"green\" ELSE \"red\" END"
+ },
+ {
+ "id": "il_tl",
+ "attr": "fill",
+ "value": "IF ENABLED(\"ML_in\")=TRUE THEN \"green\" ELSE \"red\" END"
+ }
+ ],
+ "events": [
+ {
+ "id": "IL",
+ "event": "ML_out",
+ "hovers": [{ "id": "ml_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ },
+ {
+ "id": "ML",
+ "event": "ML_in",
+ "hovers": [{ "id": "il_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ }
+ ]
+}
diff --git a/Bridge/visb_m1.json b/Bridge/visb_m1.json
new file mode 100644
index 0000000..37d159f
--- /dev/null
+++ b/Bridge/visb_m1.json
@@ -0,0 +1,55 @@
+{
+ "svg": "bridge_island_visualization.svg",
+ "items": [
+ {
+ "id": "nr_cars_on_island",
+ "attr": "text",
+ "value": "b"
+ },
+ {
+ "id": "nr_cars_on_bridge_a",
+ "attr": "text",
+ "value": "a"
+ },
+ {
+ "id": "nr_cars_on_bridge_c",
+ "attr": "text",
+ "value": "c"
+ },
+ {
+ "id": "nr_cars_on_island_and_bridge",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"~w/~w\",[n,d])"
+ },
+ {
+ "id": "IL",
+ "attr": "stroke-width",
+ "value": "1+(10*b)/d",
+ "not-working-yet-value": "1.0 + 2.0*real(b)/real(d)"
+ },
+ {
+ "id": "ml_tl",
+ "attr": "fill",
+ "value": "IF ENABLED(\"ML_out\")=TRUE THEN \"green\" ELSE \"red\" END"
+ },
+ {
+ "id": "il_tl",
+ "attr": "fill",
+ "value": "IF ENABLED(\"IL_out\")=TRUE THEN \"green\" ELSE \"red\" END"
+ }
+ ],
+ "events": [
+ {
+ "id": "IL",
+ "event": "ML_out",
+ "hovers": [{ "id": "ml_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ },
+ {
+ "id": "ML",
+ "event": "ML_in",
+ "hovers": [{ "id": "il_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ }
+ ]
+}
--
GitLab