Concurrent Programming (19530-V)

Dr. Richard S. Hall WS 01/02

- Übung 8 -

Ausgegeben: 19.12.2001
Rückgabe: 8.1.2002

1. Aufgabe

a) Wie helfen uns Endzustandsmengen (terminal state sets) Verletzungen von Fortschrittseigenschaften (progress properties) zu finden ?
b) Welchen Effekt hat das Verändern von Aktionsprioritäten auf einen LTS Graphen ? Warum würde man Aktionsprioritäten ändern wollen ?
c) Warum verursachte das Heruntersetzen der Prioritäten der exit Aktionen im SingleLangeBridge Prozess die Verletzung einer Fortschrittseigenschaft (progress property) ?

2.  Aufgabe

In Aufgabe 3 von Übung 6 modellierten wir ein Labyrinth. Erstelle in Vorbereitung auf das Projekt ein neues FSP Modell für dieses Labyrinth, das wie vorher north, south, east und west Bewegungsaktionen erlaubt, aber zusätzlich die Tatsache modelliert, daß ein Feld des Labyrinths besetzt sein kann, und zwar nur von einem Besetzenden gleichzeitig.

Hinweis: Es wird möglich sein müssen, den Status eines Feldes abzufragen, um festzustellen, ob es besetzt ist oder nicht. Dieses Modell ist so ähnlich wie das Ticket-Reservierungssystem aus Aufgabe 3 von Übung 3. Die Lösung für diese Aufgabe ist unten aufgeführt, aber die Lösung zum Labyrinth ist nicht identisch damit. Versucht also nicht, es wörtlich zu kopieren sondern benutzt es als Anregung für eigene Ideen:

const False = 0
const True = 1
range Bool = False..True

SEAT = SEAT[False],
SEAT[reserved:Bool]
    = (reserve->SEAT[True]
      |query[reserved]->SEAT[reserved]
      |when (reserved) reserve->ERROR).

range Seats = 0..1
||SEATS = (seat[Seats]:SEAT).

LOCK=(acquire->release->LOCK).

TERMINAL = (choose[s:Seats]->acquire
    ->seat[s].query[reserved:Bool]
        ->if (!reserved) then
            (seat[s].reserve->release->TERMINAL)
          else
            (release->TERMINAL)).

||CONCERT = ({a,b}:TERMINAL || {a,b}::SEATS || {a,b}::LOCK).