使用 Promela 和 SPIN 的 printf 输出？

Question

我是一名尝试使用 Promela 和 SPIN 的初学者。在开发一些简单的 Promela 规范时，我想使用 printf() 检查程序中变量的值。我已阅读 this man page 并尝试运行一个简单的 hello world 程序，但我没有看到任何输出文本。这是示例 hello world 文件：

init {
    printf("MSC: passed first test!\n")
}

我用来编译和运行的步骤是

spin -a hello.pml
cc -o run pan.c
./run

运行的输出是

hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 4.2.6 -- 27 October 2005)
        + Partial Order Reduction

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        acceptance   cycles     - (not selected)
        invalid end states      +

State-vector 12 byte, depth reached 2, errors: 0
       3 states, stored
       0 states, matched
       3 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

4.879   memory usage (Mbyte)

unreached in proctype :init:
        (0 of 2 states)

那么，我在哪里可以找到 printf 语句的输出？我也尝试过在更复杂的 promela 文件中使用 printf 语句，但显然我想让它首先适用于简单的情况。任何见解将不胜感激。谢谢！

Answer 1

当您运行 SPIN 验证时，没有打印输出；仅指示是否发现错误（和其他性能信息）。请注意，由于您是初学者，因此当您使用 'spin -a ...' 调用 spin 时，您会“运行 SPIN 验证”，然后运行编译后的代码。

有两种查看输出的方法。首先，通过spin hello.pml在模拟模式下使用SPIN。例如：

$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); }
> EOF
$ spin hello.pml 
      hello world
1 process created

其次，在验证模式下使用 SPIN，但会在程序中注入错误。发生错误后，检查跟踪文件。例如：

$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); assert (0); }
> EOF
$ spin -a hello.pml
$ gcc -o hello pan.c
$ ./hello
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: assertion violated 0 (at depth 0)
pan: wrote hello.pml.trail
...
State-vector 12 byte, depth reached 0, errors: 1
...
pan: elapsed time 0 seconds
$ spin -p -t hello.pml
using statement merging
      hello world
  1:    proc  0 (:init:) hello.pml:1 (state 1)  [printf('hello world\\n')]
spin: hello.pml:1, Error: assertion violated
spin: text of failed assertion: assert(0)
  1:    proc  0 (:init:) hello.pml:1 (state 2)  [assert(0)]
spin: trail ends after 1 steps
#processes: 1
  1:    proc  0 (:init:) hello.pml:1 (state 3) <valid end state>
1 process created

spin -p -t hello.pml之后可以在上面找到'hello world'