#define a ([] (x%2 == 1)) 			/* gilt nicht immer, da x auch gerade sein kann */
#define b (<> (x == 10))			/* gilt nicht immer, da x == 10 durch x=x+2 übersprungen werden kann  */
#define c (<> (x != 10))			/* gilt immer (Startwert!) */
#define d (<> ([] (x%2 == 1)))		/* ab einem bestimmten Zeitpunkt ist ggf. x immer ungerade gilt aber nicht für alle Zeitpunkte. Wenn nur P1 ausgeführt wird (keine Fairness) kann es vorkommen */
#define e ([] (<> (x%2 == 1)))      /* min einmal? wenn unfair dann z.b. ab 244 und dann immer P1


byte x=1;
byte y=0;

ltl formel1{e}

active proctype P1(){
	do
		:: x=x+2
	od;
}

active proctype P2(){
	do
		:: x=x+1
	od;
}

active proctype P3(){
	do
		:: y<x -> y=x
	od;
}


/*

Formulieren Sie folgende Anforderungen möglichst präzise als LTL-Formeln. Überlegen Sie zunächst, ob
diese Formeln mit oder ohne schwacher Fairness gelten. Überprüfen Sie Ihre Überlegungen mit ISPIN.
a) x ist immer ungerade
b) x ist irgendwann 10
c) x ist irgendwann nicht 10
d) es gibt eine Möglichkeit, dass x ab einem bestimmten Zeitpunkt immer ungerade ist
e) es gibt eine Möglichkeit, dass x ab einem bestimmten Zeitpunkt immer wieder ungerade ist
f) es gibt eine Möglichkeit, dass x ab einem bestimmten Zeitpunkt immer 10 ist
g) es gilt immer y ist kleiner-gleich x
h) auf y ungleich x folgt immer y gleich x
i) auf y gleich x folgt immer y ungleich x

*/