Electronic System Level Design and Verification: Practicum Opdracht 4

© Harry Broeders.

Deze pagina is bestemd voor studenten van de Haagse Hogeschool - Faculteit Technologie, Innovatie & Samenleving groep MNES = minor Embedded Systems.

Het is de bedoeling dat je maximaal 2 weken met deze opdracht bezig bent, 4 uur op het practicum en 4 uur daarbuiten.

Bij deze opdracht maken we gebruik van UPPAAL. Op de academie TISD van de HHS is UPPAAL geïnstalleerd in Q:\Grp_Elektrotechniek\Embedded_systems\uppaal-4.0.13. Je kunt het programma starten door dubbel te klikken op uppaal.jar.

Time Schedule

Omdat de modelchecker UPPAAL tijd kan modelleren is het mogelijk om door middel van een UPPAAL model een tijd schema op te stellen. We kunnen dan niet alleen een oplossing voor een scheduling probleem vinden (zoals met SPIN) maar we kunnen (met de UPPAAL verifiër) ook de snelste oplossing vinden.

Probleem

Vijf mensen moeten 2 bruggen passeren. Tussen de bruggen bevindt zich een platform (zie bovenstaande figuur). Er moet rekening gehouden worden met de volgende voorwaarden:

• Het is donker en er zitten gaten in de brug, dus om de brug over te steken is een zaklamp nodig.
• Er zijn slechts 2 zaklampen beschikbaar.
• De bruggen zijn niet erg stevig. Elke brug kan maximaal 2 mensen dragen.
• Op het platform kunnen maximaal 3 personen staan.
• De vijf personen zijn niet allemaal even snel. De tijd die een persoon nodig heeft om 1 brug over te gaan is gegeven in de onderstaande tabel:
  
  

  Persoon	Tijd nodig voor het oversteken van 1 brug (in min)
  P1	4
  P2	5
  P3	5
  P4	8
  P5	10

Opdracht

Wat is de minimale tijd waarin de 5 personen de 2 bruggen kunnen passeren onder de bovenstaande voorwaarden? Geef ook een tijdtabel waarin duidelijk wordt weergegeven wat er op elk relevant moment gebeurd.

Maak een UPPAAL model waarmee deze vraag beantwoord kan worden. Probeer niet om zelf een bepaalde strategie in het model te "programmeren". Laat het model niet-deterministisch bepalen welke personen de brug opgaan. Je kunt er echter wel vanuit gaan dat in de voorwaardse richting altijd (indien mogelijk) 2 personen de brug zullen betreden met 1 zaklamp. In de acherwaardse richting zal altijd 1 persoon de brug betreden (om de zaklamp terug te brengen). De tijd die 2 personen nodig hebben om samen een brug over te steken wordt uiteraard bepaald door de traagste.

Zorg ervoor dat je goed test of je model aan alle gestelde voorwaarden voldoet. Geef per voorwaarde de Query waarmee je hebt bewezen dat aan de voorwaarde wordt voldaan.

• Er bevinden zich nooit meer dan 2 personen op 1 brug.
• Er bevinden zich nooit meer dan 3 personen op het patform.
• ... (bedenk zelf nog meer voorwaarden waaraan je model moet voldoen).

De minimale tijd kun je vinden door te stellen dat de 5 personen zich ooit bij de finish zullen bevinden. Omdat je de snelste oplossing wilt vinden moet je de Fastest Diagnostic Trace zoeken.

In de door mij gevonden oplossing duurt het minstens 30 minuten voordat iedereen aan de overkant is. (Het is overigens best mogelijk dat jullie een ander antwoord vinden, als je maar kunt verklaren hoe dat komt...)

00 P1->B1 P2->B1
05 P1->PL P2->PL
05 P1->B2 P2->B2        P4->B1 P5->B1 
10 P1->F  P2->F
10 P1<-B2
14 P1<-PL
15                      P4->PL P5->PL
15 P1<-B1               P4->B2 P5->B2
19 P1<-S
19 P1->B1        P3->B1
24 P1->PL        P3->PL
25                      P4->F  P5->F
25 P1->B2        P3->B2
30 P1->F         P3->F

In dit schema geeft het pijltje -> of <- de looprichting aan, Px staat voor persoon met nummer x, Bx staat voor brug met nummer x. S staat voor Start, PL staat voor platform en F staat voor Finish.