SPIN: interpréter la trace d'erreur

Question

J'essaye de résoudre avec la tâche de tourner le fermier, le loup, la chèvre et le chou.

Alors, j'ai trouvé la folowing description Promela:

#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") 
} 

je y ajouter un LTL-formule: ltl ltl_0 {<> fin & & [] (wg & & gc)} pour vérifier , que le loup ne mange pas une chèvre, et que la chèvre ne mange pas le chou. Je veux avoir un exemple, comment l'agriculteur peut transporter tous ses besoins (w-g-c) sans perte.

Quand je lance la vérification, j'obtient le résultat suivant: vecteur d'état 20 octets, la profondeur atteint 59, les erreurs: 1 64 états, stockées 23 états, identifié 87 transitions (= stockés + adapté) 0 étapes atomiques conflits de hachage: 0 (résolu)

Cela signifie que le programme a généré un exemple pour moi. Mais je ne peux pas l'interpréter. Le contenu du fichier * .pml.trial est: enter image description here

S'il vous plaît, aidez-moi à interpréter.

Answer 1

Pour « interpréter », vous pouvez modifier votre code source afin que chaque fois qu'une action est prise quelque chose intellegibile est imprimé sur stdout.

.: par exemple

  :: (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; 

+ quelque chose de similaire pour les cas (f == c), (f == g) et (true).

Note: votre code source fournit déjà printf("M f %c w %c g %c c %c \n", f, w, g, c);, qui peut être utilisé pour interpréter le contre-exemple si vous gardez à l'esprit que 0 signifie left et 1 signifie right. Je préférerais un suivi verbeux, cependant.

---

Une fois que vous avez fait pour chaque transition possible, vous pouvez voir ce qui se passe au sein de votre contre-exemple en exécutant tour de la manière

~$ spin -t file_name.pml 

suivante L'option -t rejoue les dernière trail trouvée par spin sur la violation de certains assertion/propriété .

Answer 2

Il existe plusieurs façons d'interpréter la trace.

1. Utilisation iSpin:
   • aller à Simuler/Play
   • en mode, sélectionnez Assisté et entrez le nom de votre fichier de piste
   • Run

Cette volonté montrer, étape par étape, les actions entreprises par chacun des processus, y compris les informations telles que le numéro de processus, le nom du proctype, la ligne engourdie d'instruction exécutée, code d'instruction exécuté.

2. Faites la même chose avec un spin:
   Utilisez la commande

   spin -t -p xyz.pml

3. Comprendre la syntaxe du fichier de piste:
   chaque ligne sur le fichier est un étape prise par le simulateur. la première colonne est juste des numéros de série. La deuxième colonne est les numéros de processus (pids). (par exemple init sera 0, le premier processus démarrera/s'exécutera 1 et ainsi de suite.) La troisième colonne est le numéro de transition. Si vous voulez avoir une idée de ce qui se passe, vous pouvez regarder les pids et passer en revue les instructions