-
Notifications
You must be signed in to change notification settings - Fork 0
/
Robot.mch
155 lines (141 loc) · 4.42 KB
/
Robot.mch
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
/* Robot
* Author: NUVIN
* Creation date: 18/12/2022
*/
MACHINE
Robot
INCLUDES
Maze
PROMOTES
getPosition,
foundExit,
hasVisitedSquare,
robotsRoute,
resetMaze
SETS
REPORT_MESSAGE = {
Move_Viable,
Move_Blocked_By_Internal_Wall,
Move_Blocked_By_Maze_Boundary,
Teleport_Viable,
Teleport_Blocked_By_Internal_Wall,
Teleport_Blocked_By_Maze_Boundary,
Exit_Teleport_Illegal,
Robot_Already_At_Exit
}
VARIABLES
coordX,
coordY
INVARIANT
coordX : dom(validSquares) &
coordY : ran(validSquares)
INITIALISATION
coordX,coordY := prj1(NATURAL1,NATURAL1)(entranceSquare) , prj2(NATURAL1,NATURAL1)(entranceSquare)
OPERATIONS
// move NORTH operation
moveStatus <-- MoveNorth =
IF (coordX |-> coordY) /= exitSquare
THEN
IF ((coordX |-> (coordY + 1)) : validSquares)
THEN
coordY := (coordY + 1) ||
updatePath((coordX |-> (coordY + 1))) ||
moveStatus := Move_Viable
ELSIF (coordX |-> (coordY + 1)) : internalWalls
THEN
moveStatus := Move_Blocked_By_Internal_Wall
ELSE
moveStatus := Move_Blocked_By_Maze_Boundary
END
ELSE
moveStatus := Robot_Already_At_Exit
END;
// move EAST operation
moveStatus <-- MoveEast =
IF (coordX |-> coordY) /= exitSquare
THEN
IF (((coordX + 1) |-> coordY) : validSquares)
THEN
coordX := (coordX + 1)
||
updatePath(((coordX + 1) |-> coordY))
||
moveStatus := Move_Viable
ELSIF ((coordX + 1) |-> coordY) : internalWalls
THEN
moveStatus := Move_Blocked_By_Internal_Wall
ELSE
moveStatus := Move_Blocked_By_Maze_Boundary
END
ELSE
moveStatus := Robot_Already_At_Exit
END;
// move SOUTH operation
moveStatus <-- MoveSouth =
IF (coordX |-> coordY) /= exitSquare
THEN
IF ((coordX |-> (coordY - 1)) : validSquares)
THEN
coordY := (coordY - 1) ||
updatePath((coordX |-> (coordY - 1))) ||
moveStatus := Move_Viable
ELSIF (coordX |-> (coordY - 1)) : internalWalls
THEN
moveStatus := Move_Blocked_By_Internal_Wall
ELSE
moveStatus := Move_Blocked_By_Maze_Boundary
END
ELSE
moveStatus := Robot_Already_At_Exit
END;
// move WEST operation
moveStatus <-- MoveWest =
IF (coordX |-> coordY) /= exitSquare
THEN
IF (((coordX - 1) |-> coordY) : validSquares)
THEN
coordX := (coordX - 1) ||
updatePath(((coordX - 1) |-> coordY))||
moveStatus := Move_Viable
ELSIF ((coordX - 1) |-> coordY) : internalWalls
THEN
moveStatus := Move_Blocked_By_Internal_Wall
ELSE
moveStatus := Move_Blocked_By_Maze_Boundary
END
ELSE
moveStatus := Robot_Already_At_Exit
END;
// teleport robot operation
teleportStatus <-- Teleport(targetXCoord, targetYCoord) =
PRE
targetXCoord : NATURAL & targetYCoord : NATURAL
THEN
IF (coordX |-> coordY) /= exitSquare
THEN
IF ((targetXCoord |-> targetYCoord) : validSquares & (targetXCoord |-> targetYCoord) /= exitSquare)
THEN
coordX := targetXCoord ||
coordY := targetYCoord ||
updatePath((targetXCoord |-> targetYCoord))||
teleportStatus := Teleport_Viable
ELSIF (targetXCoord |-> targetYCoord) : internalWalls
THEN
teleportStatus := Teleport_Blocked_By_Internal_Wall
ELSIF((targetXCoord |-> targetYCoord) = exitSquare)
THEN
teleportStatus := Exit_Teleport_Illegal
ELSE
teleportStatus := Teleport_Blocked_By_Maze_Boundary
END
ELSE
teleportStatus := Robot_Already_At_Exit
END
END;
// reset robot & maze operation
Reset =
BEGIN
coordX,coordY := prj1(NATURAL1,NATURAL1)(entranceSquare) , prj2(NATURAL1,NATURAL1)(entranceSquare) ||
resetMaze
END
END