Lab 2 Problem 1.2 Liveness Property

xshisdi32
Mausschubser
Mausschubser
Beiträge: 73
Registriert: 10. Apr 2011 17:24
Wohnort: Bessungen, Darmstadt
Kontaktdaten:

Lab 2 Problem 1.2 Liveness Property

Beitrag von xshisdi32 »

Laut Folie 21 fängt eine Liveness Property mit "<>" an. Es würde aber Sinn machen, diese LTL mit "[] <>" anzufangen, da unsere Property immer wieder irgendwann passieren muss.

So unsere Frage ist: Kann eine Liveness Property mit "[] <>" anfangen? In die Aufgabestellung steht nämlich "every time [...]", und das andeutet unsere Meinung nach, dass "[]" benutzt werden muss.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab 2 Problem 1.2 Liveness Property

Beitrag von Nathan Wasser »

Ja, eine Liveness Property darf auch mit [] anfangen. Es ist eher das Vorhandensein eines <>, welches es zu einer Liveness Property macht.

Antworten

Zurück zu „Archiv“