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

add first version of Abrial’s bridge model

parent 265e3f10
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Bridge/bridge_island_visualization.svg 0 → 100644
+ 50
− 0
View file @ d8d19306
<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
Bridge/m0_island_bridge_3cars_mch.eventb 0 → 100644
+ 2
− 0
View file @ d8d19306
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)).
Bridge/m1_bridge_mch.eventb 0 → 100644
+ 2
− 0
View file @ d8d19306
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)).
Bridge/visb_m0.json 0 → 100644
+ 55
− 0
View file @ d8d19306
{
"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"}]
}
]
}
Bridge/visb_m1.json 0 → 100644
+ 55
− 0
View file @ d8d19306
{
"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"}]
}
]
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment