使用SPIN測試多個LTL公式

我有很多LTL公式，我試圖在同一.pml文件上進行測試。我的問題是，當在任何單個公式中發現錯誤時，跟蹤文件被寫入（或覆蓋）到相同的跟蹤文件名。我一直無法找到寫入我選擇的跟蹤文件名的方法。有誰知道這個選項是否存在？使用SPIN測試多個LTL公式

如果不是，我可以使用什麼策略同時測試同一.pml文件中的多個ltl公式，而不必每次都覆蓋相同的跟蹤文件？

我知道SPIN運行時-x選項，但這只是防止覆蓋的跟蹤文件。它不會生成具有不同名稱的跟蹤文件。

來源

2017-08-16 cmoses

AFAIK，沒有這樣的選擇。

替代方法

在LINUX + bash中，你可以選擇以下的，殘酷的，方法。

定義set_trail_name功能：

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

它有兩個參數：您的首選trail_file_nime和的pan.c位置。

然後使用它，如下所示：

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

注意

你可能想用

清理臨時文件，以豐富的腳本，例如pan, pan.*, _spin_nvr.tmp
財產狀況分析（真/假）和印刷
...

另一個完全合法的解決辦法是每次調用旋轉模型檢查後，只需重命名現有跟蹤文件。

來源

2017-08-16 09:43:07

使用SPIN測試多個LTL公式

回答

相關問題