#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

 

*/