Maze.prob

parser_version('2018-03-15 10:38:02.795').
classical_b('Maze',['E:\\Final Year\\Sem1\\6SENG003C Reasoning about Programs (SEM 1)\\TutorialWorkspaceAtelierB\\Robot_CW_Final\\Maze.mch']).
machine(abstract_machine(pos(1,1,8,1,92,4),machine(pos(2,1,8,1,8,8)),machine_header(pos(3,1,9,5,9,9),'Maze',[]),[sets(pos(4,1,11,1,12,23),[enumerated_set(pos(5,1,12,4,12,23),'MESSAGE',[identifier(pos(6,1,12,15,12,18),'Yes'),identifier(pos(7,1,12,20,12,22),'No')])]),constants(pos(8,1,14,1,16,70),[identifier(pos(9,1,16,5,16,16),entrySquare),identifier(pos(10,1,16,18,16,28),exitSquare),identifier(pos(11,1,16,30,16,40),xAxisRobot),identifier(pos(12,1,16,42,16,52),yAxisRobot),identifier(pos(13,1,16,54,16,70),mazeWallbarriers)]),properties(pos(14,1,18,1,25,156),conjunct(pos(15,1,20,5,25,156),conjunct(pos(16,1,20,5,24,44),conjunct(pos(17,1,20,5,23,65),conjunct(pos(18,1,20,5,23,38),conjunct(pos(19,1,20,5,22,68),conjunct(pos(20,1,20,5,22,39),conjunct(pos(21,1,20,5,21,48),conjunct(pos(22,1,20,5,21,27),conjunct(pos(23,1,20,5,20,48),subset(pos(24,1,20,5,20,27),identifier(pos(25,1,20,5,20,15),xAxisRobot),natural1_set(pos(26,1,20,19,20,27))),equal(pos(27,1,20,31,20,48),identifier(pos(28,1,20,31,20,41),xAxisRobot),interval(pos(29,1,20,44,20,48),integer(pos(30,1,20,44,20,45),1),integer(pos(31,1,20,47,20,48),7)))),subset(pos(32,1,21,5,21,27),identifier(pos(33,1,21,5,21,15),yAxisRobot),natural1_set(pos(34,1,21,19,21,27)))),equal(pos(35,1,21,31,21,48),identifier(pos(36,1,21,31,21,41),yAxisRobot),interval(pos(37,1,21,44,21,48),integer(pos(38,1,21,44,21,45),1),integer(pos(39,1,21,47,21,48),5)))),member(pos(40,1,22,5,22,39),identifier(pos(41,1,22,5,22,16),entrySquare),relations(pos(42,1,22,18,22,39),natural1_set(pos(43,1,22,18,22,26)),natural1_set(pos(44,1,22,31,22,39))))),equal(pos(45,1,22,43,22,68),identifier(pos(46,1,22,43,22,54),entrySquare),set_extension(pos(47,1,22,57,22,68),[couple(pos(48,1,22,59,22,66),[integer(pos(49,1,22,59,22,60),1),integer(pos(50,1,22,65,22,66),1)])]))),member(pos(51,1,23,5,23,38),identifier(pos(52,1,23,5,23,15),exitSquare),relations(pos(53,1,23,17,23,38),natural1_set(pos(54,1,23,17,23,25)),natural1_set(pos(55,1,23,30,23,38))))),equal(pos(56,1,23,41,23,65),identifier(pos(57,1,23,41,23,51),exitSquare),set_extension(pos(58,1,23,54,23,65),[couple(pos(59,1,23,56,23,63),[integer(pos(60,1,23,56,23,57),1),integer(pos(61,1,23,62,23,63),5)])]))),member(pos(62,1,24,5,24,44),identifier(pos(63,1,24,5,24,21),mazeWallbarriers),relations(pos(64,1,24,23,24,44),natural1_set(pos(65,1,24,23,24,31)),natural1_set(pos(66,1,24,36,24,44))))),equal(pos(67,1,25,5,25,156),identifier(pos(68,1,25,5,25,21),mazeWallbarriers),set_extension(pos(69,1,25,24,25,156),[couple(pos(70,1,25,26,25,33),[integer(pos(71,1,25,26,25,27),1),integer(pos(72,1,25,32,25,33),3)]),couple(pos(73,1,25,37,25,44),[integer(pos(74,1,25,37,25,38),2),integer(pos(75,1,25,43,25,44),1)]),couple(pos(76,1,25,48,25,55),[integer(pos(77,1,25,48,25,49),2),integer(pos(78,1,25,54,25,55),3)]),couple(pos(79,1,25,59,25,66),[integer(pos(80,1,25,59,25,60),2),integer(pos(81,1,25,65,25,66),5)]),couple(pos(82,1,25,70,25,77),[integer(pos(83,1,25,70,25,71),3),integer(pos(84,1,25,76,25,77),3)]),couple(pos(85,1,25,81,25,88),[integer(pos(86,1,25,81,25,82),4),integer(pos(87,1,25,87,25,88),2)]),couple(pos(88,1,25,92,25,99),[integer(pos(89,1,25,92,25,93),4),integer(pos(90,1,25,98,25,99),3)]),couple(pos(91,1,25,103,25,110),[integer(pos(92,1,25,103,25,104),4),integer(pos(93,1,25,109,25,110),4)]),couple(pos(94,1,25,114,25,121),[integer(pos(95,1,25,114,25,115),6),integer(pos(96,1,25,120,25,121),1)]),couple(pos(97,1,25,125,25,132),[integer(pos(98,1,25,125,25,126),6),integer(pos(99,1,25,131,25,132),2)]),couple(pos(100,1,25,136,25,143),[integer(pos(101,1,25,136,25,137),6),integer(pos(102,1,25,142,25,143),4)]),couple(pos(103,1,25,147,25,154),[integer(pos(104,1,25,147,25,148),7),integer(pos(105,1,25,153,25,154),4)])])))),variables(pos(106,1,27,1,29,53),[identifier(pos(107,1,29,5,29,19),visitedXsquare),identifier(pos(108,1,29,21,29,35),visitedYsquare),identifier(pos(109,1,29,37,29,53),visitedRobotpath)]),invariant(pos(110,1,31,1,35,45),conjunct(pos(111,1,33,5,35,45),conjunct(pos(112,1,33,5,34,29),member(pos(113,1,33,5,33,29),identifier(pos(114,1,33,5,33,19),visitedXsquare),natural1_set(pos(115,1,33,21,33,29))),member(pos(116,1,34,5,34,29),identifier(pos(117,1,34,5,34,19),visitedYsquare),natural1_set(pos(118,1,34,21,34,29)))),member(pos(119,1,35,5,35,45),identifier(pos(120,1,35,5,35,21),visitedRobotpath),seq(pos(121,1,35,23,35,45),mult_or_cart(pos(122,1,35,27,35,44),integer_set(pos(123,1,35,27,35,34)),integer_set(pos(124,1,35,37,35,44))))))),initialisation(pos(125,1,37,1,39,73),parallel(pos(126,1,39,5,39,73),[assign(pos(127,1,39,5,39,27),[identifier(pos(128,1,39,5,39,21),visitedRobotpath)],[empty_sequence(pos(129,1,39,25,39,27))]),assign(pos(130,1,39,31,39,50),[identifier(pos(131,1,39,31,39,45),visitedXsquare)],[integer(pos(132,1,39,49,39,50),0)]),assign(pos(133,1,39,54,39,73),[identifier(pos(134,1,39,54,39,68),visitedYsquare)],[integer(pos(135,1,39,72,39,73),0)])])),operations(pos(136,1,41,1,90,7),[operation(pos(137,1,47,4,54,7),identifier(pos(137,1,47,4,54,7),updateMaze),[],[identifier(pos(138,1,47,15,47,20),xAxis),identifier(pos(139,1,47,22,47,27),yAxis),identifier(pos(140,1,47,29,47,39),robotRoute)],precondition(pos(141,1,48,4,54,7),conjunct(pos(142,1,49,8,49,78),conjunct(pos(143,1,49,8,49,41),member(pos(144,1,49,8,49,23),identifier(pos(145,1,49,8,49,13),xAxis),natural1_set(pos(146,1,49,15,49,23))),member(pos(147,1,49,26,49,41),identifier(pos(148,1,49,26,49,31),yAxis),natural1_set(pos(149,1,49,33,49,41)))),member(pos(150,1,49,44,49,78),identifier(pos(151,1,49,44,49,54),robotRoute),seq(pos(152,1,49,56,49,78),mult_or_cart(pos(153,1,49,60,49,77),integer_set(pos(154,1,49,60,49,67)),integer_set(pos(155,1,49,70,49,77)))))),parallel(pos(156,1,51,8,53,31),[assign(pos(157,1,51,8,51,38),[identifier(pos(158,1,51,8,51,24),visitedRobotpath)],[identifier(pos(159,1,51,28,51,38),robotRoute)]),assign(pos(160,1,52,8,52,31),[identifier(pos(161,1,52,8,52,22),visitedXsquare)],[identifier(pos(162,1,52,26,52,31),xAxis)]),assign(pos(163,1,53,8,53,31),[identifier(pos(164,1,53,8,53,22),visitedYsquare)],[identifier(pos(165,1,53,26,53,31),yAxis)])]))),operation(pos(166,1,59,4,66,7),identifier(pos(166,1,59,4,66,7),foundExit),[identifier(pos(167,1,59,4,59,16),hasExitFound)],[],if(pos(168,1,60,4,66,7),member(pos(169,1,61,10,61,57),couple(pos(170,1,61,10,61,43),[identifier(pos(171,1,61,10,61,24),visitedXsquare),identifier(pos(172,1,61,29,61,43),visitedYsquare)]),identifier(pos(173,1,61,47,61,57),exitSquare)),assign(pos(174,1,63,8,63,27),[identifier(pos(175,1,63,8,63,20),hasExitFound)],[identifier(pos(176,1,63,24,63,27),'Yes')]),[],assign(pos(177,1,65,8,65,26),[identifier(pos(178,1,65,8,65,20),hasExitFound)],[identifier(pos(179,1,65,24,65,26),'No')]))),operation(pos(180,1,72,4,83,7),identifier(pos(180,1,72,4,83,7),hasVisitedSquare),[identifier(pos(181,1,72,4,72,13),isVisited)],[identifier(pos(182,1,72,36,72,46),xCellpoint),identifier(pos(183,1,72,48,72,58),yCellpoint)],precondition(pos(184,1,73,4,83,7),conjunct(pos(185,1,74,8,74,57),member(pos(186,1,74,8,74,31),identifier(pos(187,1,74,8,74,18),xCellpoint),identifier(pos(188,1,74,21,74,31),xAxisRobot)),member(pos(189,1,74,34,74,57),identifier(pos(190,1,74,34,74,44),yCellpoint),identifier(pos(191,1,74,47,74,57),yAxisRobot))),if(pos(192,1,76,8,82,11),member(pos(193,1,77,13,77,62),couple(pos(194,1,77,13,77,38),[identifier(pos(195,1,77,13,77,23),xCellpoint),identifier(pos(196,1,77,28,77,38),yCellpoint)]),range(pos(197,1,77,41,77,62),identifier(pos(198,1,77,45,77,61),visitedRobotpath))),assign(pos(199,1,79,12,79,28),[identifier(pos(200,1,79,12,79,21),isVisited)],[identifier(pos(201,1,79,25,79,28),'Yes')]),[],assign(pos(202,1,81,12,81,27),[identifier(pos(203,1,81,12,81,21),isVisited)],[identifier(pos(204,1,81,25,81,27),'No')])))),operation(pos(205,1,87,4,90,7),identifier(pos(205,1,87,4,90,7),robotsRoute),[identifier(pos(206,1,87,4,87,8),path)],[],block(pos(207,1,88,4,90,7),assign(pos(208,1,89,8,89,32),[identifier(pos(209,1,89,8,89,12),path)],[identifier(pos(210,1,89,16,89,32),visitedRobotpath)])))])])).