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)
......@@ -41,7 +41,12 @@
"repeat": ["tr1","tr2"],
"id":"train_info_text_%0",
"attr":"text",
"value":"\"Train %0 is at \" ^ TO_STRING(train_rear_end(%0)) ^ \"..\" ^ TO_STRING(train_front_end(%0)) ^ IF %0:dom(train_ma) THEN \" with MA until \" ^ TO_STRING(train_ma(%0)) ELSE \" and has no MA\" END",
"value":"\"Train %0 is at \" ^
TO_STRING(train_rear_end(%0)) ^ \"..\" ^
TO_STRING(train_front_end(%0)) ^
IF %0:dom(train_ma) THEN
\" with MA until \" ^ TO_STRING(train_ma(%0))
ELSE \" and has no MA\" END",
"comment":"adapt info field of train"
},
......
package(load_event_b_project([event_b_model(none,'TrainSimple12_corrected',[sees(none,[]),variables(none,[identifier(none,train2_front),identifier(none,train1_front),description(none,description_text(none,'movement authority limit'),identifier(none,train1_mal)),description(none,description_text(none,'movement authority limit'),identifier(none,train2_mal)),identifier(none,train1_back),identifier(none,train2_back)]),invariant(none,[member(rodinpos('TrainSimple12_corrected',inv1,'_Xcgjoc3KEe-0NqOoLhfLug'),interval(none,identifier(none,train1_back),identifier(none,train1_front)),pow1_subset(none,natural_set(none))),member(rodinpos('TrainSimple12_corrected',inv2,'_Xcgjos3KEe-0NqOoLhfLug'),interval(none,identifier(none,train2_back),identifier(none,train2_front)),pow1_subset(none,natural_set(none))),description(rodinpos('TrainSimple12_corrected',inv3,'_Xcgjo83KEe-0NqOoLhfLug'),description_text(none,'no collision'),equal(none,intersection(none,interval(none,identifier(none,train1_back),identifier(none,train1_front)),interval(none,identifier(none,train2_back),identifier(none,train2_front))),typeof(none,empty_set(none),pow_subset(none,integer_set(none))))),member(rodinpos('TrainSimple12_corrected',inv4,'_XcgjpM3KEe-0NqOoLhfLug'),identifier(none,train1_mal),natural_set(none)),member(rodinpos('TrainSimple12_corrected',inv5,'_Xcgjpc3KEe-0NqOoLhfLug'),identifier(none,train2_mal),natural_set(none)),description(rodinpos('TrainSimple12_corrected','inductive-inv1','_Xcgjps3KEe-0NqOoLhfLug'),description_text(none,'train1 respects MAL'),greater_equal(none,identifier(none,train1_mal),identifier(none,train1_front))),description(rodinpos('TrainSimple12_corrected','inductive-inv2','_Xcgjp83KEe-0NqOoLhfLug'),description_text(none,'MAL is safe'),less(none,identifier(none,train1_mal),identifier(none,train2_back)))]),theorems(none,[]),events(none,[event(rodinpos('TrainSimple12_corrected','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('TrainSimple12_corrected',ini1,'_XcfVgM3KEe-0NqOoLhfLug'),[identifier(none,train1_back),identifier(none,train1_front)],[integer(none,0),integer(none,2)]),assign(rodinpos('TrainSimple12_corrected',ini2,'_Xcf8kM3KEe-0NqOoLhfLug'),[identifier(none,train2_back),identifier(none,train2_front)],[integer(none,4),integer(none,6)]),assign(rodinpos('TrainSimple12_corrected',ini3,'_Xcf8kc3KEe-0NqOoLhfLug'),[identifier(none,train1_mal)],[integer(none,3)]),assign(rodinpos('TrainSimple12_corrected',ini4,'_Xcf8ks3KEe-0NqOoLhfLug'),[identifier(none,train2_mal)],[integer(none,20)])],[]),description_event(none,description_text(none,'train1 moves one unit forward'),event(rodinpos('TrainSimple12_corrected',move_train1,'_XchKsM3KEe-0NqOoLhfLug'),move_train1,ordinary(none),[],[],[less(rodinpos('TrainSimple12_corrected',grd,'_XchKsc3KEe-0NqOoLhfLug'),identifier(none,train1_front),identifier(none,train1_mal))],[],[assign(rodinpos('TrainSimple12_corrected',moveforward,'_XchKss3KEe-0NqOoLhfLug'),[identifier(none,train1_back),identifier(none,train1_front)],[add(none,identifier(none,train1_back),integer(none,1)),add(none,identifier(none,train1_front),integer(none,1))])],[])),description_event(none,description_text(none,'train2 moves one unit forward'),event(rodinpos('TrainSimple12_corrected',move_train2,'_XchKs83KEe-0NqOoLhfLug'),move_train2,ordinary(none),[],[],[less(rodinpos('TrainSimple12_corrected',grd,'_XchKtM3KEe-0NqOoLhfLug'),identifier(none,train2_front),identifier(none,train2_mal))],[],[assign(rodinpos('TrainSimple12_corrected',moveforward,'_XchKtc3KEe-0NqOoLhfLug'),[identifier(none,train2_back),identifier(none,train2_front)],[add(none,identifier(none,train2_back),integer(none,1)),add(none,identifier(none,train2_front),integer(none,1))])],[])),description_event(none,description_text(none,'train2 sends TPR to RBC which updates MAL of train1'),event(rodinpos('TrainSimple12_corrected',send_train2_position_report,'_XchKts3KEe-0NqOoLhfLug'),send_train2_position_report,ordinary(none),[],[],[],[],[assign(rodinpos('TrainSimple12_corrected',send,'_XchKt83KEe-0NqOoLhfLug'),[identifier(none,train1_mal)],[minus(none,identifier(none,train2_back),integer(none,1))])],[]))])])],[],[exporter_version(3),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant(inv3)],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant(inv4)],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant(inv5)],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant('inductive-inv1')],true),po('TrainSimple12_corrected','Invariant establishment',[event('INITIALISATION'),invariant('inductive-inv2')],true),po('TrainSimple12_corrected','Invariant preservation',[event(move_train1),invariant(inv1)],true),po('TrainSimple12_corrected','Invariant preservation',[event(move_train1),invariant(inv3)],false),po('TrainSimple12_corrected','Invariant preservation',[event(move_train1),invariant('inductive-inv1')],true),po('TrainSimple12_corrected','Invariant preservation',[event(move_train2),invariant(inv2)],true),po('TrainSimple12_corrected','Invariant preservation',[event(move_train2),invariant(inv3)],false),po('TrainSimple12_corrected','Invariant preservation',[event(move_train2),invariant('inductive-inv2')],true),po('TrainSimple12_corrected','Invariant preservation',[event(send_train2_position_report),invariant(inv4)],true),po('TrainSimple12_corrected','Invariant preservation',[event(send_train2_position_report),invariant('inductive-inv1')],true),po('TrainSimple12_corrected','Invariant preservation',[event(send_train2_position_report),invariant('inductive-inv2')],true)],_Error)).
package(load_event_b_project([event_b_model(none,'TrainSimple12',[sees(none,[]),variables(none,[identifier(none,train2_front),identifier(none,train1_front),description(none,description_text(none,'movement authority limit'),identifier(none,train1_mal)),description(none,description_text(none,'movement authority limit'),identifier(none,train2_mal)),identifier(none,train1_back),identifier(none,train2_back)]),invariant(none,[member(rodinpos('TrainSimple12',inv1,'_k66AUblvEe-N_pUjxTub7w'),interval(none,identifier(none,train1_back),identifier(none,train1_front)),pow1_subset(none,natural_set(none))),member(rodinpos('TrainSimple12',inv2,'_k66AUrlvEe-N_pUjxTub7w'),interval(none,identifier(none,train2_back),identifier(none,train2_front)),pow1_subset(none,natural_set(none))),description(rodinpos('TrainSimple12',inv3,'_k66AU7lvEe-N_pUjxTub7w'),description_text(none,'no collision'),equal(none,intersection(none,interval(none,identifier(none,train1_back),identifier(none,train1_front)),interval(none,identifier(none,train2_back),identifier(none,train2_front))),typeof(none,empty_set(none),pow_subset(none,integer_set(none))))),member(rodinpos('TrainSimple12',inv4,'_k66nYLlvEe-N_pUjxTub7w'),identifier(none,train1_mal),natural_set(none)),member(rodinpos('TrainSimple12',inv5,'_k66nYblvEe-N_pUjxTub7w'),identifier(none,train2_mal),natural_set(none)),description(rodinpos('TrainSimple12','inductive-inv1','_k67OcLlvEe-N_pUjxTub7w'),description_text(none,'train1 respects MAL'),greater_equal(none,identifier(none,train1_mal),identifier(none,train1_front))),description(rodinpos('TrainSimple12','inductive-inv2','_k67OcblvEe-N_pUjxTub7w'),description_text(none,'MAL is safe'),less(none,identifier(none,train1_mal),identifier(none,train2_back)))]),theorems(none,[]),events(none,[event(rodinpos('TrainSimple12','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('TrainSimple12',ini1,'_k64yMLlvEe-N_pUjxTub7w'),[identifier(none,train1_back),identifier(none,train1_front)],[integer(none,0),integer(none,2)]),assign(rodinpos('TrainSimple12',ini2,'_k64yMblvEe-N_pUjxTub7w'),[identifier(none,train2_back),identifier(none,train2_front)],[integer(none,4),integer(none,6)]),assign(rodinpos('TrainSimple12',ini3,'_k64yMrlvEe-N_pUjxTub7w'),[identifier(none,train1_mal)],[integer(none,3)]),assign(rodinpos('TrainSimple12',ini4,'_k65ZQLlvEe-N_pUjxTub7w'),[identifier(none,train2_mal)],[integer(none,20)])],[]),description_event(none,description_text(none,'train1 moves one unit forward'),event(rodinpos('TrainSimple12',move_train1,'_k67OcrlvEe-N_pUjxTub7w'),move_train1,ordinary(none),[],[],[less(rodinpos('TrainSimple12',grd,'_k671gLlvEe-N_pUjxTub7w'),identifier(none,train1_front),identifier(none,train1_mal))],[],[assign(rodinpos('TrainSimple12',moveforward,'_k671gblvEe-N_pUjxTub7w'),[identifier(none,train1_back),identifier(none,train1_front)],[add(none,identifier(none,train1_back),integer(none,1)),add(none,identifier(none,train1_back),integer(none,1))])],[])),description_event(none,description_text(none,'train2 moves one unit forward'),event(rodinpos('TrainSimple12',move_train2,'_k671grlvEe-N_pUjxTub7w'),move_train2,ordinary(none),[],[],[less(rodinpos('TrainSimple12',grd,'_k671g7lvEe-N_pUjxTub7w'),identifier(none,train2_front),identifier(none,train2_mal))],[],[assign(rodinpos('TrainSimple12',moveforward,'_k671hLlvEe-N_pUjxTub7w'),[identifier(none,train2_back),identifier(none,train2_front)],[add(none,identifier(none,train2_back),integer(none,1)),add(none,identifier(none,train2_front),integer(none,1))])],[])),description_event(none,description_text(none,'train2 sends TPR to RBC which updates MAL of train1'),event(rodinpos('TrainSimple12',send_train2_position_report,'_k69DoLlvEe-N_pUjxTub7w'),send_train2_position_report,ordinary(none),[],[],[],[],[assign(rodinpos('TrainSimple12',send,'_k69qsLlvEe-N_pUjxTub7w'),[identifier(none,train1_mal)],[minus(none,identifier(none,train2_back),integer(none,1))])],[]))])])],[],[exporter_version(3),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant(inv3)],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant(inv4)],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant(inv5)],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant('inductive-inv1')],true),po('TrainSimple12','Invariant establishment',[event('INITIALISATION'),invariant('inductive-inv2')],true),po('TrainSimple12','Invariant preservation',[event(move_train1),invariant(inv1)],true),po('TrainSimple12','Invariant preservation',[event(move_train1),invariant(inv3)],true),po('TrainSimple12','Invariant preservation',[event(move_train1),invariant('inductive-inv1')],true),po('TrainSimple12','Invariant preservation',[event(move_train2),invariant(inv2)],true),po('TrainSimple12','Invariant preservation',[event(move_train2),invariant(inv3)],true),po('TrainSimple12','Invariant preservation',[event(move_train2),invariant('inductive-inv2')],true),po('TrainSimple12','Invariant preservation',[event(send_train2_position_report),invariant(inv4)],true),po('TrainSimple12','Invariant preservation',[event(send_train2_position_report),invariant('inductive-inv1')],true),po('TrainSimple12','Invariant preservation',[event(send_train2_position_report),invariant('inductive-inv2')],true)],_Error)).
DEFINITIONS
// written by Michael Leuschel, January 2025
// this file can be loaded as a VisB visualisation for the Rodin models
// TrainSimple12 and TrainSimple12_corrected
// It illustrates various new features in ProB/VisB
// (being able to load visualisations from .def files, grouping multiple
// SVG objects in a DEFINITION like TRAIN and using ProB's string templates ```...```)
"LibrarySVG.def";
VISB_JSON_FILE == "";
VISB_SVG_BOX == rec(height:100, width:600, viewBox:"-1 -1 22 5");
VISB_SVG_OBJECTS0 == rec(svg_class:"polygon", stroke:"gray", `stroke-width`:0.1, fill:"gray",
title:```train 2 at position ${train2_back}..${train2_front}```,
transform: "translate(0,2.2)",
points:svg_axis(0..21,1,21,1)
);
TRAIN(Nr,tback,tfront,tmal,col) == (
rec(svg_class:"polygon", stroke:col, `stroke-width`:0.2, fill:"lightgray",
title:```train ${Nr} at position ${tback}..${tfront}```,
points:svg_train(tback,tfront-tback+1,1,1,2),
event:```move_train${Nr}```
),
rec(svg_class:"text", text:```${Nr}```, `font-size`:1.2, x:real(tback)+1.0, y:1.5),
rec(svg_class:"circle", stroke:"black", `stroke-width`:0.1, fill:col,
title:```MAL of train ${Nr} at position ${tmal}```,
cx:real(tmal)+1.0, cy:2.5, r:0.2
));
VISB_SVG_OBJECTS1 == (TRAIN(1,train1_back,train1_front,train1_mal,"palevioletred"),
TRAIN(2,train2_back,train2_front,train2_mal,"olivedrab"));
\ No newline at end of file