Concurrent Programming (19530-V)

Achtung: Dieses Übungsblatt ist zu Donnerstag. Dies gibt euch zwei Tage mehr für die Bearbeitung, und deshalb wird dieses Übungsblatt strenger beurteilt als sonst. Denkt daran, dass ihr alleine arbeiten sollt.

1. Aufgabe

Das Ziel dieser Aufgabe ist es, ein FSP-Modell zu erstellen, das der Projektspezifikation möglichst genau entspricht. Der unvollständige FSP-Kode unten modelliert die Datenstrukturen CELL und POSITION , in denen der Zustand eines Labyrinthfeldes und die Position eines Roboters gehalten werden kann. Das Modell ist so entworfen, dass es (wie im Projekt) mit beliebigen Labyrinthen umgehen kann, und die letztendliche Prozesskomposition GAME definiert ein einfaches 4 x 4 Labyrinth.

Es ist eure Aufgabe, den Prozess WORLD (unten markiert) zu vervollständigen. Dieser WORLD ist äquivalent zum World Interface in unserem Projekt, und stellt sicher, dass sich der Roboter entsprechend den Regeln der Welt verhält. Beispielsweise kann ein Roboter sich nicht durch Wände oder auf ein schon besetztes Feld bewegen. Denkt daran: die Projektspezifikation schreibt vor, dass, wenn ein Roboter sich für eine move-Operation entschieden hat, diese move-Operation blockierend ist. Dies bedeutet, wenn das Feld, auf das er will, gerade besetzt ist, dann muss der Roboter solange warten, bis es frei ist. Der WORLD Prozess ist im Vergleich zur Projektspezifikation leicht vereinfacht: es hat nur die Methoden north, south, east, und west. Beschreibt in einem Absatz, wie euer WORLD Prozess funktioniert.

Hinweis: Überlegt euch in einfachem Pseudo-Code, wie die Methoden von WORLD arbeiten sollten. Versucht dann, aus dem Pseudo-Code eine FSP-Implementierung zu machen. Beschäftigt euch nur mit der WORLD Implementierung.

// Einfacher Roboter.
ROBOT = ({ north, south, east, west } -> ROBOT).

// Maximale x und y Positionen des Labyrinths.
const MAX_X = 3
const MAX_Y = 3

// Zulässige Positionen für einen Roboter.
range X = 1..MAX_X - 1
range Y = 1..MAX_Y - 1

// Datenstruktur, um die Position eines Roboters zu verfolgen.
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]).

// Werte für Felder des Labyrinths.
const OPEN = 0
const WALL = 1
const FALSE = 0
const TRUE = 1
range TYPE = OPEN..WALL
range BOOL = FALSE..TRUE

// Datenstruktur für ein Feld im Labyrinth,
// welches entweder eine Wand oder ein Freiraum ist.

// Ist ein Feld ein Freiraum, kann es von einem Roboter besetzt sein.
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 zum Labyrinth für jeden Roboter. Das move
// ist blockierend (d.h. wenn ein Robot sich für ein move entscheidet,
// wartet er bis das Feld, auf das er will, unbesetzt ist).
WORLD =
    // DIESEN PROZESS MÜSST IHR IMPLEMENTIEREN.

// Indizes der Roboter.
range R=0..1

// Komposition des Systems, die dieses Labyrinth definiert:
//
//     0    1    2    3
//   0 WALL WALL WALL WALL
//   1 WALL OPEN OPEN WALL
//   2 WALL OPEN OPEN WALL
//   3 WALL WALL WALL WALL
//

// Die Roboter werden an die Positionen (1,1) und (2,1) gesetzt.
||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)).