1

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

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

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

4

1 回答 1

2

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
  • 属性状态分析（真/假）和打印
  • ...

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

于 2017-08-16T09:43:07.447 回答