时间戳

首页 > 解决方案 > 模型检查：为什么 LTL 逻辑“<>”在 Spin 中没有产生正确的反例

model-checking - 模型检查：为什么 LTL 逻辑“<>”在 Spin 中没有产生正确的反例

问题描述

更新

我之前的尝试有两个问题。通过修复它们，我成功地得到了预期的答案。

原始问题

我是模型检查和旋转的新手。我在以下示例中遇到问题。

具体而言，命令、Promela 代码和跟踪如下。

在这条线索中，结果是p满意的，因为SUM确实大于BOUND。我不明白为什么 Spin 给我一个满足的反例p？

./spin649_linux64 -f '<> p' -a sample.pml
gcc -o pan pan.c
./pan -i 
./spin649_linux64 -p -t sample.pml

#define UPDATE(c) if :: ch[c]>sz[c] -> sz[c] = ch[c] :: else fi
#define PRODUCE(c, n) ch[c] = ch[c] + n; UPDATE(c)
#define CONSUME(c, n) ch[c] = ch[c] - n
#define WAIT(c, n) ch[c] >= n

int ch[2]; int sz[2];

#define BOUND 6 
#define SUM (sz[0] + sz[1])
#define p (SUM > BOUND)

// Actor_a <==1==> Actor_b <==2==> Actor_c

// Actor_a produces 2 tokens to channel 1
// Actor_b consumes 3 tokens from channel 1 and produces 1 token to channel 2
// Actor_c consumes 2 tokens from channel 2
// sz[i] records the highest capacity seen for channel[i]
// There exist an infinite schedule that sz[0] + sz[1] is at most 6 at any moment

proctype Actor_a() {
  do 
  :: atomic{ PRODUCE(0, 2); printf("a")}
  od
}

proctype Actor_b() {
  do :: atomic { WAIT(0,3) -> CONSUME(0, 3); PRODUCE(1, 1); printf("b") }
  od
}

proctype Actor_c() {
  do :: atomic {WAIT(1, 2) -> CONSUME(1, 2); printf("c")}
  od
}

init {
  atomic {
    run Actor_a();
    run Actor_b();
    run Actor_c();
  }
}

starting claim 4
spin: couldn't find claim 4 (ignored)
Starting Actor_a with pid 2
  2:    proc  0 (:init::1) sample.pml:30 (state 1)      [(run Actor_a())]
Starting Actor_b with pid 3
  3:    proc  0 (:init::1) sample.pml:31 (state 2)      [(run Actor_b())]
Starting Actor_c with pid 4
  4:    proc  0 (:init::1) sample.pml:32 (state 3)      [(run Actor_c())]
  6:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
  7:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
  7:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a  7:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
  9:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 10:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 10:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 10:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
 12:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 13:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 13:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 13:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
 15:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 16:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 16:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 16:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
spin: trail ends after 17 steps
#processes: 4
                ch[0] = 8
                ch[1] = 0
                sz[0] = 8
                sz[1] = 0
 17:    proc  3 (Actor_c:1) sample.pml:24 (state 5)
 17:    proc  2 (Actor_b:1) sample.pml:19 (state 11)
 17:    proc  1 (Actor_a:1) sample.pml:13 (state 9)
 17:    proc  0 (:init::1) sample.pml:34 (state 5) <valid end state>
4 processes created

如果您能提供帮助，非常感谢！

标签： model-checkingpromelaspin

解决方案

最初的尝试有两个问题。通过修复它们，我成功地得到了预期的答案。

  • 从命令行使用 -f 选项指定的 LTL 将被否定。相反，我通过将 ltl { <> p} 添加到 Promela 程序中来使用内联 LTL。

  • 其次，在执行 pan 时，似乎我们需要使用 -a 来“查找接受周期”。我不完全确定这意味着什么，我的猜测是 Spin 将尝试识别无限的时间表。

推荐阅读