Animation error

When I try to animate/model check the machine MultiplePrinters in the attached archive, I get an error (see below).

Rodin does not report any static errors and all the POs are proved.

Michael

de.prob.core.PrologException: ProB reported errors:
Could not infer type of q;;
Could not infer type of q;;
Could not infer type of q1;;
Could not infer type of q2;;
Internal Error; call failed: typecheck_l([subset(rodinpos('MultiplePrinters',inv1,'_dYP0oXqpEeKnYblMwWSB1g'),identifier(none,job),identifier(none,'JOB')),member(rodinpos('MultiplePrinters',inv3,'_dYP0o3qpEeKnYblMwWSB1g'),identifier(none,position),total_function(none,identifier(none,queue),relations(none,identifier(none,'JOB'),identifier(none,'POSITION')))),forall(rodinpos('MultiplePrinters',inv4,'_Alvq4HqvEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),member(none,function(none,identifier(none,position),[identifier(none,q)]),partial_injection(none,identifier(none,job),identifier(none,'POSITION'))))),forall(rodinpos('MultiplePrinters',inv5,'_dYQbsHqpEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),finite(none,range(none,function(none,identifier(none,position),[identifier(none,q)]))))),forall(rodinpos('MultiplePrinters',inv6,'_jBuloHqpEeKnYblMwWSB1g'),[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),identifier(none,queue)),conjunct(none,member(none,identifier(none,q2),identifier(none,queue)),not_equal(none,identifier(none,q1),identifier(none,q2)))),equal(none,intersection(none,domain(none,function(none,identifier(none,position),[identifier(none,q1)])),domain(none,function(none,identifier(none,position),[identifier(none,q2)]))),empty_set(none)))),member(rodinpos('MultiplePrinters',inv7,'_B4RpwHqvEeKnYblMwWSB1g'),identifier(none,document),total_function(none,identifier(none,job),identifier(none,'DOCUMENT'))),member(rodinpos('MultiplePrinters',inv8,'_G3FGEHqvEeKnYblMwWSB1g'),identifier(none,manages),total_injection(none,identifier(none,queue),identifier(none,'PRINTER')))],env(node('PRINTER',entry(set(global('PRINTER')),[nodeid(none),section('C1'),given_set]),1,node('JOB',entry(set(global('JOB')),[nodeid(none),section('C1'),given_set]),0,node('DOCUMENT',entry(set(global('DOCUMENT')),[nodeid(none),section('C1'),given_set]),0,empty,empty),node('POSITION',entry(set(integer),[nodeid(none),section('C1')]),0,empty,empty)),node(job,entry(_472716,[nodeid(none),section('MultiplePrinters'),level(0)]),0,node('USER',entry(set(global('USER')),[nodeid(none),section('C1'),given_set]),0,node('QUEUE',entry(set(global('QUEUE')),[nodeid(none),section('C1'),given_set]),0,empty,empty),node(document,entry(_472701,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty)),node(position,entry(_472746,[nodeid(none),section('MultiplePrinters'),level(0)]),0,node(manages,entry(_472731,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty),node(queue,entry(_472761,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty))))),pred,_472685);;
Internal Error; call failed: check_model(event_b_model(none,'MultiplePrinters',[sees(none,['C1']),variables(none,[identifier(none,document),identifier(none,job),identifier(none,manages),identifier(none,position),identifier(none,queue)]),invariant(none,[subset(rodinpos('MultiplePrinters',inv1,'_dYP0oXqpEeKnYblMwWSB1g'),identifier(none,job),identifier(none,'JOB')),member(rodinpos('MultiplePrinters',inv3,'_dYP0o3qpEeKnYblMwWSB1g'),identifier(none,position),total_function(none,identifier(none,queue),relations(none,identifier(none,'JOB'),identifier(none,'POSITION')))),forall(rodinpos('MultiplePrinters',inv4,'_Alvq4HqvEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),member(none,function(none,identifier(none,position),[identifier(none,q)]),partial_injection(none,identifier(none,job),identifier(none,'POSITION'))))),forall(rodinpos('MultiplePrinters',inv5,'_dYQbsHqpEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),finite(none,range(none,function(none,identifier(none,position),[identifier(none,q)]))))),forall(rodinpos('MultiplePrinters',inv6,'_jBuloHqpEeKnYblMwWSB1g'),[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),identifier(none,queue)),conjunct(none,member(none,identifier(none,q2),identifier(none,queue)),not_equal(none,identifier(none,q1),identifier(none,q2)))),equal(none,intersection(none,domain(none,function(none,identifier(none,position),[identifier(none,q1)])),domain(none,function(none,identifier(none,position),[identifier(none,q2)]))),empty_set(none)))),member(rodinpos('MultiplePrinters',inv7,'_B4RpwHqvEeKnYblMwWSB1g'),identifier(none,document),total_function(none,identifier(none,job),identifier(none,'DOCUMENT'))),member(rodinpos('MultiplePrinters',inv8,'_G3FGEHqvEeKnYblMwWSB1g'),identifier(none,manages),total_injection(none,identifier(none,queue),identifier(none,'PRINTER')))]),theorems(none,[subset(rodinpos('MultiplePrinters',inv2,'_dYP0onqpEeKnYblMwWSB1g'),identifier(none,queue),identifier(none,'QUEUE'))]),events(none,[event(rodinpos('MultiplePrinters','INITIALISATION','_dYQbsXqpEeKnYblMwWSB1g'),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('MultiplePrinters',act1,'_dYQbsnqpEeKnYblMwWSB1g'),[identifier(none,job)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act2,'_dYQbs3qpEeKnYblMwWSB1g'),[identifier(none,position)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act3,'_dYQbtHqpEeKnYblMwWSB1g'),[identifier(none,document)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act4,'_NLOW8HqqEeKnYblMwWSB1g'),[identifier(none,queue)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act5,'_QsIR4HqqEeKnYblMwWSB1g'),[identifier(none,manages)],[empty_set(none)])],[]),event(rodinpos('MultiplePrinters','AddQueue','_XhjX8HqyEeKnYblMwWSB1g'),'AddQueue',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_gJOYYHqyEeKnYblMwWSB1g'),p),identifier(rodinpos('MultiplePrinters',[],'_Xhj_AHqyEeKnYblMwWSB1g'),q)],[not_member(rodinpos('MultiplePrinters',grd1,'_gJOYYXqyEeKnYblMwWSB1g'),identifier(none,q),identifier(none,queue)),not_member(rodinpos('MultiplePrinters',grd2,'_Xhj_AXqyEeKnYblMwWSB1g'),identifier(none,p),range(none,identifier(none,manages)))],[],[assign(rodinpos('MultiplePrinters',act1,'_Xhj_BHqyEeKnYblMwWSB1g'),[identifier(none,queue)],[union(none,identifier(none,queue),set_extension(none,[identifier(none,q)]))]),assign(rodinpos('MultiplePrinters',act2,'_gJOYYnqyEeKnYblMwWSB1g'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(none,[identifier(none,q),empty_set(none)])]))]),assign(rodinpos('MultiplePrinters',act3,'_Xhj_BXqyEeKnYblMwWSB1g'),[identifier(none,manages)],[overwrite(none,identifier(none,manages),set_extension(none,[couple(none,[identifier(none,q),identifier(none,p)])]))])],[]),event(rodinpos('MultiplePrinters','RemoveQueue','_lg8PIHzPEeKzSI8nMkOI1Q'),'RemoveQueue',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_lg82MHzPEeKzSI8nMkOI1Q'),q)],[member(rodinpos('MultiplePrinters',grd1,'_lg82MXzPEeKzSI8nMkOI1Q'),identifier(none,q),identifier(none,queue)),equal(rodinpos('MultiplePrinters',grd2,'_lg9dQHzPEeKzSI8nMkOI1Q'),function(none,identifier(none,position),[identifier(none,q)]),empty_set(none))],[],[assign(rodinpos('MultiplePrinters',act1,'_lg9dQXzPEeKzSI8nMkOI1Q'),[identifier(none,queue)],[set_subtraction(none,identifier(none,queue),set_extension(none,[identifier(none,q)]))]),assign(rodinpos('MultiplePrinters',act2,'_lg-EUHzPEeKzSI8nMkOI1Q'),[identifier(none,position)],[domain_subtraction(none,set_extension(none,[identifier(none,q)]),identifier(none,position))]),assign(rodinpos('MultiplePrinters',act3,'_lg-EUXzPEeKzSI8nMkOI1Q'),[identifier(none,manages)],[domain_subtraction(none,set_extension(none,[identifier(none,q)]),identifier(none,manages))])],[]),event(rodinpos('MultiplePrinters','QueueJob','_vf0kQHw5EeKh_LAbjBe8-w'),'QueueJob',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_vf0kQnw5EeKh_LAbjBe8-w'),d),identifier(rodinpos('MultiplePrinters',[],'_vf0kQXw5EeKh_LAbjBe8-w'),j),identifier(rodinpos('MultiplePrinters',[],'_vf1LUXw5EeKh_LAbjBe8-w'),p),identifier(rodinpos('MultiplePrinters',[],'_vf1LUHw5EeKh_LAbjBe8-w'),q)],[member(rodinpos('MultiplePrinters',grd1,'_vf1LUnw5EeKh_LAbjBe8-w'),identifier(none,j),set_subtraction(none,identifier(none,'JOB'),identifier(none,job))),member(rodinpos('MultiplePrinters',grd3,'_vf1yYXw5EeKh_LAbjBe8-w'),identifier(none,q),identifier(none,queue)),member(rodinpos('MultiplePrinters',grd4,'_vf2ZcHw5EeKh_LAbjBe8-w'),identifier(none,p),set_subtraction(none,identifier(none,'POSITION'),range(none,function(none,identifier(none,position),[identifier(none,q)])))),implication(rodinpos('MultiplePrinters',grd5,'_vf2ZcXw5EeKh_LAbjBe8-w'),not_equal(none,function(none,identifier(none,position),[identifier(none,q)]),empty_set(none)),greater(none,identifier(none,p),max(none,range(none,function(none,identifier(...),[...])))))],[member(rodinpos('MultiplePrinters',grd2,'_vf1yYHw5EeKh_LAbjBe8-w'),identifier(none,d),identifier(none,'DOCUMENT'))],[assign(rodinpos('MultiplePrinters',act1,'_vf3AgHw5EeKh_LAbjBe8-w'),[identifier(none,job)],[union(none,identifier(none,job),set_extension(none,[identifier(none,j)]))]),assign(rodinpos('MultiplePrinters',act2,'_vf3AgXw5EeKh_LAbjBe8-w'),[identifier(none,document)],[overwrite(none,identifier(none,document),set_extension(none,[couple(none,[identifier(...),identifier(...)])]))]),assign(rodinpos('MultiplePrinters',act3,'_vf3Agnw5EeKh_LAbjBe8-w'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(none,[...|...])]))])],[]),event(rodinpos('MultiplePrinters','DeQueueJob','_vf3nkHw5EeKh_LAbjBe8-w'),'DeQueueJob',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_vf4OoHw5EeKh_LAbjBe8-w'),j),identifier(rodinpos('MultiplePrinters',[],'_vf3nkXw5EeKh_LAbjBe8-w'),q)],[member(rodinpos('MultiplePrinters',grd1,'_vf4OoXw5EeKh_LAbjBe8-w'),identifier(none,j),identifier(none,job)),member(rodinpos('MultiplePrinters',grd2,'_vf4Oonw5EeKh_LAbjBe8-w'),identifier(none,q),identifier(none,queue)),member(rodinpos('MultiplePrinters',grd3,'_vf41sHw5EeKh_LAbjBe8-w'),identifier(none,j),domain(none,function(none,identifier(none,position),[identifier(none,q)]))),equal(rodinpos('MultiplePrinters',grd4,'_vf41sXw5EeKh_LAbjBe8-w'),function(none,function(none,identifier(none,position),[identifier(...)]),[identifier(none,j)]),min(none,range(none,function(none,identifier(...),[...]))))],[],[assign(rodinpos('MultiplePrinters',act1,'_vf5cwHw5EeKh_LAbjBe8-w'),[identifier(none,job)],[set_subtraction(none,identifier(none,job),set_extension(none,[identifier(none,j)]))]),assign(rodinpos('MultiplePrinters',act2,'_vf5cwXw5EeKh_LAbjBe8-w'),[identifier(none,document)],[domain_subtraction(none,set_extension(none,[identifier(none,j)]),identifier(none,document))]),assign(rodinpos('MultiplePrinters',act3,'_vf5cwnw5EeKh_LAbjBe8-w'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(...)]))])],[])])]),env(empty),[],[context('C1',[],[b(identifier('DOCUMENT'),set(global('DOCUMENT')),[nodeid(none),section('C1'),given_set]),b(identifier('JOB'),set(global('JOB')),[nodeid(none),section('C1'),given_set]),b(identifier('PRINTER'),set(global('PRINTER')),[nodeid(none),section('C1'),given_set]),b(identifier('QUEUE'),set(global('QUEUE')),[nodeid(none),section('C1'),given_set]),b(identifier('USER'),set(global('USER')),[nodeid(none),section('C1'),given_set])],[b(identifier('POSITION'),set(integer),[nodeid(none),section('C1')])],[],[b(equal(b(identifier('POSITION'),set(integer),[nodeid(none),section('C1')]),b(integer_set('NATURAL'),set(integer),[nodeid(none)])),pred,[nodeid(rodinpos('C1',axm1,'_Bs8vEHqlEeKnYblMwWSB1g'))])],[])],_472657);;
Loading Event-B Model failed; Please submit bug report.b_set_eventb_project_flat;;
Could not infer type of q;;
Could not infer type of q;;
Could not infer type of q1;;
Could not infer type of q2;;
Internal Error; call failed: typecheck_l([subset(rodinpos('MultiplePrinters',inv1,'_dYP0oXqpEeKnYblMwWSB1g'),identifier(none,job),identifier(none,'JOB')),member(rodinpos('MultiplePrinters',inv3,'_dYP0o3qpEeKnYblMwWSB1g'),identifier(none,position),total_function(none,identifier(none,queue),relations(none,identifier(none,'JOB'),identifier(none,'POSITION')))),forall(rodinpos('MultiplePrinters',inv4,'_Alvq4HqvEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),member(none,function(none,identifier(none,position),[identifier(none,q)]),partial_injection(none,identifier(none,job),identifier(none,'POSITION'))))),forall(rodinpos('MultiplePrinters',inv5,'_dYQbsHqpEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),finite(none,range(none,function(none,identifier(none,position),[identifier(none,q)]))))),forall(rodinpos('MultiplePrinters',inv6,'_jBuloHqpEeKnYblMwWSB1g'),[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),identifier(none,queue)),conjunct(none,member(none,identifier(none,q2),identifier(none,queue)),not_equal(none,identifier(none,q1),identifier(none,q2)))),equal(none,intersection(none,domain(none,function(none,identifier(none,position),[identifier(none,q1)])),domain(none,function(none,identifier(none,position),[identifier(none,q2)]))),empty_set(none)))),member(rodinpos('MultiplePrinters',inv7,'_B4RpwHqvEeKnYblMwWSB1g'),identifier(none,document),total_function(none,identifier(none,job),identifier(none,'DOCUMENT'))),member(rodinpos('MultiplePrinters',inv8,'_G3FGEHqvEeKnYblMwWSB1g'),identifier(none,manages),total_injection(none,identifier(none,queue),identifier(none,'PRINTER')))],env(node('PRINTER',entry(set(global('PRINTER')),[nodeid(none),section('C1'),given_set]),1,node('JOB',entry(set(global('JOB')),[nodeid(none),section('C1'),given_set]),0,node('DOCUMENT',entry(set(global('DOCUMENT')),[nodeid(none),section('C1'),given_set]),0,empty,empty),node('POSITION',entry(set(integer),[nodeid(none),section('C1')]),0,empty,empty)),node(job,entry(_472695,[nodeid(none),section('MultiplePrinters'),level(0)]),0,node('USER',entry(set(global('USER')),[nodeid(none),section('C1'),given_set]),0,node('QUEUE',entry(set(global('QUEUE')),[nodeid(none),section('C1'),given_set]),0,empty,empty),node(document,entry(_472680,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty)),node(position,entry(_472725,[nodeid(none),section('MultiplePrinters'),level(0)]),0,node(manages,entry(_472710,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty),node(queue,entry(_472740,[nodeid(none),section('MultiplePrinters'),level(0)]),0,empty,empty))))),pred,_472664);;
Internal Error; call failed: check_model(event_b_model(none,'MultiplePrinters',[sees(none,['C1']),variables(none,[identifier(none,document),identifier(none,job),identifier(none,manages),identifier(none,position),identifier(none,queue)]),invariant(none,[subset(rodinpos('MultiplePrinters',inv1,'_dYP0oXqpEeKnYblMwWSB1g'),identifier(none,job),identifier(none,'JOB')),member(rodinpos('MultiplePrinters',inv3,'_dYP0o3qpEeKnYblMwWSB1g'),identifier(none,position),total_function(none,identifier(none,queue),relations(none,identifier(none,'JOB'),identifier(none,'POSITION')))),forall(rodinpos('MultiplePrinters',inv4,'_Alvq4HqvEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),member(none,function(none,identifier(none,position),[identifier(none,q)]),partial_injection(none,identifier(none,job),identifier(none,'POSITION'))))),forall(rodinpos('MultiplePrinters',inv5,'_dYQbsHqpEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),finite(none,range(none,function(none,identifier(none,position),[identifier(none,q)]))))),forall(rodinpos('MultiplePrinters',inv6,'_jBuloHqpEeKnYblMwWSB1g'),[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),identifier(none,queue)),conjunct(none,member(none,identifier(none,q2),identifier(none,queue)),not_equal(none,identifier(none,q1),identifier(none,q2)))),equal(none,intersection(none,domain(none,function(none,identifier(none,position),[identifier(none,q1)])),domain(none,function(none,identifier(none,position),[identifier(none,q2)]))),empty_set(none)))),member(rodinpos('MultiplePrinters',inv7,'_B4RpwHqvEeKnYblMwWSB1g'),identifier(none,document),total_function(none,identifier(none,job),identifier(none,'DOCUMENT'))),member(rodinpos('MultiplePrinters',inv8,'_G3FGEHqvEeKnYblMwWSB1g'),identifier(none,manages),total_injection(none,identifier(none,queue),identifier(none,'PRINTER')))]),theorems(none,[subset(rodinpos('MultiplePrinters',inv2,'_dYP0onqpEeKnYblMwWSB1g'),identifier(none,queue),identifier(none,'QUEUE'))]),events(none,[event(rodinpos('MultiplePrinters','INITIALISATION','_dYQbsXqpEeKnYblMwWSB1g'),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('MultiplePrinters',act1,'_dYQbsnqpEeKnYblMwWSB1g'),[identifier(none,job)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act2,'_dYQbs3qpEeKnYblMwWSB1g'),[identifier(none,position)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act3,'_dYQbtHqpEeKnYblMwWSB1g'),[identifier(none,document)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act4,'_NLOW8HqqEeKnYblMwWSB1g'),[identifier(none,queue)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act5,'_QsIR4HqqEeKnYblMwWSB1g'),[identifier(none,manages)],[empty_set(none)])],[]),event(rodinpos('MultiplePrinters','AddQueue','_XhjX8HqyEeKnYblMwWSB1g'),'AddQueue',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_gJOYYHqyEeKnYblMwWSB1g'),p),identifier(rodinpos('MultiplePrinters',[],'_Xhj_AHqyEeKnYblMwWSB1g'),q)],[not_member(rodinpos('MultiplePrinters',grd1,'_gJOYYXqyEeKnYblMwWSB1g'),identifier(none,q),identifier(none,queue)),not_member(rodinpos('MultiplePrinters',grd2,'_Xhj_AXqyEeKnYblMwWSB1g'),identifier(none,p),range(none,identifier(none,manages)))],[],[assign(rodinpos('MultiplePrinters',act1,'_Xhj_BHqyEeKnYblMwWSB1g'),[identifier(none,queue)],[union(none,identifier(none,queue),set_extension(none,[identifier(none,q)]))]),assign(rodinpos('MultiplePrinters',act2,'_gJOYYnqyEeKnYblMwWSB1g'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(none,[identifier(none,q),empty_set(none)])]))]),assign(rodinpos('MultiplePrinters',act3,'_Xhj_BXqyEeKnYblMwWSB1g'),[identifier(none,manages)],[overwrite(none,identifier(none,manages),set_extension(none,[couple(none,[identifier(none,q),identifier(none,p)])]))])],[]),event(rodinpos('MultiplePrinters','RemoveQueue','_lg8PIHzPEeKzSI8nMkOI1Q'),'RemoveQueue',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_lg82MHzPEeKzSI8nMkOI1Q'),q)],[member(rodinpos('MultiplePrinters',grd1,'_lg82MXzPEeKzSI8nMkOI1Q'),identifier(none,q),identifier(none,queue)),equal(rodinpos('MultiplePrinters',grd2,'_lg9dQHzPEeKzSI8nMkOI1Q'),function(none,identifier(none,position),[identifier(none,q)]),empty_set(none))],[],[assign(rodinpos('MultiplePrinters',act1,'_lg9dQXzPEeKzSI8nMkOI1Q'),[identifier(none,queue)],[set_subtraction(none,identifier(none,queue),set_extension(none,[identifier(none,q)]))]),assign(rodinpos('MultiplePrinters',act2,'_lg-EUHzPEeKzSI8nMkOI1Q'),[identifier(none,position)],[domain_subtraction(none,set_extension(none,[identifier(none,q)]),identifier(none,position))]),assign(rodinpos('MultiplePrinters',act3,'_lg-EUXzPEeKzSI8nMkOI1Q'),[identifier(none,manages)],[domain_subtraction(none,set_extension(none,[identifier(none,q)]),identifier(none,manages))])],[]),event(rodinpos('MultiplePrinters','QueueJob','_vf0kQHw5EeKh_LAbjBe8-w'),'QueueJob',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_vf0kQnw5EeKh_LAbjBe8-w'),d),identifier(rodinpos('MultiplePrinters',[],'_vf0kQXw5EeKh_LAbjBe8-w'),j),identifier(rodinpos('MultiplePrinters',[],'_vf1LUXw5EeKh_LAbjBe8-w'),p),identifier(rodinpos('MultiplePrinters',[],'_vf1LUHw5EeKh_LAbjBe8-w'),q)],[member(rodinpos('MultiplePrinters',grd1,'_vf1LUnw5EeKh_LAbjBe8-w'),identifier(none,j),set_subtraction(none,identifier(none,'JOB'),identifier(none,job))),member(rodinpos('MultiplePrinters',grd3,'_vf1yYXw5EeKh_LAbjBe8-w'),identifier(none,q),identifier(none,queue)),member(rodinpos('MultiplePrinters',grd4,'_vf2ZcHw5EeKh_LAbjBe8-w'),identifier(none,p),set_subtraction(none,identifier(none,'POSITION'),range(none,function(none,identifier(none,position),[identifier(none,q)])))),implication(rodinpos('MultiplePrinters',grd5,'_vf2ZcXw5EeKh_LAbjBe8-w'),not_equal(none,function(none,identifier(none,position),[identifier(none,q)]),empty_set(none)),greater(none,identifier(none,p),max(none,range(none,function(none,identifier(...),[...])))))],[member(rodinpos('MultiplePrinters',grd2,'_vf1yYHw5EeKh_LAbjBe8-w'),identifier(none,d),identifier(none,'DOCUMENT'))],[assign(rodinpos('MultiplePrinters',act1,'_vf3AgHw5EeKh_LAbjBe8-w'),[identifier(none,job)],[union(none,identifier(none,job),set_extension(none,[identifier(none,j)]))]),assign(rodinpos('MultiplePrinters',act2,'_vf3AgXw5EeKh_LAbjBe8-w'),[identifier(none,document)],[overwrite(none,identifier(none,document),set_extension(none,[couple(none,[identifier(...),identifier(...)])]))]),assign(rodinpos('MultiplePrinters',act3,'_vf3Agnw5EeKh_LAbjBe8-w'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(none,[...|...])]))])],[]),event(rodinpos('MultiplePrinters','DeQueueJob','_vf3nkHw5EeKh_LAbjBe8-w'),'DeQueueJob',ordinary(none),[],[identifier(rodinpos('MultiplePrinters',[],'_vf4OoHw5EeKh_LAbjBe8-w'),j),identifier(rodinpos('MultiplePrinters',[],'_vf3nkXw5EeKh_LAbjBe8-w'),q)],[member(rodinpos('MultiplePrinters',grd1,'_vf4OoXw5EeKh_LAbjBe8-w'),identifier(none,j),identifier(none,job)),member(rodinpos('MultiplePrinters',grd2,'_vf4Oonw5EeKh_LAbjBe8-w'),identifier(none,q),identifier(none,queue)),member(rodinpos('MultiplePrinters',grd3,'_vf41sHw5EeKh_LAbjBe8-w'),identifier(none,j),domain(none,function(none,identifier(none,position),[identifier(none,q)]))),equal(rodinpos('MultiplePrinters',grd4,'_vf41sXw5EeKh_LAbjBe8-w'),function(none,function(none,identifier(none,position),[identifier(...)]),[identifier(none,j)]),min(none,range(none,function(none,identifier(...),[...]))))],[],[assign(rodinpos('MultiplePrinters',act1,'_vf5cwHw5EeKh_LAbjBe8-w'),[identifier(none,job)],[set_subtraction(none,identifier(none,job),set_extension(none,[identifier(none,j)]))]),assign(rodinpos('MultiplePrinters',act2,'_vf5cwXw5EeKh_LAbjBe8-w'),[identifier(none,document)],[domain_subtraction(none,set_extension(none,[identifier(none,j)]),identifier(none,document))]),assign(rodinpos('MultiplePrinters',act3,'_vf5cwnw5EeKh_LAbjBe8-w'),[identifier(none,position)],[overwrite(none,identifier(none,position),set_extension(none,[couple(...)]))])],[])])]),env(empty),[],[context('C1',[],[b(identifier('DOCUMENT'),set(global('DOCUMENT')),[nodeid(none),section('C1'),given_set]),b(identifier('JOB'),set(global('JOB')),[nodeid(none),section('C1'),given_set]),b(identifier('PRINTER'),set(global('PRINTER')),[nodeid(none),section('C1'),given_set]),b(identifier('QUEUE'),set(global('QUEUE')),[nodeid(none),section('C1'),given_set]),b(identifier('USER'),set(global('USER')),[nodeid(none),section('C1'),given_set])],[b(identifier('POSITION'),set(integer),[nodeid(none),section('C1')])],[],[b(equal(b(identifier('POSITION'),set(integer),[nodeid(none),section('C1')]),b(integer_set('NATURAL'),set(integer),[nodeid(none)])),pred,[nodeid(rodinpos('C1',axm1,'_Bs8vEHqlEeKnYblMwWSB1g'))])],[])],_472636);;
Loading Event-B Model failed; Please submit bug report.b_set_eventb_project_flat;;