1

我有非常简单的发送方-接收方协议：

#define SZ 4
int sent = 0;
int received = 0;
chan ch = [SZ] of {int};
int varch;
init {
    do
    :: ((len(ch) < SZ) && (received != 1)) ->
        d_step {
        ch ! 1; sent = 1; printf("sent\n");
    }
    :: ((len(ch) == SZ) || ((received == 1) && (len(ch) > 0))) ->
    d_step {
        ch ? varch; received = 1; printf("received\n");
    }
    :: 1 -> /* simulates ramdomness */
       atomic {
          printf("timeout1\n");/*break; */
    }
    od;
}

它发送四个数据包，然后接收它们。然后我尝试证明属性：总是发送意味着最终接收：

ltl pr { [] ( (sent == 1) -> (<> (received == 1)) ) }

...并且什么也没有发生：SPIN 没有找到这个属性证明和它的否定。

为什么？

4

1 回答 1

1

因此，经过快速检查，LTL 属性是不可能满足的。LTL 属性包括 always但一种可行的执行方式是让do::od语句/* simulates randomness */永远采用该选项。在这种情况下，将不会“接收”任何队列并且 LTL 会失败。

我的 SPIN 运行确认了上述情况（我将您的代码放入文件 'sr.pml'）

$ spin -a sr.pml
$ gcc -o pan pan.c
$ ./pan -a
pan:1: acceptance cycle (at depth 16)
pan: wrote sr.pml.trail

(Spin Version 6.3.2 -- 17 May 2014)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (pr)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 60 byte, depth reached 20, errors: 1
       12 states, stored (14 visited)
        0 states, matched
       14 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.290   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds

然后我们可以看到路径：

$ spin -p -t sr.pml
ltl pr: [] ((! ((sent==1))) || (<> ((received==1))))
starting claim 1
using statement merging
Never claim moves to line 4 [(1)]
  2:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
  4:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
  4:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
  4:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
Never claim moves to line 3 [((!(!((sent==1)))&&!((received==1))))]
  6:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
Never claim moves to line 8 [(!((received==1)))]
  8:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
  8:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
  8:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
 10:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
 12:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
 12:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
 12:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
 14:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
 16:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
 16:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
 16:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
  <<<<<START OF CYCLE>>>>>
 18:    proc  0 (:init::1) sr.pml:16 (state 11) [(1)]
          timeout1
 20:    proc  0 (:init::1) sr.pml:18 (state 12) [printf('timeout1\\n')]
spin: trail ends after 20 steps
#processes: 1
        sent = 1
        received = 0
        queue 1 (ch): [1][1][1][1]
        varch = 0
 20:    proc  0 (:init::1) sr.pml:7 (state 14)
 20:    proc  - (pr:1) _spin_nvr.tmp:7 (state 10)
1 processes created

第<<<<<START OF CYCLE>>>>16 行 ( :: 1 -> ...) 处显示的 sr.pml 将永远执行。此外，LTL 还存在其他故障。使用 './pan -a -i' 运行 SPIN 搜索以找到最短路径；它表明您的 LTL 没有找到您想要查找的内容。

于 2014-11-07T02:41:17.793 回答