-
Notifications
You must be signed in to change notification settings - Fork 0
/
Spaceship.prob
4 lines (4 loc) · 22.6 KB
/
Spaceship.prob
1
2
3
4
parser_version('456efb928642d91bb84e63d65abf3e25a59815ee').
classical_b('Spaceship',['/Users/akshayan/Desktop/w1867142_Formal Methods_CW/Old Asteroids Arcade Game/Spaceship.mch','/Users/akshayan/Desktop/w1867142_Formal Methods_CW/Old Asteroids Arcade Game/SpaceRegion.mch']).
machine(abstract_machine(p5(2,6,1,40,4),machine(p4(2,6,1,8)),machine_header(p4(2,7,5,16),'SpaceRegion',[]),[constants(p5(2,9,1,16,13),[identifier(p4(2,10,5,11),'X_Axis'),identifier(p4(2,11,5,11),'Y_Axis'),identifier(p4(2,12,5,10),'Space'),identifier(p4(2,13,5,14),'Asteroids'),identifier(p4(2,14,5,15),'EmptySpace'),identifier(p4(2,15,5,13),'Homebase'),identifier(p4(2,16,5,13),'Starbase')]),properties(p5(2,18,1,38,48),conjunct(p5(2,20,5,38,48),[subset(p4(2,20,5,23),identifier(p4(2,20,5,11),'X_Axis'),natural1_set(p4(2,20,15,23))),equal(p4(2,20,26,40),identifier(p4(2,20,26,32),'X_Axis'),interval(p4(2,20,35,40),integer(p4(2,20,35,36),1),integer(p4(2,20,38,40),12))),subset(p4(2,21,5,23),identifier(p4(2,21,5,11),'Y_Axis'),natural1_set(p4(2,21,15,23))),equal(p4(2,21,26,39),identifier(p4(2,21,26,32),'Y_Axis'),interval(p4(2,21,35,39),integer(p4(2,21,35,36),1),integer(p4(2,21,38,39),7))),member(p4(2,24,5,30),identifier(p4(2,24,5,10),'Space'),relations(p4(2,24,13,30),identifier(p4(2,24,13,19),'X_Axis'),identifier(p4(2,24,24,30),'Y_Axis'))),equal(p4(2,25,5,28),identifier(p4(2,25,5,10),'Space'),mult_or_cart(p4(2,25,13,28),identifier(p4(2,25,13,19),'X_Axis'),identifier(p4(2,25,22,28),'Y_Axis'))),subset(p4(2,28,5,23),identifier(p4(2,28,5,14),'Asteroids'),identifier(p4(2,28,18,23),'Space')),equal(p4(2,29,5,141),identifier(p4(2,29,5,14),'Asteroids'),set_extension(p4(2,29,17,141),[couple(p4(2,29,19,26),[integer(p4(2,29,19,20),3),integer(p4(2,29,25,26),2)]),couple(p4(2,29,30,37),[integer(p4(2,29,30,31),3),integer(p4(2,29,36,37),5)]),couple(p4(2,29,41,48),[integer(p4(2,29,41,42),5),integer(p4(2,29,47,48),4)]),couple(p4(2,29,52,59),[integer(p4(2,29,52,53),6),integer(p4(2,29,58,59),7)]),couple(p4(2,29,63,70),[integer(p4(2,29,63,64),7),integer(p4(2,29,69,70),1)]),couple(p4(2,29,74,81),[integer(p4(2,29,74,75),7),integer(p4(2,29,80,81),5)]),couple(p4(2,29,85,92),[integer(p4(2,29,85,86),7),integer(p4(2,29,91,92),7)]),couple(p4(2,29,96,103),[integer(p4(2,29,96,97),8),integer(p4(2,29,102,103),3)]),couple(p4(2,29,107,115),[integer(p4(2,29,107,109),10),integer(p4(2,29,114,115),6)]),couple(p4(2,29,119,127),[integer(p4(2,29,119,121),11),integer(p4(2,29,126,127),2)]),couple(p4(2,29,131,139),[integer(p4(2,29,131,133),12),integer(p4(2,29,138,139),5)])])),equal(p4(2,32,5,35),identifier(p4(2,32,5,15),'EmptySpace'),minus_or_set_subtract(p4(2,32,18,35),identifier(p4(2,32,18,23),'Space'),identifier(p4(2,32,26,35),'Asteroids'))),equal(p4(2,33,5,33),intersection(p4(2,33,5,28),identifier(p4(2,33,5,15),'EmptySpace'),identifier(p4(2,33,19,28),'Asteroids')),empty_set(p4(2,33,31,33))),equal(p4(2,34,5,36),union(p4(2,34,5,28),identifier(p4(2,34,5,15),'EmptySpace'),identifier(p4(2,34,19,28),'Asteroids')),identifier(p4(2,34,31,36),'Space')),member(p4(2,37,5,26),identifier(p4(2,37,5,13),'Homebase'),identifier(p4(2,37,16,26),'EmptySpace')),equal(p4(2,37,29,48),identifier(p4(2,37,29,37),'Homebase'),couple(p4(2,37,41,48),[integer(p4(2,37,41,42),1),integer(p4(2,37,47,48),1)])),member(p4(2,38,5,26),identifier(p4(2,38,5,13),'Starbase'),identifier(p4(2,38,16,26),'EmptySpace')),equal(p4(2,38,29,48),identifier(p4(2,38,29,37),'Starbase'),couple(p4(2,38,41,48),[integer(p4(2,38,41,42),6),integer(p4(2,38,47,48),4)]))]))])).
machine(abstract_machine(p5(1,7,1,256,4),machine(p3(7,1,8)),machine_header(p3(8,5,14),'Spaceship',[]),[sees(p5(1,10,1,11,16),[identifier(p3(11,5,16),'SpaceRegion')]),sets(p5(1,13,1,18,53),[enumerated_set(p3(15,5,121),'OUTCOME',[identifier(p3(15,16,26),'SUCCESSFUL'),identifier(p3(15,28,63),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES'),identifier(p3(15,65,90),'FAILED_DUE_TO_AN_ASTEROID'),identifier(p3(15,92,120),'FAILED_FOR_SOME_OTHER_REASON')]),enumerated_set(p3(18,5,53),'GAME_STATUS',[identifier(p3(18,20,23),'WON'),identifier(p3(18,25,29),'LOST'),identifier(p3(18,31,39),'NOT_OVER'),identifier(p3(18,41,52),'NOT_STARTED')])]),constants(p5(1,20,1,24,34),[identifier(p3(21,5,17),'InitialPower'),identifier(p3(22,5,23),'PowerForNormalMove'),identifier(p3(23,5,22),'PowerForWarpDrive'),identifier(p3(24,5,34),'PowerLossForAsteroidCollision')]),properties(p5(1,26,1,30,77),conjunct(p5(1,27,5,30,77),[member(p3(27,5,23),identifier(p3(27,5,17),'InitialPower'),nat_set(p3(27,20,23))),equal(p3(27,26,42),identifier(p3(27,26,38),'InitialPower'),integer(p3(27,41,42),0)),member(p3(28,5,29),identifier(p3(28,5,23),'PowerForNormalMove'),nat_set(p3(28,26,29))),equal(p3(28,32,54),identifier(p3(28,32,50),'PowerForNormalMove'),integer(p3(28,53,54),5)),member(p3(29,5,28),identifier(p3(29,5,22),'PowerForWarpDrive'),nat_set(p3(29,25,28))),equal(p3(29,31,53),identifier(p3(29,31,48),'PowerForWarpDrive'),integer(p3(29,51,53),20)),member(p3(30,5,40),identifier(p3(30,5,34),'PowerLossForAsteroidCollision'),nat_set(p3(30,37,40))),equal(p3(30,43,77),identifier(p3(30,43,72),'PowerLossForAsteroidCollision'),integer(p3(30,75,77),10))])),variables(p5(1,32,1,37,23),[identifier(p3(33,5,12),regionX),identifier(p3(34,5,12),regionY),identifier(p3(35,5,15),totalPower),identifier(p3(36,5,17),missionRoute),identifier(p3(37,5,23),numberOfCollisions)]),invariant(p5(1,39,1,44,29),conjunct(p5(1,40,5,44,29),[member(p3(40,5,21),identifier(p3(40,5,12),regionX),identifier(p3(40,15,21),'X_Axis')),member(p3(40,24,40),identifier(p3(40,24,31),regionY),identifier(p3(40,34,40),'Y_Axis')),member(p3(41,5,37),couple(p3(41,5,24),[identifier(p3(41,5,12),regionX),identifier(p3(41,17,24),regionY)]),identifier(p3(41,27,37),'EmptySpace')),member(p3(42,5,21),identifier(p3(42,5,15),totalPower),nat_set(p3(42,18,21))),member(p3(43,5,35),identifier(p3(43,5,17),missionRoute),seq(p3(43,20,35),identifier(p3(43,24,34),'EmptySpace'))),member(p3(44,5,29),identifier(p3(44,5,23),numberOfCollisions),nat_set(p3(44,26,29)))])),initialisation(p5(1,46,1,51,28),parallel(p5(1,47,5,51,28),[assign(p3(47,5,46),[identifier(p3(47,5,12),regionX)],[function(p3(47,16,46),first_projection(p3(47,16,36),identifier(p3(47,21,27),'X_Axis'),identifier(p3(47,29,35),'Y_Axis')),[identifier(p3(47,37,45),'Homebase')])]),assign(p3(48,5,46),[identifier(p3(48,5,12),regionY)],[function(p3(48,16,46),second_projection(p3(48,16,36),identifier(p3(48,21,27),'X_Axis'),identifier(p3(48,29,35),'Y_Axis')),[identifier(p3(48,37,45),'Homebase')])]),assign(p3(49,5,31),[identifier(p3(49,5,15),totalPower)],[identifier(p3(49,19,31),'InitialPower')]),assign(p3(50,5,31),[identifier(p3(50,5,17),missionRoute)],[sequence_extension(p3(50,21,31),[identifier(p3(50,22,30),'Homebase')])]),assign(p3(51,5,28),[identifier(p3(51,5,23),numberOfCollisions)],[integer(p3(51,27,28),0)])])),operations(p5(1,53,1,255,8),[operation(p5(1,55,5,63,8),identifier(p5(1,55,5,63,8),'NewGame'),[],[identifier(p3(55,13,18),power)],precondition(p5(1,56,5,63,8),member(p3(57,9,20),identifier(p3(57,9,14),power),nat1_set(p3(57,16,20))),parallel(p5(1,59,9,62,35),[assign(p3(59,9,28),[identifier(p3(59,9,19),totalPower)],[identifier(p3(59,23,28),power)]),assign(p3(60,9,32),[identifier(p3(60,9,27),numberOfCollisions)],[integer(p3(60,31,32),0)]),assign(p3(61,9,50),[identifier(p3(61,9,16),regionX)],[function(p3(61,20,50),first_projection(p3(61,20,40),identifier(p3(61,25,31),'X_Axis'),identifier(p3(61,33,39),'Y_Axis')),[identifier(p3(61,41,49),'Homebase')])]),assign(p3(61,54,95),[identifier(p3(61,54,61),regionY)],[function(p3(61,65,95),second_projection(p3(61,65,85),identifier(p3(61,70,76),'X_Axis'),identifier(p3(61,78,84),'Y_Axis')),[identifier(p3(61,86,94),'Homebase')])]),assign(p3(62,9,35),[identifier(p3(62,9,21),missionRoute)],[sequence_extension(p3(62,25,35),[identifier(p3(62,26,34),'Homebase')])])]))),operation(p5(1,66,5,94,8),identifier(p5(1,66,5,94,8),'MoveUp'),[identifier(p3(66,5,19),outcomeMessage)],[],precondition(p5(1,67,5,94,8),conjunct(p3(68,9,110),[member(p3(68,9,33),identifier(p3(68,9,23),outcomeMessage),identifier(p3(68,26,33),'OUTCOME')),negation(p3(68,36,110),disjunct(p3(68,41,108),equal(p3(68,41,71),couple(p3(68,41,60),[identifier(p3(68,41,48),regionX),identifier(p3(68,53,60),regionY)]),identifier(p3(68,63,71),'Starbase')),less(p3(68,77,108),identifier(p3(68,77,87),totalPower),identifier(p3(68,90,108),'PowerForNormalMove'))))]),if(p5(1,70,9,93,12),greater_equal(p3(71,13,45),identifier(p3(71,13,23),totalPower),identifier(p3(71,27,45),'PowerForNormalMove')),if(p5(1,73,13,90,16),member(p3(74,17,37),add(p3(74,17,28),identifier(p3(74,17,24),regionY),integer(p3(74,27,28),1)),identifier(p3(74,31,37),'Y_Axis')),if(p5(1,76,17,87,20),member(p3(77,22,59),couple(p3(77,22,46),[identifier(p3(77,22,29),regionX),add(p3(77,35,46),identifier(p3(77,35,42),regionY),integer(p3(77,45,46),1))]),identifier(p3(77,50,59),'Asteroids')),parallel(p5(1,79,21,81,64),[assign(p3(79,21,77),[identifier(p3(79,21,31),totalPower)],[minus_or_set_subtract(p3(79,35,77),identifier(p3(79,35,45),totalPower),identifier(p3(79,48,77),'PowerLossForAsteroidCollision'))]),assign(p3(80,21,65),[identifier(p3(80,21,39),numberOfCollisions)],[add(p3(80,43,65),identifier(p3(80,43,61),numberOfCollisions),integer(p3(80,64,65),1))]),assign(p3(81,21,64),[identifier(p3(81,21,35),outcomeMessage)],[identifier(p3(81,39,64),'FAILED_DUE_TO_AN_ASTEROID')])]),[],parallel(p5(1,83,21,86,49),[assign(p3(83,21,66),[identifier(p3(83,21,31),totalPower)],[minus_or_set_subtract(p3(83,35,66),identifier(p3(83,35,45),totalPower),identifier(p3(83,48,66),'PowerForNormalMove'))]),assign(p3(84,21,43),[identifier(p3(84,21,28),regionY)],[add(p3(84,32,43),identifier(p3(84,32,39),regionY),integer(p3(84,42,43),1))]),assign(p3(85,21,77),[identifier(p3(85,21,33),missionRoute)],[insert_tail(p3(85,37,77),identifier(p3(85,37,49),missionRoute),couple(p3(85,54,77),[identifier(p3(85,54,61),regionX),add(p3(85,66,77),identifier(p3(85,66,73),regionY),integer(p3(85,76,77),1))]))]),assign(p3(86,21,49),[identifier(p3(86,21,35),outcomeMessage)],[identifier(p3(86,39,49),'SUCCESSFUL')])])),[],assign(p3(89,17,70),[identifier(p3(89,17,31),outcomeMessage)],[identifier(p3(89,35,70),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES')])),[],assign(p3(92,13,59),[identifier(p3(92,13,27),outcomeMessage)],[identifier(p3(92,31,59),'FAILED_FOR_SOME_OTHER_REASON')])))),operation(p5(1,97,5,125,8),identifier(p5(1,97,5,125,8),'MoveDown'),[identifier(p3(97,5,19),outcomeMessage)],[],precondition(p5(1,98,5,125,8),conjunct(p3(99,9,110),[member(p3(99,9,33),identifier(p3(99,9,23),outcomeMessage),identifier(p3(99,26,33),'OUTCOME')),negation(p3(99,36,110),disjunct(p3(99,41,108),equal(p3(99,41,71),couple(p3(99,41,60),[identifier(p3(99,41,48),regionX),identifier(p3(99,53,60),regionY)]),identifier(p3(99,63,71),'Starbase')),less(p3(99,77,108),identifier(p3(99,77,87),totalPower),identifier(p3(99,90,108),'PowerForNormalMove'))))]),if(p5(1,101,9,124,12),greater_equal(p3(102,13,45),identifier(p3(102,13,23),totalPower),identifier(p3(102,27,45),'PowerForNormalMove')),if(p5(1,104,13,121,16),member(p3(105,17,37),minus_or_set_subtract(p3(105,17,28),identifier(p3(105,17,24),regionY),integer(p3(105,27,28),1)),identifier(p3(105,31,37),'Y_Axis')),if(p5(1,107,17,118,20),member(p3(108,22,59),couple(p3(108,22,46),[identifier(p3(108,22,29),regionX),minus_or_set_subtract(p3(108,35,46),identifier(p3(108,35,42),regionY),integer(p3(108,45,46),1))]),identifier(p3(108,50,59),'Asteroids')),parallel(p5(1,110,21,112,64),[assign(p3(110,21,77),[identifier(p3(110,21,31),totalPower)],[minus_or_set_subtract(p3(110,35,77),identifier(p3(110,35,45),totalPower),identifier(p3(110,48,77),'PowerLossForAsteroidCollision'))]),assign(p3(111,21,65),[identifier(p3(111,21,39),numberOfCollisions)],[add(p3(111,43,65),identifier(p3(111,43,61),numberOfCollisions),integer(p3(111,64,65),1))]),assign(p3(112,21,64),[identifier(p3(112,21,35),outcomeMessage)],[identifier(p3(112,39,64),'FAILED_DUE_TO_AN_ASTEROID')])]),[],parallel(p5(1,114,21,117,49),[assign(p3(114,21,66),[identifier(p3(114,21,31),totalPower)],[minus_or_set_subtract(p3(114,35,66),identifier(p3(114,35,45),totalPower),identifier(p3(114,48,66),'PowerForNormalMove'))]),assign(p3(115,21,43),[identifier(p3(115,21,28),regionY)],[minus_or_set_subtract(p3(115,32,43),identifier(p3(115,32,39),regionY),integer(p3(115,42,43),1))]),assign(p3(116,21,77),[identifier(p3(116,21,33),missionRoute)],[insert_tail(p3(116,37,77),identifier(p3(116,37,49),missionRoute),couple(p3(116,54,77),[identifier(p3(116,54,61),regionX),minus_or_set_subtract(p3(116,66,77),identifier(p3(116,66,73),regionY),integer(p3(116,76,77),1))]))]),assign(p3(117,21,49),[identifier(p3(117,21,35),outcomeMessage)],[identifier(p3(117,39,49),'SUCCESSFUL')])])),[],assign(p3(120,17,70),[identifier(p3(120,17,31),outcomeMessage)],[identifier(p3(120,35,70),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES')])),[],assign(p3(123,13,59),[identifier(p3(123,13,27),outcomeMessage)],[identifier(p3(123,31,59),'FAILED_FOR_SOME_OTHER_REASON')])))),operation(p5(1,128,5,156,8),identifier(p5(1,128,5,156,8),'MoveLeft'),[identifier(p3(128,5,19),outcomeMessage)],[],precondition(p5(1,129,5,156,8),conjunct(p3(130,9,110),[member(p3(130,9,33),identifier(p3(130,9,23),outcomeMessage),identifier(p3(130,26,33),'OUTCOME')),negation(p3(130,36,110),disjunct(p3(130,41,108),equal(p3(130,41,71),couple(p3(130,41,60),[identifier(p3(130,41,48),regionX),identifier(p3(130,53,60),regionY)]),identifier(p3(130,63,71),'Starbase')),less(p3(130,77,108),identifier(p3(130,77,87),totalPower),identifier(p3(130,90,108),'PowerForNormalMove'))))]),if(p5(1,132,9,155,12),greater_equal(p3(133,13,45),identifier(p3(133,13,23),totalPower),identifier(p3(133,27,45),'PowerForNormalMove')),if(p5(1,135,13,152,16),member(p3(136,17,37),minus_or_set_subtract(p3(136,17,28),identifier(p3(136,17,24),regionX),integer(p3(136,27,28),1)),identifier(p3(136,31,37),'X_Axis')),if(p5(1,138,17,149,20),member(p3(139,23,59),couple(p3(139,23,47),[minus_or_set_subtract(p3(139,23,34),identifier(p3(139,23,30),regionX),integer(p3(139,33,34),1)),identifier(p3(139,40,47),regionY)]),identifier(p3(139,50,59),'Asteroids')),parallel(p5(1,141,21,143,64),[assign(p3(141,21,77),[identifier(p3(141,21,31),totalPower)],[minus_or_set_subtract(p3(141,35,77),identifier(p3(141,35,45),totalPower),identifier(p3(141,48,77),'PowerLossForAsteroidCollision'))]),assign(p3(142,21,65),[identifier(p3(142,21,39),numberOfCollisions)],[add(p3(142,43,65),identifier(p3(142,43,61),numberOfCollisions),integer(p3(142,64,65),1))]),assign(p3(143,21,64),[identifier(p3(143,21,35),outcomeMessage)],[identifier(p3(143,39,64),'FAILED_DUE_TO_AN_ASTEROID')])]),[],parallel(p5(1,145,21,148,49),[assign(p3(145,21,66),[identifier(p3(145,21,31),totalPower)],[minus_or_set_subtract(p3(145,35,66),identifier(p3(145,35,45),totalPower),identifier(p3(145,48,66),'PowerForNormalMove'))]),assign(p3(146,21,43),[identifier(p3(146,21,28),regionX)],[minus_or_set_subtract(p3(146,32,43),identifier(p3(146,32,39),regionX),integer(p3(146,42,43),1))]),assign(p3(147,21,77),[identifier(p3(147,21,33),missionRoute)],[insert_tail(p3(147,37,77),identifier(p3(147,37,49),missionRoute),couple(p3(147,54,77),[minus_or_set_subtract(p3(147,54,65),identifier(p3(147,54,61),regionX),integer(p3(147,64,65),1)),identifier(p3(147,70,77),regionY)]))]),assign(p3(148,21,49),[identifier(p3(148,21,35),outcomeMessage)],[identifier(p3(148,39,49),'SUCCESSFUL')])])),[],assign(p3(151,17,70),[identifier(p3(151,17,31),outcomeMessage)],[identifier(p3(151,35,70),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES')])),[],assign(p3(154,13,59),[identifier(p3(154,13,27),outcomeMessage)],[identifier(p3(154,31,59),'FAILED_FOR_SOME_OTHER_REASON')])))),operation(p5(1,159,5,187,8),identifier(p5(1,159,5,187,8),'MoveRight'),[identifier(p3(159,5,19),outcomeMessage)],[],precondition(p5(1,160,5,187,8),conjunct(p3(161,9,110),[member(p3(161,9,33),identifier(p3(161,9,23),outcomeMessage),identifier(p3(161,26,33),'OUTCOME')),negation(p3(161,36,110),disjunct(p3(161,41,108),equal(p3(161,41,71),couple(p3(161,41,60),[identifier(p3(161,41,48),regionX),identifier(p3(161,53,60),regionY)]),identifier(p3(161,63,71),'Starbase')),less(p3(161,77,108),identifier(p3(161,77,87),totalPower),identifier(p3(161,90,108),'PowerForNormalMove'))))]),if(p5(1,163,9,186,12),greater_equal(p3(164,13,45),identifier(p3(164,13,23),totalPower),identifier(p3(164,27,45),'PowerForNormalMove')),if(p5(1,166,13,183,16),member(p3(167,17,37),add(p3(167,17,28),identifier(p3(167,17,24),regionX),integer(p3(167,27,28),1)),identifier(p3(167,31,37),'X_Axis')),if(p5(1,169,17,180,20),member(p3(170,23,59),couple(p3(170,23,47),[add(p3(170,23,34),identifier(p3(170,23,30),regionX),integer(p3(170,33,34),1)),identifier(p3(170,40,47),regionY)]),identifier(p3(170,50,59),'Asteroids')),parallel(p5(1,172,21,174,64),[assign(p3(172,21,77),[identifier(p3(172,21,31),totalPower)],[minus_or_set_subtract(p3(172,35,77),identifier(p3(172,35,45),totalPower),identifier(p3(172,48,77),'PowerLossForAsteroidCollision'))]),assign(p3(173,21,65),[identifier(p3(173,21,39),numberOfCollisions)],[add(p3(173,43,65),identifier(p3(173,43,61),numberOfCollisions),integer(p3(173,64,65),1))]),assign(p3(174,21,64),[identifier(p3(174,21,35),outcomeMessage)],[identifier(p3(174,39,64),'FAILED_DUE_TO_AN_ASTEROID')])]),[],parallel(p5(1,176,21,179,49),[assign(p3(176,21,66),[identifier(p3(176,21,31),totalPower)],[minus_or_set_subtract(p3(176,35,66),identifier(p3(176,35,45),totalPower),identifier(p3(176,48,66),'PowerForNormalMove'))]),assign(p3(177,21,43),[identifier(p3(177,21,28),regionX)],[add(p3(177,32,43),identifier(p3(177,32,39),regionX),integer(p3(177,42,43),1))]),assign(p3(178,21,77),[identifier(p3(178,21,33),missionRoute)],[insert_tail(p3(178,37,77),identifier(p3(178,37,49),missionRoute),couple(p3(178,54,77),[add(p3(178,54,65),identifier(p3(178,54,61),regionX),integer(p3(178,64,65),1)),identifier(p3(178,70,77),regionY)]))]),assign(p3(179,21,49),[identifier(p3(179,21,35),outcomeMessage)],[identifier(p3(179,39,49),'SUCCESSFUL')])])),[],assign(p3(182,17,70),[identifier(p3(182,17,31),outcomeMessage)],[identifier(p3(182,35,70),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES')])),[],assign(p3(185,13,59),[identifier(p3(185,13,27),outcomeMessage)],[identifier(p3(185,31,59),'FAILED_FOR_SOME_OTHER_REASON')])))),operation(p5(1,190,5,220,8),identifier(p5(1,190,5,220,8),'WarpDrive'),[identifier(p3(190,5,19),outcomeMessage)],[identifier(p3(190,34,46),newpositionX),identifier(p3(190,48,60),newpositionY)],precondition(p5(1,191,5,220,8),conjunct(p5(1,192,9,195,83),[member(p3(192,9,33),identifier(p3(192,9,23),outcomeMessage),identifier(p3(192,26,33),'OUTCOME')),member(p3(193,9,28),identifier(p3(193,9,21),newpositionX),nat1_set(p3(193,24,28))),member(p3(193,31,52),identifier(p3(193,31,43),newpositionX),identifier(p3(193,46,52),'X_Axis')),member(p3(194,2,21),identifier(p3(194,2,14),newpositionY),nat1_set(p3(194,17,21))),member(p3(194,24,45),identifier(p3(194,24,36),newpositionY),identifier(p3(194,39,45),'Y_Axis')),negation(p3(195,9,83),disjunct(p3(195,14,81),equal(p3(195,14,44),couple(p3(195,14,33),[identifier(p3(195,14,21),regionX),identifier(p3(195,26,33),regionY)]),identifier(p3(195,36,44),'Starbase')),less(p3(195,50,81),identifier(p3(195,50,60),totalPower),identifier(p3(195,63,81),'PowerForNormalMove'))))]),if(p5(1,197,9,219,12),greater_equal(p3(198,13,44),identifier(p3(198,13,23),totalPower),identifier(p3(198,27,44),'PowerForWarpDrive')),if(p5(1,200,13,216,16),conjunct(p3(201,16,61),[member(p3(201,16,37),identifier(p3(201,16,28),newpositionX),identifier(p3(201,31,37),'X_Axis')),member(p3(201,40,61),identifier(p3(201,40,52),newpositionY),identifier(p3(201,55,61),'Y_Axis'))]),if(p5(1,203,17,213,20),member(p3(204,22,63),couple(p3(204,22,51),[identifier(p3(204,22,34),newpositionX),identifier(p3(204,39,51),newpositionY)]),identifier(p3(204,54,63),'Asteroids')),parallel(p5(1,206,7,207,64),[assign(p3(206,7,51),[identifier(p3(206,7,17),totalPower)],[minus_or_set_subtract(p3(206,21,51),identifier(p3(206,21,31),totalPower),identifier(p3(206,34,51),'PowerForWarpDrive'))]),assign(p3(207,21,64),[identifier(p3(207,21,35),outcomeMessage)],[identifier(p3(207,39,64),'FAILED_DUE_TO_AN_ASTEROID')])]),[],parallel(p5(1,209,21,212,49),[assign(p3(209,21,65),[identifier(p3(209,21,31),totalPower)],[minus_or_set_subtract(p3(209,35,65),identifier(p3(209,35,45),totalPower),identifier(p3(209,48,65),'PowerForWarpDrive'))]),assign(p3(210,21,44),[identifier(p3(210,21,28),regionX)],[identifier(p3(210,32,44),newpositionX)]),assign(p3(210,48,71),[identifier(p3(210,48,55),regionY)],[identifier(p3(210,59,71),newpositionY)]),assign(p3(211,21,83),[identifier(p3(211,21,33),missionRoute)],[insert_tail(p3(211,37,83),identifier(p3(211,37,49),missionRoute),couple(p3(211,54,83),[identifier(p3(211,54,66),newpositionX),identifier(p3(211,71,83),newpositionY)]))]),assign(p3(212,21,49),[identifier(p3(212,21,35),outcomeMessage)],[identifier(p3(212,39,49),'SUCCESSFUL')])])),[],assign(p3(215,17,70),[identifier(p3(215,17,31),outcomeMessage)],[identifier(p3(215,35,70),'FAILED_DUE_TO_SPACE_BOUNDARY_ISSUES')])),[],assign(p3(218,13,59),[identifier(p3(218,13,27),outcomeMessage)],[identifier(p3(218,31,59),'FAILED_FOR_SOME_OTHER_REASON')])))),operation(p5(1,223,5,249,8),identifier(p5(1,223,5,249,8),'MissionStatus'),[identifier(p3(223,5,15),gameStatus),identifier(p3(223,17,32),currentLocation),identifier(p3(223,34,46),currentPower),identifier(p3(223,48,66),asteroidCollisions)],[],precondition(p5(1,224,5,249,8),member(p3(225,2,26),identifier(p3(225,2,12),gameStatus),identifier(p3(225,15,26),'GAME_STATUS')),parallel(p5(1,227,6,248,42),[if(p5(1,227,6,245,12),conjunct(p3(228,13,55),[equal(p3(228,13,38),identifier(p3(228,13,25),missionRoute),sequence_extension(p3(228,28,38),[identifier(p3(228,29,37),'Homebase')])),equal(p3(228,41,55),identifier(p3(228,41,51),totalPower),integer(p3(228,54,55),0))]),assign(p3(230,13,38),[identifier(p3(230,13,23),gameStatus)],[identifier(p3(230,27,38),'NOT_STARTED')]),[],if(p5(1,232,13,244,16),equal(p3(233,16,46),couple(p3(233,16,35),[identifier(p3(233,16,23),regionX),identifier(p3(233,28,35),regionY)]),identifier(p3(233,38,46),'Starbase')),assign(p3(235,17,34),[identifier(p3(235,17,27),gameStatus)],[identifier(p3(235,31,34),'WON')]),[],if(p5(1,237,17,243,6),less(p3(238,8,39),identifier(p3(238,8,18),totalPower),identifier(p3(238,21,39),'PowerForNormalMove')),assign(p3(240,7,25),[identifier(p3(240,7,17),gameStatus)],[identifier(p3(240,21,25),'LOST')]),[],assign(p3(242,14,36),[identifier(p3(242,14,24),gameStatus)],[identifier(p3(242,28,36),'NOT_OVER')])))),assign(p3(246,2,40),[identifier(p3(246,2,17),currentLocation)],[couple(p3(246,21,40),[identifier(p3(246,21,28),regionX),identifier(p3(246,33,40),regionY)])]),assign(p3(247,2,28),[identifier(p3(247,2,14),currentPower)],[identifier(p3(247,18,28),totalPower)]),assign(p3(248,2,42),[identifier(p3(248,2,20),asteroidCollisions)],[identifier(p3(248,24,42),numberOfCollisions)])]))),operation(p5(1,252,5,255,8),identifier(p5(1,252,5,255,8),'RegionsVisited'),[identifier(p3(252,5,10),route)],[],block(p5(1,253,5,255,8),assign(p3(254,9,30),[identifier(p3(254,9,14),route)],[identifier(p3(254,18,30),missionRoute)])))])])).