This repository has been archived by the owner on Jan 7, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Spaceship_And_Asteroids.prob
3 lines (3 loc) · 33 KB
/
Spaceship_And_Asteroids.prob
1
2
3
parser_version('2018-03-15 10:38:02.795').
classical_b('Spaceship_And_Asteroids',['C:\\Users\\User\\Desktop\\software engineering\\Final Year\\Reasoning\\workplace\\Spaceship_And_Asteroids\\Spaceship_And_Asteroids.mch']).
machine(abstract_machine(pos(1,1,5,1,392,4),machine(pos(2,1,5,1,5,8)),machine_header(pos(3,1,6,5,6,28),'Spaceship_And_Asteroids',[]),[sets(pos(4,1,8,1,38,6),[enumerated_set(pos(5,1,9,5,15,6),'NAVIGATION',[identifier(pos(6,1,11,9,11,15),moveUp),identifier(pos(7,1,12,9,12,17),moveDown),identifier(pos(8,1,13,9,13,20),moveForward),identifier(pos(9,1,14,9,14,21),moveBackward)]),enumerated_set(pos(10,1,17,5,22,6),'STATUS',[identifier(pos(11,1,19,9,19,17),'Game_WON'),identifier(pos(12,1,20,9,20,18),'Game_LOST'),identifier(pos(13,1,21,9,21,22),'Game_Not_Over')]),enumerated_set(pos(14,1,24,5,38,6),'REPORT',[identifier(pos(15,1,26,9,26,24),'MOVE_UP_SUCCESS'),identifier(pos(16,1,27,9,27,26),'MOVE_DOWN_SUCCESS'),identifier(pos(17,1,28,9,28,29),'MOVE_FORWARD_SUCCESS'),identifier(pos(18,1,29,9,29,30),'MOVE_BACKWARD_SUCCESS'),identifier(pos(19,1,30,9,30,43),'CANNOT_MOVE__OUT_OF_SPACE_BOUNDARY'),identifier(pos(20,1,31,9,31,52),'CANNOT_MOVE__REGION_OCCUPIED_BY_AN_ASTEROID'),identifier(pos(21,1,32,9,32,48),'CANNOT_MOVE__NOT_ENOUGH_POWER_AVAILABLE'),identifier(pos(22,1,33,9,33,25),'SPACESHIP_DOCKED'),identifier(pos(23,1,34,9,34,29),'SPACESHIP_NOT_DOCKED'),identifier(pos(24,1,35,9,35,27),'WARP_DRIVE_SUCCESS'),identifier(pos(25,1,36,9,36,65),'CANNOT_ENGAGE_WARP_DRIVE__REGION_OCCUPIED_BY_AN_ASTEROID'),identifier(pos(26,1,37,9,37,61),'CANNOT_ENGAGE_WARP_DRIVE__NOT_ENOUGH_POWER_AVAILABLE')])]),constants(pos(27,1,40,1,53,25),[identifier(pos(28,1,41,5,41,9),grid),identifier(pos(29,1,42,5,42,16),grid_x_axis),identifier(pos(30,1,43,5,43,16),grid_y_axis),identifier(pos(31,1,44,5,44,22),grid_x_axis_begin),identifier(pos(32,1,45,5,45,20),grid_x_axis_end),identifier(pos(33,1,46,5,46,22),grid_y_axis_begin),identifier(pos(34,1,47,5,47,20),grid_y_axis_end),identifier(pos(35,1,48,5,48,13),homebase),identifier(pos(36,1,49,5,49,13),starbase),identifier(pos(37,1,50,5,50,17),asteroidsPos),identifier(pos(38,1,51,5,51,13),navPower),identifier(pos(39,1,52,5,52,19),warpDrivePower),identifier(pos(40,1,53,5,53,25),asteroidCrashedPower)]),properties(pos(41,1,55,1,93,60),conjunct(pos(42,1,56,5,93,60),conjunct(pos(43,1,56,5,93,32),conjunct(pos(44,1,56,5,91,48),conjunct(pos(45,1,56,5,91,26),conjunct(pos(46,1,56,5,89,35),conjunct(pos(47,1,56,5,89,20),conjunct(pos(48,1,56,5,87,6),conjunct(pos(49,1,56,5,74,33),conjunct(pos(50,1,56,5,72,54),conjunct(pos(51,1,56,5,72,29),conjunct(pos(52,1,56,5,70,54),conjunct(pos(53,1,56,5,70,29),conjunct(pos(54,1,56,5,68,70),conjunct(pos(55,1,56,5,68,36),conjunct(pos(56,1,56,5,66,74),conjunct(pos(57,1,56,5,66,38),conjunct(pos(58,1,56,5,64,71),conjunct(pos(59,1,56,5,64,36),conjunct(pos(60,1,56,5,62,74),conjunct(pos(61,1,56,5,62,38),conjunct(pos(62,1,56,5,60,60),conjunct(pos(63,1,56,5,60,25),conjunct(pos(64,1,56,5,58,45),conjunct(pos(65,1,56,5,58,24),conjunct(pos(66,1,56,5,56,46),subset(pos(67,1,56,5,56,24),identifier(pos(68,1,56,5,56,16),grid_x_axis),nat1_set(pos(69,1,56,20,56,24))),equal(pos(70,1,56,27,56,46),identifier(pos(71,1,56,27,56,38),grid_x_axis),interval(pos(72,1,56,41,56,46),integer(pos(73,1,56,41,56,42),1),integer(pos(74,1,56,44,56,46),12)))),subset(pos(75,1,58,5,58,24),identifier(pos(76,1,58,5,58,16),grid_y_axis),nat1_set(pos(77,1,58,20,58,24)))),equal(pos(78,1,58,27,58,45),identifier(pos(79,1,58,27,58,38),grid_y_axis),interval(pos(80,1,58,41,58,45),integer(pos(81,1,58,41,58,42),1),integer(pos(82,1,58,44,58,45),7)))),member(pos(83,1,60,5,60,25),identifier(pos(84,1,60,5,60,9),grid),relations(pos(85,1,60,12,60,25),nat1_set(pos(86,1,60,12,60,16)),nat1_set(pos(87,1,60,21,60,25))))),equal(pos(88,1,60,28,60,60),identifier(pos(89,1,60,28,60,32),grid),mult_or_cart(pos(90,1,60,35,60,60),identifier(pos(91,1,60,35,60,46),grid_x_axis),identifier(pos(92,1,60,49,60,60),grid_y_axis)))),member(pos(93,1,62,5,62,38),identifier(pos(94,1,62,5,62,22),grid_x_axis_begin),relations(pos(95,1,62,25,62,38),nat1_set(pos(96,1,62,25,62,29)),nat1_set(pos(97,1,62,34,62,38))))),equal(pos(98,1,62,41,62,74),identifier(pos(99,1,62,41,62,58),grid_x_axis_begin),domain_restriction(pos(100,1,62,61,62,74),set_extension(pos(101,1,62,61,62,66),[integer(pos(102,1,62,63,62,64),1)]),identifier(pos(103,1,62,70,62,74),grid)))),member(pos(104,1,64,5,64,36),identifier(pos(105,1,64,5,64,20),grid_x_axis_end),relations(pos(106,1,64,23,64,36),nat1_set(pos(107,1,64,23,64,27)),nat1_set(pos(108,1,64,32,64,36))))),equal(pos(109,1,64,39,64,71),identifier(pos(110,1,64,39,64,54),grid_x_axis_end),domain_restriction(pos(111,1,64,57,64,71),set_extension(pos(112,1,64,57,64,63),[integer(pos(113,1,64,59,64,61),12)]),identifier(pos(114,1,64,67,64,71),grid)))),member(pos(115,1,66,5,66,38),identifier(pos(116,1,66,5,66,22),grid_y_axis_begin),relations(pos(117,1,66,25,66,38),nat1_set(pos(118,1,66,25,66,29)),nat1_set(pos(119,1,66,34,66,38))))),equal(pos(120,1,66,41,66,74),identifier(pos(121,1,66,41,66,58),grid_y_axis_begin),range_restriction(pos(122,1,66,61,66,74),identifier(pos(123,1,66,61,66,65),grid),set_extension(pos(124,1,66,69,66,74),[integer(pos(125,1,66,71,66,72),1)])))),member(pos(126,1,68,5,68,36),identifier(pos(127,1,68,5,68,20),grid_y_axis_end),relations(pos(128,1,68,23,68,36),nat1_set(pos(129,1,68,23,68,27)),nat1_set(pos(130,1,68,32,68,36))))),equal(pos(131,1,68,39,68,70),identifier(pos(132,1,68,39,68,54),grid_y_axis_end),range_restriction(pos(133,1,68,57,68,70),identifier(pos(134,1,68,57,68,61),grid),set_extension(pos(135,1,68,65,68,70),[integer(pos(136,1,68,67,68,68),7)])))),member(pos(137,1,70,5,70,29),identifier(pos(138,1,70,5,70,13),homebase),relations(pos(139,1,70,16,70,29),nat1_set(pos(140,1,70,16,70,20)),nat1_set(pos(141,1,70,25,70,29))))),equal(pos(142,1,70,32,70,54),identifier(pos(143,1,70,32,70,40),homebase),set_extension(pos(144,1,70,43,70,54),[couple(pos(145,1,70,45,70,52),[integer(pos(146,1,70,45,70,46),1),integer(pos(147,1,70,51,70,52),1)])]))),member(pos(148,1,72,5,72,29),identifier(pos(149,1,72,5,72,13),starbase),relations(pos(150,1,72,16,72,29),nat1_set(pos(151,1,72,16,72,20)),nat1_set(pos(152,1,72,25,72,29))))),equal(pos(153,1,72,32,72,54),identifier(pos(154,1,72,32,72,40),starbase),set_extension(pos(155,1,72,43,72,54),[couple(pos(156,1,72,45,72,52),[integer(pos(157,1,72,45,72,46),6),integer(pos(158,1,72,51,72,52),4)])]))),member(pos(159,1,74,5,74,33),identifier(pos(160,1,74,5,74,17),asteroidsPos),relations(pos(161,1,74,20,74,33),nat1_set(pos(162,1,74,20,74,24)),nat1_set(pos(163,1,74,29,74,33))))),equal(pos(164,1,74,36,87,6),identifier(pos(165,1,74,36,74,48),asteroidsPos),set_extension(pos(166,1,75,5,87,6),[couple(pos(167,1,76,11,76,18),[integer(pos(168,1,76,11,76,12),3),integer(pos(169,1,76,17,76,18),2)]),couple(pos(170,1,77,11,77,18),[integer(pos(171,1,77,11,77,12),3),integer(pos(172,1,77,17,77,18),5)]),couple(pos(173,1,78,11,78,18),[integer(pos(174,1,78,11,78,12),5),integer(pos(175,1,78,17,78,18),4)]),couple(pos(176,1,79,11,79,18),[integer(pos(177,1,79,11,79,12),6),integer(pos(178,1,79,17,79,18),7)]),couple(pos(179,1,80,11,80,18),[integer(pos(180,1,80,11,80,12),7),integer(pos(181,1,80,17,80,18),1)]),couple(pos(182,1,81,11,81,18),[integer(pos(183,1,81,11,81,12),7),integer(pos(184,1,81,17,81,18),5)]),couple(pos(185,1,82,11,82,18),[integer(pos(186,1,82,11,82,12),7),integer(pos(187,1,82,17,82,18),7)]),couple(pos(188,1,83,11,83,18),[integer(pos(189,1,83,11,83,12),8),integer(pos(190,1,83,17,83,18),3)]),couple(pos(191,1,84,11,84,19),[integer(pos(192,1,84,11,84,13),10),integer(pos(193,1,84,18,84,19),6)]),couple(pos(194,1,85,11,85,19),[integer(pos(195,1,85,11,85,13),11),integer(pos(196,1,85,18,85,19),2)]),couple(pos(197,1,86,11,86,19),[integer(pos(198,1,86,11,86,13),12),integer(pos(199,1,86,18,86,19),5)])]))),member(pos(200,1,89,5,89,20),identifier(pos(201,1,89,5,89,13),navPower),nat1_set(pos(202,1,89,16,89,20)))),equal(pos(203,1,89,23,89,35),identifier(pos(204,1,89,23,89,31),navPower),integer(pos(205,1,89,34,89,35),5))),member(pos(206,1,91,5,91,26),identifier(pos(207,1,91,5,91,19),warpDrivePower),nat1_set(pos(208,1,91,22,91,26)))),equal(pos(209,1,91,29,91,48),identifier(pos(210,1,91,29,91,43),warpDrivePower),integer(pos(211,1,91,46,91,48),20))),member(pos(212,1,93,5,93,32),identifier(pos(213,1,93,5,93,25),asteroidCrashedPower),nat1_set(pos(214,1,93,28,93,32)))),equal(pos(215,1,93,35,93,60),identifier(pos(216,1,93,35,93,55),asteroidCrashedPower),integer(pos(217,1,93,58,93,60),10)))),variables(pos(218,1,95,1,103,20),[identifier(pos(219,1,96,5,96,15),x_axis_pos),identifier(pos(220,1,98,5,98,15),y_axis_pos),identifier(pos(221,1,100,5,100,19),spaceshipPower),identifier(pos(222,1,102,5,102,18),spaceshipPath),identifier(pos(223,1,103,5,103,20),numberOfCrashes)]),invariant(pos(224,1,106,1,115,26),conjunct(pos(225,1,107,5,115,26),conjunct(pos(226,1,107,5,113,37),conjunct(pos(227,1,107,5,111,25),conjunct(pos(228,1,107,5,109,49),conjunct(pos(229,1,107,5,109,22),conjunct(pos(230,1,107,5,107,49),member(pos(231,1,107,5,107,22),identifier(pos(232,1,107,5,107,15),x_axis_pos),nat1_set(pos(233,1,107,18,107,22))),member(pos(234,1,107,25,107,49),identifier(pos(235,1,107,25,107,35),x_axis_pos),identifier(pos(236,1,107,38,107,49),grid_x_axis))),member(pos(237,1,109,5,109,22),identifier(pos(238,1,109,5,109,15),y_axis_pos),nat1_set(pos(239,1,109,18,109,22)))),member(pos(240,1,109,25,109,49),identifier(pos(241,1,109,25,109,35),y_axis_pos),identifier(pos(242,1,109,38,109,49),grid_y_axis))),member(pos(243,1,111,5,111,25),identifier(pos(244,1,111,5,111,19),spaceshipPower),nat_set(pos(245,1,111,22,111,25)))),member(pos(246,1,113,5,113,37),identifier(pos(247,1,113,5,113,18),spaceshipPath),seq(pos(248,1,113,21,113,37),mult_or_cart(pos(249,1,113,25,113,36),nat1_set(pos(250,1,113,25,113,29)),nat1_set(pos(251,1,113,32,113,36)))))),member(pos(252,1,115,5,115,26),identifier(pos(253,1,115,5,115,20),numberOfCrashes),nat_set(pos(254,1,115,23,115,26))))),initialisation(pos(255,1,117,1,122,25),parallel(pos(256,1,118,5,122,25),[assign(pos(257,1,118,5,118,20),[identifier(pos(258,1,118,5,118,15),x_axis_pos)],[integer(pos(259,1,118,19,118,20),1)]),assign(pos(260,1,119,5,119,20),[identifier(pos(261,1,119,5,119,15),y_axis_pos)],[integer(pos(262,1,119,19,119,20),1)]),assign(pos(263,1,120,5,120,26),[identifier(pos(264,1,120,5,120,19),spaceshipPower)],[integer(pos(265,1,120,23,120,26),100)]),assign(pos(266,1,121,5,121,24),[identifier(pos(267,1,121,5,121,18),spaceshipPath)],[empty_sequence(pos(268,1,121,22,121,24))]),assign(pos(269,1,122,5,122,25),[identifier(pos(270,1,122,5,122,20),numberOfCrashes)],[integer(pos(271,1,122,24,122,25),0)])])),operations(pos(272,1,124,1,390,8),[operation(pos(273,1,125,5,311,8),identifier(pos(273,1,125,5,311,8),spaceshipNavigation),[identifier(pos(274,1,125,5,125,11),report)],[identifier(pos(275,1,125,38,125,47),direction)],precondition(pos(276,1,126,5,311,8),member(pos(277,1,126,9,126,31),identifier(pos(278,1,126,9,126,18),direction),identifier(pos(279,1,126,21,126,31),'NAVIGATION')),if(pos(280,1,129,9,310,20),equal(pos(281,1,129,13,129,31),identifier(pos(282,1,129,13,129,22),direction),identifier(pos(283,1,129,25,129,31),moveUp)),if(pos(284,1,131,13,172,16),conjunct(pos(285,1,132,21,136,68),conjunct(pos(286,1,132,21,134,67),greater_equal(pos(287,1,132,21,132,47),identifier(pos(288,1,132,21,132,35),spaceshipPower),identifier(pos(289,1,132,39,132,47),navPower)),not_member(pos(290,1,134,22,134,67),couple(pos(291,1,134,22,134,47),[identifier(pos(292,1,134,22,134,32),x_axis_pos),identifier(pos(293,1,134,37,134,47),y_axis_pos)]),identifier(pos(294,1,134,52,134,67),grid_y_axis_end))),not_member(pos(295,1,136,22,136,68),couple(pos(296,1,136,22,136,51),[identifier(pos(297,1,136,22,136,32),x_axis_pos),add(pos(298,1,136,37,136,51),identifier(pos(299,1,136,37,136,47),y_axis_pos),integer(pos(300,1,136,50,136,51),1))]),identifier(pos(301,1,136,56,136,68),asteroidsPos))),parallel(pos(302,1,140,17,146,42),[assign(pos(303,1,140,17,140,45),[identifier(pos(304,1,140,17,140,27),y_axis_pos)],[add(pos(305,1,140,31,140,45),identifier(pos(306,1,140,31,140,41),y_axis_pos),integer(pos(307,1,140,44,140,45),1))]),assign(pos(308,1,142,17,142,60),[identifier(pos(309,1,142,17,142,31),spaceshipPower)],[minus_or_set_subtract(pos(310,1,142,35,142,60),identifier(pos(311,1,142,35,142,49),spaceshipPower),identifier(pos(312,1,142,52,142,60),navPower))]),assign(pos(313,1,144,17,144,78),[identifier(pos(314,1,144,17,144,30),spaceshipPath)],[insert_tail(pos(315,1,144,34,144,78),identifier(pos(316,1,144,34,144,47),spaceshipPath),couple(pos(317,1,144,53,144,78),[identifier(pos(318,1,144,53,144,63),x_axis_pos),identifier(pos(319,1,144,68,144,78),y_axis_pos)]))]),assign(pos(320,1,146,17,146,42),[identifier(pos(321,1,146,17,146,23),report)],[identifier(pos(322,1,146,27,146,42),'MOVE_UP_SUCCESS')])]),[if_elsif(pos(323,1,148,13,171,20),disjunct(pos(324,1,149,25,153,71),disjunct(pos(325,1,149,25,151,70),less(pos(326,1,149,25,149,50),identifier(pos(327,1,149,25,149,39),spaceshipPower),identifier(pos(328,1,149,42,149,50),navPower)),member(pos(329,1,151,26,151,70),couple(pos(330,1,151,26,151,51),[identifier(pos(331,1,151,26,151,36),x_axis_pos),identifier(pos(332,1,151,41,151,51),y_axis_pos)]),identifier(pos(333,1,151,55,151,70),grid_y_axis_end))),member(pos(334,1,153,26,153,71),couple(pos(335,1,153,26,153,55),[identifier(pos(336,1,153,26,153,36),x_axis_pos),add(pos(337,1,153,41,153,55),identifier(pos(338,1,153,41,153,51),y_axis_pos),integer(pos(339,1,153,54,153,55),1))]),identifier(pos(340,1,153,59,153,71),asteroidsPos))),if(pos(341,1,156,17,171,20),less(pos(342,1,156,22,156,47),identifier(pos(343,1,156,22,156,36),spaceshipPower),identifier(pos(344,1,156,39,156,47),navPower)),assign(pos(345,1,158,21,158,69),[identifier(pos(346,1,158,21,158,27),report)],[identifier(pos(347,1,158,30,158,69),'CANNOT_MOVE__NOT_ENOUGH_POWER_AVAILABLE')]),[if_elsif(pos(348,1,160,17,162,65),member(pos(349,1,160,24,160,68),couple(pos(350,1,160,24,160,49),[identifier(pos(351,1,160,24,160,34),x_axis_pos),identifier(pos(352,1,160,39,160,49),y_axis_pos)]),identifier(pos(353,1,160,53,160,68),grid_y_axis_end)),assign(pos(354,1,162,21,162,65),[identifier(pos(355,1,162,21,162,27),report)],[identifier(pos(356,1,162,31,162,65),'CANNOT_MOVE__OUT_OF_SPACE_BOUNDARY')])),if_elsif(pos(357,1,164,17,170,70),member(pos(358,1,164,26,164,71),couple(pos(359,1,164,26,164,55),[identifier(pos(360,1,164,26,164,36),x_axis_pos),add(pos(361,1,164,41,164,55),identifier(pos(362,1,164,41,164,51),y_axis_pos),integer(pos(363,1,164,54,164,55),1))]),identifier(pos(364,1,164,59,164,71),asteroidsPos)),parallel(pos(365,1,166,21,170,70),[assign(pos(366,1,166,21,166,74),[identifier(pos(367,1,166,21,166,27),report)],[identifier(pos(368,1,166,31,166,74),'CANNOT_MOVE__REGION_OCCUPIED_BY_AN_ASTEROID')]),assign(pos(369,1,168,21,168,59),[identifier(pos(370,1,168,21,168,36),numberOfCrashes)],[add(pos(371,1,168,40,168,59),identifier(pos(372,1,168,40,168,55),numberOfCrashes),integer(pos(373,1,168,58,168,59),1))]),assign(pos(374,1,170,21,170,70),[identifier(pos(375,1,170,21,170,35),spaceshipPower)],[minus_or_set_subtract(pos(376,1,170,39,170,70),identifier(pos(377,1,170,39,170,53),spaceshipPower),identifier(pos(378,1,170,56,170,70),warpDrivePower))])]))],skip(none)))],skip(none)),[if_elsif(pos(379,1,175,9,217,16),equal(pos(380,1,175,16,175,36),identifier(pos(381,1,175,16,175,25),direction),identifier(pos(382,1,175,28,175,36),moveDown)),if(pos(383,1,177,13,217,16),conjunct(pos(384,1,178,21,182,68),conjunct(pos(385,1,178,21,180,69),greater_equal(pos(386,1,178,21,178,47),identifier(pos(387,1,178,21,178,35),spaceshipPower),identifier(pos(388,1,178,39,178,47),navPower)),not_member(pos(389,1,180,22,180,69),couple(pos(390,1,180,22,180,47),[identifier(pos(391,1,180,22,180,32),x_axis_pos),identifier(pos(392,1,180,37,180,47),y_axis_pos)]),identifier(pos(393,1,180,52,180,69),grid_y_axis_begin))),not_member(pos(394,1,182,22,182,68),couple(pos(395,1,182,22,182,51),[identifier(pos(396,1,182,22,182,32),x_axis_pos),minus_or_set_subtract(pos(397,1,182,37,182,51),identifier(pos(398,1,182,37,182,47),y_axis_pos),integer(pos(399,1,182,50,182,51),1))]),identifier(pos(400,1,182,56,182,68),asteroidsPos))),parallel(pos(401,1,185,17,191,44),[assign(pos(402,1,185,17,185,45),[identifier(pos(403,1,185,17,185,27),y_axis_pos)],[minus_or_set_subtract(pos(404,1,185,31,185,45),identifier(pos(405,1,185,31,185,41),y_axis_pos),integer(pos(406,1,185,44,185,45),1))]),assign(pos(407,1,187,17,187,60),[identifier(pos(408,1,187,17,187,31),spaceshipPower)],[minus_or_set_subtract(pos(409,1,187,35,187,60),identifier(pos(410,1,187,35,187,49),spaceshipPower),identifier(pos(411,1,187,52,187,60),navPower))]),assign(pos(412,1,189,17,189,78),[identifier(pos(413,1,189,17,189,30),spaceshipPath)],[insert_tail(pos(414,1,189,34,189,78),identifier(pos(415,1,189,34,189,47),spaceshipPath),couple(pos(416,1,189,53,189,78),[identifier(pos(417,1,189,53,189,63),x_axis_pos),identifier(pos(418,1,189,68,189,78),y_axis_pos)]))]),assign(pos(419,1,191,17,191,44),[identifier(pos(420,1,191,17,191,23),report)],[identifier(pos(421,1,191,27,191,44),'MOVE_DOWN_SUCCESS')])]),[if_elsif(pos(422,1,193,13,216,20),disjunct(pos(423,1,194,25,198,71),disjunct(pos(424,1,194,25,196,72),less(pos(425,1,194,25,194,50),identifier(pos(426,1,194,25,194,39),spaceshipPower),identifier(pos(427,1,194,42,194,50),navPower)),member(pos(428,1,196,26,196,72),couple(pos(429,1,196,26,196,51),[identifier(pos(430,1,196,26,196,36),x_axis_pos),identifier(pos(431,1,196,41,196,51),y_axis_pos)]),identifier(pos(432,1,196,55,196,72),grid_y_axis_begin))),member(pos(433,1,198,26,198,71),couple(pos(434,1,198,26,198,55),[identifier(pos(435,1,198,26,198,36),x_axis_pos),minus_or_set_subtract(pos(436,1,198,41,198,55),identifier(pos(437,1,198,41,198,51),y_axis_pos),integer(pos(438,1,198,54,198,55),1))]),identifier(pos(439,1,198,59,198,71),asteroidsPos))),if(pos(440,1,201,17,216,20),less(pos(441,1,201,22,201,47),identifier(pos(442,1,201,22,201,36),spaceshipPower),identifier(pos(443,1,201,39,201,47),navPower)),assign(pos(444,1,203,21,203,69),[identifier(pos(445,1,203,21,203,27),report)],[identifier(pos(446,1,203,30,203,69),'CANNOT_MOVE__NOT_ENOUGH_POWER_AVAILABLE')]),[if_elsif(pos(447,1,205,17,207,65),member(pos(448,1,205,26,205,72),couple(pos(449,1,205,26,205,51),[identifier(pos(450,1,205,26,205,36),x_axis_pos),identifier(pos(451,1,205,41,205,51),y_axis_pos)]),identifier(pos(452,1,205,55,205,72),grid_y_axis_begin)),assign(pos(453,1,207,21,207,65),[identifier(pos(454,1,207,21,207,27),report)],[identifier(pos(455,1,207,31,207,65),'CANNOT_MOVE__OUT_OF_SPACE_BOUNDARY')])),if_elsif(pos(456,1,209,17,215,70),member(pos(457,1,209,26,209,71),couple(pos(458,1,209,26,209,55),[identifier(pos(459,1,209,26,209,36),x_axis_pos),minus_or_set_subtract(pos(460,1,209,41,209,55),identifier(pos(461,1,209,41,209,51),y_axis_pos),integer(pos(462,1,209,54,209,55),1))]),identifier(pos(463,1,209,59,209,71),asteroidsPos)),parallel(pos(464,1,211,21,215,70),[assign(pos(465,1,211,21,211,74),[identifier(pos(466,1,211,21,211,27),report)],[identifier(pos(467,1,211,31,211,74),'CANNOT_MOVE__REGION_OCCUPIED_BY_AN_ASTEROID')]),assign(pos(468,1,213,21,213,55),[identifier(pos(469,1,213,21,213,36),numberOfCrashes)],[identifier(pos(470,1,213,40,213,55),numberOfCrashes)]),assign(pos(471,1,215,21,215,70),[identifier(pos(472,1,215,21,215,35),spaceshipPower)],[minus_or_set_subtract(pos(473,1,215,39,215,70),identifier(pos(474,1,215,39,215,53),spaceshipPower),identifier(pos(475,1,215,56,215,70),warpDrivePower))])]))],skip(none)))],skip(none))),if_elsif(pos(476,1,220,13,263,20),equal(pos(477,1,220,20,220,43),identifier(pos(478,1,220,20,220,29),direction),identifier(pos(479,1,220,32,220,43),moveForward)),if(pos(480,1,222,17,263,20),conjunct(pos(481,1,223,25,227,74),conjunct(pos(482,1,223,25,225,73),greater_equal(pos(483,1,223,25,223,51),identifier(pos(484,1,223,25,223,39),spaceshipPower),identifier(pos(485,1,223,43,223,51),navPower)),not_member(pos(486,1,225,27,225,73),couple(pos(487,1,225,27,225,52),[identifier(pos(488,1,225,27,225,37),x_axis_pos),identifier(pos(489,1,225,42,225,52),y_axis_pos)]),identifier(pos(490,1,225,58,225,73),grid_x_axis_end))),not_member(pos(491,1,227,27,227,74),couple(pos(492,1,227,27,227,56),[add(pos(493,1,227,27,227,41),identifier(pos(494,1,227,27,227,37),x_axis_pos),integer(pos(495,1,227,40,227,41),1)),identifier(pos(496,1,227,46,227,56),y_axis_pos)]),identifier(pos(497,1,227,62,227,74),asteroidsPos))),parallel(pos(498,1,230,21,236,51),[assign(pos(499,1,230,21,230,49),[identifier(pos(500,1,230,21,230,31),x_axis_pos)],[add(pos(501,1,230,35,230,49),identifier(pos(502,1,230,35,230,45),x_axis_pos),integer(pos(503,1,230,48,230,49),1))]),assign(pos(504,1,232,21,232,64),[identifier(pos(505,1,232,21,232,35),spaceshipPower)],[minus_or_set_subtract(pos(506,1,232,39,232,64),identifier(pos(507,1,232,39,232,53),spaceshipPower),identifier(pos(508,1,232,56,232,64),navPower))]),assign(pos(509,1,234,21,234,82),[identifier(pos(510,1,234,21,234,34),spaceshipPath)],[insert_tail(pos(511,1,234,38,234,82),identifier(pos(512,1,234,38,234,51),spaceshipPath),couple(pos(513,1,234,57,234,82),[identifier(pos(514,1,234,57,234,67),x_axis_pos),identifier(pos(515,1,234,72,234,82),y_axis_pos)]))]),assign(pos(516,1,236,21,236,51),[identifier(pos(517,1,236,21,236,27),report)],[identifier(pos(518,1,236,31,236,51),'MOVE_FORWARD_SUCCESS')])]),[if_elsif(pos(519,1,238,17,262,24),disjunct(pos(520,1,239,29,243,75),disjunct(pos(521,1,239,29,241,74),less(pos(522,1,239,29,239,54),identifier(pos(523,1,239,29,239,43),spaceshipPower),identifier(pos(524,1,239,46,239,54),navPower)),member(pos(525,1,241,30,241,74),couple(pos(526,1,241,30,241,55),[identifier(pos(527,1,241,30,241,40),x_axis_pos),identifier(pos(528,1,241,45,241,55),y_axis_pos)]),identifier(pos(529,1,241,59,241,74),grid_x_axis_end))),member(pos(530,1,243,30,243,75),couple(pos(531,1,243,30,243,59),[add(pos(532,1,243,30,243,44),identifier(pos(533,1,243,30,243,40),x_axis_pos),integer(pos(534,1,243,43,243,44),1)),identifier(pos(535,1,243,49,243,59),y_axis_pos)]),identifier(pos(536,1,243,63,243,75),asteroidsPos))),if(pos(537,1,246,21,262,24),less(pos(538,1,246,26,246,51),identifier(pos(539,1,246,26,246,40),spaceshipPower),identifier(pos(540,1,246,43,246,51),navPower)),assign(pos(541,1,248,25,248,73),[identifier(pos(542,1,248,25,248,31),report)],[identifier(pos(543,1,248,34,248,73),'CANNOT_MOVE__NOT_ENOUGH_POWER_AVAILABLE')]),[if_elsif(pos(544,1,250,21,252,69),member(pos(545,1,250,30,250,74),couple(pos(546,1,250,30,250,55),[identifier(pos(547,1,250,30,250,40),x_axis_pos),identifier(pos(548,1,250,45,250,55),y_axis_pos)]),identifier(pos(549,1,250,59,250,74),grid_x_axis_end)),assign(pos(550,1,252,25,252,69),[identifier(pos(551,1,252,25,252,31),report)],[identifier(pos(552,1,252,35,252,69),'CANNOT_MOVE__OUT_OF_SPACE_BOUNDARY')])),if_elsif(pos(553,1,254,21,260,74),member(pos(554,1,254,30,254,75),couple(pos(555,1,254,30,254,59),[add(pos(556,1,254,30,254,44),identifier(pos(557,1,254,30,254,40),x_axis_pos),integer(pos(558,1,254,43,254,44),1)),identifier(pos(559,1,254,49,254,59),y_axis_pos)]),identifier(pos(560,1,254,63,254,75),asteroidsPos)),parallel(pos(561,1,256,25,260,74),[assign(pos(562,1,256,25,256,78),[identifier(pos(563,1,256,25,256,31),report)],[identifier(pos(564,1,256,35,256,78),'CANNOT_MOVE__REGION_OCCUPIED_BY_AN_ASTEROID')]),assign(pos(565,1,258,25,258,59),[identifier(pos(566,1,258,25,258,40),numberOfCrashes)],[identifier(pos(567,1,258,44,258,59),numberOfCrashes)]),assign(pos(568,1,260,25,260,74),[identifier(pos(569,1,260,25,260,39),spaceshipPower)],[minus_or_set_subtract(pos(570,1,260,43,260,74),identifier(pos(571,1,260,43,260,57),spaceshipPower),identifier(pos(572,1,260,60,260,74),warpDrivePower))])]))],skip(none)))],skip(none))),if_elsif(pos(573,1,266,17,308,24),equal(pos(574,1,266,24,266,48),identifier(pos(575,1,266,24,266,33),direction),identifier(pos(576,1,266,36,266,48),moveBackward)),if(pos(577,1,268,21,308,24),conjunct(pos(578,1,269,29,273,76),conjunct(pos(579,1,269,29,271,77),greater_equal(pos(580,1,269,29,269,55),identifier(pos(581,1,269,29,269,43),spaceshipPower),identifier(pos(582,1,269,47,269,55),navPower)),not_member(pos(583,1,271,30,271,77),couple(pos(584,1,271,30,271,55),[identifier(pos(585,1,271,30,271,40),x_axis_pos),identifier(pos(586,1,271,45,271,55),y_axis_pos)]),identifier(pos(587,1,271,60,271,77),grid_x_axis_begin))),not_member(pos(588,1,273,30,273,76),couple(pos(589,1,273,30,273,59),[minus_or_set_subtract(pos(590,1,273,30,273,44),identifier(pos(591,1,273,30,273,40),x_axis_pos),integer(pos(592,1,273,43,273,44),1)),identifier(pos(593,1,273,49,273,59),y_axis_pos)]),identifier(pos(594,1,273,64,273,76),asteroidsPos))),parallel(pos(595,1,276,25,282,56),[assign(pos(596,1,276,25,276,53),[identifier(pos(597,1,276,25,276,35),x_axis_pos)],[minus_or_set_subtract(pos(598,1,276,39,276,53),identifier(pos(599,1,276,39,276,49),x_axis_pos),integer(pos(600,1,276,52,276,53),1))]),assign(pos(601,1,278,25,278,68),[identifier(pos(602,1,278,25,278,39),spaceshipPower)],[minus_or_set_subtract(pos(603,1,278,43,278,68),identifier(pos(604,1,278,43,278,57),spaceshipPower),identifier(pos(605,1,278,60,278,68),navPower))]),assign(pos(606,1,280,25,280,86),[identifier(pos(607,1,280,25,280,38),spaceshipPath)],[insert_tail(pos(608,1,280,42,280,86),identifier(pos(609,1,280,42,280,55),spaceshipPath),couple(pos(610,1,280,61,280,86),[identifier(pos(611,1,280,61,280,71),x_axis_pos),identifier(pos(612,1,280,76,280,86),y_axis_pos)]))]),assign(pos(613,1,282,25,282,56),[identifier(pos(614,1,282,25,282,31),report)],[identifier(pos(615,1,282,35,282,56),'MOVE_BACKWARD_SUCCESS')])]),[if_elsif(pos(616,1,284,21,307,28),disjunct(pos(617,1,285,33,289,79),disjunct(pos(618,1,285,33,287,80),less(pos(619,1,285,33,285,58),identifier(pos(620,1,285,33,285,47),spaceshipPower),identifier(pos(621,1,285,50,285,58),navPower)),member(pos(622,1,287,34,287,80),couple(pos(623,1,287,34,287,59),[identifier(pos(624,1,287,34,287,44),x_axis_pos),identifier(pos(625,1,287,49,287,59),y_axis_pos)]),identifier(pos(626,1,287,63,287,80),grid_x_axis_begin))),member(pos(627,1,289,34,289,79),couple(pos(628,1,289,34,289,63),[minus_or_set_subtract(pos(629,1,289,34,289,48),identifier(pos(630,1,289,34,289,44),x_axis_pos),integer(pos(631,1,289,47,289,48),1)),identifier(pos(632,1,289,53,289,63),y_axis_pos)]),identifier(pos(633,1,289,67,289,79),asteroidsPos))),if(pos(634,1,292,25,307,28),less(pos(635,1,292,30,292,55),identifier(pos(636,1,292,30,292,44),spaceshipPower),identifier(pos(637,1,292,47,292,55),navPower)),assign(pos(638,1,294,29,294,77),[identifier(pos(639,1,294,29,294,35),report)],[identifier(pos(640,1,294,38,294,77),'CANNOT_MOVE__NOT_ENOUGH_POWER_AVAILABLE')]),[if_elsif(pos(641,1,296,25,298,73),member(pos(642,1,296,34,296,80),couple(pos(643,1,296,34,296,59),[identifier(pos(644,1,296,34,296,44),x_axis_pos),identifier(pos(645,1,296,49,296,59),y_axis_pos)]),identifier(pos(646,1,296,63,296,80),grid_x_axis_begin)),assign(pos(647,1,298,29,298,73),[identifier(pos(648,1,298,29,298,35),report)],[identifier(pos(649,1,298,39,298,73),'CANNOT_MOVE__OUT_OF_SPACE_BOUNDARY')])),if_elsif(pos(650,1,300,25,306,78),member(pos(651,1,300,34,300,79),couple(pos(652,1,300,34,300,63),[minus_or_set_subtract(pos(653,1,300,34,300,48),identifier(pos(654,1,300,34,300,44),x_axis_pos),integer(pos(655,1,300,47,300,48),1)),identifier(pos(656,1,300,53,300,63),y_axis_pos)]),identifier(pos(657,1,300,67,300,79),asteroidsPos)),parallel(pos(658,1,302,29,306,78),[assign(pos(659,1,302,29,302,82),[identifier(pos(660,1,302,29,302,35),report)],[identifier(pos(661,1,302,39,302,82),'CANNOT_MOVE__REGION_OCCUPIED_BY_AN_ASTEROID')]),assign(pos(662,1,304,29,304,63),[identifier(pos(663,1,304,29,304,44),numberOfCrashes)],[identifier(pos(664,1,304,48,304,63),numberOfCrashes)]),assign(pos(665,1,306,29,306,78),[identifier(pos(666,1,306,29,306,43),spaceshipPower)],[minus_or_set_subtract(pos(667,1,306,47,306,78),identifier(pos(668,1,306,47,306,61),spaceshipPower),identifier(pos(669,1,306,64,306,78),warpDrivePower))])]))],skip(none)))],skip(none)))],skip(none)))),operation(pos(670,1,316,5,356,8),identifier(pos(670,1,316,5,356,8),engageWarpDrive),[identifier(pos(671,1,316,5,316,11),report)],[identifier(pos(672,1,316,33,316,43),new_x_axis),identifier(pos(673,1,316,45,316,55),new_y_axis)],precondition(pos(674,1,317,5,356,8),member(pos(675,1,317,9,317,41),couple(pos(676,1,317,9,317,34),[identifier(pos(677,1,317,9,317,19),new_x_axis),identifier(pos(678,1,317,24,317,34),new_y_axis)]),identifier(pos(679,1,317,37,317,41),grid)),if(pos(680,1,319,9,355,12),conjunct(pos(681,1,321,17,323,58),greater_equal(pos(682,1,321,17,321,49),identifier(pos(683,1,321,17,321,31),spaceshipPower),identifier(pos(684,1,321,35,321,49),warpDrivePower)),not_member(pos(685,1,323,17,323,58),couple(pos(686,1,323,17,323,42),[identifier(pos(687,1,323,17,323,27),new_x_axis),identifier(pos(688,1,323,32,323,42),new_y_axis)]),identifier(pos(689,1,323,46,323,58),asteroidsPos))),parallel(pos(690,1,326,13,334,41),[assign(pos(691,1,326,13,326,37),[identifier(pos(692,1,326,13,326,23),x_axis_pos)],[identifier(pos(693,1,326,27,326,37),new_x_axis)]),assign(pos(694,1,328,13,328,37),[identifier(pos(695,1,328,13,328,23),y_axis_pos)],[identifier(pos(696,1,328,27,328,37),new_y_axis)]),assign(pos(697,1,330,13,330,62),[identifier(pos(698,1,330,13,330,27),spaceshipPower)],[minus_or_set_subtract(pos(699,1,330,31,330,62),identifier(pos(700,1,330,31,330,45),spaceshipPower),identifier(pos(701,1,330,48,330,62),warpDrivePower))]),assign(pos(702,1,332,13,332,74),[identifier(pos(703,1,332,13,332,26),spaceshipPath)],[insert_tail(pos(704,1,332,30,332,74),identifier(pos(705,1,332,30,332,43),spaceshipPath),couple(pos(706,1,332,49,332,74),[identifier(pos(707,1,332,49,332,59),x_axis_pos),identifier(pos(708,1,332,64,332,74),y_axis_pos)]))]),assign(pos(709,1,334,13,334,41),[identifier(pos(710,1,334,13,334,19),report)],[identifier(pos(711,1,334,23,334,41),'WARP_DRIVE_SUCCESS')])]),[if_elsif(pos(712,1,336,9,354,16),disjunct(pos(713,1,338,17,340,57),less(pos(714,1,338,17,338,48),identifier(pos(715,1,338,17,338,31),spaceshipPower),identifier(pos(716,1,338,34,338,48),warpDrivePower)),member(pos(717,1,340,17,340,57),couple(pos(718,1,340,17,340,42),[identifier(pos(719,1,340,17,340,27),new_x_axis),identifier(pos(720,1,340,32,340,42),new_y_axis)]),identifier(pos(721,1,340,45,340,57),asteroidsPos))),if(pos(722,1,343,13,354,16),less(pos(723,1,343,18,343,49),identifier(pos(724,1,343,18,343,32),spaceshipPower),identifier(pos(725,1,343,35,343,49),warpDrivePower)),assign(pos(726,1,345,17,345,79),[identifier(pos(727,1,345,17,345,23),report)],[identifier(pos(728,1,345,27,345,79),'CANNOT_ENGAGE_WARP_DRIVE__NOT_ENOUGH_POWER_AVAILABLE')]),[if_elsif(pos(729,1,347,13,353,66),member(pos(730,1,347,21,347,61),couple(pos(731,1,347,21,347,46),[identifier(pos(732,1,347,21,347,31),new_x_axis),identifier(pos(733,1,347,36,347,46),new_y_axis)]),identifier(pos(734,1,347,49,347,61),asteroidsPos)),parallel(pos(735,1,349,17,353,66),[assign(pos(736,1,349,17,349,83),[identifier(pos(737,1,349,17,349,23),report)],[identifier(pos(738,1,349,27,349,83),'CANNOT_ENGAGE_WARP_DRIVE__REGION_OCCUPIED_BY_AN_ASTEROID')]),assign(pos(739,1,351,17,351,51),[identifier(pos(740,1,351,17,351,32),numberOfCrashes)],[identifier(pos(741,1,351,36,351,51),numberOfCrashes)]),assign(pos(742,1,353,17,353,66),[identifier(pos(743,1,353,17,353,31),spaceshipPower)],[minus_or_set_subtract(pos(744,1,353,35,353,66),identifier(pos(745,1,353,35,353,49),spaceshipPower),identifier(pos(746,1,353,52,353,66),warpDrivePower))])]))],skip(none)))],skip(none)))),operation(pos(747,1,359,5,362,8),identifier(pos(747,1,359,5,362,8),getCurrentPos),[identifier(pos(748,1,359,5,359,8),pos)],[],block(pos(749,1,360,5,362,8),assign(pos(750,1,361,9,361,41),[identifier(pos(751,1,361,9,361,12),pos)],[couple(pos(752,1,361,16,361,41),[identifier(pos(753,1,361,16,361,26),x_axis_pos),identifier(pos(754,1,361,31,361,41),y_axis_pos)])]))),operation(pos(755,1,365,5,368,8),identifier(pos(755,1,365,5,368,8),missionRoute),[identifier(pos(756,1,365,5,365,10),route)],[],block(pos(757,1,366,5,368,8),assign(pos(758,1,367,9,367,31),[identifier(pos(759,1,367,9,367,14),route)],[identifier(pos(760,1,367,18,367,31),spaceshipPath)]))),operation(pos(761,1,371,5,378,8),identifier(pos(761,1,371,5,378,8),missionStatus),[identifier(pos(762,1,371,5,371,20),currentLocation),identifier(pos(763,1,371,22,371,34),currentPower),identifier(pos(764,1,371,36,371,51),asteroidCrashes)],[],block(pos(765,1,372,5,378,8),parallel(pos(766,1,373,9,377,43),[assign(pos(767,1,373,9,373,54),[identifier(pos(768,1,373,9,373,24),currentLocation)],[couple(pos(769,1,373,29,373,54),[identifier(pos(770,1,373,29,373,39),x_axis_pos),identifier(pos(771,1,373,44,373,54),y_axis_pos)])]),assign(pos(772,1,375,9,375,39),[identifier(pos(773,1,375,9,375,21),currentPower)],[identifier(pos(774,1,375,25,375,39),spaceshipPower)]),assign(pos(775,1,377,9,377,43),[identifier(pos(776,1,377,9,377,24),asteroidCrashes)],[identifier(pos(777,1,377,28,377,43),numberOfCrashes)])]))),operation(pos(778,1,381,5,390,8),identifier(pos(778,1,381,5,390,8),dockedAtStarbase),[identifier(pos(779,1,381,5,381,11),report)],[],block(pos(780,1,382,5,390,8),if(pos(781,1,383,9,389,12),member(pos(782,1,383,14,383,50),couple(pos(783,1,383,14,383,39),[identifier(pos(784,1,383,14,383,24),x_axis_pos),identifier(pos(785,1,383,29,383,39),y_axis_pos)]),identifier(pos(786,1,383,42,383,50),starbase)),assign(pos(787,1,385,13,385,39),[identifier(pos(788,1,385,13,385,19),report)],[identifier(pos(789,1,385,23,385,39),'SPACESHIP_DOCKED')]),[],assign(pos(790,1,388,13,388,43),[identifier(pos(791,1,388,13,388,19),report)],[identifier(pos(792,1,388,23,388,43),'SPACESHIP_NOT_DOCKED')]))))])])).