weak fairness

mahi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 5. Aug 2012 14:06

weak fairness

Beitrag von mahi »

Wie kann ich ohne spin schließen dass eine LTL Formel nur mit weak fairness erfüllbar ist? Gibt es da ne Vorgehensweise? Die Lösungen dazu sind schwammig..
Bedanke mich im Voraus.

mahii

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: weak fairness

Beitrag von JannikV »

Joa, durch draufgucken.

Ne, also du kannst versuchen einen Lauf zu finden, der das Erfüllen der Formel umgeht.
Beispiel:

Code: Alles auswählen

active proctype p() {
    bool var = false;
    do
        :: var = true;
        :: var = false;
    od
}
Ohne weak fairness gilt hier folgende Formel zum Beispiel nicht:
\(\diamond var\)
Denn wenn wir einfach immer den unteren Fall von do nehmen wird var niemals true werden.

VG

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: weak fairness

Beitrag von L4_ »

JannikV hat geschrieben: Ohne weak fairness gilt hier folgende Formel zum Beispiel nicht:
\(\diamond var\)
Denn wenn wir einfach immer den unteren Fall von do nehmen wird var niemals true werden.
Ich bin bei der Bedeutung von "weak fairness" und dem Gegenteil davon immer noch nicht im klaren.

In deinem Beispiel hätte ich jetzt gesagt, dass mit weak fairness die Formel nicht gilt, da der erste Guard einfach "unfairer Weise" nie genommen wird.

Mit "nicht weak fairness" würde die Formel dennoch gelten.
Oder was verstehe ich hierbei falsch?

VG

niwo
Erstie
Erstie
Beiträge: 15
Registriert: 15. Jan 2009 14:02

Re: weak fairness

Beitrag von niwo »

weak fairness bedeutet, dass jede ausführbare Anweisung auch mindestens einmal ausgeführt wird.

Im Beispiel würde das bedeuten, dass var zu irgendeinem Zeitpunkt einmal true sein muss.
Und das ist genau der Fall, wenn in der Schleife mindestens einmal die erste Anweisung ausgeführt wird.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: weak fairness

Beitrag von L4_ »

Okay, ich glaub es sitzt nun ;)

Wenn ich nun "pan" mit -f starte, dann wird weak fairness erzwungen.
Ist denn dann ohne -f keine weak fairness, sprich gilt dann starke fairness?

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

Re: weak fairness

Beitrag von Nathan Wasser »

Es gibt:

1. keine Fairness (wenn nichts anderes vorrausgesetzt wird ist das der Default)

2. weak Fairness

3. strong Fairness (in der Vorlesung nur kurz erwähnt, Spin kann nur ohne Fairness oder mit weak Fairness arbeiten)

Ohne Fairness darf der Scheduler beliebig "unfair" sein und zum Beispiel ein Statement, welches ausgewertet werden kann, nie auswerten. (Dies setzt natürlich vorraus, dass es andere Statements gibt, die zum gleichen Zeitpunkt auch zur Auswahl standen; der Scheduler darf nicht einfach das Programm anhalten und nicht weiter arbeiten lassen, wenn es Statements gibt, die auswertbar sind.)

Bei weak Fairness ist der Scheduler etwas weniger "unfair" und stellt sicher, dass zumindest Statements, welche die ganze Zeit ausgewertet werden könnten, auch irgendwann ausgewertet werden. Wenn aber ein Statement mal auswertbar ist, mal nicht, dann darf der Scheduler es auch bei weak Fairness ignorieren.

Also: "Ohne weak Fairness" bedeutet gar keine Fairness, nicht irgendwie stärkere Fairness (das wäre strong Fairness).

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: weak fairness

Beitrag von L4_ »

Okay super, das hilft mir nun noch besser und jetzt verstehe ich auch die Formel aus Ü3, Problem6 besser:

Weak fairness:
Für alle Aktionen A gilt:
[] enabled A -> <> taken A

Und wenn die Voraussetzung falsch ist, darf spin den Zweig ignorieren.
Danke! :)

Antworten

Zurück zu „Archiv“