Concurrent Programming (19530-V)

Attention: Please notice that this assignment is due on Thursday; this gives you an extra two days to work on it. As a result of this fact, this assigment will be graded more strictly than normal assignments. Remember that you are expected to work alone.

1. Exercise

The goal of this assignment is to create an FSP model that closely parallels the project specification. The incomplete FSP code below, creates CELL and POSITION data structures for keep tracking of the state of a maze cell and the position of a robot, respectively. The FSP model is also designed so that it can work with an arbitrary maze, just like our project; the final GAME composition defines a simple 4 x 4 maze.

Your task is to complete the WORLD process (marked below). This WORLD process is equivalent to the World interface in our project, it ensures that the robot behaves according to the rules of the world. For example, a robot cannot move through walls and a robot cannot move onto an occupied cell. Remember also that the project specification says that once a robot decides to move, then the move operation is blocking; this means that if the cell is currently occupied, then the robot will wait until the cell becomes unoccupied. The WORLD process here is slightly simplified from the project specification, it only has the methods north, south, east, and west. Write a paragraph describing how your WORLD process works.

Hint: Try to sketch out simple pseudo-code for how the WORLD methods should work, then try to create an FSP implementation from the pseudo-code. Do not concern yourself with anything other than the WORLD implementation.

// Simple robot.
ROBOT = ({ north, south, east, west } -> ROBOT).

// Maximum x and y positions for maze.
const MAX_X = 3
const MAX_Y = 3

// Valid positions for a robot.
range X = 1..MAX_X - 1
range Y = 1..MAX_Y - 1

// Data structure to keep track of robot position.
POSITION(X = 1, Y = 1) = POS[X][Y],
POS[x:X][y:Y] =
    (getPos[x][y] -> POS[x][y]
    |setPos[new_x:X][new_y:Y] -> POS[new_x][new_y]).

// Values for maze cells.
const OPEN = 0
const WALL = 1
const FALSE = 0
const TRUE = 1
range TYPE = OPEN..WALL
range BOOL = FALSE..TRUE

// Data structure to keep track of a maze cell,
// which is either a wall or an open space and
// if it is an open space it may also be occupied
// or not.
CELL(T=OPEN, O=FALSE) = C[T][O],
C[OPEN][occupied:BOOL] =
    (getType[OPEN] -> C[OPEN][occupied]
    |getOccupied[occupied] -> C[OPEN][occupied]
    |setOccupied[new_occupied:BOOL] -> C[OPEN][new_occupied]),
C[WALL][occupied:BOOL] =
    (getType[WALL] -> C[WALL][occupied]).

// Interface to the maze for each robot; the semantics
// are a blocking move (i.e., once the robot decides to
// move it waits until the maze cell becomes unoccupied).
WORLD =
    // YOU MUST IMPLEMENT THIS PROCESS.

// Range of robots.
range R=0..1

// System composition, which creates a maze like this:
//
//     0    1    2    3
//   0 WALL WALL WALL WALL
//   1 WALL OPEN OPEN WALL
//   2 WALL OPEN OPEN WALL
//   3 WALL WALL WALL WALL
//
// Puts robots at positions (1,1) and (2,1).
||GAME = (a[R]:ROBOT || a[0]:POSITION(1, 1) || a[1]:POSITION(2,1)
    || a[R]:WORLD
    || a[R]::maze[1..2][0]:CELL(WALL, FALSE)
    || a[R]::maze[0]   [1]:CELL(WALL, FALSE)
    || a[R]::maze[3]   [1]:CELL(WALL, FALSE)
    || a[R]::maze[0]   [2]:CELL(WALL, FALSE)
    || a[R]::maze[3]   [2]:CELL(WALL, FALSE)
    || a[R]::maze[1..2][3]:CELL(WALL, FALSE)
    || a[R]::maze[1..2][1]:CELL(OPEN, TRUE)
    || a[R]::maze[1..2][2]:CELL(OPEN, FALSE)).