Practicum: Verkeersdeadlock

Het doel van deze opgave is dat je leert op zelf een Uppaal model te maken. Beschouw de verkeerschaos die hieronder is afgebeeld:

Doel is om deze situatie in Uppaal te modelleren. Voor de eenvoud nemen we aan dat er slechts 4 trucks zijn, eentje voor ieder van de vier richtingen, die zo lang zijn dat ze twee kruispunten en alle ruimte daartussen kunnen vullen. We geven de kruispunten namen A, B, C en D:

Truck 1 komt bij het kruispunt A aan. Als A beschikbaar is (true) dan mag hij doorrijden. Daarna is het kruispunt bij A dus bezet en dus niet meer beschikbaar (false). De truck kan doorrijden als kruispunt B beschikbaar is (true). Als hij doorrijdt dan is ook punt B niet meer beschikbaar (false). Als de truck nog verder doorrijdt komt punt A weer beschikbaar (true), en als hij daarna nog verder doorrijdt komt ook punt B weer beschikbaar (true).

Dit principe geldt uiteraard ook voor truck 2, 3 en 4.

Maak een model dat het bovenstaande simuleert. Hint (andere oplossingen mogen ook): Gebruik 4 variabelen van type bool (true of false) waarmee je aangeeft of de kruispunten A, B, C en D vrij zijn. Maak 1 template voor een truck en geef die 2 variabelen van type bool als parameter (nl de kruispunten die de truck moet oversteken) door bij het parameter veld te schrijven: bool &first, bool &second. Bij de system declarations zet je:

Truck1 = Truck(A,B);
Truck2 = Truck(B,D);
Truck3 = Truck(D,C);
Truck4 = Truck(C,A);

system Truck1,Truck2,Truck3,Truck4;

Met jouw model moet je kunnen laten zien dat er een opstopping kan ontstaan. In Uppaal kun je testen of je model een deadlock bevat (een toestand waarin geen transities mogelijk zijn) met de query

A[] not deadlock