add train12 example

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Train12/TrainSimple12_corrected_mch.eventb

+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)).
+

Train12/TrainSimple12_mch.eventb

+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)).
+

Train12/VisBTrainSimple.def

+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