Skip to content
Snippets Groups Projects
Commit 18dc4b26 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

example with new DEFINITION file for Event-B model 


for Abrial’s bounded retransmission protocol

Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent a273eb8f
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
BRP/brp_1_prob_mch.eventb 0 → 100644
+ 2
− 0
View file @ 18dc4b26
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)).
BRP/brp_3_prob_mch.eventb 0 → 100644
+ 2
− 0
View file @ 18dc4b26
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)).
BRP/brp_3_prob_mch.html 0 → 100644
+ 438
− 0
View file @ 18dc4b26
<!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&lt;-&gt;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&lt;-&gt;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>
BRP/visb_brp.def 0 → 100644
+ 18
− 0
View file @ 18dc4b26
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)}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment