同じ.pmlファイルでテストしようとしている多くのLTL式があります。私の問題は、単一のltl式でエラーが見つかった場合、トレイルファイルは同じトレイルファイル名に書き込まれる（または上書きされる）ことです。私は私の選択のトレイルファイル名に書き込む方法を見つけることができませんでした。このオプションが存在するか知っていますか？複数のLTL式をSPINでテストする
そうでない場合は、毎回同じトレイルファイルを上書きせずに同じ.pmlファイルから複数のltl式を同時にテストするための戦略は何ですか？
私はSPINランタイム-xオプションを認識していますが、トレイルファイルが上書きされないようにするだけです。異なる名前のトレイルファイルは生成されません。
AFAIKのようなオプションはありません。
回避策
のLinux + bashのためには、以下の、残忍な、アプローチを選ぶことができます。
はset_trail_name関数を定義：お好みのtrail_file_nimeとpan.cの所在地：
~$ function set_trail_name() { sed -i "s/^\\(char \\*TrailFile =\\)\\(.*\\)$/\\1 \"${1}\";/" "${2}"; }
~$ export -f set_trail_name
それは2つのパラメータを取ります。次のように
そして、それを使用する：
~$ 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
をあなたは、例えば、さらに一歩行くことができますそれが簡単にそれを実行できるようになり
#!/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 "${@}"
：
~$ ./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
あなたも、例えば、さらなるステップのカップルを行くことができますそれは些細なそれを実行できるようになり
#!/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 "${@}"
：
~$ ./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
あなたは一時ファイルの、例えばpan, pan.*, _spin_nvr.tmp
もう完全に合法的な解決策は単純スピンモデル検査への各呼び出しの後、既存の証跡ファイルの名前を変更する可能性があります。