1		package(load_event_b_project([event_b_model(none,
2		m_partner_behaviour_wodel123,
3		[sees(none,
4		[ctx_choreography]),
5		refines(none,
6		m_choreography),
7		variables(none,
8		[identifier(none,
9		'CustomerRequirement_TUCC_ID_SET'),
10		identifier(none,
11		'CustomerRequirement_blocked'),
12		identifier(none,
13		'CustomerRequirement_st_Example'),
14		identifier(none,
15		'EndStateVar'),
16		identifier(none,
17		'MessageHeader_BusinessScope_InstanceID'),
18		identifier(none,
19		'SalesOrder_TUCC_ID_SET'),
20		identifier(none,
21		'SalesOrder_blocked'),
22		identifier(none,
23		'SalesOrder_st_Example'),
24		identifier(none,
25		channel_CustomerRequirement_SalesOrder_EO),
26		identifier(none,
27		channel_CustomerRequirement_SalesOrder_EOIO),
28		identifier(none,
29		channel_SalesOrder_CustomerRequirement_EO),
30		identifier(none,
31		channel_SalesOrder_CustomerRequirement_EOIO),
32		identifier(none,
33		events),
34		identifier(none,
35		msg),
36		identifier(none,
37		types)]),
38		invariant(none,
39		[member(rodinpos(invariant7,
40		invariant7),
41		identifier(none,
42		'SalesOrder_st_Example'),
43		identifier(none,
44		'Example')),
45		member(rodinpos(invariant8,
46		invariant8),
47		identifier(none,
48		'CustomerRequirement_st_Example'),
49		identifier(none,
50		'Example')),
51		member(rodinpos(invariant9,
52		invariant9),
53		identifier(none,
54		'SalesOrder_TUCC_ID_SET'),
55		pow_subset(none,
56		identifier(none,
57		'BusinessScopeInstanceIDDt'))),
58		member(rodinpos(invariant10,
59		invariant10),
60		identifier(none,
61		'CustomerRequirement_TUCC_ID_SET'),
62		pow_subset(none,
63		identifier(none,
64		'BusinessScopeInstanceIDDt'))),
65		member(rodinpos(invariant11,
66		invariant11),
67		identifier(none,
68		msg),
69		natural_set(none)),
70		member(rodinpos(invariant12,
71		invariant12),
72		identifier(none,
73		types),
74		partial_function(none,
75		natural_set(none),
76		identifier(none,
77		'MESSAGES'))),
78		member(rodinpos(invariant13,
79		invariant13),
80		identifier(none,
81		events),
82		partial_function(none,
83		natural_set(none),
84		identifier(none,
85		'EVENTS'))),
86		member(rodinpos(invariant14,
87		invariant14),
88		identifier(none,
89		'SalesOrder_blocked'),
90		natural_set(none)),
91		member(rodinpos(invariant15,
92		invariant15),
93		identifier(none,
94		'CustomerRequirement_blocked'),
95		natural_set(none)),
96		member(rodinpos(invariant16,
97		invariant16),
98		identifier(none,
99		channel_SalesOrder_CustomerRequirement_EO),
100		pow_subset(none,
101		natural_set(none))),
102		member(rodinpos(invariant17,
103		invariant17),
104		identifier(none,
105		channel_CustomerRequirement_SalesOrder_EO),
106		pow_subset(none,
107		natural_set(none))),
108		member(rodinpos(invariant18,
109		invariant18),
110		identifier(none,
111		channel_SalesOrder_CustomerRequirement_EOIO),
112		pow_subset(none,
113		natural_set(none))),
114		member(rodinpos(invariant19,
115		invariant19),
116		identifier(none,
117		channel_CustomerRequirement_SalesOrder_EOIO),
118		pow_subset(none,
119		natural_set(none))),
120		member(rodinpos(invariant20,
121		invariant20),
122		identifier(none,
123		'MessageHeader_BusinessScope_InstanceID'),
124		partial_function(none,
125		natural_set(none),
126		identifier(none,
127		'BusinessScopeInstanceIDDt'))),
128		member(rodinpos(invariant21,
129		invariant21),
130		identifier(none,
131		'EndStateVar'),
132		bool_set(none))]),
133		theorems(none,
134		[]),
135		events(none,
136		[event(rodinpos('INITIALISATION',
137		'INITIALISATION'),
138		'INITIALISATION',
139		['INITIALISATION'],
140		[],
141		[],
142		[assign(rodinpos(act47,
143		act47),
144		[identifier(none,
145		'SalesOrder_st_Example')],
146		[identifier(none,
147		mcm_Start_Example)]),
148		assign(rodinpos(act48,
149		act48),
150		[identifier(none,
151		'CustomerRequirement_st_Example')],
152		[identifier(none,
153		mcm_Start_Example)]),
154		assign(rodinpos(act49,
155		act49),
156		[identifier(none,
157		'SalesOrder_TUCC_ID_SET')],
158		[empty_set(none)]),
159		assign(rodinpos(act50,
160		act50),
161		[identifier(none,
162		'CustomerRequirement_TUCC_ID_SET')],
163		[empty_set(none)]),
164		assign(rodinpos(act51,
165		act51),
166		[identifier(none,
167		msg)],
168		[integer(none,
169		0)]),
170		assign(rodinpos(act52,
171		act52),
172		[identifier(none,
173		types)],
174		[empty_set(none)]),
175		assign(rodinpos(act53,
176		act53),
177		[identifier(none,
178		events)],
179		[empty_set(none)]),
180		assign(rodinpos(act54,
181		act54),
182		[identifier(none,
183		'SalesOrder_blocked')],
184		[integer(none,
185		0)]),
186		assign(rodinpos(act55,
187		act55),
188		[identifier(none,
189		'CustomerRequirement_blocked')],
190		[integer(none,
191		0)]),
192		assign(rodinpos(act56,
193		act56),
194		[identifier(none,
195		channel_SalesOrder_CustomerRequirement_EO)],
196		[empty_set(none)]),
197		assign(rodinpos(act57,
198		act57),
199		[identifier(none,
200		channel_CustomerRequirement_SalesOrder_EO)],
201		[empty_set(none)]),
202		assign(rodinpos(act58,
203		act58),
204		[identifier(none,
205		channel_SalesOrder_CustomerRequirement_EOIO)],
206		[empty_set(none)]),
207		assign(rodinpos(act59,
208		act59),
209		[identifier(none,
210		channel_CustomerRequirement_SalesOrder_EOIO)],
211		[empty_set(none)]),
212		assign(rodinpos(act129,
213		act129),
214		[identifier(none,
215		'MessageHeader_BusinessScope_InstanceID')],
216		[empty_set(none)]),
217		assign(rodinpos(act130,
218		act130),
219		[identifier(none,
220		'EndStateVar')],
221		[boolean_false(none)])],
222		[]),
223		event(rodinpos(send_ProductAvailableToPromiseCheckRequest,
224		send_ProductAvailableToPromiseCheckRequest),
225		send_ProductAvailableToPromiseCheckRequest,
226		['ProductAvailableToPromiseCheckRequest'],
227		[identifier(rodinpos([],
228		t1),
229		t1)],
230		[disjunct(rodinpos(guard26,
231		guard26),
232		equal(none,
233		identifier(none,
234		'SalesOrder_st_Example'),
235		identifier(none,
236		mcm_Reserved_Example)),
237		equal(none,
238		identifier(none,
239		'SalesOrder_st_Example'),
240		identifier(none,
241		mcm_Start_Example))),
242		member(rodinpos(guard27,
243		guard27),
244		identifier(none,
245		t1),
246		identifier(none,
247		'BusinessScopeInstanceIDDt')),
248		negation(rodinpos(guard28,
249		guard28),
250		member(none,
251		identifier(none,
252		t1),
253		identifier(none,
254		'SalesOrder_TUCC_ID_SET'))),
255		implication(rodinpos(guard29,
256		guard29),
257		member(none,
258		identifier(none,
259		msg),
260		domain(none,
261		identifier(none,
262		'MessageHeader_BusinessScope_InstanceID'))),
263		equal(none,
264		function(none,
265		identifier(none,
266		'MessageHeader_BusinessScope_InstanceID'),
267		[identifier(none,
268		msg)]),
269		identifier(none,
270		t1))),
271		not_equal(rodinpos(guard30,
272		guard30),
273		identifier(none,
274		'SalesOrder_st_Example'),
275		identifier(none,
276		mcm_Reserved_Example)),
277		equal(rodinpos(guard31,
278		guard31),
279		identifier(none,
280		'SalesOrder_blocked'),
281		integer(none,
282		0))],
283		[assign(rodinpos(act60,
284		act60),
285		[identifier(none,
286		'MessageHeader_BusinessScope_InstanceID')],
287		[overwrite(none,
288		identifier(none,
289		'MessageHeader_BusinessScope_InstanceID'),
290		set_extension(none,
291		[couple(none,
292		[identifier(none,
293		msg),
294		identifier(none,
295		t1)])]))]),
296		assign(rodinpos(act61,
297		act61),
298		[identifier(none,
299		events)],
300		[overwrite(none,
301		identifier(none,
302		events),
303		set_extension(none,
304		[couple(none,
305		[identifier(none,
306		msg),
307		identifier(none,
308		'ProductAvailableToPromiseCheckRequestEvt')])]))]),
309		assign(rodinpos(act62,
310		act62),
311		[identifier(none,
312		types)],
313		[overwrite(none,
314		identifier(none,
315		types),
316		set_extension(none,
317		[couple(none,
318		[identifier(none,
319		msg),
320		identifier(none,
321		'ProductAvailableToPromiseCheckRequest')])]))]),
322		assign(rodinpos(act63,
323		act63),
324		[identifier(none,
325		'SalesOrder_st_Example')],
326		[identifier(none,
327		mcm_Requested_Example)]),
328		assign(rodinpos(act64,
329		act64),
330		[identifier(none,
331		'SalesOrder_TUCC_ID_SET')],
332		[union(none,
333		identifier(none,
334		'SalesOrder_TUCC_ID_SET'),
335		set_extension(none,
336		[identifier(none,
337		t1)]))]),
338		assign(rodinpos(act65,
339		act65),
340		[identifier(none,
341		channel_SalesOrder_CustomerRequirement_EOIO)],
342		[union(none,
343		identifier(none,
344		channel_SalesOrder_CustomerRequirement_EOIO),
345		set_extension(none,
346		[identifier(none,
347		msg)]))]),
348		assign(rodinpos(act66,
349		act66),
350		[identifier(none,
351		'SalesOrder_blocked')],
352		[integer(none,
353		2)]),
354		assign(rodinpos(act67,
355		act67),
356		[identifier(none,
357		msg)],
358		[add(none,
359		identifier(none,
360		msg),
361		integer(none,
362		1))]),
363		assign(rodinpos(act131,
364		act131),
365		[identifier(none,
366		'EndStateVar')],
367		[boolean_false(none)])],
368		[]),
369		event(rodinpos(receive_ProductAvailableToPromiseCheckRequest,
370		receive_ProductAvailableToPromiseCheckRequest),
371		receive_ProductAvailableToPromiseCheckRequest,
372		[],
373		[identifier(rodinpos([],
374		m),
375		m)],
376		[disjunct(rodinpos(guard32,
377		guard32),
378		equal(none,
379		identifier(none,
380		'CustomerRequirement_st_Example'),
381		identifier(none,
382		mcm_Reserved_Example)),
383		equal(none,
384		identifier(none,
385		'CustomerRequirement_st_Example'),
386		identifier(none,
387		mcm_Start_Example))),
388		member(rodinpos(guard33,
389		guard33),
390		identifier(none,
391		m),
392		domain(none,
393		identifier(none,
394		'MessageHeader_BusinessScope_InstanceID'))),
395		negation(rodinpos(guard34,
396		guard34),
397		member(none,
398		function(none,
399		identifier(none,
400		'MessageHeader_BusinessScope_InstanceID'),
401		[identifier(none,
402		m)]),
403		identifier(none,
404		'CustomerRequirement_TUCC_ID_SET'))),
405		member(rodinpos(guard35,
406		guard35),
407		identifier(none,
408		m),
409		natural_set(none)),
410		member(rodinpos(guard36,
411		guard36),
412		identifier(none,
413		m),
414		domain(none,
415		identifier(none,
416		types))),
417		equal(rodinpos(guard37,
418		guard37),
419		function(none,
420		identifier(none,
421		types),
422		[identifier(none,
423		m)]),
424		identifier(none,
425		'ProductAvailableToPromiseCheckRequest')),
426		member(rodinpos(guard38,
427		guard38),
428		identifier(none,
429		m),
430		identifier(none,
431		channel_SalesOrder_CustomerRequirement_EOIO)),
432		forall(rodinpos(guard39,
433		guard39),
434		[identifier(none,
435		x)],
436		implication(none,
437		member(none,
438		identifier(none,
439		x),
440		identifier(none,
441		channel_SalesOrder_CustomerRequirement_EOIO)),
442		greater_equal(none,
443		identifier(none,
444		x),
445		identifier(none,
446		m)))),
447		member(rodinpos(guard40,
448		guard40),
449		identifier(none,
450		m),
451		domain(none,
452		identifier(none,
453		'MessageHeader_BusinessScope_InstanceID')))],
454		[assign(rodinpos(act68,
455		act68),
456		[identifier(none,
457		'CustomerRequirement_st_Example')],
458		[identifier(none,
459		mcm_Requested_Example)]),
460		assign(rodinpos(act69,
461		act69),
462		[identifier(none,
463		'CustomerRequirement_TUCC_ID_SET')],
464		[union(none,
465		identifier(none,
466		'CustomerRequirement_TUCC_ID_SET'),
467		set_extension(none,
468		[function(none,
469		identifier(none,
470		'MessageHeader_BusinessScope_InstanceID'),
471		[identifier(none,
472		m)])]))]),
473		assign(rodinpos(act70,
474		act70),
475		[identifier(none,
476		channel_SalesOrder_CustomerRequirement_EOIO)],
477		[set_subtraction(none,
478		identifier(none,
479		channel_SalesOrder_CustomerRequirement_EOIO),
480		set_extension(none,
481		[identifier(none,
482		m)]))]),
483		assign(rodinpos(act132,
484		act132),
485		[identifier(none,
486		'EndStateVar')],
487		[boolean_false(none)])],
488		[]),
489		event(rodinpos(send_ProductAvailableToPromiseCheckConfirmation,
490		send_ProductAvailableToPromiseCheckConfirmation),
491		send_ProductAvailableToPromiseCheckConfirmation,
492		['ProductAvailableToPromiseCheckConfirmation'],
493		[],
494		[equal(rodinpos(guard41,
495		guard41),
496		identifier(none,
497		'CustomerRequirement_st_Example'),
498		identifier(none,
499		mcm_Requested_Example)),
500		equal(rodinpos(guard42,
501		guard42),
502		identifier(none,
503		'CustomerRequirement_blocked'),
504		integer(none,
505		0))],
506		[assign(rodinpos(act71,
507		act71),
508		[identifier(none,
509		events)],
510		[overwrite(none,
511		identifier(none,
512		events),
513		set_extension(none,
514		[couple(none,
515		[identifier(none,
516		msg),
517		identifier(none,
518		'ProductAvailableToPromiseCheckConfirmationEvt')])]))]),
519		assign(rodinpos(act72,
520		act72),
521		[identifier(none,
522		types)],
523		[overwrite(none,
524		identifier(none,
525		types),
526		set_extension(none,
527		[couple(none,
528		[identifier(none,
529		msg),
530		identifier(none,
531		'ProductAvailableToPromiseCheckConfirmation')])]))]),
532		assign(rodinpos(act73,
533		act73),
534		[identifier(none,
535		'CustomerRequirement_st_Example')],
536		[identifier(none,
537		mcm_Reserved_Example)]),
538		assign(rodinpos(act74,
539		act74),
540		[identifier(none,
541		channel_CustomerRequirement_SalesOrder_EOIO)],
542		[union(none,
543		identifier(none,
544		channel_CustomerRequirement_SalesOrder_EOIO),
545		set_extension(none,
546		[identifier(none,
547		msg)]))]),
548		assign(rodinpos(act75,
549		act75),
550		[identifier(none,
551		msg)],
552		[add(none,
553		identifier(none,
554		msg),
555		integer(none,
556		1))]),
557		assign(rodinpos(act133,
558		act133),
559		[identifier(none,
560		'EndStateVar')],
561		[boolean_false(none)])],
562		[]),
563		event(rodinpos(receive_ProductAvailableToPromiseCheckConfirmation,
564		receive_ProductAvailableToPromiseCheckConfirmation),
565		receive_ProductAvailableToPromiseCheckConfirmation,
566		[],
567		[identifier(rodinpos([],
568		m),
569		m)],
570		[equal(rodinpos(guard43,
571		guard43),
572		identifier(none,
573		'SalesOrder_st_Example'),
574		identifier(none,
575		mcm_Requested_Example)),
576		member(rodinpos(guard44,
577		guard44),
578		identifier(none,
579		m),
580		natural_set(none)),
581		member(rodinpos(guard45,
582		guard45),
583		identifier(none,
584		m),
585		domain(none,
586		identifier(none,
587		types))),
588		equal(rodinpos(guard46,
589		guard46),
590		function(none,
591		identifier(none,
592		types),
593		[identifier(none,
594		m)]),
595		identifier(none,
596		'ProductAvailableToPromiseCheckConfirmation')),
597		member(rodinpos(guard47,
598		guard47),
599		identifier(none,
600		m),
601		identifier(none,
602		channel_CustomerRequirement_SalesOrder_EOIO)),
603		forall(rodinpos(guard48,
604		guard48),
605		[identifier(none,
606		x)],
607		implication(none,
608		member(none,
609		identifier(none,
610		x),
611		identifier(none,
612		channel_CustomerRequirement_SalesOrder_EOIO)),
613		greater_equal(none,
614		identifier(none,
615		x),
616		identifier(none,
617		m))))],
618		[assign(rodinpos(act76,
619		act76),
620		[identifier(none,
621		'SalesOrder_st_Example')],
622		[identifier(none,
623		mcm_Reserved_Example)]),
624		assign(rodinpos(act77,
625		act77),
626		[identifier(none,
627		channel_CustomerRequirement_SalesOrder_EOIO)],
628		[set_subtraction(none,
629		identifier(none,
630		channel_CustomerRequirement_SalesOrder_EOIO),
631		set_extension(none,
632		[identifier(none,
633		m)]))]),
634		becomes_such(rodinpos(act78,
635		act78),
636		[identifier(none,
637		'SalesOrder_blocked')],
638		disjunct(none,
639		conjunct(none,
640		equal(none,
641		identifier(none,
642		'SalesOrder_blocked'),
643		integer(none,
644		2)),
645		equal(none,
646		identifier(none,
647		'SalesOrder_blocked\''),
648		integer(none,
649		0))),
650		conjunct(none,
651		not_equal(none,
652		identifier(none,
653		'SalesOrder_blocked'),
654		integer(none,
655		2)),
656		equal(none,
657		identifier(none,
658		'SalesOrder_blocked\''),
659		identifier(none,
660		'SalesOrder_blocked'))))),
661		assign(rodinpos(act134,
662		act134),
663		[identifier(none,
664		'EndStateVar')],
665		[boolean_false(none)])],
666		[]),
667		event(rodinpos(send_CustomerRequirementFulfillmentRequest,
668		send_CustomerRequirementFulfillmentRequest),
669		send_CustomerRequirementFulfillmentRequest,
670		['CustomerRequirementFulfillmentRequest'],
671		[identifier(rodinpos([],
672		t2),
673		t2)],
674		[equal(rodinpos(guard49,
675		guard49),
676		identifier(none,
677		'SalesOrder_st_Example'),
678		identifier(none,
679		mcm_Reserved_Example)),
680		member(rodinpos(guard50,
681		guard50),
682		identifier(none,
683		t2),
684		identifier(none,
685		'BusinessScopeInstanceIDDt')),
686		member(rodinpos(guard51,
687		guard51),
688		identifier(none,
689		t2),
690		identifier(none,
691		'SalesOrder_TUCC_ID_SET')),
692		implication(rodinpos(guard52,
693		guard52),
694		member(none,
695		identifier(none,
696		msg),
697		domain(none,
698		identifier(none,
699		'MessageHeader_BusinessScope_InstanceID'))),
700		equal(none,
701		function(none,
702		identifier(none,
703		'MessageHeader_BusinessScope_InstanceID'),
704		[identifier(none,
705		msg)]),
706		identifier(none,
707		t2))),
708		equal(rodinpos(guard53,
709		guard53),
710		identifier(none,
711		'SalesOrder_blocked'),
712		integer(none,
713		0))],
714		[assign(rodinpos(act79,
715		act79),
716		[identifier(none,
717		'MessageHeader_BusinessScope_InstanceID')],
718		[overwrite(none,
719		identifier(none,
720		'MessageHeader_BusinessScope_InstanceID'),
721		set_extension(none,
722		[couple(none,
723		[identifier(none,
724		msg),
725		identifier(none,
726		t2)])]))]),
727		assign(rodinpos(act80,
728		act80),
729		[identifier(none,
730		events)],
731		[overwrite(none,
732		identifier(none,
733		events),
734		set_extension(none,
735		[couple(none,
736		[identifier(none,
737		msg),
738		identifier(none,
739		'CustomerRequirementFulfillmentRequestEvt')])]))]),
740		assign(rodinpos(act81,
741		act81),
742		[identifier(none,
743		types)],
744		[overwrite(none,
745		identifier(none,
746		types),
747		set_extension(none,
748		[couple(none,
749		[identifier(none,
750		msg),
751		identifier(none,
752		'CustomerRequirementFulfillmentRequest')])]))]),
753		assign(rodinpos(act82,
754		act82),
755		[identifier(none,
756		'SalesOrder_st_Example')],
757		[identifier(none,
758		mcm_Ordered_Example)]),
759		assign(rodinpos(act83,
760		act83),
761		[identifier(none,
762		'SalesOrder_TUCC_ID_SET')],
763		[set_subtraction(none,
764		identifier(none,
765		'SalesOrder_TUCC_ID_SET'),
766		set_extension(none,
767		[identifier(none,
768		t2)]))]),
769		assign(rodinpos(act84,
770		act84),
771		[identifier(none,
772		channel_SalesOrder_CustomerRequirement_EO)],
773		[union(none,
774		identifier(none,
775		channel_SalesOrder_CustomerRequirement_EO),
776		set_extension(none,
777		[identifier(none,
778		msg)]))]),
779		assign(rodinpos(act85,
780		act85),
781		[identifier(none,
782		msg)],
783		[add(none,
784		identifier(none,
785		msg),
786		integer(none,
787		1))]),
788		assign(rodinpos(act135,
789		act135),
790		[identifier(none,
791		'EndStateVar')],
792		[boolean_false(none)])],
793		[]),
794		event(rodinpos(receive_CustomerRequirementFulfillmentRequest,
795		receive_CustomerRequirementFulfillmentRequest),
796		receive_CustomerRequirementFulfillmentRequest,
797		[],
798		[identifier(rodinpos([],
799		m),
800		m)],
801		[equal(rodinpos(guard54,
802		guard54),
803		identifier(none,
804		'CustomerRequirement_st_Example'),
805		identifier(none,
806		mcm_Reserved_Example)),
807		member(rodinpos(guard55,
808		guard55),
809		identifier(none,
810		m),
811		domain(none,
812		identifier(none,
813		'MessageHeader_BusinessScope_InstanceID'))),
814		member(rodinpos(guard56,
815		guard56),
816		function(none,
817		identifier(none,
818		'MessageHeader_BusinessScope_InstanceID'),
819		[identifier(none,
820		m)]),
821		identifier(none,
822		'CustomerRequirement_TUCC_ID_SET')),
823		member(rodinpos(guard57,
824		guard57),
825		identifier(none,
826		m),
827		natural_set(none)),
828		member(rodinpos(guard58,
829		guard58),
830		identifier(none,
831		m),
832		domain(none,
833		identifier(none,
834		types))),
835		equal(rodinpos(guard59,
836		guard59),
837		function(none,
838		identifier(none,
839		types),
840		[identifier(none,
841		m)]),
842		identifier(none,
843		'CustomerRequirementFulfillmentRequest')),
844		member(rodinpos(guard60,
845		guard60),
846		identifier(none,
847		m),
848		identifier(none,
849		channel_SalesOrder_CustomerRequirement_EO)),
850		member(rodinpos(guard61,
851		guard61),
852		identifier(none,
853		m),
854		domain(none,
855		identifier(none,
856		'MessageHeader_BusinessScope_InstanceID')))],
857		[assign(rodinpos(act86,
858		act86),
859		[identifier(none,
860		'CustomerRequirement_st_Example')],
861		[identifier(none,
862		mcm_Ordered_Example)]),
863		assign(rodinpos(act87,
864		act87),
865		[identifier(none,
866		'CustomerRequirement_TUCC_ID_SET')],
867		[set_subtraction(none,
868		identifier(none,
869		'CustomerRequirement_TUCC_ID_SET'),
870		set_extension(none,
871		[function(none,
872		identifier(none,
873		'MessageHeader_BusinessScope_InstanceID'),
874		[identifier(none,
875		m)])]))]),
876		assign(rodinpos(act88,
877		act88),
878		[identifier(none,
879		channel_SalesOrder_CustomerRequirement_EO)],
880		[set_subtraction(none,
881		identifier(none,
882		channel_SalesOrder_CustomerRequirement_EO),
883		set_extension(none,
884		[identifier(none,
885		m)]))]),
886		assign(rodinpos(act136,
887		act136),
888		[identifier(none,
889		'EndStateVar')],
890		[boolean_false(none)])],
891		[]),
892		event(rodinpos(send_ProvisionalCustomerRequirementDeleteNotification,
893		send_ProvisionalCustomerRequirementDeleteNotification),
894		send_ProvisionalCustomerRequirementDeleteNotification,
895		['ProvisionalCustomerRequirementDeleteNotification'],
896		[identifier(rodinpos([],
897		t3),
898		t3)],
899		[equal(rodinpos(guard62,
900		guard62),
901		identifier(none,
902		'SalesOrder_st_Example'),
903		identifier(none,
904		mcm_Reserved_Example)),
905		member(rodinpos(guard63,
906		guard63),
907		identifier(none,
908		t3),
909		identifier(none,
910		'BusinessScopeInstanceIDDt')),
911		conjunct(rodinpos(guard64,
912		guard64),
913		equal(none,
914		set_subtraction(none,
915		identifier(none,
916		'SalesOrder_TUCC_ID_SET'),
917		set_extension(none,
918		[identifier(none,
919		t3)])),
920		empty_set(none)),
921		member(none,
922		identifier(none,
923		t3),
924		identifier(none,
925		'SalesOrder_TUCC_ID_SET'))),
926		implication(rodinpos(guard65,
927		guard65),
928		member(none,
929		identifier(none,
930		msg),
931		domain(none,
932		identifier(none,
933		'MessageHeader_BusinessScope_InstanceID'))),
934		equal(none,
935		function(none,
936		identifier(none,
937		'MessageHeader_BusinessScope_InstanceID'),
938		[identifier(none,
939		msg)]),
940		identifier(none,
941		t3))),
942		equal(rodinpos(guard66,
943		guard66),
944		identifier(none,
945		'SalesOrder_blocked'),
946		integer(none,
947		0))],
948		[assign(rodinpos(act89,
949		act89),
950		[identifier(none,
951		'MessageHeader_BusinessScope_InstanceID')],
952		[overwrite(none,
953		identifier(none,
954		'MessageHeader_BusinessScope_InstanceID'),
955		set_extension(none,
956		[couple(none,
957		[identifier(none,
958		msg),
959		identifier(none,
960		t3)])]))]),
961		assign(rodinpos(act90,
962		act90),
963		[identifier(none,
964		events)],
965		[overwrite(none,
966		identifier(none,
967		events),
968		set_extension(none,
969		[couple(none,
970		[identifier(none,
971		msg),
972		identifier(none,
973		'ProvisionalCustomerRequirementDeleteNotificationEvt')])]))]),
974		assign(rodinpos(act91,
975		act91),
976		[identifier(none,
977		types)],
978		[overwrite(none,
979		identifier(none,
980		types),
981		set_extension(none,
982		[couple(none,
983		[identifier(none,
984		msg),
985		identifier(none,
986		'ProvisionalCustomerRequirementDeleteNotification')])]))]),
987		assign(rodinpos(act92,
988		act92),
989		[identifier(none,
990		'SalesOrder_st_Example')],
991		[identifier(none,
992		mcm_Start_Example)]),
993		assign(rodinpos(act93,
994		act93),
995		[identifier(none,
996		'SalesOrder_TUCC_ID_SET')],
997		[empty_set(none)]),
998		assign(rodinpos(act94,
999		act94),
1000		[identifier(none,
1001		channel_SalesOrder_CustomerRequirement_EO)],
1002		[union(none,
1003		identifier(none,
1004		channel_SalesOrder_CustomerRequirement_EO),
1005		set_extension(none,
1006		[identifier(none,
1007		msg)]))]),
1008		assign(rodinpos(act95,
1009		act95),
1010		[identifier(none,
1011		msg)],
1012		[add(none,
1013		identifier(none,
1014		msg),
1015		integer(none,
1016		1))]),
1017		assign(rodinpos(act137,
1018		act137),
1019		[identifier(none,
1020		'EndStateVar')],
1021		[boolean_false(none)])],
1022		[]),
1023		event(rodinpos(receive_ProvisionalCustomerRequirementDeleteNotification,
1024		receive_ProvisionalCustomerRequirementDeleteNotification),
1025		receive_ProvisionalCustomerRequirementDeleteNotification,
1026		[],
1027		[identifier(rodinpos([],
1028		m),
1029		m)],
1030		[equal(rodinpos(guard67,
1031		guard67),
1032		identifier(none,
1033		'CustomerRequirement_st_Example'),
1034		identifier(none,
1035		mcm_Reserved_Example)),
1036		member(rodinpos(guard68,
1037		guard68),
1038		identifier(none,
1039		m),
1040		domain(none,
1041		identifier(none,
1042		'MessageHeader_BusinessScope_InstanceID'))),
1043		member(rodinpos(guard69,
1044		guard69),
1045		identifier(none,
1046		m),
1047		domain(none,
1048		identifier(none,
1049		'MessageHeader_BusinessScope_InstanceID'))),
1050		conjunct(rodinpos(guard70,
1051		guard70),
1052		equal(none,
1053		set_subtraction(none,
1054		identifier(none,
1055		'CustomerRequirement_TUCC_ID_SET'),
1056		set_extension(none,
1057		[function(none,
1058		identifier(none,
1059		'MessageHeader_BusinessScope_InstanceID'),
1060		[identifier(none,
1061		m)])])),
1062		empty_set(none)),
1063		member(none,
1064		function(none,
1065		identifier(none,
1066		'MessageHeader_BusinessScope_InstanceID'),
1067		[identifier(none,
1068		m)]),
1069		identifier(none,
1070		'CustomerRequirement_TUCC_ID_SET'))),
1071		member(rodinpos(guard71,
1072		guard71),
1073		identifier(none,
1074		m),
1075		natural_set(none)),
1076		member(rodinpos(guard72,
1077		guard72),
1078		identifier(none,
1079		m),
1080		domain(none,
1081		identifier(none,
1082		types))),
1083		equal(rodinpos(guard73,
1084		guard73),
1085		function(none,
1086		identifier(none,
1087		types),
1088		[identifier(none,
1089		m)]),
1090		identifier(none,
1091		'ProvisionalCustomerRequirementDeleteNotification')),
1092		member(rodinpos(guard74,
1093		guard74),
1094		identifier(none,
1095		m),
1096		identifier(none,
1097		channel_SalesOrder_CustomerRequirement_EO))],
1098		[assign(rodinpos(act96,
1099		act96),
1100		[identifier(none,
1101		'CustomerRequirement_st_Example')],
1102		[identifier(none,
1103		mcm_Start_Example)]),
1104		assign(rodinpos(act97,
1105		act97),
1106		[identifier(none,
1107		'CustomerRequirement_TUCC_ID_SET')],
1108		[empty_set(none)]),
1109		assign(rodinpos(act98,
1110		act98),
1111		[identifier(none,
1112		channel_SalesOrder_CustomerRequirement_EO)],
1113		[set_subtraction(none,
1114		identifier(none,
1115		channel_SalesOrder_CustomerRequirement_EO),
1116		set_extension(none,
1117		[identifier(none,
1118		m)]))]),
1119		assign(rodinpos(act138,
1120		act138),
1121		[identifier(none,
1122		'EndStateVar')],
1123		[boolean_false(none)])],
1124		[]),
1125		event(rodinpos(receive_ProvisionalCustomerRequirementDeleteNotification1,
1126		receive_ProvisionalCustomerRequirementDeleteNotification1),
1127		receive_ProvisionalCustomerRequirementDeleteNotification1,
1128		[],
1129		[identifier(rodinpos([],
1130		m),
1131		m)],
1132		[equal(rodinpos(guard81,
1133		guard81),
1134		identifier(none,
1135		'CustomerRequirement_st_Example'),
1136		identifier(none,
1137		mcm_Reserved_Example)),
1138		member(rodinpos(guard82,
1139		guard82),
1140		identifier(none,
1141		m),
1142		domain(none,
1143		identifier(none,
1144		'MessageHeader_BusinessScope_InstanceID'))),
1145		member(rodinpos(guard83,
1146		guard83),
1147		identifier(none,
1148		m),
1149		domain(none,
1150		identifier(none,
1151		'MessageHeader_BusinessScope_InstanceID'))),
1152		conjunct(rodinpos(guard84,
1153		guard84),
1154		not_equal(none,
1155		set_subtraction(none,
1156		identifier(none,
1157		'CustomerRequirement_TUCC_ID_SET'),
1158		set_extension(none,
1159		[function(none,
1160		identifier(none,
1161		'MessageHeader_BusinessScope_InstanceID'),
1162		[identifier(none,
1163		m)])])),
1164		empty_set(none)),
1165		member(none,
1166		function(none,
1167		identifier(none,
1168		'MessageHeader_BusinessScope_InstanceID'),
1169		[identifier(none,
1170		m)]),
1171		identifier(none,
1172		'CustomerRequirement_TUCC_ID_SET'))),
1173		member(rodinpos(guard85,
1174		guard85),
1175		identifier(none,
1176		m),
1177		natural_set(none)),
1178		member(rodinpos(guard86,
1179		guard86),
1180		identifier(none,
1181		m),
1182		domain(none,
1183		identifier(none,
1184		types))),
1185		equal(rodinpos(guard87,
1186		guard87),
1187		function(none,
1188		identifier(none,
1189		types),
1190		[identifier(none,
1191		m)]),
1192		identifier(none,
1193		'ProvisionalCustomerRequirementDeleteNotification')),
1194		member(rodinpos(guard88,
1195		guard88),
1196		identifier(none,
1197		m),
1198		identifier(none,
1199		channel_SalesOrder_CustomerRequirement_EO)),
1200		member(rodinpos(guard89,
1201		guard89),
1202		identifier(none,
1203		m),
1204		domain(none,
1205		identifier(none,
1206		'MessageHeader_BusinessScope_InstanceID')))],
1207		[assign(rodinpos(act106,
1208		act106),
1209		[identifier(none,
1210		'CustomerRequirement_st_Example')],
1211		[identifier(none,
1212		mcm_Reserved_Example)]),
1213		assign(rodinpos(act107,
1214		act107),
1215		[identifier(none,
1216		'CustomerRequirement_TUCC_ID_SET')],
1217		[set_subtraction(none,
1218		identifier(none,
1219		'CustomerRequirement_TUCC_ID_SET'),
1220		set_extension(none,
1221		[function(none,
1222		identifier(none,
1223		'MessageHeader_BusinessScope_InstanceID'),
1224		[identifier(none,
1225		m)])]))]),
1226		assign(rodinpos(act108,
1227		act108),
1228		[identifier(none,
1229		channel_SalesOrder_CustomerRequirement_EO)],
1230		[set_subtraction(none,
1231		identifier(none,
1232		channel_SalesOrder_CustomerRequirement_EO),
1233		set_extension(none,
1234		[identifier(none,
1235		m)]))]),
1236		assign(rodinpos(act140,
1237		act140),
1238		[identifier(none,
1239		'EndStateVar')],
1240		[boolean_false(none)])],
1241		[]),
1242		event(rodinpos(receive_ProvisionalCustomerRequirementDeleteNotification2,
1243		receive_ProvisionalCustomerRequirementDeleteNotification2),
1244		receive_ProvisionalCustomerRequirementDeleteNotification2,
1245		[],
1246		[identifier(rodinpos([],
1247		m),
1248		m)],
1249		[member(rodinpos(guard96,
1250		guard96),
1251		identifier(none,
1252		m),
1253		domain(none,
1254		identifier(none,
1255		'MessageHeader_BusinessScope_InstanceID'))),
1256		member(rodinpos(guard97,
1257		guard97),
1258		function(none,
1259		identifier(none,
1260		'MessageHeader_BusinessScope_InstanceID'),
1261		[identifier(none,
1262		m)]),
1263		identifier(none,
1264		'CustomerRequirement_TUCC_ID_SET')),
1265		equal(rodinpos(guard98,
1266		guard98),
1267		identifier(none,
1268		'CustomerRequirement_st_Example'),
1269		identifier(none,
1270		mcm_Ordered_Example)),
1271		member(rodinpos(guard99,
1272		guard99),
1273		identifier(none,
1274		m),
1275		natural_set(none)),
1276		member(rodinpos(guard100,
1277		guard100),
1278		identifier(none,
1279		m),
1280		domain(none,
1281		identifier(none,
1282		types))),
1283		equal(rodinpos(guard101,
1284		guard101),
1285		function(none,
1286		identifier(none,
1287		types),
1288		[identifier(none,
1289		m)]),
1290		identifier(none,
1291		'ProvisionalCustomerRequirementDeleteNotification')),
1292		member(rodinpos(guard102,
1293		guard102),
1294		identifier(none,
1295		m),
1296		identifier(none,
1297		channel_SalesOrder_CustomerRequirement_EO)),
1298		member(rodinpos(guard103,
1299		guard103),
1300		identifier(none,
1301		m),
1302		domain(none,
1303		identifier(none,
1304		'MessageHeader_BusinessScope_InstanceID')))],
1305		[assign(rodinpos(act116,
1306		act116),
1307		[identifier(none,
1308		'CustomerRequirement_st_Example')],
1309		[identifier(none,
1310		mcm_Ordered_Example)]),
1311		assign(rodinpos(act117,
1312		act117),
1313		[identifier(none,
1314		'CustomerRequirement_TUCC_ID_SET')],
1315		[set_subtraction(none,
1316		identifier(none,
1317		'CustomerRequirement_TUCC_ID_SET'),
1318		set_extension(none,
1319		[function(none,
1320		identifier(none,
1321		'MessageHeader_BusinessScope_InstanceID'),
1322		[identifier(none,
1323		m)])]))]),
1324		assign(rodinpos(act118,
1325		act118),
1326		[identifier(none,
1327		channel_SalesOrder_CustomerRequirement_EO)],
1328		[set_subtraction(none,
1329		identifier(none,
1330		channel_SalesOrder_CustomerRequirement_EO),
1331		set_extension(none,
1332		[identifier(none,
1333		m)]))]),
1334		assign(rodinpos(act142,
1335		act142),
1336		[identifier(none,
1337		'EndStateVar')],
1338		[boolean_false(none)])],
1339		[]),
1340		event(rodinpos(receive_ProvisionalCustomerRequirementDeleteNotification3,
1341		receive_ProvisionalCustomerRequirementDeleteNotification3),
1342		receive_ProvisionalCustomerRequirementDeleteNotification3,
1343		[],
1344		[identifier(rodinpos([],
1345		m),
1346		m)],
1347		[equal(rodinpos(guard110,
1348		guard110),
1349		identifier(none,
1350		'CustomerRequirement_st_Example'),
1351		identifier(none,
1352		mcm_Requested_Example)),
1353		member(rodinpos(guard111,
1354		guard111),
1355		identifier(none,
1356		m),
1357		domain(none,
1358		identifier(none,
1359		'MessageHeader_BusinessScope_InstanceID'))),
1360		member(rodinpos(guard112,
1361		guard112),
1362		identifier(none,
1363		m),
1364		domain(none,
1365		identifier(none,
1366		'MessageHeader_BusinessScope_InstanceID'))),
1367		conjunct(rodinpos(guard113,
1368		guard113),
1369		not_equal(none,
1370		set_subtraction(none,
1371		identifier(none,
1372		'CustomerRequirement_TUCC_ID_SET'),
1373		set_extension(none,
1374		[function(none,
1375		identifier(none,
1376		'MessageHeader_BusinessScope_InstanceID'),
1377		[identifier(none,
1378		m)])])),
1379		empty_set(none)),
1380		member(none,
1381		function(none,
1382		identifier(none,
1383		'MessageHeader_BusinessScope_InstanceID'),
1384		[identifier(none,
1385		m)]),
1386		identifier(none,
1387		'CustomerRequirement_TUCC_ID_SET'))),
1388		member(rodinpos(guard114,
1389		guard114),
1390		identifier(none,
1391		m),
1392		natural_set(none)),
1393		member(rodinpos(guard115,
1394		guard115),
1395		identifier(none,
1396		m),
1397		domain(none,
1398		identifier(none,
1399		types))),
1400		equal(rodinpos(guard116,
1401		guard116),
1402		function(none,
1403		identifier(none,
1404		types),
1405		[identifier(none,
1406		m)]),
1407		identifier(none,
1408		'ProvisionalCustomerRequirementDeleteNotification')),
1409		member(rodinpos(guard117,
1410		guard117),
1411		identifier(none,
1412		m),
1413		identifier(none,
1414		channel_SalesOrder_CustomerRequirement_EO)),
1415		member(rodinpos(guard118,
1416		guard118),
1417		identifier(none,
1418		m),
1419		domain(none,
1420		identifier(none,
1421		'MessageHeader_BusinessScope_InstanceID')))],
1422		[assign(rodinpos(act126,
1423		act126),
1424		[identifier(none,
1425		'CustomerRequirement_st_Example')],
1426		[identifier(none,
1427		mcm_Requested_Example)]),
1428		assign(rodinpos(act127,
1429		act127),
1430		[identifier(none,
1431		'CustomerRequirement_TUCC_ID_SET')],
1432		[set_subtraction(none,
1433		identifier(none,
1434		'CustomerRequirement_TUCC_ID_SET'),
1435		set_extension(none,
1436		[function(none,
1437		identifier(none,
1438		'MessageHeader_BusinessScope_InstanceID'),
1439		[identifier(none,
1440		m)])]))]),
1441		assign(rodinpos(act128,
1442		act128),
1443		[identifier(none,
1444		channel_SalesOrder_CustomerRequirement_EO)],
1445		[set_subtraction(none,
1446		identifier(none,
1447		channel_SalesOrder_CustomerRequirement_EO),
1448		set_extension(none,
1449		[identifier(none,
1450		m)]))]),
1451		assign(rodinpos(act144,
1452		act144),
1453		[identifier(none,
1454		'EndStateVar')],
1455		[boolean_false(none)])],
1456		[]),
1457		event(rodinpos(endStateEvent1,
1458		endStateEvent1),
1459		endStateEvent1,
1460		[endStateEvent1],
1461		[],
1462		[disjunct(rodinpos(guard119,
1463		guard119),
1464		equal(none,
1465		identifier(none,
1466		'SalesOrder_st_Example'),
1467		identifier(none,
1468		mcm_Start_Example)),
1469		equal(none,
1470		identifier(none,
1471		'SalesOrder_st_Example'),
1472		identifier(none,
1473		mcm_Ordered_Example))),
1474		disjunct(rodinpos(guard120,
1475		guard120),
1476		equal(none,
1477		identifier(none,
1478		'CustomerRequirement_st_Example'),
1479		identifier(none,
1480		mcm_Start_Example)),
1481		equal(none,
1482		identifier(none,
1483		'CustomerRequirement_st_Example'),
1484		identifier(none,
1485		mcm_Ordered_Example))),
1486		equal(rodinpos(guard121,
1487		guard121),
1488		identifier(none,
1489		channel_SalesOrder_CustomerRequirement_EO),
1490		empty_set(none)),
1491		equal(rodinpos(guard122,
1492		guard122),
1493		identifier(none,
1494		channel_CustomerRequirement_SalesOrder_EO),
1495		empty_set(none)),
1496		equal(rodinpos(guard123,
1497		guard123),
1498		identifier(none,
1499		channel_SalesOrder_CustomerRequirement_EOIO),
1500		empty_set(none)),
1501		equal(rodinpos(guard124,
1502		guard124),
1503		identifier(none,
1504		channel_CustomerRequirement_SalesOrder_EOIO),
1505		empty_set(none))],
1506		[assign(rodinpos(act145,
1507		act145),
1508		[identifier(none,
1509		'EndStateVar')],
1510		[boolean_true(none)])],
1511		[])])]),
1512		event_b_model(none,
1513		m_choreography,
1514		[sees(none,
1515		[ctx_choreography]),
1516		variables(none,
1517		[identifier(none,
1518		'EndStateVar'),
1519		identifier(none,
1520		'MessageHeader_BusinessScope_InstanceID'),
1521		identifier(none,
1522		'TUCC_ID_SET'),
1523		identifier(none,
1524		msg),
1525		identifier(none,
1526		st_Example),
1527		identifier(none,
1528		types)]),
1529		invariant(none,
1530		[member(rodinpos(invariant1,
1531		invariant1),
1532		identifier(none,
1533		st_Example),
1534		identifier(none,
1535		'Example')),
1536		member(rodinpos(invariant2,
1537		invariant2),
1538		identifier(none,
1539		'TUCC_ID_SET'),
1540		pow_subset(none,
1541		identifier(none,
1542		'BusinessScopeInstanceIDDt'))),
1543		member(rodinpos(invariant3,
1544		invariant3),
1545		identifier(none,
1546		msg),
1547		natural_set(none)),
1548		member(rodinpos(invariant4,
1549		invariant4),
1550		identifier(none,
1551		types),
1552		partial_function(none,
1553		natural_set(none),
1554		identifier(none,
1555		'MESSAGES'))),
1556		member(rodinpos(invariant5,
1557		invariant5),
1558		identifier(none,
1559		'MessageHeader_BusinessScope_InstanceID'),
1560		partial_function(none,
1561		natural_set(none),
1562		identifier(none,
1563		'BusinessScopeInstanceIDDt'))),
1564		member(rodinpos(invariant6,
1565		invariant6),
1566		identifier(none,
1567		'EndStateVar'),
1568		bool_set(none))]),
1569		theorems(none,
1570		[]),
1571		events(none,
1572		[event(rodinpos('INITIALISATION',
1573		'INITIALISATION'),
1574		'INITIALISATION',
1575		[],
1576		[],
1577		[],
1578		[assign(rodinpos(act0,
1579		act0),
1580		[identifier(none,
1581		st_Example)],
1582		[identifier(none,
1583		mcm_Start_Example)]),
1584		assign(rodinpos(act1,
1585		act1),
1586		[identifier(none,
1587		'TUCC_ID_SET')],
1588		[empty_set(none)]),
1589		assign(rodinpos(act2,
1590		act2),
1591		[identifier(none,
1592		msg)],
1593		[integer(none,
1594		0)]),
1595		assign(rodinpos(act3,
1596		act3),
1597		[identifier(none,
1598		types)],
1599		[empty_set(none)]),
1600		assign(rodinpos(act37,
1601		act37),
1602		[identifier(none,
1603		'MessageHeader_BusinessScope_InstanceID')],
1604		[empty_set(none)]),
1605		assign(rodinpos(act38,
1606		act38),
1607		[identifier(none,
1608		'EndStateVar')],
1609		[boolean_false(none)])],
1610		[]),
1611		event(rodinpos('ProductAvailableToPromiseCheckRequest',
1612		'ProductAvailableToPromiseCheckRequest'),
1613		'ProductAvailableToPromiseCheckRequest',
1614		[],
1615		[identifier(rodinpos([],
1616		t1),
1617		t1)],
1618		[disjunct(rodinpos(guard0,
1619		guard0),
1620		equal(none,
1621		identifier(none,
1622		st_Example),
1623		identifier(none,
1624		mcm_Reserved_Example)),
1625		equal(none,
1626		identifier(none,
1627		st_Example),
1628		identifier(none,
1629		mcm_Start_Example))),
1630		member(rodinpos(guard1,
1631		guard1),
1632		identifier(none,
1633		t1),
1634		identifier(none,
1635		'BusinessScopeInstanceIDDt')),
1636		negation(rodinpos(guard2,
1637		guard2),
1638		member(none,
1639		identifier(none,
1640		t1),
1641		identifier(none,
1642		'TUCC_ID_SET'))),
1643		implication(rodinpos(guard3,
1644		guard3),
1645		member(none,
1646		identifier(none,
1647		msg),
1648		domain(none,
1649		identifier(none,
1650		'MessageHeader_BusinessScope_InstanceID'))),
1651		equal(none,
1652		function(none,
1653		identifier(none,
1654		'MessageHeader_BusinessScope_InstanceID'),
1655		[identifier(none,
1656		msg)]),
1657		identifier(none,
1658		t1)))],
1659		[assign(rodinpos(act4,
1660		act4),
1661		[identifier(none,
1662		'MessageHeader_BusinessScope_InstanceID')],
1663		[overwrite(none,
1664		identifier(none,
1665		'MessageHeader_BusinessScope_InstanceID'),
1666		set_extension(none,
1667		[couple(none,
1668		[identifier(none,
1669		msg),
1670		identifier(none,
1671		t1)])]))]),
1672		assign(rodinpos(act5,
1673		act5),
1674		[identifier(none,
1675		types)],
1676		[overwrite(none,
1677		identifier(none,
1678		types),
1679		set_extension(none,
1680		[couple(none,
1681		[identifier(none,
1682		msg),
1683		identifier(none,
1684		'ProductAvailableToPromiseCheckRequest')])]))]),
1685		assign(rodinpos(act6,
1686		act6),
1687		[identifier(none,
1688		st_Example)],
1689		[identifier(none,
1690		mcm_Requested_Example)]),
1691		assign(rodinpos(act7,
1692		act7),
1693		[identifier(none,
1694		'TUCC_ID_SET')],
1695		[union(none,
1696		identifier(none,
1697		'TUCC_ID_SET'),
1698		set_extension(none,
1699		[identifier(none,
1700		t1)]))]),
1701		assign(rodinpos(act8,
1702		act8),
1703		[identifier(none,
1704		msg)],
1705		[add(none,
1706		identifier(none,
1707		msg),
1708		integer(none,
1709		1))]),
1710		assign(rodinpos(act39,
1711		act39),
1712		[identifier(none,
1713		'EndStateVar')],
1714		[boolean_false(none)])],
1715		[]),
1716		event(rodinpos('ProductAvailableToPromiseCheckConfirmation',
1717		'ProductAvailableToPromiseCheckConfirmation'),
1718		'ProductAvailableToPromiseCheckConfirmation',
1719		[],
1720		[],
1721		[equal(rodinpos(guard4,
1722		guard4),
1723		identifier(none,
1724		st_Example),
1725		identifier(none,
1726		mcm_Requested_Example))],
1727		[assign(rodinpos(act9,
1728		act9),
1729		[identifier(none,
1730		types)],
1731		[overwrite(none,
1732		identifier(none,
1733		types),
1734		set_extension(none,
1735		[couple(none,
1736		[identifier(none,
1737		msg),
1738		identifier(none,
1739		'ProductAvailableToPromiseCheckConfirmation')])]))]),
1740		assign(rodinpos(act10,
1741		act10),
1742		[identifier(none,
1743		st_Example)],
1744		[identifier(none,
1745		mcm_Reserved_Example)]),
1746		assign(rodinpos(act11,
1747		act11),
1748		[identifier(none,
1749		msg)],
1750		[add(none,
1751		identifier(none,
1752		msg),
1753		integer(none,
1754		1))]),
1755		assign(rodinpos(act40,
1756		act40),
1757		[identifier(none,
1758		'EndStateVar')],
1759		[boolean_false(none)])],
1760		[]),
1761		event(rodinpos('CustomerRequirementFulfillmentRequest',
1762		'CustomerRequirementFulfillmentRequest'),
1763		'CustomerRequirementFulfillmentRequest',
1764		[],
1765		[identifier(rodinpos([],
1766		t2),
1767		t2)],
1768		[equal(rodinpos(guard5,
1769		guard5),
1770		identifier(none,
1771		st_Example),
1772		identifier(none,
1773		mcm_Reserved_Example)),
1774		member(rodinpos(guard6,
1775		guard6),
1776		identifier(none,
1777		t2),
1778		identifier(none,
1779		'BusinessScopeInstanceIDDt')),
1780		member(rodinpos(guard7,
1781		guard7),
1782		identifier(none,
1783		t2),
1784		identifier(none,
1785		'TUCC_ID_SET')),
1786		implication(rodinpos(guard8,
1787		guard8),
1788		member(none,
1789		identifier(none,
1790		msg),
1791		domain(none,
1792		identifier(none,
1793		'MessageHeader_BusinessScope_InstanceID'))),
1794		equal(none,
1795		function(none,
1796		identifier(none,
1797		'MessageHeader_BusinessScope_InstanceID'),
1798		[identifier(none,
1799		msg)]),
1800		identifier(none,
1801		t2)))],
1802		[assign(rodinpos(act12,
1803		act12),
1804		[identifier(none,
1805		'MessageHeader_BusinessScope_InstanceID')],
1806		[overwrite(none,
1807		identifier(none,
1808		'MessageHeader_BusinessScope_InstanceID'),
1809		set_extension(none,
1810		[couple(none,
1811		[identifier(none,
1812		msg),
1813		identifier(none,
1814		t2)])]))]),
1815		assign(rodinpos(act13,
1816		act13),
1817		[identifier(none,
1818		types)],
1819		[overwrite(none,
1820		identifier(none,
1821		types),
1822		set_extension(none,
1823		[couple(none,
1824		[identifier(none,
1825		msg),
1826		identifier(none,
1827		'CustomerRequirementFulfillmentRequest')])]))]),
1828		assign(rodinpos(act14,
1829		act14),
1830		[identifier(none,
1831		st_Example)],
1832		[identifier(none,
1833		mcm_Ordered_Example)]),
1834		assign(rodinpos(act15,
1835		act15),
1836		[identifier(none,
1837		'TUCC_ID_SET')],
1838		[set_subtraction(none,
1839		identifier(none,
1840		'TUCC_ID_SET'),
1841		set_extension(none,
1842		[identifier(none,
1843		t2)]))]),
1844		assign(rodinpos(act16,
1845		act16),
1846		[identifier(none,
1847		msg)],
1848		[add(none,
1849		identifier(none,
1850		msg),
1851		integer(none,
1852		1))]),
1853		assign(rodinpos(act41,
1854		act41),
1855		[identifier(none,
1856		'EndStateVar')],
1857		[boolean_false(none)])],
1858		[]),
1859		event(rodinpos('ProvisionalCustomerRequirementDeleteNotification',
1860		'ProvisionalCustomerRequirementDeleteNotification'),
1861		'ProvisionalCustomerRequirementDeleteNotification',
1862		[],
1863		[identifier(rodinpos([],
1864		t3),
1865		t3)],
1866		[equal(rodinpos(guard9,
1867		guard9),
1868		identifier(none,
1869		st_Example),
1870		identifier(none,
1871		mcm_Reserved_Example)),
1872		member(rodinpos(guard10,
1873		guard10),
1874		identifier(none,
1875		t3),
1876		identifier(none,
1877		'BusinessScopeInstanceIDDt')),
1878		conjunct(rodinpos(guard11,
1879		guard11),
1880		equal(none,
1881		set_subtraction(none,
1882		identifier(none,
1883		'TUCC_ID_SET'),
1884		set_extension(none,
1885		[identifier(none,
1886		t3)])),
1887		empty_set(none)),
1888		member(none,
1889		identifier(none,
1890		t3),
1891		identifier(none,
1892		'TUCC_ID_SET'))),
1893		implication(rodinpos(guard12,
1894		guard12),
1895		member(none,
1896		identifier(none,
1897		msg),
1898		domain(none,
1899		identifier(none,
1900		'MessageHeader_BusinessScope_InstanceID'))),
1901		equal(none,
1902		function(none,
1903		identifier(none,
1904		'MessageHeader_BusinessScope_InstanceID'),
1905		[identifier(none,
1906		msg)]),
1907		identifier(none,
1908		t3)))],
1909		[assign(rodinpos(act17,
1910		act17),
1911		[identifier(none,
1912		'MessageHeader_BusinessScope_InstanceID')],
1913		[overwrite(none,
1914		identifier(none,
1915		'MessageHeader_BusinessScope_InstanceID'),
1916		set_extension(none,
1917		[couple(none,
1918		[identifier(none,
1919		msg),
1920		identifier(none,
1921		t3)])]))]),
1922		assign(rodinpos(act18,
1923		act18),
1924		[identifier(none,
1925		types)],
1926		[overwrite(none,
1927		identifier(none,
1928		types),
1929		set_extension(none,
1930		[couple(none,
1931		[identifier(none,
1932		msg),
1933		identifier(none,
1934		'ProvisionalCustomerRequirementDeleteNotification')])]))]),
1935		assign(rodinpos(act19,
1936		act19),
1937		[identifier(none,
1938		st_Example)],
1939		[identifier(none,
1940		mcm_Start_Example)]),
1941		assign(rodinpos(act20,
1942		act20),
1943		[identifier(none,
1944		'TUCC_ID_SET')],
1945		[empty_set(none)]),
1946		assign(rodinpos(act21,
1947		act21),
1948		[identifier(none,
1949		msg)],
1950		[add(none,
1951		identifier(none,
1952		msg),
1953		integer(none,
1954		1))]),
1955		assign(rodinpos(act42,
1956		act42),
1957		[identifier(none,
1958		'EndStateVar')],
1959		[boolean_false(none)])],
1960		[]),
1961		event(rodinpos('ProvisionalCustomerRequirementDeleteNotification1',
1962		'ProvisionalCustomerRequirementDeleteNotification1'),
1963		'ProvisionalCustomerRequirementDeleteNotification1',
1964		[],
1965		[identifier(rodinpos([],
1966		t4),
1967		t4)],
1968		[equal(rodinpos(guard13,
1969		guard13),
1970		identifier(none,
1971		st_Example),
1972		identifier(none,
1973		mcm_Reserved_Example)),
1974		member(rodinpos(guard14,
1975		guard14),
1976		identifier(none,
1977		t4),
1978		identifier(none,
1979		'BusinessScopeInstanceIDDt')),
1980		conjunct(rodinpos(guard15,
1981		guard15),
1982		not_equal(none,
1983		set_subtraction(none,
1984		identifier(none,
1985		'TUCC_ID_SET'),
1986		set_extension(none,
1987		[identifier(none,
1988		t4)])),
1989		empty_set(none)),
1990		member(none,
1991		identifier(none,
1992		t4),
1993		identifier(none,
1994		'TUCC_ID_SET'))),
1995		implication(rodinpos(guard16,
1996		guard16),
1997		member(none,
1998		identifier(none,
1999		msg),
2000		domain(none,
2001		identifier(none,
2002		'MessageHeader_BusinessScope_InstanceID'))),
2003		equal(none,
2004		function(none,
2005		identifier(none,
2006		'MessageHeader_BusinessScope_InstanceID'),
2007		[identifier(none,
2008		msg)]),
2009		identifier(none,
2010		t4)))],
2011		[assign(rodinpos(act22,
2012		act22),
2013		[identifier(none,
2014		'MessageHeader_BusinessScope_InstanceID')],
2015		[overwrite(none,
2016		identifier(none,
2017		'MessageHeader_BusinessScope_InstanceID'),
2018		set_extension(none,
2019		[couple(none,
2020		[identifier(none,
2021		msg),
2022		identifier(none,
2023		t4)])]))]),
2024		assign(rodinpos(act23,
2025		act23),
2026		[identifier(none,
2027		types)],
2028		[overwrite(none,
2029		identifier(none,
2030		types),
2031		set_extension(none,
2032		[couple(none,
2033		[identifier(none,
2034		msg),
2035		identifier(none,
2036		'ProvisionalCustomerRequirementDeleteNotification')])]))]),
2037		assign(rodinpos(act24,
2038		act24),
2039		[identifier(none,
2040		st_Example)],
2041		[identifier(none,
2042		mcm_Reserved_Example)]),
2043		assign(rodinpos(act25,
2044		act25),
2045		[identifier(none,
2046		'TUCC_ID_SET')],
2047		[set_subtraction(none,
2048		identifier(none,
2049		'TUCC_ID_SET'),
2050		set_extension(none,
2051		[identifier(none,
2052		t4)]))]),
2053		assign(rodinpos(act26,
2054		act26),
2055		[identifier(none,
2056		msg)],
2057		[add(none,
2058		identifier(none,
2059		msg),
2060		integer(none,
2061		1))]),
2062		assign(rodinpos(act43,
2063		act43),
2064		[identifier(none,
2065		'EndStateVar')],
2066		[boolean_false(none)])],
2067		[]),
2068		event(rodinpos('ProvisionalCustomerRequirementDeleteNotification2',
2069		'ProvisionalCustomerRequirementDeleteNotification2'),
2070		'ProvisionalCustomerRequirementDeleteNotification2',
2071		[],
2072		[identifier(rodinpos([],
2073		t5),
2074		t5)],
2075		[member(rodinpos(guard17,
2076		guard17),
2077		identifier(none,
2078		t5),
2079		identifier(none,
2080		'BusinessScopeInstanceIDDt')),
2081		member(rodinpos(guard18,
2082		guard18),
2083		identifier(none,
2084		t5),
2085		identifier(none,
2086		'TUCC_ID_SET')),
2087		implication(rodinpos(guard19,
2088		guard19),
2089		member(none,
2090		identifier(none,
2091		msg),
2092		domain(none,
2093		identifier(none,
2094		'MessageHeader_BusinessScope_InstanceID'))),
2095		equal(none,
2096		function(none,
2097		identifier(none,
2098		'MessageHeader_BusinessScope_InstanceID'),
2099		[identifier(none,
2100		msg)]),
2101		identifier(none,
2102		t5))),
2103		equal(rodinpos(guard20,
2104		guard20),
2105		identifier(none,
2106		st_Example),
2107		identifier(none,
2108		mcm_Ordered_Example))],
2109		[assign(rodinpos(act27,
2110		act27),
2111		[identifier(none,
2112		'MessageHeader_BusinessScope_InstanceID')],
2113		[overwrite(none,
2114		identifier(none,
2115		'MessageHeader_BusinessScope_InstanceID'),
2116		set_extension(none,
2117		[couple(none,
2118		[identifier(none,
2119		msg),
2120		identifier(none,
2121		t5)])]))]),
2122		assign(rodinpos(act28,
2123		act28),
2124		[identifier(none,
2125		types)],
2126		[overwrite(none,
2127		identifier(none,
2128		types),
2129		set_extension(none,
2130		[couple(none,
2131		[identifier(none,
2132		msg),
2133		identifier(none,
2134		'ProvisionalCustomerRequirementDeleteNotification')])]))]),
2135		assign(rodinpos(act29,
2136		act29),
2137		[identifier(none,
2138		st_Example)],
2139		[identifier(none,
2140		mcm_Ordered_Example)]),
2141		assign(rodinpos(act30,
2142		act30),
2143		[identifier(none,
2144		'TUCC_ID_SET')],
2145		[set_subtraction(none,
2146		identifier(none,
2147		'TUCC_ID_SET'),
2148		set_extension(none,
2149		[identifier(none,
2150		t5)]))]),
2151		assign(rodinpos(act31,
2152		act31),
2153		[identifier(none,
2154		msg)],
2155		[add(none,
2156		identifier(none,
2157		msg),
2158		integer(none,
2159		1))]),
2160		assign(rodinpos(act44,
2161		act44),
2162		[identifier(none,
2163		'EndStateVar')],
2164		[boolean_false(none)])],
2165		[]),
2166		event(rodinpos('ProvisionalCustomerRequirementDeleteNotification3',
2167		'ProvisionalCustomerRequirementDeleteNotification3'),
2168		'ProvisionalCustomerRequirementDeleteNotification3',
2169		[],
2170		[identifier(rodinpos([],
2171		t6),
2172		t6)],
2173		[equal(rodinpos(guard21,
2174		guard21),
2175		identifier(none,
2176		st_Example),
2177		identifier(none,
2178		mcm_Requested_Example)),
2179		member(rodinpos(guard22,
2180		guard22),
2181		identifier(none,
2182		t6),
2183		identifier(none,
2184		'BusinessScopeInstanceIDDt')),
2185		conjunct(rodinpos(guard23,
2186		guard23),
2187		not_equal(none,
2188		set_subtraction(none,
2189		identifier(none,
2190		'TUCC_ID_SET'),
2191		set_extension(none,
2192		[identifier(none,
2193		t6)])),
2194		empty_set(none)),
2195		member(none,
2196		identifier(none,
2197		t6),
2198		identifier(none,
2199		'TUCC_ID_SET'))),
2200		implication(rodinpos(guard24,
2201		guard24),
2202		member(none,
2203		identifier(none,
2204		msg),
2205		domain(none,
2206		identifier(none,
2207		'MessageHeader_BusinessScope_InstanceID'))),
2208		equal(none,
2209		function(none,
2210		identifier(none,
2211		'MessageHeader_BusinessScope_InstanceID'),
2212		[identifier(none,
2213		msg)]),
2214		identifier(none,
2215		t6)))],
2216		[assign(rodinpos(act32,
2217		act32),
2218		[identifier(none,
2219		'MessageHeader_BusinessScope_InstanceID')],
2220		[overwrite(none,
2221		identifier(none,
2222		'MessageHeader_BusinessScope_InstanceID'),
2223		set_extension(none,
2224		[couple(none,
2225		[identifier(none,
2226		msg),
2227		identifier(none,
2228		t6)])]))]),
2229		assign(rodinpos(act33,
2230		act33),
2231		[identifier(none,
2232		types)],
2233		[overwrite(none,
2234		identifier(none,
2235		types),
2236		set_extension(none,
2237		[couple(none,
2238		[identifier(none,
2239		msg),
2240		identifier(none,
2241		'ProvisionalCustomerRequirementDeleteNotification')])]))]),
2242		assign(rodinpos(act34,
2243		act34),
2244		[identifier(none,
2245		st_Example)],
2246		[identifier(none,
2247		mcm_Requested_Example)]),
2248		assign(rodinpos(act35,
2249		act35),
2250		[identifier(none,
2251		'TUCC_ID_SET')],
2252		[set_subtraction(none,
2253		identifier(none,
2254		'TUCC_ID_SET'),
2255		set_extension(none,
2256		[identifier(none,
2257		t6)]))]),
2258		assign(rodinpos(act36,
2259		act36),
2260		[identifier(none,
2261		msg)],
2262		[add(none,
2263		identifier(none,
2264		msg),
2265		integer(none,
2266		1))]),
2267		assign(rodinpos(act45,
2268		act45),
2269		[identifier(none,
2270		'EndStateVar')],
2271		[boolean_false(none)])],
2272		[]),
2273		event(rodinpos(endStateEvent1,
2274		endStateEvent1),
2275		endStateEvent1,
2276		[],
2277		[],
2278		[disjunct(rodinpos(guard25,
2279		guard25),
2280		equal(none,
2281		identifier(none,
2282		st_Example),
2283		identifier(none,
2284		mcm_Start_Example)),
2285		equal(none,
2286		identifier(none,
2287		st_Example),
2288		identifier(none,
2289		mcm_Ordered_Example)))],
2290		[assign(rodinpos(act46,
2291		act46),
2292		[identifier(none,
2293		'EndStateVar')],
2294		[boolean_true(none)])],
2295		[])])])],
2296		[event_b_context(none,
2297		ctx_choreography,
2298		[extends(none,
2299		[]),
2300		constants(none,
2301		[identifier(none,
2302		'CustomerRequirementFulfillmentRequest'),
2303		identifier(none,
2304		'CustomerRequirementFulfillmentRequestEvt'),
2305		identifier(none,
2306		'ProductAvailableToPromiseCheckConfirmation'),
2307		identifier(none,
2308		'ProductAvailableToPromiseCheckConfirmationEvt'),
2309		identifier(none,
2310		'ProductAvailableToPromiseCheckRequest'),
2311		identifier(none,
2312		'ProductAvailableToPromiseCheckRequestEvt'),
2313		identifier(none,
2314		'ProvisionalCustomerRequirementDeleteNotification'),
2315		identifier(none,
2316		'ProvisionalCustomerRequirementDeleteNotification1Evt'),
2317		identifier(none,
2318		'ProvisionalCustomerRequirementDeleteNotification2Evt'),
2319		identifier(none,
2320		'ProvisionalCustomerRequirementDeleteNotification3Evt'),
2321		identifier(none,
2322		'ProvisionalCustomerRequirementDeleteNotificationEvt'),
2323		identifier(none,
2324		mcm_Ordered_Example),
2325		identifier(none,
2326		mcm_Requested_Example),
2327		identifier(none,
2328		mcm_Reserved_Example),
2329		identifier(none,
2330		mcm_Start_Example)]),
2331		axioms(none,
2332		[greater(rodinpos(axm2,
2333		internal_axm2),
2334		card(none,
2335		identifier(none,
2336		'Example')),
2337		integer(none,
2338		3)),
2339		greater(rodinpos(axm1,
2340		internal_axm1),
2341		card(none,
2342		identifier(none,
2343		'BusinessScopeInstanceIDDt')),
2344		integer(none,
2345		1)),
2346		member(rodinpos(ax1,
2347		ax1),
2348		identifier(none,
2349		mcm_Start_Example),
2350		identifier(none,
2351		'Example')),
2352		not_equal(rodinpos(ax2,
2353		ax2),
2354		identifier(none,
2355		mcm_Start_Example),
2356		identifier(none,
2357		mcm_Requested_Example)),
2358		not_equal(rodinpos(ax3,
2359		ax3),
2360		identifier(none,
2361		mcm_Start_Example),
2362		identifier(none,
2363		mcm_Reserved_Example)),
2364		not_equal(rodinpos(ax4,
2365		ax4),
2366		identifier(none,
2367		mcm_Start_Example),
2368		identifier(none,
2369		mcm_Ordered_Example)),
2370		member(rodinpos(ax5,
2371		ax5),
2372		identifier(none,
2373		mcm_Requested_Example),
2374		identifier(none,
2375		'Example')),
2376		not_equal(rodinpos(ax6,
2377		ax6),
2378		identifier(none,
2379		mcm_Requested_Example),
2380		identifier(none,
2381		mcm_Reserved_Example)),
2382		not_equal(rodinpos(ax7,
2383		ax7),
2384		identifier(none,
2385		mcm_Requested_Example),
2386		identifier(none,
2387		mcm_Ordered_Example)),
2388		member(rodinpos(ax8,
2389		ax8),
2390		identifier(none,
2391		mcm_Reserved_Example),
2392		identifier(none,
2393		'Example')),
2394		not_equal(rodinpos(ax9,
2395		ax9),
2396		identifier(none,
2397		mcm_Reserved_Example),
2398		identifier(none,
2399		mcm_Ordered_Example)),
2400		member(rodinpos(ax10,
2401		ax10),
2402		identifier(none,
2403		mcm_Ordered_Example),
2404		identifier(none,
2405		'Example')),
2406		equal(rodinpos(ax11,
2407		ax11),
2408		identifier(none,
2409		'MESSAGES'),
2410		set_extension(none,
2411		[identifier(none,
2412		'ProductAvailableToPromiseCheckRequest'),
2413		identifier(none,
2414		'ProductAvailableToPromiseCheckConfirmation'),
2415		identifier(none,
2416		'CustomerRequirementFulfillmentRequest'),
2417		identifier(none,
2418		'ProvisionalCustomerRequirementDeleteNotification')])),
2419		equal(rodinpos(ax12,
2420		ax12),
2421		identifier(none,
2422		'EVENTS'),
2423		set_extension(none,
2424		[identifier(none,
2425		'ProductAvailableToPromiseCheckRequestEvt'),
2426		identifier(none,
2427		'ProductAvailableToPromiseCheckConfirmationEvt'),
2428		identifier(none,
2429		'CustomerRequirementFulfillmentRequestEvt'),
2430		identifier(none,
2431		'ProvisionalCustomerRequirementDeleteNotificationEvt'),
2432		identifier(none,
2433		'ProvisionalCustomerRequirementDeleteNotification1Evt'),
2434		identifier(none,
2435		'ProvisionalCustomerRequirementDeleteNotification2Evt'),
2436		identifier(none,
2437		'ProvisionalCustomerRequirementDeleteNotification3Evt')])),
2438		not_equal(rodinpos(ax13,
2439		ax13),
2440		identifier(none,
2441		'ProductAvailableToPromiseCheckRequestEvt'),
2442		identifier(none,
2443		'ProductAvailableToPromiseCheckConfirmationEvt')),
2444		not_equal(rodinpos(ax14,
2445		ax14),
2446		identifier(none,
2447		'ProductAvailableToPromiseCheckRequestEvt'),
2448		identifier(none,
2449		'CustomerRequirementFulfillmentRequestEvt')),
2450		not_equal(rodinpos(ax15,
2451		ax15),
2452		identifier(none,
2453		'ProductAvailableToPromiseCheckRequestEvt'),
2454		identifier(none,
2455		'ProvisionalCustomerRequirementDeleteNotificationEvt')),
2456		not_equal(rodinpos(ax16,
2457		ax16),
2458		identifier(none,
2459		'ProductAvailableToPromiseCheckRequestEvt'),
2460		identifier(none,
2461		'ProvisionalCustomerRequirementDeleteNotification1Evt')),
2462		not_equal(rodinpos(ax17,
2463		ax17),
2464		identifier(none,
2465		'ProductAvailableToPromiseCheckRequestEvt'),
2466		identifier(none,
2467		'ProvisionalCustomerRequirementDeleteNotification2Evt')),
2468		not_equal(rodinpos(ax18,
2469		ax18),
2470		identifier(none,
2471		'ProductAvailableToPromiseCheckRequestEvt'),
2472		identifier(none,
2473		'ProvisionalCustomerRequirementDeleteNotification3Evt')),
2474		not_equal(rodinpos(ax19,
2475		ax19),
2476		identifier(none,
2477		'ProductAvailableToPromiseCheckRequest'),
2478		identifier(none,
2479		'ProductAvailableToPromiseCheckConfirmation')),
2480		not_equal(rodinpos(ax20,
2481		ax20),
2482		identifier(none,
2483		'ProductAvailableToPromiseCheckRequest'),
2484		identifier(none,
2485		'CustomerRequirementFulfillmentRequest')),
2486		not_equal(rodinpos(ax21,
2487		ax21),
2488		identifier(none,
2489		'ProductAvailableToPromiseCheckRequest'),
2490		identifier(none,
2491		'ProvisionalCustomerRequirementDeleteNotification')),
2492		not_equal(rodinpos(ax22,
2493		ax22),
2494		identifier(none,
2495		'ProductAvailableToPromiseCheckConfirmationEvt'),
2496		identifier(none,
2497		'CustomerRequirementFulfillmentRequestEvt')),
2498		not_equal(rodinpos(ax23,
2499		ax23),
2500		identifier(none,
2501		'ProductAvailableToPromiseCheckConfirmationEvt'),
2502		identifier(none,
2503		'ProvisionalCustomerRequirementDeleteNotificationEvt')),
2504		not_equal(rodinpos(ax24,
2505		ax24),
2506		identifier(none,
2507		'ProductAvailableToPromiseCheckConfirmationEvt'),
2508		identifier(none,
2509		'ProvisionalCustomerRequirementDeleteNotification1Evt')),
2510		not_equal(rodinpos(ax25,
2511		ax25),
2512		identifier(none,
2513		'ProductAvailableToPromiseCheckConfirmationEvt'),
2514		identifier(none,
2515		'ProvisionalCustomerRequirementDeleteNotification2Evt')),
2516		not_equal(rodinpos(ax26,
2517		ax26),
2518		identifier(none,
2519		'ProductAvailableToPromiseCheckConfirmationEvt'),
2520		identifier(none,
2521		'ProvisionalCustomerRequirementDeleteNotification3Evt')),
2522		not_equal(rodinpos(ax27,
2523		ax27),
2524		identifier(none,
2525		'ProductAvailableToPromiseCheckConfirmation'),
2526		identifier(none,
2527		'CustomerRequirementFulfillmentRequest')),
2528		not_equal(rodinpos(ax28,
2529		ax28),
2530		identifier(none,
2531		'ProductAvailableToPromiseCheckConfirmation'),
2532		identifier(none,
2533		'ProvisionalCustomerRequirementDeleteNotification')),
2534		not_equal(rodinpos(ax29,
2535		ax29),
2536		identifier(none,
2537		'CustomerRequirementFulfillmentRequestEvt'),
2538		identifier(none,
2539		'ProvisionalCustomerRequirementDeleteNotificationEvt')),
2540		not_equal(rodinpos(ax30,
2541		ax30),
2542		identifier(none,
2543		'CustomerRequirementFulfillmentRequestEvt'),
2544		identifier(none,
2545		'ProvisionalCustomerRequirementDeleteNotification1Evt')),
2546		not_equal(rodinpos(ax31,
2547		ax31),
2548		identifier(none,
2549		'CustomerRequirementFulfillmentRequestEvt'),
2550		identifier(none,
2551		'ProvisionalCustomerRequirementDeleteNotification2Evt')),
2552		not_equal(rodinpos(ax32,
2553		ax32),
2554		identifier(none,
2555		'CustomerRequirementFulfillmentRequestEvt'),
2556		identifier(none,
2557		'ProvisionalCustomerRequirementDeleteNotification3Evt')),
2558		not_equal(rodinpos(ax33,
2559		ax33),
2560		identifier(none,
2561		'CustomerRequirementFulfillmentRequest'),
2562		identifier(none,
2563		'ProvisionalCustomerRequirementDeleteNotification')),
2564		not_equal(rodinpos(ax34,
2565		ax34),
2566		identifier(none,
2567		'ProvisionalCustomerRequirementDeleteNotificationEvt'),
2568		identifier(none,
2569		'ProvisionalCustomerRequirementDeleteNotification1Evt')),
2570		not_equal(rodinpos(ax35,
2571		ax35),
2572		identifier(none,
2573		'ProvisionalCustomerRequirementDeleteNotificationEvt'),
2574		identifier(none,
2575		'ProvisionalCustomerRequirementDeleteNotification2Evt')),
2576		not_equal(rodinpos(ax36,
2577		ax36),
2578		identifier(none,
2579		'ProvisionalCustomerRequirementDeleteNotificationEvt'),
2580		identifier(none,
2581		'ProvisionalCustomerRequirementDeleteNotification3Evt')),
2582		not_equal(rodinpos(ax37,
2583		ax37),
2584		identifier(none,
2585		'ProvisionalCustomerRequirementDeleteNotification1Evt'),
2586		identifier(none,
2587		'ProvisionalCustomerRequirementDeleteNotification2Evt')),
2588		not_equal(rodinpos(ax38,
2589		ax38),
2590		identifier(none,
2591		'ProvisionalCustomerRequirementDeleteNotification1Evt'),
2592		identifier(none,
2593		'ProvisionalCustomerRequirementDeleteNotification3Evt')),
2594		not_equal(rodinpos(ax39,
2595		ax39),
2596		identifier(none,
2597		'ProvisionalCustomerRequirementDeleteNotification2Evt'),
2598		identifier(none,
2599		'ProvisionalCustomerRequirementDeleteNotification3Evt'))]),
2600		theorems(none,
2601		[]),
2602		sets(none,
2603		[deferred_set(none,
2604		'BusinessScopeInstanceIDDt'),
2605		deferred_set(none,
2606		'CustomerRequirementFulfillmentRequestMessageDt'),
2607		deferred_set(none,
2608		'EVENTS'),
2609		deferred_set(none,
2610		'Example'),
2611		deferred_set(none,
2612		'MESSAGES'),
2613		deferred_set(none,
2614		'ProductAvailableToPromiseCheckConfirmationMessageDt'),
2615		deferred_set(none,
2616		'ProductAvailableToPromiseCheckRequestMessageDt'),
2617		deferred_set(none,
2618		'ProvisionalCustomerRequirementDeleteNotificationMessageDt')])])],
2619		[discharged(m_partner_behaviour_wodel123,
2620		'INITIALISATION',
2621		invariant11),
2622		discharged(m_partner_behaviour_wodel123,
2623		'INITIALISATION',
2624		invariant12),
2625		discharged(m_partner_behaviour_wodel123,
2626		'INITIALISATION',
2627		invariant13),
2628		discharged(m_partner_behaviour_wodel123,
2629		'INITIALISATION',
2630		invariant14),
2631		discharged(m_partner_behaviour_wodel123,
2632		'INITIALISATION',
2633		invariant15),
2634		discharged(m_partner_behaviour_wodel123,
2635		'INITIALISATION',
2636		invariant16),
2637		discharged(m_partner_behaviour_wodel123,
2638		'INITIALISATION',
2639		invariant17),
2640		discharged(m_partner_behaviour_wodel123,
2641		'INITIALISATION',
2642		invariant18),
2643		discharged(m_partner_behaviour_wodel123,
2644		'INITIALISATION',
2645		invariant19),
2646		discharged(m_partner_behaviour_wodel123,
2647		'INITIALISATION',
2648		invariant20),
2649		discharged(m_partner_behaviour_wodel123,
2650		send_ProductAvailableToPromiseCheckRequest,
2651		invariant11),
2652		discharged(m_partner_behaviour_wodel123,
2653		send_ProductAvailableToPromiseCheckRequest,
2654		invariant12),
2655		discharged(m_partner_behaviour_wodel123,
2656		send_ProductAvailableToPromiseCheckRequest,
2657		invariant13),
2658		discharged(m_partner_behaviour_wodel123,
2659		send_ProductAvailableToPromiseCheckRequest,
2660		invariant14),
2661		discharged(m_partner_behaviour_wodel123,
2662		send_ProductAvailableToPromiseCheckRequest,
2663		invariant18),
2664		discharged(m_partner_behaviour_wodel123,
2665		send_ProductAvailableToPromiseCheckRequest,
2666		invariant20),
2667		discharged(m_partner_behaviour_wodel123,
2668		receive_ProductAvailableToPromiseCheckRequest,
2669		invariant18),
2670		discharged(m_partner_behaviour_wodel123,
2671		send_ProductAvailableToPromiseCheckConfirmation,
2672		invariant11),
2673		discharged(m_partner_behaviour_wodel123,
2674		send_ProductAvailableToPromiseCheckConfirmation,
2675		invariant12),
2676		discharged(m_partner_behaviour_wodel123,
2677		send_ProductAvailableToPromiseCheckConfirmation,
2678		invariant13),
2679		discharged(m_partner_behaviour_wodel123,
2680		send_ProductAvailableToPromiseCheckConfirmation,
2681		invariant19),
2682		discharged(m_partner_behaviour_wodel123,
2683		receive_CustomerRequirementFulfillmentRequest,
2684		invariant16),
2685		discharged(m_partner_behaviour_wodel123,
2686		send_ProvisionalCustomerRequirementDeleteNotification,
2687		invariant11),
2688		discharged(m_partner_behaviour_wodel123,
2689		send_ProvisionalCustomerRequirementDeleteNotification,
2690		invariant12),
2691		discharged(m_partner_behaviour_wodel123,
2692		send_ProvisionalCustomerRequirementDeleteNotification,
2693		invariant13),
2694		discharged(m_partner_behaviour_wodel123,
2695		send_ProvisionalCustomerRequirementDeleteNotification,
2696		invariant16),
2697		discharged(m_partner_behaviour_wodel123,
2698		send_ProvisionalCustomerRequirementDeleteNotification,
2699		invariant20),
2700		discharged(m_partner_behaviour_wodel123,
2701		receive_ProvisionalCustomerRequirementDeleteNotification,
2702		invariant16),
2703		discharged(m_partner_behaviour_wodel123,
2704		receive_ProvisionalCustomerRequirementDeleteNotification1,
2705		invariant16),
2706		discharged(m_partner_behaviour_wodel123,
2707		receive_ProvisionalCustomerRequirementDeleteNotification2,
2708		invariant16),
2709		discharged(m_partner_behaviour_wodel123,
2710		receive_ProvisionalCustomerRequirementDeleteNotification3,
2711		invariant16),
2712		discharged(m_choreography,
2713		'INITIALISATION',
2714		invariant3),
2715		discharged(m_choreography,
2716		'INITIALISATION',
2717		invariant4),
2718		discharged(m_choreography,
2719		'INITIALISATION',
2720		invariant5),
2721		discharged(m_choreography,
2722		'ProductAvailableToPromiseCheckRequest',
2723		invariant3),
2724		discharged(m_choreography,
2725		'ProductAvailableToPromiseCheckRequest',
2726		invariant4),
2727		discharged(m_choreography,
2728		'ProductAvailableToPromiseCheckRequest',
2729		invariant5),
2730		discharged(m_choreography,
2731		'ProductAvailableToPromiseCheckConfirmation',
2732		invariant3),
2733		discharged(m_choreography,
2734		'ProductAvailableToPromiseCheckConfirmation',
2735		invariant4),
2736		discharged(m_choreography,
2737		'CustomerRequirementFulfillmentRequest',
2738		invariant3),
2739		discharged(m_choreography,
2740		'CustomerRequirementFulfillmentRequest',
2741		invariant4),
2742		discharged(m_choreography,
2743		'CustomerRequirementFulfillmentRequest',
2744		invariant5),
2745		discharged(m_choreography,
2746		'ProvisionalCustomerRequirementDeleteNotification',
2747		invariant3),
2748		discharged(m_choreography,
2749		'ProvisionalCustomerRequirementDeleteNotification',
2750		invariant4),
2751		discharged(m_choreography,
2752		'ProvisionalCustomerRequirementDeleteNotification',
2753		invariant5),
2754		discharged(m_choreography,
2755		'ProvisionalCustomerRequirementDeleteNotification1',
2756		invariant3),
2757		discharged(m_choreography,
2758		'ProvisionalCustomerRequirementDeleteNotification1',
2759		invariant4),
2760		discharged(m_choreography,
2761		'ProvisionalCustomerRequirementDeleteNotification1',
2762		invariant5),
2763		discharged(m_choreography,
2764		'ProvisionalCustomerRequirementDeleteNotification2',
2765		invariant3),
2766		discharged(m_choreography,
2767		'ProvisionalCustomerRequirementDeleteNotification2',
2768		invariant4),
2769		discharged(m_choreography,
2770		'ProvisionalCustomerRequirementDeleteNotification2',
2771		invariant5),
2772		discharged(m_choreography,
2773		'ProvisionalCustomerRequirementDeleteNotification3',
2774		invariant3),
2775		discharged(m_choreography,
2776		'ProvisionalCustomerRequirementDeleteNotification3',
2777		invariant4),
2778		discharged(m_choreography,
2779		'ProvisionalCustomerRequirementDeleteNotification3',
2780		invariant5)],
2781		Error)).