parser_version('2013-02-27 13:50:48.994').
classical_b('Q4',['/Users/frappier/Documents/UdeS/cours/igl501/14A-igl501/intra/Q4.mch']).
machine(abstract_machine(pos(1,1,1,1,109,3),machine(pos(2,1,1,1,1,7)),machine_header(pos(3,1,1,9,1,10),'Q4',[]),[sets(pos(4,1,2,1,5,32),[enumerated_set(pos(5,1,3,3,3,20),'COURTIER',[identifier(pos(6,1,3,15,3,16),c1),identifier(pos(7,1,3,18,3,19),c2)]),enumerated_set(pos(8,1,4,3,4,23),'SUPERVISEUR',[identifier(pos(9,1,4,18,4,19),s1),identifier(pos(10,1,4,21,4,22),s2)]),enumerated_set(pos(11,1,5,3,5,32),'TRANSACTION',[identifier(pos(12,1,5,18,5,19),t1),identifier(pos(13,1,5,21,5,22),t2),identifier(pos(14,1,5,24,5,25),t3),identifier(pos(15,1,5,27,5,28),t4),identifier(pos(16,1,5,30,5,31),t5)])]),definitions(pos(17,1,6,1,7,34),[expression_definition(pos(18,1,7,3,7,34),somme,[identifier(pos(19,1,7,9,7,9),'S')],general_sum(pos(20,1,7,15,7,34),[identifier(pos(21,1,7,21,7,21),z)],member(pos(22,1,7,25,7,29),identifier(pos(23,1,7,25,7,25),z),identifier(pos(24,1,7,29,7,29),'S')),identifier(pos(25,1,7,33,7,33),z)))]),variables(pos(26,1,8,1,9,165),[identifier(pos(27,1,9,3,9,10),courtier),identifier(pos(28,1,9,13,9,23),superviseur),identifier(pos(29,1,9,26,9,37),supervisePar),identifier(pos(30,1,9,40,9,56),limiteQuotidienne),identifier(pos(31,1,9,59,9,78),limiteParTransaction),identifier(pos(32,1,9,81,9,93),limiteGlobale),identifier(pos(33,1,9,96,9,106),transaction),identifier(pos(34,1,9,109,9,115),montant),identifier(pos(35,1,9,118,9,123),auteur),identifier(pos(36,1,9,126,9,145),transactionEnAttente),identifier(pos(37,1,9,148,9,158),approbation),identifier(pos(38,1,9,161,9,165),refus)]),invariant(pos(39,1,11,1,46,39),conjunct(pos(40,1,12,5,46,39),conjunct(pos(41,1,12,5,45,65),conjunct(pos(42,1,12,5,43,11),conjunct(pos(43,1,12,5,35,11),conjunct(pos(44,1,12,5,29,64),conjunct(pos(45,1,12,5,26,90),conjunct(pos(46,1,12,5,23,39),conjunct(pos(47,1,12,5,22,45),conjunct(pos(48,1,12,5,21,39),conjunct(pos(49,1,12,5,20,37),conjunct(pos(50,1,12,5,19,33),conjunct(pos(51,1,12,5,18,30),conjunct(pos(52,1,12,5,17,43),conjunct(pos(53,1,12,5,16,23),conjunct(pos(54,1,12,5,15,40),conjunct(pos(55,1,12,5,14,43),conjunct(pos(56,1,12,5,13,30),subset(pos(57,1,12,5,12,24),identifier(pos(58,1,12,5,12,12),courtier),identifier(pos(59,1,12,17,12,24),'COURTIER')),subset(pos(60,1,13,5,13,30),identifier(pos(61,1,13,5,13,15),superviseur),identifier(pos(62,1,13,20,13,30),'SUPERVISEUR'))),member(pos(63,1,14,5,14,43),identifier(pos(64,1,14,5,14,16),supervisePar),total_function(pos(65,1,14,20,14,43),identifier(pos(66,1,14,20,14,27),courtier),identifier(pos(67,1,14,33,14,43),superviseur)))),member(pos(68,1,15,5,15,40),identifier(pos(69,1,15,5,15,21),limiteQuotidienne),total_function(pos(70,1,15,25,15,40),identifier(pos(71,1,15,25,15,32),courtier),nat_set(pos(72,1,15,38,15,40))))),member(pos(73,1,16,5,16,23),identifier(pos(74,1,16,5,16,17),limiteGlobale),nat_set(pos(75,1,16,21,16,23)))),member(pos(76,1,17,5,17,43),identifier(pos(77,1,17,5,17,24),limiteParTransaction),total_function(pos(78,1,17,28,17,43),identifier(pos(79,1,17,28,17,35),courtier),nat_set(pos(80,1,17,41,17,43))))),subset(pos(81,1,18,5,18,30),identifier(pos(82,1,18,5,18,15),transaction),identifier(pos(83,1,18,20,18,30),'TRANSACTION'))),member(pos(84,1,19,5,19,33),identifier(pos(85,1,19,5,19,11),montant),total_function(pos(86,1,19,15,19,33),identifier(pos(87,1,19,15,19,25),transaction),nat_set(pos(88,1,19,31,19,33))))),member(pos(89,1,20,5,20,37),identifier(pos(90,1,20,5,20,10),auteur),total_function(pos(91,1,20,14,20,37),identifier(pos(92,1,20,14,20,24),transaction),identifier(pos(93,1,20,30,20,37),courtier)))),subset(pos(94,1,21,5,21,39),identifier(pos(95,1,21,5,21,24),transactionEnAttente),identifier(pos(96,1,21,29,21,39),transaction))),member(pos(97,1,22,5,22,45),identifier(pos(98,1,22,5,22,15),approbation),partial_function(pos(99,1,22,19,22,45),identifier(pos(100,1,22,19,22,29),transaction),identifier(pos(101,1,22,35,22,45),superviseur)))),member(pos(102,1,23,5,23,39),identifier(pos(103,1,23,5,23,9),refus),partial_function(pos(104,1,23,13,23,39),identifier(pos(105,1,23,13,23,23),transaction),identifier(pos(106,1,23,29,23,39),superviseur)))),forall(pos(107,1,26,5,26,90),[identifier(pos(108,1,26,7,26,7),c)],implication(pos(109,1,26,11,26,89),member(pos(110,1,26,11,26,22),identifier(pos(111,1,26,11,26,11),c),identifier(pos(112,1,26,15,26,22),courtier)),less_equal(pos(113,1,26,27,26,89),definition(pos(114,1,26,27,26,65),somme,[image(pos(115,1,26,33,26,64),identifier(pos(116,1,26,33,26,39),montant),minus_or_set_subtract(pos(117,1,26,41,26,63),image(pos(118,1,26,41,26,52),reverse(pos(119,1,26,41,26,47),identifier(pos(120,1,26,41,26,46),auteur)),set_extension(pos(121,1,26,49,26,51),[identifier(pos(122,1,26,50,26,50),c)])),domain(pos(123,1,26,54,26,63),identifier(pos(124,1,26,58,26,62),refus))))]),function(pos(125,1,26,70,26,89),identifier(pos(126,1,26,70,26,86),limiteQuotidienne),[identifier(pos(127,1,26,88,26,88),c)]))))),forall(pos(128,1,29,5,29,64),[identifier(pos(129,1,29,7,29,7),c)],implication(pos(130,1,29,11,29,63),member(pos(131,1,29,11,29,22),identifier(pos(132,1,29,11,29,11),c),identifier(pos(133,1,29,15,29,22),courtier)),less_equal(pos(134,1,29,27,29,63),function(pos(135,1,29,27,29,46),identifier(pos(136,1,29,27,29,43),limiteQuotidienne),[identifier(pos(137,1,29,45,29,45),c)]),identifier(pos(138,1,29,51,29,63),limiteGlobale))))),forall(pos(139,1,32,5,35,11),[identifier(pos(140,1,32,7,32,7),t)],implication(pos(141,1,32,13,34,56),member(pos(142,1,32,13,32,36),identifier(pos(143,1,32,13,32,13),t),identifier(pos(144,1,32,17,32,36),transactionEnAttente)),greater(pos(145,1,34,13,34,56),function(pos(146,1,34,13,34,22),identifier(pos(147,1,34,13,34,19),montant),[identifier(pos(148,1,34,21,34,21),t)]),function(pos(149,1,34,26,34,56),identifier(pos(150,1,34,26,34,45),limiteParTransaction),[function(pos(151,1,34,47,34,55),identifier(pos(152,1,34,47,34,52),auteur),[identifier(pos(153,1,34,54,34,54),t)])]))))),forall(pos(154,1,38,5,43,11),[identifier(pos(155,1,38,7,38,7),t)],implication(pos(156,1,38,15,42,65),conjunct(pos(157,1,38,15,40,58),conjunct(pos(158,1,38,15,39,39),member(pos(159,1,38,15,38,29),identifier(pos(160,1,38,15,38,15),t),identifier(pos(161,1,38,19,38,29),transaction)),not_member(pos(162,1,39,15,39,39),identifier(pos(163,1,39,15,39,15),t),identifier(pos(164,1,39,20,39,39),transactionEnAttente))),greater(pos(165,1,40,15,40,58),function(pos(166,1,40,15,40,24),identifier(pos(167,1,40,15,40,21),montant),[identifier(pos(168,1,40,23,40,23),t)]),function(pos(169,1,40,28,40,58),identifier(pos(170,1,40,28,40,47),limiteParTransaction),[function(pos(171,1,40,49,40,57),identifier(pos(172,1,40,49,40,54),auteur),[identifier(pos(173,1,40,56,40,56),t)])]))),member(pos(174,1,42,13,42,65),couple(pos(175,1,42,13,42,41),[identifier(pos(176,1,42,13,42,13),t),function(pos(177,1,42,19,42,41),identifier(pos(178,1,42,19,42,30),supervisePar),[function(pos(179,1,42,32,42,40),identifier(pos(180,1,42,32,42,37),auteur),[identifier(pos(181,1,42,39,42,39),t)])])]),union(pos(182,1,42,46,42,65),identifier(pos(183,1,42,46,42,56),approbation),identifier(pos(184,1,42,61,42,65),refus)))))),equal(pos(185,1,45,6,45,65),intersection(pos(186,1,45,6,45,60),union(pos(187,1,45,6,45,35),domain(pos(188,1,45,6,45,21),identifier(pos(189,1,45,10,45,20),approbation)),domain(pos(190,1,45,26,45,35),identifier(pos(191,1,45,30,45,34),refus))),identifier(pos(192,1,45,41,45,60),transactionEnAttente)),empty_set(pos(193,1,45,64,45,65)))),equal(pos(194,1,46,5,46,39),intersection(pos(195,1,46,5,46,34),domain(pos(196,1,46,5,46,20),identifier(pos(197,1,46,9,46,19),approbation)),domain(pos(198,1,46,25,46,34),identifier(pos(199,1,46,29,46,33),refus))),empty_set(pos(200,1,46,38,46,39))))),initialisation(pos(201,1,48,1,60,17),parallel(pos(202,1,49,7,60,17),[assign(pos(203,1,49,7,49,27),[identifier(pos(204,1,49,7,49,14),courtier)],[identifier(pos(205,1,49,20,49,27),'COURTIER')]),assign(pos(206,1,50,7,50,32),[identifier(pos(207,1,50,7,50,17),superviseur)],[identifier(pos(208,1,50,22,50,32),'SUPERVISEUR')]),assign(pos(209,1,51,7,51,44),[identifier(pos(210,1,51,7,51,18),supervisePar)],[set_extension(pos(211,1,51,23,51,44),[couple(pos(212,1,51,24,51,32),[identifier(pos(213,1,51,24,51,25),c1),identifier(pos(214,1,51,31,51,32),s1)]),couple(pos(215,1,51,35,51,43),[identifier(pos(216,1,51,35,51,36),c2),identifier(pos(217,1,51,42,51,43),s2)])])]),assign(pos(218,1,52,7,52,47),[identifier(pos(219,1,52,7,52,23),limiteQuotidienne)],[set_extension(pos(220,1,52,28,52,47),[couple(pos(221,1,52,29,52,36),[identifier(pos(222,1,52,29,52,30),c1),integer(pos(223,1,52,36,52,36),2)]),couple(pos(224,1,52,39,52,46),[identifier(pos(225,1,52,39,52,40),c2),integer(pos(226,1,52,46,52,46),3)])])]),assign(pos(227,1,53,7,53,24),[identifier(pos(228,1,53,7,53,19),limiteGlobale)],[integer(pos(229,1,53,24,53,24),3)]),assign(pos(230,1,54,7,54,50),[identifier(pos(231,1,54,7,54,26),limiteParTransaction)],[set_extension(pos(232,1,54,31,54,50),[couple(pos(233,1,54,32,54,39),[identifier(pos(234,1,54,32,54,33),c1),integer(pos(235,1,54,39,54,39),1)]),couple(pos(236,1,54,42,54,49),[identifier(pos(237,1,54,42,54,43),c2),integer(pos(238,1,54,49,54,49),2)])])]),assign(pos(239,1,55,7,55,23),[identifier(pos(240,1,55,7,55,17),transaction)],[empty_set(pos(241,1,55,22,55,23))]),assign(pos(242,1,56,7,56,19),[identifier(pos(243,1,56,7,56,13),montant)],[empty_set(pos(244,1,56,18,56,19))]),assign(pos(245,1,57,7,57,18),[identifier(pos(246,1,57,7,57,12),auteur)],[empty_set(pos(247,1,57,17,57,18))]),assign(pos(248,1,58,7,58,32),[identifier(pos(249,1,58,7,58,26),transactionEnAttente)],[empty_set(pos(250,1,58,31,58,32))]),assign(pos(251,1,59,7,59,23),[identifier(pos(252,1,59,7,59,17),approbation)],[empty_set(pos(253,1,59,22,59,23))]),assign(pos(254,1,60,7,60,17),[identifier(pos(255,1,60,7,60,11),refus)],[empty_set(pos(256,1,60,16,60,17))])])),operations(pos(257,1,63,1,108,5),[operation(pos(258,1,64,3,84,5),identifier(pos(258,1,64,3,84,5),transiger),[],[identifier(pos(259,1,64,13,64,13),c),identifier(pos(260,1,64,15,64,15),m)],precondition(pos(261,1,65,3,84,5),conjunct(pos(262,1,66,7,69,37),conjunct(pos(263,1,66,7,68,62),conjunct(pos(264,1,66,7,67,14),member(pos(265,1,66,7,66,18),identifier(pos(266,1,66,7,66,7),c),identifier(pos(267,1,66,11,66,18),courtier)),member(pos(268,1,67,7,67,14),identifier(pos(269,1,67,7,67,7),m),nat1_set(pos(270,1,67,11,67,14)))),less_equal(pos(271,1,68,7,68,62),add(pos(272,1,68,7,68,38),definition(pos(273,1,68,7,68,34),somme,[image(pos(274,1,68,13,68,33),identifier(pos(275,1,68,13,68,19),montant),image(pos(276,1,68,21,68,32),reverse(pos(277,1,68,21,68,27),identifier(pos(278,1,68,21,68,26),auteur)),set_extension(pos(279,1,68,29,68,31),[identifier(pos(280,1,68,30,68,30),c)])))]),identifier(pos(281,1,68,38,68,38),m)),function(pos(282,1,68,43,68,62),identifier(pos(283,1,68,43,68,59),limiteQuotidienne),[identifier(pos(284,1,68,61,68,61),c)]))),not_equal(pos(285,1,69,7,69,37),minus_or_set_subtract(pos(286,1,69,7,69,31),identifier(pos(287,1,69,7,69,17),'TRANSACTION'),identifier(pos(288,1,69,21,69,31),transaction)),empty_set(pos(289,1,69,36,69,37)))),any(pos(290,1,71,5,83,7),[identifier(pos(291,1,71,9,71,9),t)],member(pos(292,1,73,7,73,35),identifier(pos(293,1,73,7,73,7),t),minus_or_set_subtract(pos(294,1,73,11,73,35),identifier(pos(295,1,73,11,73,21),'TRANSACTION'),identifier(pos(296,1,73,25,73,35),transaction))),parallel(pos(297,1,75,11,82,25),[assign(pos(298,1,75,11,75,43),[identifier(pos(299,1,75,11,75,21),transaction)],[union(pos(300,1,75,26,75,43),identifier(pos(301,1,75,26,75,36),transaction),set_extension(pos(302,1,75,41,75,43),[identifier(pos(303,1,75,42,75,42),t)]))]),if(pos(304,1,76,11,80,13),greater(pos(305,1,77,13,77,39),identifier(pos(306,1,77,13,77,13),m),function(pos(307,1,77,17,77,39),identifier(pos(308,1,77,17,77,36),limiteParTransaction),[identifier(pos(309,1,77,38,77,38),c)])),assign(pos(310,1,79,13,79,63),[identifier(pos(311,1,79,13,79,32),transactionEnAttente)],[union(pos(312,1,79,37,79,63),identifier(pos(313,1,79,37,79,56),transactionEnAttente),set_extension(pos(314,1,79,61,79,63),[identifier(pos(315,1,79,62,79,62),t)]))]),[],skip(none)),assign(pos(316,1,81,11,81,24),[function(pos(317,1,81,11,81,19),identifier(pos(318,1,81,11,81,16),auteur),[identifier(pos(319,1,81,18,81,18),t)])],[identifier(pos(320,1,81,24,81,24),c)]),assign(pos(321,1,82,11,82,25),[function(pos(322,1,82,11,82,20),identifier(pos(323,1,82,11,82,17),montant),[identifier(pos(324,1,82,19,82,19),t)])],[identifier(pos(325,1,82,25,82,25),m)])])))),operation(pos(326,1,86,3,96,5),identifier(pos(326,1,86,3,96,5),approuver),[],[identifier(pos(327,1,86,13,86,13),s),identifier(pos(328,1,86,15,86,15),t)],precondition(pos(329,1,87,3,96,5),conjunct(pos(330,1,88,7,90,30),conjunct(pos(331,1,88,7,89,33),member(pos(332,1,88,7,88,21),identifier(pos(333,1,88,7,88,7),s),identifier(pos(334,1,88,11,88,21),superviseur)),equal(pos(335,1,89,7,89,33),identifier(pos(336,1,89,7,89,7),s),function(pos(337,1,89,11,89,33),identifier(pos(338,1,89,11,89,22),supervisePar),[function(pos(339,1,89,24,89,32),identifier(pos(340,1,89,24,89,29),auteur),[identifier(pos(341,1,89,31,89,31),t)])]))),member(pos(342,1,90,7,90,30),identifier(pos(343,1,90,7,90,7),t),identifier(pos(344,1,90,11,90,30),transactionEnAttente))),parallel(pos(345,1,94,9,95,27),[assign(pos(346,1,94,9,94,58),[identifier(pos(347,1,94,9,94,28),transactionEnAttente)],[minus_or_set_subtract(pos(348,1,94,33,94,58),identifier(pos(349,1,94,33,94,52),transactionEnAttente),set_extension(pos(350,1,94,56,94,58),[identifier(pos(351,1,94,57,94,57),t)]))]),assign(pos(352,1,95,9,95,27),[function(pos(353,1,95,9,95,22),identifier(pos(354,1,95,9,95,19),approbation),[identifier(pos(355,1,95,21,95,21),t)])],[identifier(pos(356,1,95,27,95,27),s)])]))),operation(pos(357,1,98,3,108,5),identifier(pos(357,1,98,3,108,5),refuser),[],[identifier(pos(358,1,98,11,98,11),s),identifier(pos(359,1,98,13,98,13),t)],precondition(pos(360,1,99,3,108,5),conjunct(pos(361,1,100,7,102,30),conjunct(pos(362,1,100,7,101,33),member(pos(363,1,100,7,100,21),identifier(pos(364,1,100,7,100,7),s),identifier(pos(365,1,100,11,100,21),superviseur)),equal(pos(366,1,101,7,101,33),identifier(pos(367,1,101,7,101,7),s),function(pos(368,1,101,11,101,33),identifier(pos(369,1,101,11,101,22),supervisePar),[function(pos(370,1,101,24,101,32),identifier(pos(371,1,101,24,101,29),auteur),[identifier(pos(372,1,101,31,101,31),t)])]))),member(pos(373,1,102,7,102,30),identifier(pos(374,1,102,7,102,7),t),identifier(pos(375,1,102,11,102,30),transactionEnAttente))),parallel(pos(376,1,106,9,107,21),[assign(pos(377,1,106,9,106,58),[identifier(pos(378,1,106,9,106,28),transactionEnAttente)],[minus_or_set_subtract(pos(379,1,106,33,106,58),identifier(pos(380,1,106,33,106,52),transactionEnAttente),set_extension(pos(381,1,106,56,106,58),[identifier(pos(382,1,106,57,106,57),t)]))]),assign(pos(383,1,107,9,107,21),[function(pos(384,1,107,9,107,16),identifier(pos(385,1,107,9,107,13),refus),[identifier(pos(386,1,107,15,107,15),t)])],[identifier(pos(387,1,107,21,107,21),s)])])))])])).