1 package(load_event_b_project([event_b_model(none,'Model_Machine_4',[sees(none,['PurchaseOrder_Context']),variables(none,[identifier(none,'Invoice_Var'),identifier(none,'PO_Var'),identifier(none,flow01),identifier(none,flow02),identifier(none,flow03),identifier(none,link1),identifier(none,link2),identifier(none,sequ0),identifier(none,sequ1),identifier(none,sequ2),identifier(none,sequ3),identifier(none,shippingInfo_Var),identifier(none,shippingRequest_Var),identifier(none,shippingSchedule_Var)]),invariant(none,[subset(rodinpos(inv0,inv0),identifier(none,'PO_Var'),identifier(none,'POMessage')),less_equal(rodinpos(inv1,inv1),card(none,identifier(none,'PO_Var')),integer(none,1)),subset(rodinpos(inv2,inv2),identifier(none,'Invoice_Var'),identifier(none,'InvMessage')),less_equal(rodinpos(inv3,inv3),card(none,identifier(none,'Invoice_Var')),integer(none,1)),subset(rodinpos(inv4,inv4),identifier(none,shippingRequest_Var),identifier(none,shippingRequestMessage)),less_equal(rodinpos(inv5,inv5),card(none,identifier(none,shippingRequest_Var)),integer(none,1)),subset(rodinpos(inv6,inv6),identifier(none,shippingInfo_Var),identifier(none,shippingInfoMessage)),less_equal(rodinpos(inv7,inv7),card(none,identifier(none,shippingInfo_Var)),integer(none,1)),subset(rodinpos(inv8,inv8),identifier(none,shippingSchedule_Var),identifier(none,scheduleMessage)),less_equal(rodinpos(inv9,inv9),card(none,identifier(none,shippingSchedule_Var)),integer(none,1)),member(rodinpos(inv10,inv10),identifier(none,sequ0),set_extension(none,[integer(none,0),integer(none,1),integer(none,2),integer(none,3)])),member(rodinpos(inv11,inv11),identifier(none,flow01),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(inv12,inv12),identifier(none,sequ1),set_extension(none,[integer(none,0),integer(none,1),integer(none,2),integer(none,3)])),member(rodinpos(inv13,inv13),identifier(none,flow02),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(inv14,inv14),identifier(none,sequ2),set_extension(none,[integer(none,0),integer(none,1),integer(none,2),integer(none,3)])),member(rodinpos(inv15,inv15),identifier(none,flow03),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(inv16,inv16),identifier(none,sequ3),set_extension(none,[integer(none,0),integer(none,1),integer(none,2)])),member(rodinpos(inv17,shippingSchedule_Vav),identifier(none,link1),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(inv18,shippingSchedule_Vaw),identifier(none,link2),set_extension(none,[integer(none,0),integer(none,1)])),equivalence(rodinpos(prop1,shippingSchedule_Vax),less_equal(none,identifier(none,sequ0),integer(none,2)),not_equal(none,identifier(none,'PO_Var'),empty_set(none))),equivalence(rodinpos(prop2,shippingSchedule_Vay),less_equal(none,identifier(none,sequ1),integer(none,2)),not_equal(none,identifier(none,shippingRequest_Var),empty_set(none))),equivalence(rodinpos(prop3,shippingSchedule_Vaz),less_equal(none,identifier(none,sequ1),integer(none,1)),conjunct(none,equal(none,identifier(none,link1),integer(none,0)),not_equal(none,identifier(none,shippingInfo_Var),empty_set(none)))),equivalence(rodinpos(prop4,'shippingSchedule_Va{'),equal(none,identifier(none,link1),integer(none,0)),not_equal(none,identifier(none,shippingInfo_Var),empty_set(none))),equivalence(rodinpos(prop5,'shippingSchedule_Va|'),equal(none,identifier(none,sequ1),integer(none,0)),conjunct(none,equal(none,identifier(none,link2),integer(none,0)),not_equal(none,identifier(none,shippingSchedule_Var),empty_set(none)))),equivalence(rodinpos(prop6,'shippingSchedule_Va}'),equal(none,identifier(none,link2),integer(none,0)),not_equal(none,identifier(none,shippingSchedule_Var),empty_set(none))),equivalence(rodinpos(prop7,'shippingSchedule_Va~'),equal(none,identifier(none,sequ2),integer(none,0)),not_equal(none,identifier(none,'Invoice_Var'),empty_set(none))),implication(rodinpos(prop11,'shippingSchedule_Vb*'),less_equal(none,identifier(none,sequ2),integer(none,1)),equal(none,identifier(none,link1),integer(none,0))),implication(rodinpos(prop12,'shippingSchedule_Vb+'),equal(none,identifier(none,sequ3),integer(none,0)),equal(none,identifier(none,link2),integer(none,0))),implication(rodinpos(prop13,'shippingSchedule_Vb,'),equal(none,identifier(none,sequ0),integer(none,3)),conjunct(none,equal(none,identifier(none,flow01),integer(none,1)),conjunct(none,equal(none,identifier(none,flow02),integer(none,1)),equal(none,identifier(none,flow03),integer(none,1))))),implication(rodinpos(prop14,'shippingSchedule_Vb-'),member(none,identifier(none,sequ0),set_extension(none,[integer(none,0),integer(none,1)])),conjunct(none,equal(none,identifier(none,flow01),integer(none,0)),conjunct(none,equal(none,identifier(none,flow02),integer(none,0)),equal(none,identifier(none,flow03),integer(none,0))))),implication(rodinpos(prop15,'shippingSchedule_Vb.'),equal(none,identifier(none,flow01),integer(none,0)),equal(none,identifier(none,sequ1),integer(none,0))),implication(rodinpos(prop16,'shippingSchedule_Vb/'),equal(none,identifier(none,flow02),integer(none,0)),equal(none,identifier(none,sequ2),integer(none,0))),implication(rodinpos(prop17,shippingSchedule_Vb0),equal(none,identifier(none,flow03),integer(none,0)),equal(none,identifier(none,sequ3),integer(none,0))),implication(rodinpos(prop18,shippingSchedule_Vb1),equal(none,identifier(none,sequ0),integer(none,3)),conjunct(none,equal(none,identifier(none,sequ1),integer(none,3)),conjunct(none,equal(none,identifier(none,sequ2),integer(none,3)),equal(none,identifier(none,sequ3),integer(none,2))))),implication(rodinpos(prop19,shippingSchedule_Vb2),less_equal(none,identifier(none,sequ2),integer(none,1)),equal(none,identifier(none,link1),integer(none,0))),implication(rodinpos(prop20,shippingSchedule_Vb3),equal(none,identifier(none,sequ3),integer(none,0)),equal(none,identifier(none,link2),integer(none,0)))]),theorems(none,[]),variant(none,add(none,identifier(none,sequ0),add(none,identifier(none,flow01),add(none,identifier(none,sequ1),add(none,identifier(none,flow02),add(none,identifier(none,sequ2),add(none,identifier(none,flow03),add(none,identifier(none,sequ3),add(none,identifier(none,link1),identifier(none,link2)))))))))),events(none,[event(rodinpos('INITIALISATION',shippingSchedule_Vas),'INITIALISATION',ordinary(none),[],[],[],[assign(rodinpos(act1,'\''),[identifier(none,'PO_Var')],[empty_set(none)]),assign(rodinpos(act2,'('),[identifier(none,'Invoice_Var')],[empty_set(none)]),assign(rodinpos(act3,')'),[identifier(none,shippingRequest_Var)],[empty_set(none)]),assign(rodinpos(act4,'*'),[identifier(none,shippingInfo_Var)],[empty_set(none)]),assign(rodinpos(act5,'+'),[identifier(none,shippingSchedule_Var)],[empty_set(none)]),assign(rodinpos(act6,','),[identifier(none,sequ0)],[integer(none,3)]),assign(rodinpos(act7,'-'),[identifier(none,flow01)],[integer(none,1)]),assign(rodinpos(act8,'.'),[identifier(none,flow02)],[integer(none,1)]),assign(rodinpos(act9,'/'),[identifier(none,flow03)],[integer(none,1)]),assign(rodinpos(act10,'0'),[identifier(none,sequ1)],[integer(none,3)]),assign(rodinpos(act11,'1'),[identifier(none,sequ2)],[integer(none,3)]),assign(rodinpos(act12,'2'),[identifier(none,sequ3)],[integer(none,2)]),assign(rodinpos(act13,'3'),[identifier(none,link1)],[integer(none,1)]),assign(rodinpos(act14,'4'),[identifier(none,link2)],[integer(none,1)])],[]),event(rodinpos('Purchase_Order_Process','Purchase_Order_Process'),'Purchase_Order_Process',ordinary(none),[],[],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,0))],[],[]),event(rodinpos('Receive_Order','Receive_Order'),'Receive_Order',convergent(none),[],[identifier(rodinpos([],receive),receive)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,3)),member(rodinpos('Guard1','Guard1'),identifier(none,receive),domain(none,identifier(none,sendPurchaseOrder)))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,'PO_Var')],[set_extension(none,[identifier(none,receive)])]),assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ0)],[minus(none,identifier(none,sequ0),integer(none,1))])],[]),event(rodinpos('Purchase_Order_Processing','Purchase_Order_Processing'),'Purchase_Order_Processing',convergent(none),[],[],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow01),integer(none,0)),equal(rodinpos('Guard2','Guard2'),identifier(none,flow02),integer(none,0)),equal(rodinpos('Guard3','Guard3'),identifier(none,flow03),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,sequ0)],[minus(none,identifier(none,sequ0),integer(none,1))])],[]),event(rodinpos('Arrange_Logistics','Arrange_Logistics'),'Arrange_Logistics',convergent(none),[],[],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow01),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ1),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,flow01)],[minus(none,identifier(none,flow01),integer(none,1))])],[]),event(rodinpos('Assign_Customer_Info','Assign_Customer_Info'),'Assign_Customer_Info',convergent(none),[],[identifier(rodinpos([],from_0),from_0),identifier(rodinpos([],to_0),to_0)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow01),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ1),integer(none,3)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,'PO_Var'),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,from_0),identifier(none,'PO_Var')),member(rodinpos('Guard5','Guard6'),identifier(none,to_0),identifier(none,shippingRequestMessage)),equal(rodinpos('Guard6','Guard7'),function(none,identifier(none,customerInfo_SRM),[identifier(none,to_0)]),function(none,identifier(none,customerInfo_PM),[identifier(none,from_0)]))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,shippingRequest_Var)],[set_extension(none,[identifier(none,to_0)])]),assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ1)],[minus(none,identifier(none,sequ1),integer(none,1))])],[]),event(rodinpos('Request_Shipping','Request_Shipping'),'Request_Shipping',convergent(none),[],[identifier(rodinpos([],in),in)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow01),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ1),integer(none,2)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,shippingRequest_Var),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,in),identifier(none,shippingRequest_Var))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,shippingInfo_Var)],[set_extension(none,[function(none,identifier(none,requestShipping),[identifier(none,in)])])]),assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ1)],[minus(none,identifier(none,sequ1),integer(none,1))]),assign(rodinpos(act1,ouu),[identifier(none,link1)],[integer(none,0)])],[]),event(rodinpos('Receive_Schedule','Receive_Schedule'),'Receive_Schedule',convergent(none),[],[identifier(rodinpos([],receive),receive)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow01),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ1),integer(none,1)),member(rodinpos('Guard3','Guard3'),identifier(none,receive),domain(none,identifier(none,sendSchedule)))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,shippingSchedule_Var)],[set_extension(none,[identifier(none,receive)])]),assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ1)],[minus(none,identifier(none,sequ1),integer(none,1))]),assign(rodinpos(act1,receivf),[identifier(none,link2)],[integer(none,0)])],[]),event(rodinpos('Compute_Price','Compute_Price'),'Compute_Price',convergent(none),[],[],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow02),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ2),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,flow02)],[minus(none,identifier(none,flow02),integer(none,1))])],[]),event(rodinpos('Initiate_Price_Calculation','Initiate_Price_Calculation'),'Initiate_Price_Calculation',convergent(none),[],[identifier(rodinpos([],in),in)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow02),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ2),integer(none,3)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,'PO_Var'),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,in),identifier(none,'PO_Var'))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,sequ2)],[minus(none,identifier(none,sequ2),integer(none,1))])],[]),event(rodinpos('Complete_Price_Calculation','Complete_Price_Calculation'),'Complete_Price_Calculation',convergent(none),[],[identifier(rodinpos([],in),in)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow02),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ2),integer(none,2)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,shippingInfo_Var),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,in),identifier(none,shippingInfo_Var)),equal(rodinpos(grd1,ouu),identifier(none,link1),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,sequ2)],[minus(none,identifier(none,sequ2),integer(none,1))])],[]),event(rodinpos('Receive_Invoice','Receive_Invoice'),'Receive_Invoice',convergent(none),[],[identifier(rodinpos([],receive),receive)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow02),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ2),integer(none,1)),member(rodinpos('Guard3','Guard3'),identifier(none,receive),domain(none,identifier(none,sendInvoice)))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,'Invoice_Var')],[set_extension(none,[identifier(none,receive)])]),assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ2)],[minus(none,identifier(none,sequ2),integer(none,1))])],[]),event(rodinpos('Production_Scheduling','Production_Scheduling'),'Production_Scheduling',convergent(none),[],[],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow03),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ3),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,flow03)],[minus(none,identifier(none,flow03),integer(none,1))])],[]),event(rodinpos('Initiate_Production_Scheduling','Initiate_Production_Scheduling'),'Initiate_Production_Scheduling',convergent(none),[],[identifier(rodinpos([],in),in)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow03),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ3),integer(none,2)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,'PO_Var'),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,in),identifier(none,'PO_Var'))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,sequ3)],[minus(none,identifier(none,sequ3),integer(none,1))])],[]),event(rodinpos('Complete_Production_Scheduling','Complete_Production_Scheduling'),'Complete_Production_Scheduling',convergent(none),[],[identifier(rodinpos([],in),in)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,2)),equal(rodinpos('Guard1','Guard1'),identifier(none,flow03),integer(none,1)),equal(rodinpos('Guard2','Guard2'),identifier(none,sequ3),integer(none,1)),not_equal(rodinpos('Guard3','Guard3'),identifier(none,shippingSchedule_Var),empty_set(none)),member(rodinpos('Guard4','Guard4'),identifier(none,in),identifier(none,shippingSchedule_Var)),equal(rodinpos(grd1,ouu),identifier(none,link2),integer(none,0))],[assign(rodinpos('Sub0','Sub0'),[identifier(none,sequ3)],[minus(none,identifier(none,sequ3),integer(none,1))])],[]),event(rodinpos('Reply_Invoice','Reply_Invoice'),'Reply_Invoice',convergent(none),[],[identifier(rodinpos([],reply),reply)],[equal(rodinpos('Guard0','Guard0'),identifier(none,sequ0),integer(none,1)),not_equal(rodinpos('Guard1','Guard1'),identifier(none,'Invoice_Var'),empty_set(none)),member(rodinpos('Guard2','Guard2'),identifier(none,reply),range(none,identifier(none,sendPurchaseOrder))),member(rodinpos('Guard3','Guard3'),identifier(none,reply),identifier(none,'Invoice_Var'))],[assign(rodinpos('Sub1','Sub1'),[identifier(none,sequ0)],[minus(none,identifier(none,sequ0),integer(none,1))])],[])])])],[event_b_context(none,'PurchaseOrder_Context',[extends(none,[]),constants(none,[identifier(none,'IVC_IM'),identifier(none,customerInfo_PM),identifier(none,customerInfo_SRM),identifier(none,initiatePriceCalculation),identifier(none,problemInfo),identifier(none,purchaseOrder_PM),identifier(none,requestProductionScheduling),identifier(none,requestShipping),identifier(none,schedule_SM),identifier(none,sendInvoice),identifier(none,sendPurchaseOrder),identifier(none,sendSchedule),identifier(none,sendShippingPrice),identifier(none,sendShippingSchedule),identifier(none,shippingInfo_SIM)]),axioms(none,[not_equal(rodinpos(axi0,axi0),identifier(none,'Void'),empty_set(none)),finite(rodinpos(axi1,axi1),identifier(none,'Void')),not_equal(rodinpos(axi2,axi2),identifier(none,shippingRequestMessage),empty_set(none)),finite(rodinpos(axi3,axi3),identifier(none,shippingRequestMessage)),member(rodinpos(axi4,axi4),identifier(none,customerInfo_SRM),total_function(none,identifier(none,shippingRequestMessage),identifier(none,customerInfoType))),not_equal(rodinpos(axi5,axi5),identifier(none,shippingInfoMessage),empty_set(none)),finite(rodinpos(axi6,axi6),identifier(none,shippingInfoMessage)),member(rodinpos(axi7,axi7),identifier(none,shippingInfo_SIM),total_function(none,identifier(none,shippingInfoMessage),identifier(none,shippingInfoType))),not_equal(rodinpos(axi8,axi8),identifier(none,scheduleMessage),empty_set(none)),finite(rodinpos(axi9,axi9),identifier(none,scheduleMessage)),member(rodinpos(axi10,axi10),identifier(none,schedule_SM),total_function(none,identifier(none,scheduleMessage),identifier(none,scheduleInfoType))),not_equal(rodinpos(axi11,axi11),identifier(none,'POMessage'),empty_set(none)),finite(rodinpos(axi12,axi12),identifier(none,'POMessage')),member(rodinpos(axi13,axi13),identifier(none,customerInfo_PM),total_function(none,identifier(none,'POMessage'),identifier(none,customerInfoType))),member(rodinpos(axi14,axi14),identifier(none,purchaseOrder_PM),total_function(none,identifier(none,'POMessage'),identifier(none,purchaseOrderType))),not_equal(rodinpos(axi15,axi15),identifier(none,'InvMessage'),empty_set(none)),finite(rodinpos(axi16,axi16),identifier(none,'InvMessage')),member(rodinpos(axi17,axi17),identifier(none,'IVC_IM'),total_function(none,identifier(none,'InvMessage'),identifier(none,'InvoiceType'))),not_equal(rodinpos(axi18,axi18),identifier(none,orderFault),empty_set(none)),finite(rodinpos(axi19,axi19),identifier(none,orderFault)),member(rodinpos(axi20,axi20),identifier(none,problemInfo),total_function(none,identifier(none,orderFault),identifier(none,orderFaultType))),member(rodinpos(axi21,axi21),identifier(none,sendPurchaseOrder),total_function(none,identifier(none,'POMessage'),identifier(none,'InvMessage'))),member(rodinpos(axi22,axi22),identifier(none,sendInvoice),total_function(none,identifier(none,'InvMessage'),identifier(none,'Void'))),member(rodinpos(axi23,axi23),identifier(none,sendSchedule),total_function(none,identifier(none,scheduleMessage),identifier(none,'Void'))),member(rodinpos(axi24,axi24),identifier(none,initiatePriceCalculation),total_function(none,identifier(none,'POMessage'),identifier(none,'Void'))),member(rodinpos(axi25,axi25),identifier(none,sendShippingPrice),total_function(none,identifier(none,shippingInfoMessage),identifier(none,'Void'))),member(rodinpos(axi26,axi26),identifier(none,requestShipping),total_function(none,identifier(none,shippingRequestMessage),identifier(none,shippingInfoMessage))),member(rodinpos(axi27,axi27),identifier(none,requestProductionScheduling),total_function(none,identifier(none,'POMessage'),identifier(none,'Void'))),member(rodinpos(axi28,axi28),identifier(none,sendShippingSchedule),total_function(none,identifier(none,scheduleMessage),identifier(none,'Void'))),equal(rodinpos(prop1,shippingRequestMessagf),domain(none,identifier(none,sendInvoice)),range(none,identifier(none,sendPurchaseOrder)))]),theorems(none,[]),sets(none,[deferred_set(none,'InvMessage'),deferred_set(none,'InvoiceType'),deferred_set(none,'POMessage'),deferred_set(none,'Void'),deferred_set(none,customerInfoType),deferred_set(none,orderFault),deferred_set(none,orderFaultType),deferred_set(none,purchaseOrderType),deferred_set(none,scheduleInfoType),deferred_set(none,scheduleMessage),deferred_set(none,shippingInfoMessage),deferred_set(none,shippingInfoType),deferred_set(none,shippingRequestMessage)])])],[discharged('Model_Machine_4','INITIALISATION',inv1),discharged('Model_Machine_4','INITIALISATION',inv3),discharged('Model_Machine_4','INITIALISATION',inv5),discharged('Model_Machine_4','INITIALISATION',inv7),discharged('Model_Machine_4','INITIALISATION',inv9),discharged('Model_Machine_4','INITIALISATION',inv10),discharged('Model_Machine_4','INITIALISATION',inv11),discharged('Model_Machine_4','INITIALISATION',inv12),discharged('Model_Machine_4','INITIALISATION',inv13),discharged('Model_Machine_4','INITIALISATION',inv14),discharged('Model_Machine_4','INITIALISATION',inv15),discharged('Model_Machine_4','INITIALISATION',inv16),discharged('Model_Machine_4','INITIALISATION',inv17),discharged('Model_Machine_4','INITIALISATION',inv18),discharged('Model_Machine_4','INITIALISATION',prop1),discharged('Model_Machine_4','INITIALISATION',prop2),discharged('Model_Machine_4','INITIALISATION',prop3),discharged('Model_Machine_4','INITIALISATION',prop4),discharged('Model_Machine_4','INITIALISATION',prop5),discharged('Model_Machine_4','INITIALISATION',prop6),discharged('Model_Machine_4','INITIALISATION',prop7),discharged('Model_Machine_4','INITIALISATION',prop11),discharged('Model_Machine_4','INITIALISATION',prop12),discharged('Model_Machine_4','INITIALISATION',prop13),discharged('Model_Machine_4','INITIALISATION',prop14),discharged('Model_Machine_4','INITIALISATION',prop15),discharged('Model_Machine_4','INITIALISATION',prop16),discharged('Model_Machine_4','INITIALISATION',prop17),discharged('Model_Machine_4','INITIALISATION',prop18),discharged('Model_Machine_4','INITIALISATION',prop19),discharged('Model_Machine_4','INITIALISATION',prop20),discharged('Model_Machine_4','Receive_Order',inv1),discharged('Model_Machine_4','Receive_Order',inv10),discharged('Model_Machine_4','Receive_Order',prop1),discharged('Model_Machine_4','Receive_Order',prop13),discharged('Model_Machine_4','Receive_Order',prop14),discharged('Model_Machine_4','Receive_Order',prop18),discharged('Model_Machine_4','Purchase_Order_Processing',inv10),discharged('Model_Machine_4','Purchase_Order_Processing',prop1),discharged('Model_Machine_4','Purchase_Order_Processing',prop13),discharged('Model_Machine_4','Purchase_Order_Processing',prop14),discharged('Model_Machine_4','Purchase_Order_Processing',prop18),discharged('Model_Machine_4','Arrange_Logistics',inv11),discharged('Model_Machine_4','Arrange_Logistics',prop13),discharged('Model_Machine_4','Arrange_Logistics',prop14),discharged('Model_Machine_4','Arrange_Logistics',prop15),discharged('Model_Machine_4','Assign_Customer_Info',inv5),discharged('Model_Machine_4','Assign_Customer_Info',inv12),discharged('Model_Machine_4','Assign_Customer_Info',prop2),discharged('Model_Machine_4','Assign_Customer_Info',prop3),discharged('Model_Machine_4','Assign_Customer_Info',prop5),discharged('Model_Machine_4','Assign_Customer_Info',prop15),discharged('Model_Machine_4','Assign_Customer_Info',prop18),discharged('Model_Machine_4','Request_Shipping',inv7),discharged('Model_Machine_4','Request_Shipping',inv12),discharged('Model_Machine_4','Request_Shipping',inv17),discharged('Model_Machine_4','Request_Shipping',prop2),discharged('Model_Machine_4','Request_Shipping',prop3),discharged('Model_Machine_4','Request_Shipping',prop4),discharged('Model_Machine_4','Request_Shipping',prop5),discharged('Model_Machine_4','Request_Shipping',prop11),discharged('Model_Machine_4','Request_Shipping',prop15),discharged('Model_Machine_4','Request_Shipping',prop18),discharged('Model_Machine_4','Request_Shipping',prop19),discharged('Model_Machine_4','Receive_Schedule',inv9),discharged('Model_Machine_4','Receive_Schedule',inv12),discharged('Model_Machine_4','Receive_Schedule',inv18),discharged('Model_Machine_4','Receive_Schedule',prop2),discharged('Model_Machine_4','Receive_Schedule',prop3),discharged('Model_Machine_4','Receive_Schedule',prop5),discharged('Model_Machine_4','Receive_Schedule',prop6),discharged('Model_Machine_4','Receive_Schedule',prop12),discharged('Model_Machine_4','Receive_Schedule',prop15),discharged('Model_Machine_4','Receive_Schedule',prop18),discharged('Model_Machine_4','Receive_Schedule',prop20),discharged('Model_Machine_4','Compute_Price',inv13),discharged('Model_Machine_4','Compute_Price',prop13),discharged('Model_Machine_4','Compute_Price',prop14),discharged('Model_Machine_4','Compute_Price',prop16),discharged('Model_Machine_4','Initiate_Price_Calculation',inv14),discharged('Model_Machine_4','Initiate_Price_Calculation',prop7),discharged('Model_Machine_4','Initiate_Price_Calculation',prop11),discharged('Model_Machine_4','Initiate_Price_Calculation',prop16),discharged('Model_Machine_4','Initiate_Price_Calculation',prop18),discharged('Model_Machine_4','Initiate_Price_Calculation',prop19),discharged('Model_Machine_4','Complete_Price_Calculation',inv14),discharged('Model_Machine_4','Complete_Price_Calculation',prop7),discharged('Model_Machine_4','Complete_Price_Calculation',prop11),discharged('Model_Machine_4','Complete_Price_Calculation',prop16),discharged('Model_Machine_4','Complete_Price_Calculation',prop18),discharged('Model_Machine_4','Complete_Price_Calculation',prop19),discharged('Model_Machine_4','Receive_Invoice',inv3),discharged('Model_Machine_4','Receive_Invoice',inv14),discharged('Model_Machine_4','Receive_Invoice',prop7),discharged('Model_Machine_4','Receive_Invoice',prop11),discharged('Model_Machine_4','Receive_Invoice',prop16),discharged('Model_Machine_4','Receive_Invoice',prop18),discharged('Model_Machine_4','Receive_Invoice',prop19),discharged('Model_Machine_4','Production_Scheduling',inv15),discharged('Model_Machine_4','Production_Scheduling',prop13),discharged('Model_Machine_4','Production_Scheduling',prop14),discharged('Model_Machine_4','Production_Scheduling',prop17),discharged('Model_Machine_4','Initiate_Production_Scheduling',inv16),discharged('Model_Machine_4','Initiate_Production_Scheduling',prop12),discharged('Model_Machine_4','Initiate_Production_Scheduling',prop17),discharged('Model_Machine_4','Initiate_Production_Scheduling',prop18),discharged('Model_Machine_4','Initiate_Production_Scheduling',prop20),discharged('Model_Machine_4','Complete_Production_Scheduling',inv16),discharged('Model_Machine_4','Complete_Production_Scheduling',prop12),discharged('Model_Machine_4','Complete_Production_Scheduling',prop17),discharged('Model_Machine_4','Complete_Production_Scheduling',prop18),discharged('Model_Machine_4','Complete_Production_Scheduling',prop20),discharged('Model_Machine_4','Reply_Invoice',inv10),discharged('Model_Machine_4','Reply_Invoice',prop1),discharged('Model_Machine_4','Reply_Invoice',prop13),discharged('Model_Machine_4','Reply_Invoice',prop14),discharged('Model_Machine_4','Reply_Invoice',prop18)],Error)).