Test de plusieurs formules LTL avec SPIN

J'ai plusieurs formules LTL que j'essaie de tester sur le même fichier .pml. Mon problème est que lorsqu'une erreur est trouvée dans une seule formule ltl, le fichier de chemin est écrit (ou écrasé) au même nom de fichier de chemin. Je n'ai pas réussi à trouver un moyen d'écrire sur un nom de fichier de trail de mon choix. Est-ce que quelqu'un sait si cette option existe? Sinon, quelle est la stratégie que je pourrais utiliser pour tester simultanément plusieurs formules ltl à partir du même fichier .pml sans écraser le même fichier de trace à chaque fois?Test de plusieurs formules LTL avec SPIN

Je suis conscient de l'option SPIN runtime -x, mais cela empêche simplement l'écrasement d'un fichier de trace. Il ne génère pas de fichiers de trace avec des noms différents.

Source

2017-08-16 cmoses

AFAIK, il n'existe pas une telle option.

Contournement

Pour linux + bash, vous pouvez opter pour ce qui suit, brutale, approche.

Définition de la fonction set_trail_name:

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

Il prend deux paramètres: votre trail_file_nime préféré et l'emplacement de pan.c.

utiliser ensuite comme suit:

~$ 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

# 1 Contournement AMÉLIORATION

Vous pouvez aller un peu plus loin, par exemple

#!/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 "${@}"

ce qui le rend plus facile de l'exécuter:

~$ ./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

# 2 Contournement AMÉLIORATION

Vous pouvez même aller quelques pas plus loin, par exemple

#!/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 "${@}"

ce qui le rend trivial pour l'exécuter:

~$ ./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

Vous pouvez enrichir les scripts avec

nettoyage des fichiers temporaires , par exemple. pan, pan.*, _spin_nvr.tmp
analyse de l'état de la propriété (vrai/faux) et de l'impression
...

Une autre solution tout à fait légitime pourrait être de simplement renommer les fichiers existants piste après chaque appel au vérificateur de modèle Spin.

Source

2017-08-16 09:43:07

Test de plusieurs formules LTL avec SPIN

Répondre

Questions connexes