Lab 2: Problem 1.1

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

Lab 2: Problem 1.1

Beitrag von xshisdi32 »

Wie kann man zwei Prozesse unterscheiden, wenn man nur Labels nutzen darf? In Ben-Ari steht auf Seite 38, dass man Prozesse mittels PID unterscheiden kann, aber das dürfen wir ja nicht. Man könnte auch den Writer Prozesscode duplizieren, aber das ist ja auch nicht zugelassen.

Wir wissen nicht, wie man ausschließen kann, dass zwei Prozesse gleichzeitig schreiben, wenn man die einzelne Writers nicht unterscheiden kann.

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab 2: Problem 1.1

Beitrag von himbaer »

Wo steht, dass man die Prozess-ID nicht benutzen darf?
Du kannst doch mittels Prozessname[_pid]@Labelname prüfen, ob sich ein Prozess gerade an einer bestimmten Stelle (markiert mit Labelname) befindet.
meine Testsignatur :!:

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: Lab 2: Problem 1.1

Beitrag von FGB »

Huhu,

vielleicht hat mir ja jemand einen Tipp:


Bekomme irgendwie nicht das richtige Ergebnis für Prob 1.1

Aufgabe: Formulate an LTL safety property that states that no process reads or writes, while another process is writing.
Daraus schließe ich folgende Annahmen:
  • Immer wenn ein Prozess schreibt, wird nie gelesen.
    Immer wenn Prozess 1 schreibt, darf nie gelesen werden und Prozess 2 darf nie schreiben.
    Immer wenn Prozess 2 schreibt, darf nie gelesen werden und Prozess 1 darf nie schreiben.
    Wenn ein Prozess liest, wird nicht gelesen.
Mein LTL passt irgendwie nicht. Habe Sprungmarken bei beiden Prozessen eingefügt.
Ich wollte die Komplexität der Formel immer erweitern. Sprich wenn meine erste Annahme validiert wird, erweitere sie um die Nächste.
Als Grundlage nehme ich die Infos von dem Foliensatz "TemporalModelCheckingWithSPIN", Folie 28.

Zum 1. Punkt:
"Immer wenn ein Prozess schreibt folgt, dass kein Prozess liest": []writer@cs -> !reader@cs

Passt denn das Vorgehen?

Danke und Grüße
Felix

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

Re: Lab 2: Problem 1.1

Beitrag von Nathan Wasser »

Dir ist bewußt, dass Du in Aufgabe 1.1 nur die LTL Formel schreiben sollst. Wie es in Aufgabe 1.2 direkt am Anfang steht: Die Formel gilt (noch) nicht in diesem Modell.

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: Lab 2: Problem 1.1

Beitrag von FGB »

Hi Nathan,

ne, war mir leider nicht bewusst :-(

Formulate an LTL safety property that states that no process reads or writes, while another process is writing. Do not add any ghost variables or change the model in any way except for adding labels.

Hier steht ja auch "... exept for adding labels.". Daraus hab ich auch geschlossen, dass wir das Modell um die Sprungmarken ergänzen dürfen.
Deswegen hab ich versucht meine Formel in SPIN zu validieren.

Also schreibe ich einfach nur die LTL Formel und lass das einfach mal so, in der Hoffnung, es passt ?!

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Re: Lab 2: Problem 1.1

Beitrag von Boddlnagg »

Ja, in Aufgabe 1.1 schreibst du die Formel hin (inkl. Labels), in Aufgabe 1.2 schreibst du noch eine Formel hin, und erst in Aufgabe 1.3 änderst du das Modell so, dass die Formeln erfolgreich verifiziert werden können.

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: Lab 2: Problem 1.1

Beitrag von FGB »

Alles klar,

danke!

Antworten

Zurück zu „Archiv“