SPIN: interpretiere die Fehlerspur

Question

Ich versuche mit Spin die Aufgabe über den Bauer, Wolf, Ziege und Kohl zu lösen.

So fand ich die Folowing Promela Beschreibung:

#define fin (all_right_side == true) 
#define wg (g_and_w == false) 
#define gc (g_and_c == false) 

ltl ltl_0 { <> fin && [] (wg && gc) } 

bool all_right_side, g_and_w, g_and_c; 
active proctype river() 
{ 
bit f = 0, 
w = 0, 
g = 0, 
c = 0; 

all_right_side = false; 
g_and_w = false; 
g_and_c = false; 
printf("MSC: f %c w %c g %c c %c \n", f, w, g, c); 

do 
:: (f==1) && (f == w) && (f ==g) && (f == c) -> 
     all_right_side = true; 
     break; 
:: else -> 
     if 
      :: (f == w) -> 
        f = 1 - f; 
        w = 1 - w; 
      :: (f == c) -> 
        f = 1 - f; 
        w = 1 - c; 
      :: (f == g) -> 
        f = 1 - f; 
        w = 1 - g; 
      :: (true) -> 
        f = 1 - f; 
     fi; 

     printf("M f %c w %c g %c c %c \n", f, w, g, c); 

     if 
      :: (f != g && g == c) -> 
        g_and_c = true; 
      :: (f != g && g == w) -> 
        g_and_w = true; 
      ::else -> 
        skip 
     fi 
od; 

printf ("MSC: OK!\n") 
} 

ich hinzufügen, dass es eine LTL-Formel: ltl ltl_0 {<> fin & & [] (wg & & gc)} zu überprüfen , als würde der Wolf keine Ziege essen, und die Ziege würde den Kohl nicht essen. Ich möchte ein Beispiel bekommen, wie der Landwirt alle seine Bedürfnisse (w-g-c) ohne Verlust transportieren kann.

Wenn ich Verifizierung ausgeführt, habe ich das folgende Ergebnis: Zustandsvektor 20 Byte, Tiefe 59 erreicht ist, Fehler: 1 64 Zustände, gespeichert 23 Staaten, angepasst 87 Transitionen (= gespeichert + matched) 0 atomare Schritte Hash-Konflikte: 0 (aufgelöst)

Das bedeutet, dass das Programm ein Beispiel für mich generiert hat. Aber ich kann es nicht interpretieren. Der Inhalt von * .pml.trial Datei ist: enter image description here

Bitte, hilf mir zu interpretieren.

Answer 1

Um „interpretieren“ es, könnten Sie den Quellcode ändern, so dass jedes Mal, wenn eine Aktion etwas genommen wird intellegibile auf stdout gedruckt wird.

z.B .:

  :: (f == w) -> 
        if 
         :: f == 0 -> printf("LEFT ---[farmer, wolf]--> RIGHT\n"); 
         :: f == 1 -> printf("LEFT <--[farmer, wolf]--- RIGHT\n"); 
         :: else -> skip; 
        fi; 
        f = 1 - f; 
        w = 1 - w; 

+ etwas ähnliches für die Fälle (f == c), (f == g) und (true).

Hinweis: Ihren Quellcode bietet bereits printf("M f %c w %c g %c c %c \n", f, w, g, c);, die-interpretieren die Gegenbeispiel verwendet werden können, wenn Sie daran denken, dass 0 bedeutet left und 1 bedeutet right. Ich würde jedoch eine mehr ausführliche Ablaufverfolgung bevorzugen.

---

Nachdem Sie dies für jeden möglichen Übergang getan haben, können Sie sehen, was in Ihrem Gegenbeispiel durch Ausführen Spin auf folgende Weise

~$ spin -t file_name.pml 

Die Option -t Replays die geschieht neueste trail von spin auf die Verletzung von einigen Assertion/Eigenschaft gefunden.

Answer 2

Es gibt einige Möglichkeiten, wie Sie die Spur interpretieren können.

1. Verwendung iSpin:
   • gehen zu Simulieren/Wiedergabe
   • in-Modus, wählen Sie Guided und den Namen Ihrer Spur
   • Run

Dies wird Datei eingeben Zeigen Sie Schritt für Schritt die Aktionen, die von jedem der Prozesse ausgeführt wurden, einschließlich Informationen wie Prozessnummer, Proktypenname, Zeilennummer Befehl ausgeführt, Code des Befehls ausgeführt.

2. das gleiche tun mit Spin:
   Verwenden Sie den Befehl

   spin -t -p xyz.pml

3. die Spur Datei Syntax verstehen:
   jede Zeile in der Datei ist ein Schritt durch den Simulator genommen. die erste Spalte ist nur Seriennummern. Die zweite Spalte ist Prozessnummern (PIDs). (zB init wird 0 sein, der erste Prozess, der gestartet wird/läuft wird 1 sein und so weiter.) Die dritte Spalte ist die Übergangsnummer. Wenn Sie nur eine Vorstellung davon bekommen möchten, was gerade passiert, können Sie die Pids anschauen und die Anweisungen

durchgehen