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);