Testen mehrerer LTL-Formeln mit SPIN

Ich habe viele LTL-Formeln, die ich versuche, auf der gleichen .pml-Datei zu testen. Mein Problem ist, dass, wenn ein Fehler in einer einzelnen Formel gefunden wird, die Trail-Datei in den gleichen Trail-Dateinamen geschrieben (oder überschrieben) wird. Ich konnte keine Möglichkeit finden, in einen Trail-Dateinamen meiner Wahl zu schreiben. Weiß jemand, ob diese Option existiert?Testen mehrerer LTL-Formeln mit SPIN

Wenn nicht, was ist eine Strategie, die ich verwenden könnte, um mehrere ltl-Formeln aus derselben .pml-Datei gleichzeitig zu testen, ohne jedes Mal dieselbe Pfaddatei zu überschreiben?

Ich kenne die SPIN Laufzeit-Option-X, aber das verhindert nur eine Trail-Datei überschrieben werden. Es erzeugt keine Trail-Dateien mit unterschiedlichen Namen.

Quelle

2017-08-16 cmoses

AFAIK, gibt es keine solche Option.

Abhilfe

Für Linux + bash, können Sie die folgenden, brutal, Ansatz entscheiden.

definieren set_trail_name Funktion:

~$ function set_trail_name() { sed -i "s/^\\(char \\*TrailFile =\\)\\(.*\\)$/\\1 \"${1}\";/" "${2}"; } 
~$ export -f set_trail_name

Es dauert zwei Parameter: Ihren bevorzugten trail_file_nime und den Standort von pan.c.

verwenden Sie es dann wie folgt:

~$ spin -a test.pml 
ltl p1: [] (<> (! (q0))) 
ltl p2: [] (<> (q1)) 
    the model contains 2 never claims: p2, p1 
... 

~$ set_trail_name my_p1_name pan.c 
~$ gcc -o pan pan.c 
~$ ./pan -a -N p1 
pan: ltl formula p1 
pan:1: acceptance cycle (at depth 4) 
pan: wrote my_p1_name.trail 
... 

~$ ls *.trail 
my_p1_name.trail 

~$ set_trail_name my_p2_name pan.c 
~$ gcc -o pan pan.c 
~$ pan -a -N p2 
pan: ltl formula p2 
pan:1: acceptance cycle (at depth 2) 
pan: wrote my_p2_name.trail 
... 

~$ ls *.trail 
my_p1_name.trail  my_p2_name.trail

Abhilfe VERBESSERUNG # 1

Sie können einen Schritt weiter gehen, z.B.

#!/bin/bash 

function set_trail_name() { 
    sed -i "s/^\\(char \\*TrailFile =\\)\\(.*\\)$/\\1 \"${1}\";/" "${2}"; 
} 

function check_property() { 
    set -e 

    spin -a "${1}" 1>/dev/null 
    set_trail_name "${2}" pan.c 
    gcc -o pan pan.c 
    ./pan -a -N "${2}" 

    set +e 
} 

check_property "${@}"

, die es leichter macht, um sie auszuführen:

~$ ./run_spin.sh test.pml p1 
pan: ltl formula p1 
pan:1: acceptance cycle (at depth 4) 
pan: wrote p1.trail 
... 

~$ ~$ ./run_spin.sh test.pml p2 
pan: ltl formula p2 
pan:1: acceptance cycle (at depth 2) 
pan: wrote p2.trail

Abhilfe VERBESSERUNG # 2

Sie können sogar ein paar Schritte weiter gehen, z.B.

#!/bin/bash 

function set_trail_name() 
{ 
    sed -i "s/^\\(char \\*TrailFile =\\)\\(.*\\)$/\\1 \"${1}\";/" "${2}"; 
} 

function check_property() 
{ 
    echo -e "\\n>>> Testing property ${1} ...\\n" 

    set_trail_name "${1}" pan.c 
    gcc -o pan pan.c 
    ./pan -a -N "${1}" 
} 

function check_properties() 
{ 
    set -e 

    spin -a "${1}" 1>/dev/null 
    mapfile -t properties < <(gawk 'match($0, /^ltl ([^{]+) .*$/, a) { print a[1] }' "${1}") 

    for prop in "${properties[@]}" 
    do 
     check_property "${prop}" 
    done 

    set +e 
} 

check_properties "${@}"

Was es trivial macht es laufen:

~$ ./run_spin.sh test.pml 

>>> Testing property p1 ... 

pan: ltl formula p1 
pan:1: acceptance cycle (at depth 4) 
pan: wrote p1.trail 
... 

>>> Testing property p2 ... 

pan: ltl formula p2 
pan:1: acceptance cycle (at depth 2) 
pan: wrote p2.trail 
...

NOTES

Sie können die Skripte mit

Bereinigung von temporären Dateien bereichern wollen , z.B. pan, pan.*, _spin_nvr.tmp
Analyse des Eigenschaftsstatus (richtig/falsch) und Drucken
...

Eine weitere völlig legitime Lösung einfach sein könnte, um bestehende Trail-Dateien nach jedem Aufruf des Checker Spin Modells zu umbenennen.

Quelle

2017-08-16 09:43:07

Testen mehrerer LTL-Formeln mit SPIN

Antwort

Verwandte Themen