© Harry Broeders.
Deze pagina is bestemd voor studenten van de Haagse Hogeschool - Academie voor Technology, Innovation & Society Delft groep MNES = minor Embedded Systems.
Bewijs dat de deur op verdieping X altijd open gaat als de lift op
deze verdieping X aankomt. Tip: Je kunt hierbij handig gebruik maken van
een logische implicatie. Zie: http://nl.wikipedia.org/wiki/Logische_implicatie.
Z'n implicatie kan in een LTL formule worden opgenomen. Bijvoorbeeld:
[]((oorzaak) -> <> (gevolg)) wat betekent: altijd als
oorzaak waar is dan zal ooit/uiteindelijk gevolg waar
zijn. Hierbij zijn oorzaak en gevolg proposities
(formules die waar of onwaar kunnen zijn). Als je een model op deze LTL formule
wilt onderzoeken moet je eerst de LTL formule invoeren in het daarvoor bestemde
veld, dan op "Translate" drukken en vervolgens
in de dropdownbox waarin standaard "Safety" geselecteerd staat "Acceptance"
selecteren en daarna op "Verify" drukken.
Het is het eenvoudigst om dit voor elke verdieping afzonderlijk te bewijzen. Begin bijvoorbeeld met: Bewijs dat de deur op verdieping 2 altijd open gaat als de lift op verdieping 2 aankomt.
De propositie gevolg die beschrijft of de deur op verdieping 2
open is, is natuurlijk simpel: deur_open[2]. De propositie
oorzaak die alleen waar is als de lift op verdieping 2 aankomt is
niet zo simpel. Je zult hiervoor een extra array in het model moeten
opnemen:
bool arrive[NF];
Bij aankomst op een verdieping x (in proctype
elevator) kun je dan arrive[x]
true maken en meteen weer false maken. De propositie
arrive[2] kan dan als oorzaak gebruikt worden.
Om te controleren of je op correcte wijze hebt bewezen dat de deur op verdieping 2 altijd open gaat als de lift op verdieping 2 aankomt kun je laten zien dat SPIN wel een fout geeft als je probeert te bewijzen dat de deur op verdieping 3 altijd open gaat als de lift op verdieping 2 aankomt.