De klant kan niet van zijn patroon afwijken; als hij pint verwacht hij een tientje en is niet bereid iets anders te doen tot hij zijn tientje ontvangen heeft. De automaat mag echter van de bank niet meer uitbetalen en wil alleen de pas teruggeven. Als correctie moet je een transitie toevoegen zodat de klant ook zijn pas aanpakt als hij geen geld krijgt.
UPPAAL verbiedt niet dat variabelen negatieve waarden aannemen. De variabele Flappentapper.in_kas kan dus een negatieve waarde aannemen terwijl een echte flappentapper geen negatief kassaldo kan hebben. Je moet een transitie toevoegen voor het geval de flappentapper minder dan € 10 in kas heeft: dan weigert hij ook uit te betalen. Let goed op waar je die transitie plaatst: de flappentapper mag geen toestemming aan de bank vragen, want als de bank toestemming verleent gaat zij ervan uit dat de klant ook geld krijgt en verlaagt zij het banksaldo.
De eerste eigenschap geldt niet altijd; zij zou alleen kunnen gelden als de klant zijn geld aanpakt precies op het moment dat de bank het saldo verlaagt. Omdat er echter geen directe communicatie is tussen de klant en de bank kan dat niet.
De tweede eigenschap geldt ook nog niet, maar je kunt het model aanpassen zodat de eigenschap wel gaat gelden. Daartoe moet de bank eerst het saldo verlagen en pas daarna akkoord gaan met uitbetaling van dat saldo.
Als je deze drie veranderingen hebt doorgevoerd krijg je het onderstaande model. Ik heb hierin in het blauw de nieuwe of veranderde toestanden gemarkeerd:
Nadat de klant zijn pas heeft ingevoerd, kan hij niet alleen een verzoek! aan de flappentapper richten, maar ook een opdracht!. De flappentapper verwacht dan geld van de klant en deelt aan de bank de storting mee. Om de eigenschap uit opgave 3 te bewaren moet de flappentapper dus eerst het geld aannemen. De uitbreiding hiermee heb ik hieronder in het paars gemarkeerd:
De uitwerking is eenvoudiger dan het lijkt. Je kunt als “reboot” een transitie toevoegen die precies de andere kant op wijst dan de “crash”-transitie. Dan krijg je ongeveer het volgende model, waarin ik oranje heb gemarkeerd wat nieuw is: