diff --git a/BRP/brp_1_prob_mch.eventb b/BRP/brp_1_prob_mch.eventb
new file mode 100644
index 0000000000000000000000000000000000000000..dde08c2d4b0177c5ec52a0c5c496dad074b9f0c2
--- /dev/null
+++ b/BRP/brp_1_prob_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,brp_1_prob,[sees(none,[brp_ctx_1,brp_ctx_2,brp_ctx_2_prob]),refines(none,brp_1),variables(none,[identifier(none,h),identifier(none,r),identifier(none,s_st),identifier(none,r_st)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos(brp_1_prob,'INITIALISATION',internal_element5),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_1_prob,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_1_prob,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_1_prob,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)])],[]),event(rodinpos(brp_1_prob,brp,internal_element6),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_1_prob,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[]),event(rodinpos(brp_1_prob,'RCV_current_data',internal_element7),'RCV_current_data',ordinary(none),['RCV_current_data'],[],[equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),less(rodinpos(brp_1_prob,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1_prob,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),function(none,identifier(none,f),[add(none,identifier(none,r),integer(none,1))])])]))])],[]),event(rodinpos(brp_1_prob,'RCV_success',internal_element8),'RCV_success',ordinary(none),['RCV_success'],[],[equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1_prob,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_1_prob,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1_prob,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),function(none,identifier(none,f),[identifier(none,n)])])]))])],[]),event(rodinpos(brp_1_prob,'RCV_failure',internal_element9),'RCV_failure',ordinary(none),['RCV_failure'],[],[equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1_prob,grd2,internal_element2),identifier(none,s_st),identifier(none,failure))],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[]),event(rodinpos(brp_1_prob,'SND_success','internal_element:'),'SND_success',ordinary(none),['SND_success'],[],[equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_1_prob,grd2,internal_element2),identifier(none,r_st),identifier(none,success))],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)])],[]),event(rodinpos(brp_1_prob,'SND_failure','internal_element;'),'SND_failure',ordinary(none),['SND_failure'],[],[equal(rodinpos(brp_1_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working))],[],[assign(rodinpos(brp_1_prob,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)])],[])])]),event_b_model(none,brp_1,[sees(none,[brp_ctx_1,brp_ctx_2]),refines(none,brp_0),variables(none,[identifier(none,h),identifier(none,r),identifier(none,s_st),identifier(none,r_st)]),invariant(none,[member(rodinpos(brp_1,inv1_1,internal_element1I),identifier(none,r),interval(none,integer(none,0),identifier(none,n))),equal(rodinpos(brp_1,inv1_2,internal_element2I),identifier(none,h),domain_restriction(none,interval(none,integer(none,1),identifier(none,r)),identifier(none,f))),equivalence(rodinpos(brp_1,inv1_3,internal_element3I),equal(none,identifier(none,r_st),identifier(none,success)),equal(none,identifier(none,r),identifier(none,n))),implication(rodinpos(brp_1,inv1_4,internal_element4I),equal(none,identifier(none,s_st),identifier(none,success)),equal(none,identifier(none,r_st),identifier(none,success)))]),theorems(none,[]),events(none,[event(rodinpos(brp_1,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_1,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_1,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)])],[]),description_event(none,description_text(none,'the protocol terminates on the sender side with ${r} packets sent'),event(rodinpos(brp_1,brp,internal_element1),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[witness(none,identifier(none,'i\''),equal(rodinpos(brp_1,'i\'',internal_element1),identifier(none,'i\''),identifier(none,r))),witness(none,identifier(none,'g\''),equal(rodinpos(brp_1,'g\'',internal_element2),identifier(none,'g\''),identifier(none,h)))])),description_event(none,description_text(none,'the receiver receives packet nr. ${r} : ${f(r)}'),event(rodinpos(brp_1,'RCV_current_data',internal_element2),'RCV_current_data',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),less(rodinpos(brp_1,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),function(none,identifier(none,f),[add(none,identifier(none,r),integer(none,1))])])]))])],[])),description_event(none,description_text(none,'the receiver receives last packet nr. ${n} : ${f(n)}'),event(rodinpos(brp_1,'RCV_success',internal_element3),'RCV_success',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),function(none,identifier(none,f),[identifier(none,n)])])]))])],[])),description_event(none,description_text(none,'the receiver times out and aborts'),event(rodinpos(brp_1,'RCV_failure',internal_element4),'RCV_failure',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,s_st),identifier(none,failure))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[])),description_event(none,description_text(none,'the sender detectcs successful completion'),event(rodinpos(brp_1,'SND_success',internal_element5),'SND_success',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,r_st),identifier(none,success))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)])],[])),description_event(none,description_text(none,'the sender times out and stops the transfer'),event(rodinpos(brp_1,'SND_failure',internal_element6),'SND_failure',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)])],[]))])]),event_b_model(none,brp_0,[sees(none,[brp_ctx_1]),variables(none,[identifier(none,g),identifier(none,i)]),invariant(none,[description(rodinpos(brp_0,inv1,internal_element1I),description_text(none,'the number of blocks already received'),member(none,identifier(none,i),interval(none,integer(none,0),identifier(none,n)))),description(rodinpos(brp_0,inv2,internal_element2I),description_text(none,'the file as received thus far'),member(none,identifier(none,g),total_function(none,interval(none,integer(none,1),identifier(none,i)),identifier(none,'D'))))]),theorems(none,[]),events(none,[event(rodinpos(brp_0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(brp_0,act1,internal_element1),[identifier(none,i)],[integer(none,0)]),assign(rodinpos(brp_0,act2,internal_element2),[identifier(none,g)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))])],[]),event(rodinpos(brp_0,brp,internal_element1),brp,ordinary(none),[],[],[],[],[becomes_such(rodinpos(brp_0,act1,internal_element1),[identifier(none,i),identifier(none,g)],conjunct(none,[member(none,identifier(none,'i\''),interval(none,integer(none,0),identifier(none,n))),equal(none,identifier(none,'g\''),domain_restriction(none,interval(none,integer(none,1),identifier(none,'i\'')),identifier(none,f)))]))],[])])])],[event_b_context(none,brp_ctx_1,[extends(none,[]),constants(none,[identifier(none,f),identifier(none,n)]),abstract_constants(none,[]),axioms(none,[description(rodinpos(brp_ctx_1,axm0_1,internal_element1A),description_text(none,'the number of blocks in the file to be transmitted'),less(none,integer(none,0),identifier(none,n))),description(rodinpos(brp_ctx_1,axm0_2,internal_element2A),description_text(none,'the file to be transmitted'),member(none,identifier(none,f),total_function(none,interval(none,integer(none,1),identifier(none,n)),identifier(none,'D'))))]),theorems(none,[]),sets(none,[description(none,description_text(none,'block contents of files'),deferred_set(none,'D'))])]),event_b_context(none,brp_ctx_2,[extends(none,[]),constants(none,[identifier(none,success),identifier(none,working),identifier(none,failure)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(brp_ctx_2,axm1_1,internal_element1A),identifier(none,'STATUS'),set_extension(none,[identifier(none,working),identifier(none,success),identifier(none,failure)])),not_equal(rodinpos(brp_ctx_2,axm1_2,internal_element2A),identifier(none,working),identifier(none,success)),not_equal(rodinpos(brp_ctx_2,axm1_3,internal_element3A),identifier(none,working),identifier(none,failure)),not_equal(rodinpos(brp_ctx_2,axm1_4,internal_element4A),identifier(none,success),identifier(none,failure))]),theorems(none,[]),sets(none,[deferred_set(none,'STATUS')])]),event_b_context(none,brp_ctx_2_prob,[extends(none,[brp_ctx_1,brp_ctx_2]),constants(none,[identifier(none,data3),identifier(none,data2),identifier(none,data1)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(brp_ctx_2_prob,prob_setn3,'_RUCGAFXNEeOWZpgIVh-bvA'),identifier(none,n),integer(none,3)),partition(rodinpos(brp_ctx_2_prob,part,'_ft64EVswEeOs_cZHGUQdmA'),identifier(none,'D'),[set_extension(none,[identifier(none,data1)]),set_extension(none,[identifier(none,data2)]),set_extension(none,[identifier(none,data3)])]),conjunct(rodinpos(brp_ctx_2_prob,surj,'_koqDAFtMEeO19YSL__geAg'),[not_equal(none,function(none,identifier(none,f),[integer(none,1)]),function(none,identifier(none,f),[integer(none,2)])),conjunct(none,[not_equal(none,function(none,identifier(none,f),[integer(none,2)]),function(none,identifier(none,f),[integer(none,3)])),not_equal(none,function(none,identifier(none,f),[integer(none,1)]),function(none,identifier(none,f),[integer(none,3)]))])]),conjunct(rodinpos(brp_ctx_2_prob,fix,'_yp0O4FaREey1S6QrNV5qvw'),[equal(none,function(none,identifier(none,f),[integer(none,1)]),identifier(none,data1)),conjunct(none,[equal(none,function(none,identifier(none,f),[integer(none,2)]),identifier(none,data2)),equal(none,function(none,identifier(none,f),[integer(none,3)]),identifier(none,data3))])])]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(brp_ctx_2_prob,'Well-definedness of Axiom',[axiom(surj)],true),po(brp_ctx_2_prob,'Well-definedness of Axiom',[axiom(fix)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_1)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_2)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_3)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_4)],true),po(brp_1,'Action simulation',[event(brp),action(act1),event(brp)],true),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_1)],true),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_2)],false),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_3)],true),po(brp_1,'Well-definedness of action',[action(act2)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_1)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_2)],false),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_3)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_4)],true),po(brp_1,'Well-definedness of action',[action(act3)],true),po(brp_1,'Invariant preservation',[event('RCV_failure'),invariant(inv1_3)],true),po(brp_1,'Invariant preservation',[event('RCV_failure'),invariant(inv1_4)],true),po(brp_1,'Invariant preservation',[event('SND_success'),invariant(inv1_4)],true),po(brp_1,'Invariant preservation',[event('SND_failure'),invariant(inv1_4)],true),po(brp_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(brp_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(brp_0,'Invariant preservation',[event(brp),invariant(inv1)],true),po(brp_0,'Invariant preservation',[event(brp),invariant(inv2)],true),po(brp_0,'Feasibility of action',[action(act1)],true)],_Error)).
+
diff --git a/BRP/brp_3_prob_mch.eventb b/BRP/brp_3_prob_mch.eventb
new file mode 100644
index 0000000000000000000000000000000000000000..aea66ab14e7a3c7a088053d9e7a8e7b5d3780f43
--- /dev/null
+++ b/BRP/brp_3_prob_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,brp_3_prob,[sees(none,[brp_ctx_1,brp_ctx_2,brp_ctx_2_prob,brp_ctx_3,brp_ctx_3_prob]),refines(none,brp_3),variables(none,[identifier(none,c),identifier(none,d),identifier(none,h),identifier(none,l),identifier(none,r),identifier(none,s),identifier(none,v),identifier(none,w),identifier(none,s_st),identifier(none,ab),identifier(none,db),identifier(none,r_st)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos(brp_3_prob,'INITIALISATION',internal_element13),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)]),assign(rodinpos(brp_3_prob,act5,internal_element5),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3_prob,act6,internal_element6),[identifier(none,s)],[integer(none,0)]),assign(rodinpos(brp_3_prob,act7,internal_element7),[identifier(none,d)],[function(none,identifier(none,f),[integer(none,1)])]),assign(rodinpos(brp_3_prob,act9,internal_element9),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act10,internal_element10),[identifier(none,ab)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act11,internal_element11),[identifier(none,v)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act12,internal_element12),[identifier(none,l)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act13,internal_element13),[identifier(none,c)],[integer(none,0)])],[]),event(rodinpos(brp_3_prob,brp,internal_element14),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[]),event(rodinpos(brp_3_prob,'RCV_current_data',internal_element15),'RCV_current_data',ordinary(none),['RCV_current_data'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_3_prob,grd3,internal_element3),identifier(none,db),boolean_true(none)),equal(rodinpos(brp_3_prob,grd4,internal_element4),identifier(none,l),boolean_false(none))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),identifier(none,d)])]))]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,v)],[boolean_true(none)])],[]),event(rodinpos(brp_3_prob,'RCV_success',internal_element16),'RCV_success',ordinary(none),['RCV_success'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_3_prob,grd3,internal_element3),identifier(none,db),boolean_true(none)),equal(rodinpos(brp_3_prob,grd4,internal_element4),identifier(none,l),boolean_true(none))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),identifier(none,d)])]))]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act5,internal_element5),[identifier(none,v)],[boolean_true(none)])],[]),event(rodinpos(brp_3_prob,'RCV_failure',internal_element17),'RCV_failure',ordinary(none),['RCV_failure'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,c),add(none,identifier(none,'MAX'),integer(none,1)))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[]),event(rodinpos(brp_3_prob,'SND_success',internal_element18),'SND_success',ordinary(none),['SND_success'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,ab),boolean_true(none)),equal(rodinpos(brp_3_prob,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3_prob,'SND_failure',internal_element19),'SND_failure',ordinary(none),['SND_failure'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,w),boolean_false(none)),equal(rodinpos(brp_3_prob,grd3,internal_element3),identifier(none,ab),boolean_false(none)),equal(rodinpos(brp_3_prob,grd4,internal_element4),identifier(none,db),boolean_false(none)),equal(rodinpos(brp_3_prob,grd5,internal_element5),identifier(none,v),boolean_false(none)),equal(rodinpos(brp_3_prob,grd6,internal_element6),identifier(none,c),identifier(none,'MAX'))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(brp_3_prob,'SND_rcv_current_ack','internal_element1:'),'SND_rcv_current_ack',ordinary(none),['SND_rcv_current_ack'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,ab),boolean_true(none)),less(rodinpos(brp_3_prob,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,s)],[add(none,identifier(none,s),integer(none,1))]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3_prob,'SND_snd_current_data','internal_element1;'),'SND_snd_current_data',ordinary(none),['SND_snd_current_data'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,w),boolean_true(none)),less(rodinpos(brp_3_prob,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,w)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,db)],[boolean_true(none)]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,l)],[boolean_false(none)])],[]),event(rodinpos(brp_3_prob,'SND_snd_last_data','internal_element1='),'SND_snd_last_data',ordinary(none),['SND_snd_last_data'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,w),boolean_true(none)),equal(rodinpos(brp_3_prob,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,w)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act3,internal_element3),[identifier(none,db)],[boolean_true(none)]),assign(rodinpos(brp_3_prob,act4,internal_element4),[identifier(none,l)],[boolean_true(none)])],[]),event(rodinpos(brp_3_prob,'SND_time_out_current','internal_element1>'),'SND_time_out_current',ordinary(none),['SND_time_out_current'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3_prob,grd2,internal_element2),identifier(none,w),boolean_false(none)),equal(rodinpos(brp_3_prob,grd3,internal_element3),identifier(none,ab),boolean_false(none)),equal(rodinpos(brp_3_prob,grd4,internal_element4),identifier(none,db),boolean_false(none)),equal(rodinpos(brp_3_prob,grd5,internal_element5),identifier(none,v),boolean_false(none)),less(rodinpos(brp_3_prob,grd6,internal_element6),identifier(none,c),identifier(none,'MAX'))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3_prob,act2,internal_element2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(brp_3_prob,'DMN_data_channel','internal_element1?'),'DMN_data_channel',ordinary(none),['DMN_data_channel'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,db),boolean_true(none))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,db)],[boolean_false(none)])],[]),event(rodinpos(brp_3_prob,'DMN_ack_channel','internal_element1@'),'DMN_ack_channel',ordinary(none),['DMN_ack_channel'],[],[equal(rodinpos(brp_3_prob,grd1,internal_element1),identifier(none,ab),boolean_true(none))],[],[assign(rodinpos(brp_3_prob,act1,internal_element1),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3_prob,'RCV_snd_ack','_SuEf8JdKEeWM7fNBUrLJSw'),'RCV_snd_ack',ordinary(none),['RCV_snd_ack'],[],[equal(rodinpos(brp_3_prob,grd1,'_OqumUJdKEeWM7fNBUrLJSw'),identifier(none,v),boolean_true(none))],[],[assign(rodinpos(brp_3_prob,act1,'_OqumUZdKEeWM7fNBUrLJSw'),[identifier(none,v)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act2,'_OqumUpdKEeWM7fNBUrLJSw'),[identifier(none,ab)],[boolean_true(none)])],[]),event(rodinpos(brp_3_prob,'RCV_rcv_retry','_SuEf8pdKEeWM7fNBUrLJSw'),'RCV_rcv_retry',ordinary(none),['RCV_rcv_retry'],[],[equal(rodinpos(brp_3_prob,grd1,'_OqumVJdKEeWM7fNBUrLJSw'),identifier(none,db),boolean_true(none)),not_equal(rodinpos(brp_3_prob,grd2,'_OqumVZdKEeWM7fNBUrLJSw'),identifier(none,r),identifier(none,s))],[],[assign(rodinpos(brp_3_prob,act1,'_OqumVpdKEeWM7fNBUrLJSw'),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3_prob,act2,'_OqvNYJdKEeWM7fNBUrLJSw'),[identifier(none,v)],[boolean_true(none)])],[])])]),event_b_model(none,brp_3,[sees(none,[brp_ctx_1,brp_ctx_2,brp_ctx_3]),refines(none,brp_2),variables(none,[identifier(none,c),identifier(none,d),identifier(none,h),identifier(none,l),identifier(none,r),identifier(none,s),identifier(none,v),identifier(none,w),identifier(none,s_st),identifier(none,ab),identifier(none,db),identifier(none,r_st)]),invariant(none,[implication(rodinpos(brp_3,inv3_1,internal_element1I),equal(none,identifier(none,w),boolean_true(none)),equal(none,identifier(none,db),boolean_false(none))),implication(rodinpos(brp_3,inv3_2,internal_element2I),equal(none,identifier(none,w),boolean_true(none)),equal(none,identifier(none,ab),boolean_false(none))),implication(rodinpos(brp_3,inv3_3,internal_element3I),equal(none,identifier(none,w),boolean_true(none)),equal(none,identifier(none,v),boolean_false(none))),implication(rodinpos(brp_3,inv3_4,internal_element4I),equal(none,identifier(none,db),boolean_true(none)),equal(none,identifier(none,ab),boolean_false(none))),implication(rodinpos(brp_3,inv3_5,internal_element5I),equal(none,identifier(none,db),boolean_true(none)),equal(none,identifier(none,v),boolean_false(none))),implication(rodinpos(brp_3,inv3_6,internal_element6I),equal(none,identifier(none,ab),boolean_true(none)),equal(none,identifier(none,v),boolean_false(none))),implication(rodinpos(brp_3,inv3_7,internal_element7I),conjunct(none,[equal(none,identifier(none,db),boolean_true(none)),conjunct(none,[equal(none,identifier(none,r),identifier(none,s)),equal(none,identifier(none,l),boolean_false(none))])]),less(none,add(none,identifier(none,s),integer(none,1)),identifier(none,n))),implication(rodinpos(brp_3,inv3_8,internal_element8I),conjunct(none,[equal(none,identifier(none,db),boolean_true(none)),conjunct(none,[equal(none,identifier(none,r),identifier(none,s)),equal(none,identifier(none,l),boolean_true(none))])]),equal(none,add(none,identifier(none,s),integer(none,1)),identifier(none,n))),member(rodinpos(brp_3,inv3_9,internal_element9I),identifier(none,c),interval(none,integer(none,0),add(none,identifier(none,'MAX'),integer(none,1)))),equivalence(rodinpos(brp_3,inv3_10,internal_element10I),equal(none,identifier(none,c),add(none,identifier(none,'MAX'),integer(none,1))),equal(none,identifier(none,s_st),identifier(none,failure))),implication(rodinpos(brp_3,inv3_11,internal_element11I),equal(none,identifier(none,ab),boolean_true(none)),not_equal(none,identifier(none,r),identifier(none,s))),implication(rodinpos(brp_3,inv3_12,internal_element12I),equal(none,identifier(none,v),boolean_true(none)),not_equal(none,identifier(none,r),identifier(none,s)))]),theorems(none,[]),events(none,[event(rodinpos(brp_3,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)]),assign(rodinpos(brp_3,act5,internal_element5),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3,act6,internal_element6),[identifier(none,s)],[integer(none,0)]),assign(rodinpos(brp_3,act7,internal_element7),[identifier(none,d)],[function(none,identifier(none,f),[integer(none,1)])]),assign(rodinpos(brp_3,act9,internal_element9),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3,act10,internal_element10),[identifier(none,ab)],[boolean_false(none)]),assign(rodinpos(brp_3,act11,internal_element11),[identifier(none,v)],[boolean_false(none)]),assign(rodinpos(brp_3,act12,internal_element12),[identifier(none,l)],[boolean_false(none)]),assign(rodinpos(brp_3,act13,internal_element13),[identifier(none,c)],[integer(none,0)])],[]),event(rodinpos(brp_3,brp,internal_element1),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[]),event(rodinpos(brp_3,'RCV_current_data',internal_element2),'RCV_current_data',ordinary(none),['RCV_current_data'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_3,grd3,internal_element3),identifier(none,db),boolean_true(none)),equal(rodinpos(brp_3,grd4,internal_element4),identifier(none,l),boolean_false(none))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),identifier(none,d)])]))]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,v)],[boolean_true(none)])],[]),event(rodinpos(brp_3,'RCV_success',internal_element3),'RCV_success',ordinary(none),['RCV_success'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_3,grd3,internal_element3),identifier(none,db),boolean_true(none)),equal(rodinpos(brp_3,grd4,internal_element4),identifier(none,l),boolean_true(none))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),identifier(none,d)])]))]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3,act5,internal_element5),[identifier(none,v)],[boolean_true(none)])],[]),event(rodinpos(brp_3,'RCV_failure',internal_element4),'RCV_failure',ordinary(none),['RCV_failure'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,c),add(none,identifier(none,'MAX'),integer(none,1)))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[]),event(rodinpos(brp_3,'SND_success',internal_element5),'SND_success',ordinary(none),['SND_success'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,ab),boolean_true(none)),equal(rodinpos(brp_3,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3,'SND_failure',internal_element6),'SND_failure',ordinary(none),['SND_failure'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,w),boolean_false(none)),equal(rodinpos(brp_3,grd3,internal_element3),identifier(none,ab),boolean_false(none)),equal(rodinpos(brp_3,grd4,internal_element4),identifier(none,db),boolean_false(none)),equal(rodinpos(brp_3,grd5,internal_element5),identifier(none,v),boolean_false(none)),equal(rodinpos(brp_3,grd6,internal_element6),identifier(none,c),identifier(none,'MAX'))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(brp_3,'SND_rcv_current_ack',internal_element7),'SND_rcv_current_ack',ordinary(none),['SND_rcv_current_ack'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,ab),boolean_true(none)),less(rodinpos(brp_3,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,s)],[add(none,identifier(none,s),integer(none,1))]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3,'SND_snd_current_data',internal_element8),'SND_snd_current_data',ordinary(none),['SND_snd_current_data'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,w),boolean_true(none)),less(rodinpos(brp_3,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,w)],[boolean_false(none)]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,db)],[boolean_true(none)]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,l)],[boolean_false(none)])],[]),event(rodinpos(brp_3,'SND_snd_last_data',internal_element9),'SND_snd_last_data',ordinary(none),['SND_snd_last_data'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,w),boolean_true(none)),equal(rodinpos(brp_3,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,w)],[boolean_false(none)]),assign(rodinpos(brp_3,act3,internal_element3),[identifier(none,db)],[boolean_true(none)]),assign(rodinpos(brp_3,act4,internal_element4),[identifier(none,l)],[boolean_true(none)])],[]),event(rodinpos(brp_3,'SND_time_out_current',internal_element10),'SND_time_out_current',ordinary(none),['SND_time_out_current'],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_3,grd2,internal_element2),identifier(none,w),boolean_false(none)),equal(rodinpos(brp_3,grd3,internal_element3),identifier(none,ab),boolean_false(none)),equal(rodinpos(brp_3,grd4,internal_element4),identifier(none,db),boolean_false(none)),equal(rodinpos(brp_3,grd5,internal_element5),identifier(none,v),boolean_false(none)),less(rodinpos(brp_3,grd6,internal_element6),identifier(none,c),identifier(none,'MAX'))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_3,act2,internal_element2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(brp_3,'DMN_data_channel',internal_element11),'DMN_data_channel',ordinary(none),[],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,db),boolean_true(none))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,db)],[boolean_false(none)])],[]),event(rodinpos(brp_3,'DMN_ack_channel',internal_element12),'DMN_ack_channel',ordinary(none),[],[],[equal(rodinpos(brp_3,grd1,internal_element1),identifier(none,ab),boolean_true(none))],[],[assign(rodinpos(brp_3,act1,internal_element1),[identifier(none,ab)],[boolean_false(none)])],[]),event(rodinpos(brp_3,'RCV_snd_ack','_Oqt_QJdKEeWM7fNBUrLJSw'),'RCV_snd_ack',ordinary(none),[],[],[equal(rodinpos(brp_3,grd1,'_OqumUJdKEeWM7fNBUrLJSw'),identifier(none,v),boolean_true(none))],[],[assign(rodinpos(brp_3,act1,'_OqumUZdKEeWM7fNBUrLJSw'),[identifier(none,v)],[boolean_false(none)]),assign(rodinpos(brp_3,act2,'_OqumUpdKEeWM7fNBUrLJSw'),[identifier(none,ab)],[boolean_true(none)])],[]),event(rodinpos(brp_3,'RCV_rcv_retry','_OqumU5dKEeWM7fNBUrLJSw'),'RCV_rcv_retry',ordinary(none),[],[],[equal(rodinpos(brp_3,grd1,'_OqumVJdKEeWM7fNBUrLJSw'),identifier(none,db),boolean_true(none)),not_equal(rodinpos(brp_3,grd2,'_OqumVZdKEeWM7fNBUrLJSw'),identifier(none,r),identifier(none,s))],[],[assign(rodinpos(brp_3,act1,'_OqumVpdKEeWM7fNBUrLJSw'),[identifier(none,db)],[boolean_false(none)]),assign(rodinpos(brp_3,act2,'_OqvNYJdKEeWM7fNBUrLJSw'),[identifier(none,v)],[boolean_true(none)])],[])])]),event_b_model(none,brp_2,[sees(none,[brp_ctx_1,brp_ctx_2]),refines(none,brp_1),variables(none,[identifier(none,d),identifier(none,h),identifier(none,r),identifier(none,s),identifier(none,w),identifier(none,s_st),identifier(none,r_st)]),invariant(none,[member(rodinpos(brp_2,inv2_1,internal_element1I),identifier(none,s),interval(none,integer(none,0),minus(none,identifier(none,n),integer(none,1)))),member(rodinpos(brp_2,inv2_2,internal_element2I),identifier(none,r),interval(none,identifier(none,s),add(none,identifier(none,s),integer(none,1)))),implication(rodinpos(brp_2,inv2_3,internal_element3I),equal(none,identifier(none,w),boolean_false(none)),equal(none,identifier(none,d),function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])))]),theorems(none,[]),events(none,[event(rodinpos(brp_2,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_2,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_2,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)]),assign(rodinpos(brp_2,act5,internal_element5),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_2,act6,internal_element6),[identifier(none,s)],[integer(none,0)]),assign(rodinpos(brp_2,act7,internal_element7),[identifier(none,d)],[function(none,identifier(none,f),[integer(none,1)])])],[]),event(rodinpos(brp_2,brp,internal_element1),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[]),event(rodinpos(brp_2,'RCV_current_data',internal_element2),'RCV_current_data',ordinary(none),['RCV_current_data'],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),less(rodinpos(brp_2,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n)),equal(rodinpos(brp_2,grd3,internal_element3),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_2,grd4,internal_element4),identifier(none,w),boolean_false(none))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),identifier(none,d)])]))])],[]),event(rodinpos(brp_2,'RCV_success',internal_element3),'RCV_success',ordinary(none),['RCV_success'],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n)),equal(rodinpos(brp_2,grd3,internal_element3),identifier(none,r),identifier(none,s)),equal(rodinpos(brp_2,grd4,internal_element4),identifier(none,w),boolean_false(none))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_2,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),identifier(none,d)])]))])],[]),event(rodinpos(brp_2,'RCV_failure',internal_element4),'RCV_failure',ordinary(none),['RCV_failure'],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,s_st),identifier(none,failure))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[]),event(rodinpos(brp_2,'SND_success',internal_element5),'SND_success',ordinary(none),['SND_success'],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,w),boolean_false(none)),equal(rodinpos(brp_2,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n)),equal(rodinpos(brp_2,grd4,internal_element4),identifier(none,r),add(none,identifier(none,s),integer(none,1)))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)])],[]),event(rodinpos(brp_2,'SND_failure',internal_element6),'SND_failure',ordinary(none),['SND_failure'],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)])],[]),event(rodinpos(brp_2,'SND_rcv_current_ack',internal_element7),'SND_rcv_current_ack',ordinary(none),[],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,w),boolean_false(none)),less(rodinpos(brp_2,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n)),equal(rodinpos(brp_2,grd4,internal_element4),identifier(none,r),add(none,identifier(none,s),integer(none,1)))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,w)],[boolean_true(none)]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,s)],[add(none,identifier(none,s),integer(none,1))])],[]),event(rodinpos(brp_2,'SND_snd_current_data',internal_element8),'SND_snd_current_data',ordinary(none),[],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,w),boolean_true(none)),less(rodinpos(brp_2,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,w)],[boolean_false(none)])],[]),event(rodinpos(brp_2,'SND_snd_last_data',internal_element9),'SND_snd_last_data',ordinary(none),[],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,w),boolean_true(none)),equal(rodinpos(brp_2,grd3,internal_element3),add(none,identifier(none,s),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,d)],[function(none,identifier(none,f),[add(none,identifier(none,s),integer(none,1))])]),assign(rodinpos(brp_2,act2,internal_element2),[identifier(none,w)],[boolean_false(none)])],[]),event(rodinpos(brp_2,'SND_time_out_current',internal_element10),'SND_time_out_current',ordinary(none),[],[],[equal(rodinpos(brp_2,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_2,grd2,internal_element2),identifier(none,w),boolean_false(none))],[],[assign(rodinpos(brp_2,act1,internal_element1),[identifier(none,w)],[boolean_true(none)])],[])])]),event_b_model(none,brp_1,[sees(none,[brp_ctx_1,brp_ctx_2]),refines(none,brp_0),variables(none,[identifier(none,h),identifier(none,r),identifier(none,s_st),identifier(none,r_st)]),invariant(none,[member(rodinpos(brp_1,inv1_1,internal_element1I),identifier(none,r),interval(none,integer(none,0),identifier(none,n))),equal(rodinpos(brp_1,inv1_2,internal_element2I),identifier(none,h),domain_restriction(none,interval(none,integer(none,1),identifier(none,r)),identifier(none,f))),equivalence(rodinpos(brp_1,inv1_3,internal_element3I),equal(none,identifier(none,r_st),identifier(none,success)),equal(none,identifier(none,r),identifier(none,n))),implication(rodinpos(brp_1,inv1_4,internal_element4I),equal(none,identifier(none,s_st),identifier(none,success)),equal(none,identifier(none,r_st),identifier(none,success)))]),theorems(none,[]),events(none,[event(rodinpos(brp_1,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r)],[integer(none,0)]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,h)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))]),assign(rodinpos(brp_1,act3,internal_element3),[identifier(none,r_st)],[identifier(none,working)]),assign(rodinpos(brp_1,act4,internal_element4),[identifier(none,s_st)],[identifier(none,working)])],[]),description_event(none,description_text(none,'the protocol terminates on the sender side with ${r} packets sent'),event(rodinpos(brp_1,brp,internal_element1),brp,ordinary(none),[brp],[],[not_equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),not_equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,r_st),identifier(none,working))],[],[],[witness(none,identifier(none,'i\''),equal(rodinpos(brp_1,'i\'',internal_element1),identifier(none,'i\''),identifier(none,r))),witness(none,identifier(none,'g\''),equal(rodinpos(brp_1,'g\'',internal_element2),identifier(none,'g\''),identifier(none,h)))])),description_event(none,description_text(none,'the receiver receives packet nr. ${r} : ${f(r)}'),event(rodinpos(brp_1,'RCV_current_data',internal_element2),'RCV_current_data',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),less(rodinpos(brp_1,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),function(none,identifier(none,f),[add(none,identifier(none,r),integer(none,1))])])]))])],[])),description_event(none,description_text(none,'the receiver receives last packet nr. ${n} : ${f(n)}'),event(rodinpos(brp_1,'RCV_success',internal_element3),'RCV_success',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),add(none,identifier(none,r),integer(none,1)),identifier(none,n))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r_st)],[identifier(none,success)]),assign(rodinpos(brp_1,act2,internal_element2),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(brp_1,act3,internal_element3),[identifier(none,h)],[union(none,identifier(none,h),set_extension(none,[couple(none,[identifier(none,n),function(none,identifier(none,f),[identifier(none,n)])])]))])],[])),description_event(none,description_text(none,'the receiver times out and aborts'),event(rodinpos(brp_1,'RCV_failure',internal_element4),'RCV_failure',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,r_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,s_st),identifier(none,failure))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,r_st)],[identifier(none,failure)])],[])),description_event(none,description_text(none,'the sender detectcs successful completion'),event(rodinpos(brp_1,'SND_success',internal_element5),'SND_success',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working)),equal(rodinpos(brp_1,grd2,internal_element2),identifier(none,r_st),identifier(none,success))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,s_st)],[identifier(none,success)])],[])),description_event(none,description_text(none,'the sender times out and stops the transfer'),event(rodinpos(brp_1,'SND_failure',internal_element6),'SND_failure',ordinary(none),[],[],[equal(rodinpos(brp_1,grd1,internal_element1),identifier(none,s_st),identifier(none,working))],[],[assign(rodinpos(brp_1,act1,internal_element1),[identifier(none,s_st)],[identifier(none,failure)])],[]))])]),event_b_model(none,brp_0,[sees(none,[brp_ctx_1]),variables(none,[identifier(none,g),identifier(none,i)]),invariant(none,[description(rodinpos(brp_0,inv1,internal_element1I),description_text(none,'the number of blocks already received'),member(none,identifier(none,i),interval(none,integer(none,0),identifier(none,n)))),description(rodinpos(brp_0,inv2,internal_element2I),description_text(none,'the file as received thus far'),member(none,identifier(none,g),total_function(none,interval(none,integer(none,1),identifier(none,i)),identifier(none,'D'))))]),theorems(none,[]),events(none,[event(rodinpos(brp_0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(brp_0,act1,internal_element1),[identifier(none,i)],[integer(none,0)]),assign(rodinpos(brp_0,act2,internal_element2),[identifier(none,g)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'D'))))])],[]),event(rodinpos(brp_0,brp,internal_element1),brp,ordinary(none),[],[],[],[],[becomes_such(rodinpos(brp_0,act1,internal_element1),[identifier(none,i),identifier(none,g)],conjunct(none,[member(none,identifier(none,'i\''),interval(none,integer(none,0),identifier(none,n))),equal(none,identifier(none,'g\''),domain_restriction(none,interval(none,integer(none,1),identifier(none,'i\'')),identifier(none,f)))]))],[])])])],[event_b_context(none,brp_ctx_1,[extends(none,[]),constants(none,[identifier(none,f),identifier(none,n)]),abstract_constants(none,[]),axioms(none,[description(rodinpos(brp_ctx_1,axm0_1,internal_element1A),description_text(none,'the number of blocks in the file to be transmitted'),less(none,integer(none,0),identifier(none,n))),description(rodinpos(brp_ctx_1,axm0_2,internal_element2A),description_text(none,'the file to be transmitted'),member(none,identifier(none,f),total_function(none,interval(none,integer(none,1),identifier(none,n)),identifier(none,'D'))))]),theorems(none,[]),sets(none,[description(none,description_text(none,'block contents of files'),deferred_set(none,'D'))])]),event_b_context(none,brp_ctx_2,[extends(none,[]),constants(none,[identifier(none,success),identifier(none,working),identifier(none,failure)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(brp_ctx_2,axm1_1,internal_element1A),identifier(none,'STATUS'),set_extension(none,[identifier(none,working),identifier(none,success),identifier(none,failure)])),not_equal(rodinpos(brp_ctx_2,axm1_2,internal_element2A),identifier(none,working),identifier(none,success)),not_equal(rodinpos(brp_ctx_2,axm1_3,internal_element3A),identifier(none,working),identifier(none,failure)),not_equal(rodinpos(brp_ctx_2,axm1_4,internal_element4A),identifier(none,success),identifier(none,failure))]),theorems(none,[]),sets(none,[deferred_set(none,'STATUS')])]),event_b_context(none,brp_ctx_2_prob,[extends(none,[brp_ctx_1,brp_ctx_2]),constants(none,[identifier(none,data3),identifier(none,data2),identifier(none,data1)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(brp_ctx_2_prob,prob_setn3,'_RUCGAFXNEeOWZpgIVh-bvA'),identifier(none,n),integer(none,3)),partition(rodinpos(brp_ctx_2_prob,part,'_ft64EVswEeOs_cZHGUQdmA'),identifier(none,'D'),[set_extension(none,[identifier(none,data1)]),set_extension(none,[identifier(none,data2)]),set_extension(none,[identifier(none,data3)])]),conjunct(rodinpos(brp_ctx_2_prob,surj,'_koqDAFtMEeO19YSL__geAg'),[not_equal(none,function(none,identifier(none,f),[integer(none,1)]),function(none,identifier(none,f),[integer(none,2)])),conjunct(none,[not_equal(none,function(none,identifier(none,f),[integer(none,2)]),function(none,identifier(none,f),[integer(none,3)])),not_equal(none,function(none,identifier(none,f),[integer(none,1)]),function(none,identifier(none,f),[integer(none,3)]))])]),conjunct(rodinpos(brp_ctx_2_prob,fix,'_yp0O4FaREey1S6QrNV5qvw'),[equal(none,function(none,identifier(none,f),[integer(none,1)]),identifier(none,data1)),conjunct(none,[equal(none,function(none,identifier(none,f),[integer(none,2)]),identifier(none,data2)),equal(none,function(none,identifier(none,f),[integer(none,3)]),identifier(none,data3))])])]),theorems(none,[]),sets(none,[])]),event_b_context(none,brp_ctx_3,[extends(none,[]),constants(none,[identifier(none,'MAX')]),abstract_constants(none,[]),axioms(none,[member(rodinpos(brp_ctx_3,axm3_1,internal_element1A),identifier(none,'MAX'),natural_set(none))]),theorems(none,[]),sets(none,[])]),event_b_context(none,brp_ctx_3_prob,[extends(none,[brp_ctx_3]),constants(none,[]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(brp_ctx_3_prob,mx,'_uZ29oJdiEeWM7fNBUrLJSw'),identifier(none,'MAX'),integer(none,2))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(brp_ctx_2_prob,'Well-definedness of Axiom',[axiom(surj)],true),po(brp_ctx_2_prob,'Well-definedness of Axiom',[axiom(fix)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_1)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_2)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_3)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_4)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_5)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_6)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_7)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_8)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_9)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_10)],false),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_11)],true),po(brp_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_12)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_11)],true),po(brp_3,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv3_12)],true),po(brp_3,'Guard strengthening (split)',[event('RCV_current_data'),guard(grd2),event('RCV_current_data'),event('RCV_current_data')],true),po(brp_3,'Guard strengthening (split)',[event('RCV_current_data'),guard(grd4),event('RCV_current_data'),event('RCV_current_data')],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_11)],true),po(brp_3,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv3_12)],true),po(brp_3,'Guard strengthening (split)',[event('RCV_success'),guard(grd2),event('RCV_success'),event('RCV_success')],true),po(brp_3,'Guard strengthening (split)',[event('RCV_success'),guard(grd4),event('RCV_success'),event('RCV_success')],true),po(brp_3,'Guard strengthening (split)',[event('RCV_failure'),guard(grd2),event('RCV_failure'),event('RCV_failure')],true),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_9)],true),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_10)],false),po(brp_3,'Invariant preservation',[event('SND_success'),event('SND_success'),invariant(inv3_11)],true),po(brp_3,'Guard strengthening (split)',[event('SND_success'),guard(grd2),event('SND_success'),event('SND_success')],true),po(brp_3,'Guard strengthening (split)',[event('SND_success'),guard(grd4),event('SND_success'),event('SND_success')],true),po(brp_3,'Invariant preservation',[event('SND_failure'),event('SND_failure'),invariant(inv3_9)],true),po(brp_3,'Invariant preservation',[event('SND_failure'),event('SND_failure'),invariant(inv3_10)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_9)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_10)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_11)],true),po(brp_3,'Invariant preservation',[event('SND_rcv_current_ack'),event('SND_rcv_current_ack'),invariant(inv3_12)],true),po(brp_3,'Guard strengthening (split)',[event('SND_rcv_current_ack'),guard(grd2),event('SND_rcv_current_ack'),event('SND_rcv_current_ack')],true),po(brp_3,'Guard strengthening (split)',[event('SND_rcv_current_ack'),guard(grd4),event('SND_rcv_current_ack'),event('SND_rcv_current_ack')],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('SND_snd_current_data'),event('SND_snd_current_data'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('SND_snd_last_data'),event('SND_snd_last_data'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('SND_time_out_current'),event('SND_time_out_current'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('SND_time_out_current'),event('SND_time_out_current'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('SND_time_out_current'),event('SND_time_out_current'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('SND_time_out_current'),event('SND_time_out_current'),invariant(inv3_9)],true),po(brp_3,'Invariant preservation',[event('SND_time_out_current'),event('SND_time_out_current'),invariant(inv3_10)],true),po(brp_3,'Invariant preservation',[event('DMN_data_channel'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('DMN_data_channel'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('DMN_data_channel'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('DMN_data_channel'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('DMN_data_channel'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('DMN_ack_channel'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('DMN_ack_channel'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('DMN_ack_channel'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('DMN_ack_channel'),invariant(inv3_11)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_2)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_11)],true),po(brp_3,'Invariant preservation',[event('RCV_snd_ack'),invariant(inv3_12)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_1)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_3)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_4)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_5)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_6)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_7)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_8)],true),po(brp_3,'Invariant preservation',[event('RCV_rcv_retry'),invariant(inv3_12)],true),po(brp_2,'Well-definedness of Invariant',[invariant(inv2_3)],true),po(brp_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_1)],true),po(brp_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_2)],true),po(brp_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_3)],true),po(brp_2,'Well-definedness of action',[action(act7)],true),po(brp_2,'Invariant preservation',[event('RCV_current_data'),event('RCV_current_data'),invariant(inv2_2)],true),po(brp_2,'Action simulation',[event('RCV_current_data'),action(act2),event('RCV_current_data')],true),po(brp_2,'Invariant preservation',[event('RCV_success'),event('RCV_success'),invariant(inv2_2)],true),po(brp_2,'Action simulation',[event('RCV_success'),action(act3),event('RCV_success')],true),po(brp_2,'Guard strengthening (split)',[event('SND_success'),guard(grd2),event('SND_success'),event('SND_success')],true),po(brp_2,'Invariant preservation',[event('SND_rcv_current_ack'),invariant(inv2_1)],true),po(brp_2,'Invariant preservation',[event('SND_rcv_current_ack'),invariant(inv2_2)],true),po(brp_2,'Invariant preservation',[event('SND_rcv_current_ack'),invariant(inv2_3)],true),po(brp_2,'Invariant preservation',[event('SND_snd_current_data'),invariant(inv2_3)],true),po(brp_2,'Well-definedness of action',[action(act1)],true),po(brp_2,'Invariant preservation',[event('SND_snd_last_data'),invariant(inv2_3)],true),po(brp_2,'Well-definedness of action',[action(act1)],true),po(brp_2,'Invariant preservation',[event('SND_time_out_current'),invariant(inv2_3)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_1)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_2)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_3)],true),po(brp_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_4)],true),po(brp_1,'Action simulation',[event(brp),action(act1),event(brp)],true),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_1)],true),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_2)],false),po(brp_1,'Invariant preservation',[event('RCV_current_data'),invariant(inv1_3)],true),po(brp_1,'Well-definedness of action',[action(act2)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_1)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_2)],false),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_3)],true),po(brp_1,'Invariant preservation',[event('RCV_success'),invariant(inv1_4)],true),po(brp_1,'Well-definedness of action',[action(act3)],true),po(brp_1,'Invariant preservation',[event('RCV_failure'),invariant(inv1_3)],true),po(brp_1,'Invariant preservation',[event('RCV_failure'),invariant(inv1_4)],true),po(brp_1,'Invariant preservation',[event('SND_success'),invariant(inv1_4)],true),po(brp_1,'Invariant preservation',[event('SND_failure'),invariant(inv1_4)],true),po(brp_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(brp_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(brp_0,'Invariant preservation',[event(brp),invariant(inv1)],true),po(brp_0,'Invariant preservation',[event(brp),invariant(inv2)],true),po(brp_0,'Feasibility of action',[action(act1)],true)],_Error)).
+
diff --git a/BRP/brp_3_prob_mch.html b/BRP/brp_3_prob_mch.html
new file mode 100644
index 0000000000000000000000000000000000000000..8cabe066e4e06db53b09dba1cf4a5f6ae4d5067f
--- /dev/null
+++ b/BRP/brp_3_prob_mch.html
@@ -0,0 +1,438 @@
+<!DOCTYPE html>
+<html>
+<head>
+ <!-- html file generated by ProB from a VisB visualization -->
+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
+ <meta http-equiv="content-type" content="text/html; charset=utf-8">
+ <script>
+ function setAttr(id, attribute, value){
+ const obj = document.getElementById(id);
+ if (obj == null) {
+ if (id !== "visb_debug_messages") {
+ console.error("Unknown SVG id " + id + " for attribute " + attribute);
+ }
+ } else if(attribute==="text") {
+ if (obj.closest('foreignObject')) {
+ obj.innerHTML = value;
+ } else {
+ obj.textContent = value;
+ }
+ } else if(attribute==="class" && value !== "") {
+ if(value[0]==="+") {
+ obj.classList.add(value.substring(1));
+ } else if(value[0]==="-") {
+ obj.classList.remove(value.substring(1));
+ } else {
+ obj.setAttribute(attribute, value);
+ }
+ } else {
+ obj.setAttribute(attribute, value);
+ }
+ }
+ function sleep(ms) {
+ return new Promise(resolve => setTimeout(resolve, ms));
+ }
+ let lastSelectedRow = 0;
+ function highlightRow(id) {
+ if (lastSelectedRow>0) {setAttr("row"+lastSelectedRow,"bgcolor","")}
+ if (document.getElementById("row"+id) != null) {
+ setAttr("row"+id,"bgcolor","yellow");
+ lastSelectedRow = id;
+ }
+ }
+ function backStep() {
+ if (lastSelectedRow>1) {
+ const prev = lastSelectedRow - 1;
+ document.getElementById("row"+prev).click();
+ }
+ }
+ function forwardStep() {
+ if (lastSelectedRow>0) {
+ const nxt = lastSelectedRow + 1;
+ const row = document.getElementById("row" + (nxt));
+ if (row != null) { row.click() }
+ }
+ }
+ </script>
+
+ <style>
+ table {
+ font-family: arial, sans-serif;
+ font-size: 11px;
+ border-collapse: collapse;
+ width: 100%;
+ }
+ td, th {
+ border: 1px solid #dddddd;
+ text-align: left;
+ padding: 2px;
+ }
+/*
+ tr:nth-child(even) {
+ background-color: #dddddd;
+ }
+ */
+ </style>
+
+ <style>
+ .collapsible {
+ cursor: pointer;
+ }
+ .collapsible-style {
+ background-color: #777;
+ color: white;
+ padding: 6px;
+ width: 100%;
+ border: none;
+ text-align: left;
+ outline: none;
+ font-size: 12px;
+ }
+
+ .active, .collapsible:hover {
+ background-color: #555;
+ }
+
+ .collapsible:after {
+ content: '\002B';
+ color: white;
+ font-weight: bold;
+ float: right;
+ margin-left: 5px;
+ }
+
+ .active:after {
+ content: "\2212";
+ }
+
+ .coll-content-hid {
+ padding: 0 12px;
+ max-height: 30vh;
+ display: none;
+ overflow: auto;
+ background-color: #f1f1f1;
+ }
+ .coll-content-vis {
+ padding: 0 12px;
+ max-height: 30vh;
+ display: block;
+ overflow: auto;
+ background-color: #f1f1f1;
+ }
+ .visb-messages {
+ text-align: left;
+ outline: none;
+ font-size: 12px;
+ font-family: arial, sans-serif;
+ }
+ .svg-outer-container {
+ width: 100%;
+ height: 100%;
+ overflow: auto;
+ visibility: hidden;
+ resize: vertical;
+ }
+ .svg-inner-container {
+ width: 100%;
+ height: 100%;
+ display: flex;
+ transform-origin: left top;
+ /*cursor: grab;*/
+ }
+ .svg-inner-container:active {
+ cursor: grabbing;
+ }
+ svg {
+ width: 100%;
+ height: 100%;
+ }
+ .seq-chart-container {
+ width: 100%;
+ height: 100%;
+ overflow: auto;
+ resize: vertical;
+ }
+ </style>
+
+
+
+ <script>
+ const differences = [
+ [
+ {id: "visb_debug_messages", attr: "text", val: "Step 1/1, State ID: 5, Event: "},
+ {id: "dcf903643b0cad1b752d514f0e0272cc59db95d8", attr: "fill", val: "brown"},
+ {id: "visb_title__1", attr: "text", val: "Packet at position 2"},
+ {id: "dcf903643b0cad1b752d514f0e0272cc59db95d8", attr: "y", val: "40.0"},
+ {id: "c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4", attr: "fill", val: "olive"},
+ {id: "visb_title__2", attr: "text", val: "Packet at position 3"},
+ {id: "c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4", attr: "y", val: "60.0"},
+ {id: "99852a08e4430cc11bbc4024aecda23e07d97369", attr: "fill", val: "white"},
+ {id: "visb_title__3", attr: "text", val: "Packet at position 4"},
+ {id: "99852a08e4430cc11bbc4024aecda23e07d97369", attr: "y", val: "80.0"},
+ {id: "0dc8c8a9d3ccd4dac8bfba08183049141d24a1db", attr: "fill", val: "white"},
+ {id: "visb_title__4", attr: "text", val: "Packet at position 5"},
+ {id: "0dc8c8a9d3ccd4dac8bfba08183049141d24a1db", attr: "y", val: "100.0"},
+ {id: "8f7d96168b21c39adae40a6b891ffc38476ec068", attr: "fill", val: "green"},
+ {id: "visb_title__5", attr: "text", val: "Packet at position 1"},
+ {id: "8f7d96168b21c39adae40a6b891ffc38476ec068", attr: "y", val: "20.0"},
+ {id: "5fbaf8471f17137d0b5a04be74f971ac446a3b9d", attr: "fill", val: "white"},
+ {id: "visb_title__6", attr: "text", val: "Packet at position 1"},
+ {id: "5fbaf8471f17137d0b5a04be74f971ac446a3b9d", attr: "y", val: "20.0"},
+ {id: "0cb90f31a4b31af152b607c414d1d702bb4ad956", attr: "fill", val: "white"},
+ {id: "visb_title__7", attr: "text", val: "Packet at position 5"},
+ {id: "0cb90f31a4b31af152b607c414d1d702bb4ad956", attr: "y", val: "100.0"},
+ {id: "ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0", attr: "fill", val: "white"},
+ {id: "visb_title__8", attr: "text", val: "Packet at position 4"},
+ {id: "ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0", attr: "y", val: "80.0"},
+ {id: "7673a90e80cf71cc35e50c60c96ceee720e509c3", attr: "fill", val: "white"},
+ {id: "visb_title__9", attr: "text", val: "Packet at position 3"},
+ {id: "7673a90e80cf71cc35e50c60c96ceee720e509c3", attr: "y", val: "60.0"},
+ {id: "b189f6518dc79b567372d086468aa87b56ec1555", attr: "fill", val: "white"},
+ {id: "visb_title__10", attr: "text", val: "Packet at position 2"},
+ {id: "b189f6518dc79b567372d086468aa87b56ec1555", attr: "y", val: "40.0"},
+ {id: "a0028c9b03d87aa039426030a5e3f308bab1d912", attr: "fill", val: "white"},
+ {id: "visb_title__11", attr: "text", val: "Packet at position 4"},
+ {id: "a0028c9b03d87aa039426030a5e3f308bab1d912", attr: "y", val: "80.0"},
+ {id: "f403521da54e936b4c5ac6d1cffa8045c4536ffb", attr: "fill", val: "white"},
+ {id: "visb_title__12", attr: "text", val: "Packet at position 3"},
+ {id: "f403521da54e936b4c5ac6d1cffa8045c4536ffb", attr: "y", val: "60.0"},
+ {id: "6875f825d52a8aa516485ca8edfcaf8e3b4ad35b", attr: "fill", val: "white"},
+ {id: "visb_title__13", attr: "text", val: "Packet at position 2"},
+ {id: "6875f825d52a8aa516485ca8edfcaf8e3b4ad35b", attr: "y", val: "40.0"},
+ {id: "e4c40e27c9cf272e335810e609461f6d5c56773d", attr: "fill", val: "white"},
+ {id: "visb_title__14", attr: "text", val: "Packet at position 5"},
+ {id: "e4c40e27c9cf272e335810e609461f6d5c56773d", attr: "y", val: "100.0"},
+ {id: "b767cf0b58fa58dc23f9f36be265982e806dec52", attr: "fill", val: "green"},
+ {id: "visb_title__15", attr: "text", val: "Packet at position 1"},
+ {id: "b767cf0b58fa58dc23f9f36be265982e806dec52", attr: "y", val: "20.0"},
+ {id: "bVar_ab", attr: "text", val: "TRUE"},
+ {id: "bVar_c", attr: "text", val: "0"},
+ {id: "bVar_d", attr: "text", val: "data1"},
+ {id: "bVar_db", attr: "text", val: "FALSE"},
+ {id: "bVar_g", attr: "text", val: "{}"},
+ {id: "bVar_h", attr: "text", val: "{(1|->data1)}"},
+ {id: "bVar_i", attr: "text", val: "0"},
+ {id: "bVar_l", attr: "text", val: "FALSE"},
+ {id: "bVar_r", attr: "text", val: "1"},
+ {id: "bVar_r_st", attr: "text", val: "working"},
+ {id: "bVar_s", attr: "text", val: "0"},
+ {id: "bVar_s_st", attr: "text", val: "working"},
+ {id: "bVar_v", attr: "text", val: "FALSE"},
+ {id: "bVar_w", attr: "text", val: "FALSE"},
+ ]
+ ]
+
+ const transitions = new Map();
+ for (let j = 0; j < differences.length; j++) {
+ const transitionAttributeValues = new Map();
+ for (let i = 0; i <= j; i++) {
+ const transitionI = differences[i];
+ for (const attrValue of transitionI) {
+ const key = {id: attrValue.id, attr: attrValue.attr};
+ transitionAttributeValues.set(key, attrValue.val);
+ }
+ }
+ transitions.set(j+1, transitionAttributeValues);
+ }
+
+ function replayStep(stepNr) {
+ transitions.get(stepNr).forEach((value, key) => {
+ setAttr(key.id, key.attr, value);
+ });
+ highlightRow(stepNr);
+ }
+
+ async function runAll(delay) {
+ for (let i = 1; i <= transitions.size; i++) {
+ replayStep(i);
+ await sleep(delay);
+ }
+ }
+
+ </script>
+
+ <script> function registerHovers() {} </script>
+ </head>
+<body>
+
+
+ <button type="button" class="collapsible collapsible-style active">SVG Visualisation</button>
+ <div>
+ <div text-align="left" id="visb_svg_outer_container" class="svg-outer-container">
+ <div id="visb_svg_inner_container" class="svg-inner-container">
+<svg xmlns="http://www.w3.org/2000/svg"
+ width="60.0" height="125.0" viewBox="0 0 60.0 125.0" >
+<script>let visb_vars = {};</script>
+ <text id="185c017c3519945db675741b005ddd058ee0e5ea" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
+ <rect id="dcf903643b0cad1b752d514f0e0272cc59db95d8" fill="brown" height="20.0" stroke="black" width="20.0" x="10.0" y="40.0">
+ <title id="visb_title__1">Packet at position 2</title>
+</rect>
+ <text id="21fbf8bea61dfc7508d1536d7e49aee85f7aa6bc" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
+ <rect id="c2e9e97db8eadaa62d715bc87d998e8fd2fe22a4" fill="olive" height="20.0" stroke="black" width="20.0" x="10.0" y="60.0">
+ <title id="visb_title__2">Packet at position 3</title>
+</rect>
+ <text id="668b03895b45f81c53cd13e6a8ce2be6ad1e9b61" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
+ <rect id="99852a08e4430cc11bbc4024aecda23e07d97369" fill="white" height="20.0" stroke="black" width="20.0" x="10.0" y="80.0">
+ <title id="visb_title__3">Packet at position 4</title>
+</rect>
+ <text id="9e57278e1d7bf120da2d1bef7864d939a65c197b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
+ <rect id="0dc8c8a9d3ccd4dac8bfba08183049141d24a1db" fill="white" height="20.0" stroke="black" width="20.0" x="10.0" y="100.0">
+ <title id="visb_title__4">Packet at position 5</title>
+</rect>
+ <text id="acfc5e145aae9a6a80390a9c27f172053824ca63" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="20.0" y="10.0">f</text>
+ <rect id="8f7d96168b21c39adae40a6b891ffc38476ec068" fill="green" height="20.0" stroke="black" width="20.0" x="10.0" y="20.0">
+ <title id="visb_title__5">Packet at position 1</title>
+</rect>
+ <text id="3c145d8704ce2d495bcf484ef6030e0f6361e477" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
+ <rect id="5fbaf8471f17137d0b5a04be74f971ac446a3b9d" fill="white" height="20.0" stroke="black" width="20.0" x="40.0" y="20.0">
+ <title id="visb_title__6">Packet at position 1</title>
+</rect>
+ <text id="66f9ec9c178d2c9393636aff340877e90ad52e20" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
+ <rect id="0cb90f31a4b31af152b607c414d1d702bb4ad956" fill="white" height="20.0" stroke="black" width="20.0" x="40.0" y="100.0">
+ <title id="visb_title__7">Packet at position 5</title>
+</rect>
+ <text id="6c577c7b9481f803c18ae3297a56415a093d067b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
+ <rect id="ef4c7f5c7a96170df87a126c4c1f8b4bc47619d0" fill="white" height="20.0" stroke="black" width="20.0" x="40.0" y="80.0">
+ <title id="visb_title__8">Packet at position 4</title>
+</rect>
+ <text id="7e83e68e85ae62405e98a47bbc8b96b3bfda30ee" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
+ <rect id="7673a90e80cf71cc35e50c60c96ceee720e509c3" fill="white" height="20.0" stroke="black" width="20.0" x="40.0" y="60.0">
+ <title id="visb_title__9">Packet at position 3</title>
+</rect>
+ <text id="e36cfd8dc56c5b35e489917b7427e221de9c5d26" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="50.0" y="10.0">g</text>
+ <rect id="b189f6518dc79b567372d086468aa87b56ec1555" fill="white" height="20.0" stroke="black" width="20.0" x="40.0" y="40.0">
+ <title id="visb_title__10">Packet at position 2</title>
+</rect>
+ <text id="0a6a56bb334abae4f7e4338b2e753441d4438030" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
+ <rect id="a0028c9b03d87aa039426030a5e3f308bab1d912" fill="white" height="20.0" stroke="black" width="20.0" x="70.0" y="80.0">
+ <title id="visb_title__11">Packet at position 4</title>
+</rect>
+ <text id="3aee0fe6e417da9d537d27629417ae588e9d9b6b" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
+ <rect id="f403521da54e936b4c5ac6d1cffa8045c4536ffb" fill="white" height="20.0" stroke="black" width="20.0" x="70.0" y="60.0">
+ <title id="visb_title__12">Packet at position 3</title>
+</rect>
+ <text id="4ebfbc87d748752c9e96d6d2d36883d1be653a67" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
+ <rect id="6875f825d52a8aa516485ca8edfcaf8e3b4ad35b" fill="white" height="20.0" stroke="black" width="20.0" x="70.0" y="40.0">
+ <title id="visb_title__13">Packet at position 2</title>
+</rect>
+ <text id="6fbff960756ae2f6a255f05ea36f74dfe76b28d3" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
+ <rect id="e4c40e27c9cf272e335810e609461f6d5c56773d" fill="white" height="20.0" stroke="black" width="20.0" x="70.0" y="100.0">
+ <title id="visb_title__14">Packet at position 5</title>
+</rect>
+ <text id="ce5ae6be0a3b304d088edf9f6c02bdf6f04330d9" alignment-baseline="center" dominant-baseline="center" font-size="8.0" x="80.0" y="10.0">h</text>
+ <rect id="b767cf0b58fa58dc23f9f36be265982e806dec52" fill="green" height="20.0" stroke="black" width="20.0" x="70.0" y="20.0">
+ <title id="visb_title__15">Packet at position 1</title>
+</rect>
+</svg>
+ </div>
+ </div>
+ </div>
+ <button type="button" class="collapsible collapsible-style">Variables (14)</button>
+<div class="coll-content-hid">
+ <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> </tr>
+
+ <tr id="row_bVar_ab" title="Type: BOOL"> <td>1</td> <td id="name_bVar_ab">ab</td> <td id="bVar_ab">?</td> </tr>
+
+ <tr id="row_bVar_c" title="Type: INT"> <td>2</td> <td id="name_bVar_c">c</td> <td id="bVar_c">?</td> </tr>
+
+ <tr id="row_bVar_d" title="Type: D"> <td>3</td> <td id="name_bVar_d">d</td> <td id="bVar_d">?</td> </tr>
+
+ <tr id="row_bVar_db" title="Type: BOOL"> <td>4</td> <td id="name_bVar_db">db</td> <td id="bVar_db">?</td> </tr>
+
+ <tr id="row_bVar_g" title="Type: (INT<->D)"> <td>5</td> <td id="name_bVar_g">g</td> <td id="bVar_g">?</td> </tr>
+
+ <tr id="row_bVar_h" title="Type: (INT<->D)"> <td>6</td> <td id="name_bVar_h">h</td> <td id="bVar_h">?</td> </tr>
+
+ <tr id="row_bVar_i" title="Type: INT"> <td>7</td> <td id="name_bVar_i">i</td> <td id="bVar_i">?</td> </tr>
+
+ <tr id="row_bVar_l" title="Type: BOOL"> <td>8</td> <td id="name_bVar_l">l</td> <td id="bVar_l">?</td> </tr>
+
+ <tr id="row_bVar_r" title="Type: INT"> <td>9</td> <td id="name_bVar_r">r</td> <td id="bVar_r">?</td> </tr>
+
+ <tr id="row_bVar_r_st" title="Type: STATUS"> <td>10</td> <td id="name_bVar_r_st">r_st</td> <td id="bVar_r_st">?</td> </tr>
+
+ <tr id="row_bVar_s" title="Type: INT"> <td>11</td> <td id="name_bVar_s">s</td> <td id="bVar_s">?</td> </tr>
+
+ <tr id="row_bVar_s_st" title="Type: STATUS"> <td>12</td> <td id="name_bVar_s_st">s_st</td> <td id="bVar_s_st">?</td> </tr>
+
+ <tr id="row_bVar_v" title="Type: BOOL"> <td>13</td> <td id="name_bVar_v">v</td> <td id="bVar_v">?</td> </tr>
+
+ <tr id="row_bVar_w" title="Type: BOOL"> <td>14</td> <td id="name_bVar_w">w</td> <td id="bVar_w">?</td> </tr>
+ </table>
+ </div>
+ <button type="button" class="collapsible-style">Info</button>
+<div class="coll-content-vis visb-messages">
+Generated on 25/11/2024 at 13:53 using <a href="https://prob.hhu.de/">ProB</a> version 1.13.1-nightly
+<br>Main specification file: brp_3_prob_mch.eventb (modified on 25/11/2024 at 13:52)
+<br>Main specification name: brp_3_prob
+<br>Main VisB JSON file: visb_brp.def (modified on 25/11/2024 at 13:51)
+ <script> replayStep(1); </script>
+ </div>
+ <script>
+ registerHovers();
+
+ const collapsibles = document.getElementsByClassName("collapsible");
+ for (let ii = 0; ii < collapsibles.length; ii++) {
+ collapsibles[ii].onclick = function() {
+ this.classList.toggle("active");
+ this.nextElementSibling.style.display = this.classList.contains("active") ? "block" : "none";
+ };
+ }
+
+ const outerContainer = document.getElementById('visb_svg_outer_container');
+ const innerContainer = document.getElementById('visb_svg_inner_container');
+ let scale = 1;
+ let isDragging = false;
+ let startMouseX, startMouseY;
+ let scrollSpeed = 1.03;
+ let minScale = 0.5;
+ let maxScale = 100.0;
+
+ outerContainer.onwheel = (e) => {
+ e.preventDefault();
+ const oldScale = scale;
+ scale *= (e.deltaY < 0) ? scrollSpeed : 1 / scrollSpeed;
+ scale = Math.max(scale, minScale);
+ scale = Math.min(scale, maxScale);
+
+ const rect = outerContainer.getBoundingClientRect();
+ const mouseX = e.clientX - rect.left + outerContainer.scrollLeft;
+ const mouseY = e.clientY - rect.top + outerContainer.scrollTop;
+ const scaleChange = scale / oldScale;
+
+ innerContainer.style.transform = `scale(${scale})`;
+ outerContainer.scrollBy({
+ left: mouseX * (scaleChange - 1),
+ top: mouseY * (scaleChange - 1),
+ behavior: 'instant'
+ });
+ };
+
+ outerContainer.onmousedown = (e) => {
+ isDragging = true;
+ startMouseX = e.clientX;
+ startMouseY = e.clientY;
+ };
+
+ document.onmousemove = (e) => {
+ if (!isDragging) return;
+ const dx = startMouseX - e.clientX;
+ const dy = startMouseY - e.clientY;
+ outerContainer.scrollBy(dx,dy);
+ startMouseX = e.clientX;
+ startMouseY = e.clientY;
+ };
+
+ document.onmouseup = () => isDragging = false;
+ outerContainer.onmouseleave = () => isDragging = false;
+
+ const outerContainerHeight = parseFloat(window.getComputedStyle(outerContainer).height);
+ if (outerContainerHeight > window.innerHeight * 0.7) {
+ outerContainer.style.height = '70vh';
+ }
+ outerContainer.style.visibility = 'visible';
+ </script>
+
+ </body>
+</html>
+
diff --git a/BRP/visb_brp.def b/BRP/visb_brp.def
new file mode 100644
index 0000000000000000000000000000000000000000..363491cb8e52c611097a1096f7de4b06b0635c9b
--- /dev/null
+++ b/BRP/visb_brp.def
@@ -0,0 +1,18 @@
+DEFINITIONS
+ //"LibraryStrings.def";
+ DPWID == 20.0;
+ DOM == 1..5;
+ DPCOL(d) == IF d=data1 THEN "green" ELSIF d=data2 THEN "brown" ELSE "olive" END;
+ DataPacket(name,array,pos,xoffset) ==
+ (rec(svg_class:"text", x:xoffset + 0.5 * DPWID, y:0.5 * DPWID,
+ `alignment-baseline`:"center",
+ `dominant-baseline`:"center", text:name, `font-size`:8.0),
+ rec(svg_class:"rect",x:xoffset, y:real(pos+0)*DPWID, height:DPWID, width:DPWID,
+ fill:IF pos:dom(array) THEN DPCOL(array(pos)) ELSE "white" END,
+ stroke:"black", title:```Packet at position ${pos}```));
+
+ VISB_SVG_BOX == rec(height:DPWID*(1.25+real(max(DOM))),
+ width:DPWID*3.0);
+ VISB_SVG_OBJECTS1 == {(i).i:DOM|DataPacket("f",f,i,0.5*DPWID)};
+ VISB_SVG_OBJECTS2 == {(i).i:DOM|DataPacket("g",g,i,2.0*DPWID)};
+ VISB_SVG_OBJECTS3 == {(i).i:DOM|DataPacket("h",h,i,3.5*DPWID)}