diff --git a/Bridge/bridge_island_visualization.svg b/Bridge/bridge_island_visualization.svg
index 831a36a1ef2aefa6a4323c2e94c136ef604cff89..ee3cd9f4d4fdece765b2e984deb0c2647ce9ae08 100644
--- a/Bridge/bridge_island_visualization.svg
+++ b/Bridge/bridge_island_visualization.svg
@@ -17,7 +17,7 @@
</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"/>
+ <rect id="bridge" 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"/>
diff --git a/Bridge/m1_different_refinemeht.eventb b/Bridge/m1_different_refinemeht.eventb
new file mode 100644
index 0000000000000000000000000000000000000000..c00b707d81e100537d3376d30d017ab9821023de
--- /dev/null
+++ b/Bridge/m1_different_refinemeht.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,m1_different_refinement,[sees(none,[cd]),refines(none,m0),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),invariant(none,[member(rodinpos(m1_different_refinement,inv1,'_hLHFAJqHEe-t5cJ-lqEKKA'),identifier(none,a),natural_set(none)),member(rodinpos(m1_different_refinement,inv2,'_hLHFAZqHEe-t5cJ-lqEKKA'),identifier(none,b),natural_set(none)),member(rodinpos(m1_different_refinement,inv3,'_hLHFApqHEe-t5cJ-lqEKKA'),identifier(none,c),natural_set(none)),description(rodinpos(m1_different_refinement,inv4_changed,'_hLHFA5qHEe-t5cJ-lqEKKA'),'Gluing invariant connecting the concrete variables\n instead of settting sum(a, b, c) to the abstract one (n)\n we set b to n ',equal(none,identifier(none,n),identifier(none,b))),description(rodinpos(m1_different_refinement,inv5,'_hLHFBJqHEe-t5cJ-lqEKKA'),'The bridge is one\21022\way',disjunct(none,equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,c),integer(none,0)))),description(rodinpos(m1_different_refinement,inv6,'__GX-4JqHEe-t5cJ-lqEKKA'),'new invariant',less_equal(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)))]),theorems(none,[member(rodinpos(m1_different_refinement,thm1,'_hLHFBZqHEe-t5cJ-lqEKKA'),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),natural_set(none))]),variant(none,add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b))),events(none,[event(rodinpos(m1_different_refinement,'INITIALISATION',internal_element2),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m1_different_refinement,act2,'_hLEBsJqHEe-t5cJ-lqEKKA'),[identifier(none,a)],[integer(none,0)]),assign(rodinpos(m1_different_refinement,act3,'_hLEBsZqHEe-t5cJ-lqEKKA'),[identifier(none,b)],[integer(none,0)]),assign(rodinpos(m1_different_refinement,act4,'_hLEBspqHEe-t5cJ-lqEKKA'),[identifier(none,c)],[integer(none,0)])],[]),description_event(none,'leaving mainland',event(rodinpos(m1_different_refinement,'ML_out1','__GWwwJqHEe-t5cJ-lqEKKA'),'ML_out1',ordinary(none),[],[],[less(rodinpos(m1_different_refinement,grd1,'_hLEowJqHEe-t5cJ-lqEKKA'),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(m1_different_refinement,grd2,'_hLEowZqHEe-t5cJ-lqEKKA'),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_different_refinement,act1,'_hLEowpqHEe-t5cJ-lqEKKA'),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[])),description_event(none,'entering island',event(rodinpos(m1_different_refinement,'IL_in','_hLFP0JqHEe-t5cJ-lqEKKA'),'IL_in',ordinary(none),['ML_out'],[],[greater(rodinpos(m1_different_refinement,grd1,'_hLFP0ZqHEe-t5cJ-lqEKKA'),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_different_refinement,act1,'_hLFP0pqHEe-t5cJ-lqEKKA'),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m1_different_refinement,act2,'_hLFP05qHEe-t5cJ-lqEKKA'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[])),description_event(none,'leaving island',event(rodinpos(m1_different_refinement,'IL_out','_hLFP1JqHEe-t5cJ-lqEKKA'),'IL_out',ordinary(none),['ML_in'],[],[less(rodinpos(m1_different_refinement,grd1,'_hLF24JqHEe-t5cJ-lqEKKA'),integer(none,0),identifier(none,b)),equal(rodinpos(m1_different_refinement,grd2,'_hLF24ZqHEe-t5cJ-lqEKKA'),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_different_refinement,act1,'_hLF24pqHEe-t5cJ-lqEKKA'),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m1_different_refinement,act2,'_hLF245qHEe-t5cJ-lqEKKA'),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[])),description_event(none,'entering mainland',event(rodinpos(m1_different_refinement,'ML_in1','__GX-4ZqHEe-t5cJ-lqEKKA'),'ML_in1',ordinary(none),[],[],[greater(rodinpos(m1_different_refinement,grd1,'_hLGd8JqHEe-t5cJ-lqEKKA'),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_different_refinement,act2,'_hLGd8ZqHEe-t5cJ-lqEKKA'),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]))])]),event_b_model(none,m0,[sees(none,[cd]),variables(none,[identifier(none,n)]),invariant(none,[description(rodinpos(m0,inv1,internal_inv1I),'number of cars',member(none,identifier(none,n),natural_set(none))),less_equal(rodinpos(m0,inv2,internal_inv2I),identifier(none,n),identifier(none,d))]),theorems(none,[disjunct(rodinpos(m0,thm1,internal_thm1T),greater(none,identifier(none,n),integer(none,0)),less(none,identifier(none,n),identifier(none,d)))]),events(none,[event(rodinpos(m0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),description_event(none,'Leaving the mainland',event(rodinpos(m0,'ML_out',internal_evt3),'ML_out',ordinary(none),[],[],[less(rodinpos(m0,grd1,internal_element1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[])),description_event(none,'Entering the mainland',event(rodinpos(m0,'ML_in',internal_evt4),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[]))])])],[event_b_context(none,cd,[extends(none,[]),constants(none,[identifier(none,d)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(cd,axm1,internal_axm1A),identifier(none,d),natural_set(none)),greater(rodinpos(cd,axm2,internal_axm2A),identifier(none,d),integer(none,0))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(m1_different_refinement,'Theorem',[invariant(thm1)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4_changed)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m1_different_refinement,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out1'),invariant(inv1)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out1'),invariant(inv5)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out1'),invariant(inv6)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out'),event('IL_in'),invariant(inv1)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out'),event('IL_in'),invariant(inv2)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out'),event('IL_in'),invariant(inv4_changed)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out'),event('IL_in'),invariant(inv5)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_out'),event('IL_in'),invariant(inv6)],true),po(m1_different_refinement,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('IL_in')],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in'),event('IL_out'),invariant(inv2)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in'),event('IL_out'),invariant(inv3)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in'),event('IL_out'),invariant(inv4_changed)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in'),event('IL_out'),invariant(inv5)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in'),event('IL_out'),invariant(inv6)],true),po(m1_different_refinement,'Guard strengthening (split)',[event('ML_in'),guard(grd1),event('ML_in'),event('IL_out')],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in1'),invariant(inv3)],true),po(m1_different_refinement,'Invariant preservation',[event('ML_in1'),invariant(inv5)],true),po(m0,'Theorem',[invariant(thm1)],true),po(m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(m0,'Invariant preservation',[event('ML_out'),invariant(inv1)],true),po(m0,'Invariant preservation',[event('ML_out'),invariant(inv2)],true),po(m0,'Invariant preservation',[event('ML_in'),invariant(inv1)],true),po(m0,'Invariant preservation',[event('ML_in'),invariant(inv2)],true)],_Error)).
+
diff --git a/Bridge/visb_m0.json b/Bridge/visb_m0.json
index d7e3dcae39006ed70be7fc6158af4d85b18e9b72..00c8da710550749ffce4794b5204b05f60d3717e 100644
--- a/Bridge/visb_m0.json
+++ b/Bridge/visb_m0.json
@@ -19,7 +19,7 @@
{
"id": "nr_cars_on_island_and_bridge",
"attr": "text",
- "value": "FORMAT_TO_STRING(\"~w/~w\",[n,d])"
+ "value": "FORMAT_TO_STRING(\"n/d=~w/~w\",[n,d])"
},
{
"id": "IL",
diff --git a/Bridge/visb_m1.json b/Bridge/visb_m1.json
index ddbddc7b752a38f0e42e95aa87573ae24ae39dec..b80e2dc6bafda86ea40dd1760ecdccdea0a0a820 100644
--- a/Bridge/visb_m1.json
+++ b/Bridge/visb_m1.json
@@ -19,7 +19,7 @@
{
"id": "nr_cars_on_island_and_bridge",
"attr": "text",
- "value": "FORMAT_TO_STRING(\"cars: ~w/~w\",[n,d])"
+ "value": "FORMAT_TO_STRING(\"cars: n/d=~w/~w\",[n,d])"
},
{
"id": "IL",
@@ -41,15 +41,23 @@
"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"}]
+ "event": "IL_in"
},
{
"id": "ML",
- "event": "ML_in",
- "hovers": [{ "id": "il_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ "event": "ML_in"
+ },
+ {
+ "id": "bridge",
+ "event": "IL_out",
+ "hovers": [{ "id": "ml_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"},
+ { "id": "il_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
{ "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ },
+ {
+ "id": "bridge",
+ "event": "ML_out"
}
]
}
diff --git a/Bridge/visb_m1_different.json b/Bridge/visb_m1_different.json
new file mode 100644
index 0000000000000000000000000000000000000000..ae67c330d96ea4108c3030d5b1fb47be05bf435e
--- /dev/null
+++ b/Bridge/visb_m1_different.json
@@ -0,0 +1,63 @@
+{
+ "svg": "bridge_island_visualization.svg",
+ "items": [
+ {
+ "id": "nr_cars_on_island",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"b=~w\",[b])"
+ },
+ {
+ "id": "nr_cars_on_bridge_a",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"a=~w\",[a])"
+ },
+ {
+ "id": "nr_cars_on_bridge_c",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"c=~w\",[c])"
+ },
+ {
+ "id": "nr_cars_on_island_and_bridge",
+ "attr": "text",
+ "value": "FORMAT_TO_STRING(\"cars: n/d=~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_out1\")=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": "IL_in"
+ },
+ {
+ "id": "ML",
+ "event": "ML_in1"
+ },
+ {
+ "id": "bridge",
+ "event": "ML_out1",
+ "hovers": [{ "id": "ml_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"},
+ { "id": "il_tl", "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+ },
+ {
+ "id": "bridge",
+ "event": "IL_out"
+ }
+ ]
+}