Lab 2 Problem 1.2 Interpretation

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

Lab 2 Problem 1.2 Interpretation

Beitrag von xshisdi32 »

Wir finden es problematisch, diesen Satz zu verstehen:

Code: Alles auswählen

every time a reader process wants to read, it can only be stopped from doing so by 

           --------------a---------------
at least one writer process being able to write an infinite number of times.
------------------------b---------------------------------------------------
Wir haben es deshalb in zwei boolsche Variablen aufgeteilt (a und b). "a" soll also heißen, dass ein Leseprozess lesen möchte. "b" soll heißen, dass eine Schreibprozess immer wieder schreiben kann (falls "being able to" in "kann" übersetzt werden darf).

Wir haben eine Wahrheitstabelle aufgestellt:

Code: Alles auswählen

//   a b gewünscht
//   0 0 1 // Leseprocezessen wollen nicht lesen, Schreibprozesse sind nicht "able to" schreiben (Situation zugelassen)
//   0 1 1 // Leseprocezessen wollen nicht lesen, Schreibprozesse sind "able to" schreiben (Situation zugelassen)
//   1 0 1 // Leseprocezessen wollen lesen, Schreibprozesse sind nicht "able to" schreiben (Situation zugelassen)
//   1 1 0 // Leseprocezessen wollen lesen, Schreibprozesse sind "able to" schreiben (Situation NICHT zugelassen) 
Wir haben erkannt, dass diese Funktion durch NAND modelliert werden könnte. Da diese LTL immer gelten sollte, würde man das in Promela mit

Code: Alles auswählen

[] !(a && b)
modellieren können.

Ist unsere Vorgangsweise angemessen und korrekt?

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

Re: Lab 2 Problem 1.2 Interpretation

Beitrag von Nathan Wasser »

Nein.

Erstmal würde ich Wahrheitstabellen bei LTL Formeln eher weit aus dem Weg gehen, da um eine nicht-triviale LTL Formel mittels Wahrheitstabelle auszudrücken man unendlich viel Platz und Zeit bräuchte...

Aber zurück zur Frage:

Ihr lässt da einiges weg. Dadurch sind auch Eintragungen in eurer Wahrheitstabelle (und wieder: schlechte Idee!) falsch, wie zum Beispiel:

"Leseprocezessen wollen lesen, Schreibprozesse sind "able to" schreiben (Situation NICHT zugelassen)"

Diese Situation ist sehr wohl zugelassen. Wenn ein Leseprozess lesen will und ein Schreibprozess unendlich oft schreibt, dann kann es halt nur sein, dass der Leseprozess nie lesen wird.

Wenn ihr also das ganze durch Variablen abkürzt, werdet ihr mindestens 3 Variablen brauchen.

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

Re: Lab 2 Problem 1.2 Interpretation

Beitrag von xshisdi32 »

OK. Danke sehr :)

Antworten

Zurück zu „Archiv“