使用 SPIN 测试多个 LTL 公式

Question

我尝试在同一个 .pml 文件上测试许多 LTL 公式。我的问题是，当在任何单个 ltl 公式中发现错误时，跟踪文件将写入（或覆盖）相同的跟踪文件名。我一直无法找到写入我选择的跟踪文件名的方法。有谁知道这个选项是否存在？

如果不是，我可以使用什么策略同时测试同一个 .pml 文件中的多个 ltl 公式，而不会每次都覆盖同一个跟踪文件？

我知道 SPIN runtime -x 选项，但这只是防止跟踪文件被覆盖。它不会生成具有不同名称的跟踪文件。

Answer 1

AFAIK，没有这个选项。

解决方法

对于 linux+bash，您可以选择以下残酷的方法。

定义set_trail_name函数：

~$ function set_trail_name() { sed -i "s/^\(char \*TrailFile =\)\(.*\)$/\1 \"\";/" ""; }
~$ 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 \"\";/" "";
}

function check_property() {
    set -e

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

    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 \"\";/" "";
}

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

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

function check_properties()
{
    set -e

    spin -a "" 1>/dev/null
    mapfile -t properties < <(gawk 'match([=14=], /^ltl ([^{]+) .*$/, a) { print a[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
分析属性状态（true/false）和打印
...

另一个完全合法的解决方案可能是在每次调用 Spin 模型检查器后简单地重命名现有的轨迹文件。

使用 SPIN 测试多个 LTL 公式

Testing Multiple LTL Formulae with SPIN

model-checking

spin

promela