Weak fairness

JanH
Neuling
Neuling
Beiträge: 10
Registriert: 5. Okt 2010 00:11

Weak fairness

Beitrag von JanH »

Hallo,
ich habe noch eine Frage zu weak fairness:

Code: Alles auswählen

int var = 0;

active proctype p1()
{
  do
		:: var = 1
		:: var = 2
  od
}

active proctype p2()
{
	var = 3
}

ltl m1 { <>(var == 1) }
ltl m2 { <>(var == 2) }
ltl m3 { <>(var == 3) }
Ich dachte dass m1, m2 und m3 wahr sind, laut spin gilt aber nur m3. Das heißt, auch wenn unendlich oft zwischen var = 1 und var = 2 ausgesucht werden kann, kann es vorkommen, dass mit weak fairness immer das gleiche ausgewählt wird?

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

Re: Weak fairness

Beitrag von Nathan Wasser »

Die Statements sind nicht dauerhaft enabled, da nach der Ausführung von zum Beispiel "var = 1" im nächsten Schritt zum Schleifenanfang gesprungen werden muss. In diesem Zustand ist "var = 2" also nicht enabled.

JanH
Neuling
Neuling
Beiträge: 10
Registriert: 5. Okt 2010 00:11

Re: Weak fairness

Beitrag von JanH »

Danke. Somit ist also auch dieses Beispiel falsch.

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

Re: Weak fairness

Beitrag von Nathan Wasser »

Naja, falsch nicht. Da wird gesagt, dass ohne weak fairness <>var nicht allgemeingültig ist. Das ist korrekt. Mit weak fairness ist die Aussage aber auch nicht allgemeingültig. Das wäre ein Fall für strong fairness, kann SPIN aber leider nicht.

Antworten

Zurück zu „Archiv“