-
Notifications
You must be signed in to change notification settings - Fork 0
/
SpaceRegion.prob
3 lines (3 loc) · 3.12 KB
/
SpaceRegion.prob
1
2
3
parser_version('456efb928642d91bb84e63d65abf3e25a59815ee').
classical_b('SpaceRegion',['/Users/akshayan/Desktop/w1867142_Formal Methods_CW/Old Asteroids Arcade Game/SpaceRegion.mch']).
machine(abstract_machine(p5(1,6,1,40,4),machine(p3(6,1,8)),machine_header(p3(7,5,16),'SpaceRegion',[]),[constants(p5(1,9,1,16,13),[identifier(p3(10,5,11),'X_Axis'),identifier(p3(11,5,11),'Y_Axis'),identifier(p3(12,5,10),'Space'),identifier(p3(13,5,14),'Asteroids'),identifier(p3(14,5,15),'EmptySpace'),identifier(p3(15,5,13),'Homebase'),identifier(p3(16,5,13),'Starbase')]),properties(p5(1,18,1,38,48),conjunct(p5(1,20,5,38,48),[subset(p3(20,5,23),identifier(p3(20,5,11),'X_Axis'),natural1_set(p3(20,15,23))),equal(p3(20,26,40),identifier(p3(20,26,32),'X_Axis'),interval(p3(20,35,40),integer(p3(20,35,36),1),integer(p3(20,38,40),12))),subset(p3(21,5,23),identifier(p3(21,5,11),'Y_Axis'),natural1_set(p3(21,15,23))),equal(p3(21,26,39),identifier(p3(21,26,32),'Y_Axis'),interval(p3(21,35,39),integer(p3(21,35,36),1),integer(p3(21,38,39),7))),member(p3(24,5,30),identifier(p3(24,5,10),'Space'),relations(p3(24,13,30),identifier(p3(24,13,19),'X_Axis'),identifier(p3(24,24,30),'Y_Axis'))),equal(p3(25,5,28),identifier(p3(25,5,10),'Space'),mult_or_cart(p3(25,13,28),identifier(p3(25,13,19),'X_Axis'),identifier(p3(25,22,28),'Y_Axis'))),subset(p3(28,5,23),identifier(p3(28,5,14),'Asteroids'),identifier(p3(28,18,23),'Space')),equal(p3(29,5,141),identifier(p3(29,5,14),'Asteroids'),set_extension(p3(29,17,141),[couple(p3(29,19,26),[integer(p3(29,19,20),3),integer(p3(29,25,26),2)]),couple(p3(29,30,37),[integer(p3(29,30,31),3),integer(p3(29,36,37),5)]),couple(p3(29,41,48),[integer(p3(29,41,42),5),integer(p3(29,47,48),4)]),couple(p3(29,52,59),[integer(p3(29,52,53),6),integer(p3(29,58,59),7)]),couple(p3(29,63,70),[integer(p3(29,63,64),7),integer(p3(29,69,70),1)]),couple(p3(29,74,81),[integer(p3(29,74,75),7),integer(p3(29,80,81),5)]),couple(p3(29,85,92),[integer(p3(29,85,86),7),integer(p3(29,91,92),7)]),couple(p3(29,96,103),[integer(p3(29,96,97),8),integer(p3(29,102,103),3)]),couple(p3(29,107,115),[integer(p3(29,107,109),10),integer(p3(29,114,115),6)]),couple(p3(29,119,127),[integer(p3(29,119,121),11),integer(p3(29,126,127),2)]),couple(p3(29,131,139),[integer(p3(29,131,133),12),integer(p3(29,138,139),5)])])),equal(p3(32,5,35),identifier(p3(32,5,15),'EmptySpace'),minus_or_set_subtract(p3(32,18,35),identifier(p3(32,18,23),'Space'),identifier(p3(32,26,35),'Asteroids'))),equal(p3(33,5,33),intersection(p3(33,5,28),identifier(p3(33,5,15),'EmptySpace'),identifier(p3(33,19,28),'Asteroids')),empty_set(p3(33,31,33))),equal(p3(34,5,36),union(p3(34,5,28),identifier(p3(34,5,15),'EmptySpace'),identifier(p3(34,19,28),'Asteroids')),identifier(p3(34,31,36),'Space')),member(p3(37,5,26),identifier(p3(37,5,13),'Homebase'),identifier(p3(37,16,26),'EmptySpace')),equal(p3(37,29,48),identifier(p3(37,29,37),'Homebase'),couple(p3(37,41,48),[integer(p3(37,41,42),1),integer(p3(37,47,48),1)])),member(p3(38,5,26),identifier(p3(38,5,13),'Starbase'),identifier(p3(38,16,26),'EmptySpace')),equal(p3(38,29,48),identifier(p3(38,29,37),'Starbase'),couple(p3(38,41,48),[integer(p3(38,41,42),6),integer(p3(38,47,48),4)]))]))])).