Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • master
1 result

Target

Select target project
  • general/stups/visb-visualisation-examples
1 result
Select Git revision
  • master
1 result
Show changes
Commits on Source (2)
Show whitespace changes
Inline Side-by-side
Bridge/bridge_island_visualization.svg
View file @ a273eb8f
......@@ -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"/>
......
Bridge/m1_different_refinemeht.eventb 0 → 100644
View file @ a273eb8f
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)).
Bridge/visb_m0.json
View file @ a273eb8f
......@@ -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",
......
Bridge/visb_m1.json
View file @ a273eb8f
......@@ -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"
}
]
}
Bridge/visb_m1_different.json 0 → 100644
View file @ a273eb8f
{
"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"
}
]
}
Reals/WaterTankReals.tla
View file @ a273eb8f
......@@ -29,7 +29,8 @@ maxw == high_threshold+inflow \* maximum capacity as shown
Invariant == level > 0.0 /\ level <= maxw
convy(lvl) == bot-lvl
VISB_SVG_BOX == [width |-> wid+4.0*lft, height |-> bot+lft]
VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level), height |-> level, width |-> wid,
VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level),
height |-> level, width |-> wid,
fill |-> "lightsteelblue"]
VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid,
fill |-> "none", stroke |-> "black", stroke_width|->1.0]
......@@ -44,6 +45,7 @@ VISB_SVG_OBJECTS4 == [svg_class |-> "rect", x|->lft, y |-> 2.0*lft, height |-> l
stroke |-> "black", stroke_width|->1.0]
VISB_SVG_OBJECTS5 == [svg_class |-> "text", x|->lft+5.0, y |-> 2.0*lft-8.0, text|->"Pump:", font_size|->8.0]
VISB_SVG_OBJECTS6 == [svg_class |-> "text", x|->lft+9.5, y |-> 2.0*lft+7.2, text|->IF pump THEN "on" ELSE "off", font_size|->8.0]
--------------------------------------------------------------
THEOREM WaterTank => []Init
==============================================================
\ No newline at end of file