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