1. IntroductionThis coursework requires you to develop a B specification of a Robot moving around a simple Maze,using the B tools Atelier B & ProB.Figure 1. gives the layout of the rectangular shaped maze, the Robot is represented by "" & itsstarting position is the entry square (1, 1).The aim is to move the robot from the entry square through the maze using the various movementoperations to get to the exit square of the maze (1, 5).Figure 1. The Maze & RobotNotes The squares of the maze form a grid of squares 7 wide by 5 high. The robot occupies only one square at a time & can only be in an "empty maze square", i.e. asquare inside the maze and not one of the maze's internal walls.For example, the robot can be in square (5, 3), one of the maze's "path" squares, but not (4,2) an "internal wall" square. The robot starts off in the entrance square, i.e. the bottom left square (1, 1). The robot can be moved around the maze by using one of four directions: North , South ,East and West ; or it can "teleport" to one of the maze's "path" squares. Once the robot has found the exit square it can not make any further moves.2. Develop a B Specification of a Robot moving around a MazeYour B specification, i.e. collection of B machines, should include the following elements.(a) Sets and ConstantsAny sets and constants that are required to define the data and state of the maze and robot, and theirproperties.(Hints: Represent the maze and the maze's internal walls as relations.)(b) System StateThe state variables required to represent the data for the robot and the maze. Including the stateinvariant and initialisation.(c) Robot Movement Operations in the MazeThe following operations are the basic movements that all move the robot one square in theappropriate direction in the maze. MoveNorth MoveSouth MoveEast MoveWestNote that if any attempted movement can not be performed, either because of the boundary wall ofthe maze, i.e. attempting to move North when in square (4, 5), or an internal maze wall, i.e. attemptingto move East when in square (3, 2), then an error message is output indicating the reason it could notmake the move.The Robot can also "teleport" to a "path" square within the maze. TeleportThe operation inputs a square that the Robot attempts to teleport to. If the input square is suitable forthe Robot to teleport to it does so and reports success. However, if it is not a suitable square for it toteleport to, it outputs an error message indicating why.Note that all operations must report the outcome of an attempted movement, that is, either it wassuccessful, failed due to the maze's boundary, failed due to an internal wall, or for some otherreason.(d) Enquiry Operations about Robot in the MazeYou must also specify the following enquiry operations, that all output information about the state ofthe Robot: getPosition - outputs the current position of the robot in the maze. foundExit - outputs yes if the robot is currently in the exit square of the maze, no otherwise. hasVisitedSquare - inputs a square and reports yes if that square has been previously visitedby the robot, no otherwise.Note that a square is designated as having being visited by the Robot if it has been on thesquare more than once. That is, a square "has been visited" only after the robot has been onit and then has moved off it.(Hint: you will need to keep a record of the squares visited.) robotsRoute - outputs the sequence of squares the Robot has visited, in the order visited,i.e. its route through the maze.(e) Reset OperationA Reset operation to reinitialise the system, i.e. moves the robot back to the entry square, deletes therobots route and visited squares.General RequirementsThe B specification should use the appropriate features to define the data & operations in anymachines that you define. If you use a collection of machines then you must use the appropriate Bstructuring features to combine them.The specification must be syntactically & type correct, as checked by using the Atelier B tool.The specification must be animated by ProB. That is it must initialise correctly & all operations canbe animated successfully & can be used to move the Robot from the entry square to the exit squareusing a combination of all of the movement operation