Interstaatliche Hochschule für Technik Buchs NTB, STRTDiskrete Mathematik
Block Informatik«Datum»
Lösungen zur Serie 22Aufgabe 3

Eine sehr (zu) einfache Lösung für die Spezifikation in der Stunde:
> steuerung := G gruen;
Eine einfache Lösung für die Spezifikation auf dem Übungsblatt: (d.h. die Aufgabe ist lösbar)
> spezifikation := G( (taste -> F gruen) & F ~gruen );
> steuerung := G ( gruen <-> X~gruen );
> ok := steuerung -> spezifikation;
> provable(ok);