Practicum: Frisdrankenmachine

Instructie

Open de onderstaande files in Uppaal:

Dit model beschrijft een simpele frisdrankenmachine. Deze machine verkoopt slechts één soort frisdrank en ieder blikje kost precies één Euro. We nemen aan dat de frisdrankenmachine beschikt over een onbeperkte hoeveelheid blikjes. Het Uppaal model beschrijft het gedrag van de frisdrankenmachine met behulp van drie templates/automaten.

De eerste automaat, Geldinzameling, houdt bij wat het tegoed is van de klant. Telkens wanneer een klant een munt inwerpt wordt via een muntIn?-transitie het tegoed van de klant (variabele tegoed) met één verhoogt. We nemen aan dat het tegoed maximaal 10 Euro bedraagt: wanneer een klant een tegoed van 10 Euro heeft is het onmogelijk om nog een munt in de automaat te duwen.
De tweede automaat, Geldteurggave, beschrijft wat er gebeurt wanneer de klant op de annuleerknop drukt. Via een annuleer?-transitie springt de automaat naar een toestand waarin allereerst een signaal stop naar de Blikjesafgave wordt gestuurd om de boel daar te stoppen. Vervolgens worden alle munten die de klant tegoed heeft één voor één teruggegeven (muntUit!). Daarna springt de automaat via een herstart!-transitie terug naar de begintoestand.
De derde automaat, BlikjesAfgave, handelt bestellingen af: wanneer een klant op de knop "blikje" drukt (vraagBlikje?) en het tegoed is positief, dan wordt een blikje geleverd (blikjeUit!) en wordt het tegoed met één verminderd. Het heeft geen zin meerdere keren op de knop "blikje" te drukken terwijl er nog geen blikje uit de machine is gekomen: herhaalde verzoeken worden genegeerd. Wanneer een stop signaal binnenkomt dan worden alle verdere verzoeken genegeerd totdat de machine weer is herstart.

In het model is ook een "nette klant" opgenomen. Deze klant werpt eerst een munt in, vraagt vervolgens om een blikje, neemt dit blikje in ontvangst, werpt opnieuw een munt in, enzovoorts. Nadat de klant een munt heeft ingeworpen kan zij ook besluiten om de bestelling te annuleren. Wanneer een bestelling wordt geannuleerd geeft de machine het tegoed terug.

(Terzijde: Merk op dat in de Geldteruggave automaat de toestand tussen de annuleer?-transitie en de stop!-transitie gelabeld is met een C. De toestand is committed gemaakt. Dit betekent dat in deze toestand de stop!-transitie direct gebeurt, zonder dat een andere automaat de kans heeft om eerder nog een transitie te doen.)

Maak de volgende opdrachten. Lever een bestand in met je antwoorden op de vragen en tevens voor iedere opgave een Uppaal xml en q bestand.

Opdracht 1 (3 punten)

Check de eigenschap in BlikjesAutomaat.q. Leg uit waarom er een deadlock zit in het model. Wat zou jij doen als je om een blikje hebt gevraagd en de automaat geeft je in plaats daarvan je geld terug? Pas de automaat NetteKlant op dit punt aan en check dat de deadlock zich niet meer kan voordoen.

Opdracht 2 (3 punten)

Maak een nieuw template (klik op "insert template" bij "Edit") en modelleer hiermee het gedrag van een "blinde aap" die in volstrekt willekeurige volgorde munten inwerpt, knoppen indrukt, en alle munten en blikjes pakt die uit de machine komen. Vervang bij de Systems Declarations NetteKlant door BlindeAap en check of zich nu een deadlock kan voordoen.

De blinde aap kan dus op elk moment (1) op de annuleerknop drukken, (2) een munt ingooien, (3) om een blikje vragen, (4) een munt pakken die uit de machine komt, en (5) een blikje pakken dat uit de machine komt. (Tip: het model is echt heel simpel!)

Opdracht 3 (3 punten)

Voeg de volgende regels toe aan de Declarations


int saldo=10;
int drank;

De bedoeling is dat saldo aangeeft hoeveel geld de klant op zak heeft en drank hoeveel blikjes zij al heeft ontvangen. Pas je model van de blinde aap dienovereenkomstig aan (indien het je niet gelukt is om een werkend model van de blinde aap te maken kun je ook gebruik maken van het model dat je bij opdracht 1 hebt gemaakt):

(a) voeg een guard saldo > 0 en een update saldo := saldo -1 toe aan iedere muntIn!-transitie,

(b) voeg een update saldo := saldo + 1 toe aan iedere muntUit?-transitie, en

Kan zich een deadlock voordoen in het resulterende model? Leg uit waarom er wel of geen deadlock is.

Welke relatie zal er altijd gelden tussen de variabelen saldo, drank en tegoed? Geef een Uppaal query waarmee dit kan worden aangetoond.

Opdracht 4 (bonus, 2 punten)

Pas het model dat je gemaakt hebt voor opdracht 1 aan zodat de prijs van een blikje 3 Euro wordt. Pas tevens het gedrag van de NetteKlant aan zodat de klant meerdere munten kan invoeren voordat zij om een blikje vraagt. Probeer met Uppaal aan te tonen dat de frisdrankenautomaat geen geld kan kwijtraken of verdienen (uitgaande van de waarde van 3 Euro per blikje).