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;
}

4 つのパケットを送信してから受信します。次に、プロパティを証明しようとします: 常に送信は最終的に受信を意味します:

ltl pr { [] ( (送信 == 1) -> (<> (受信 == 1)) }

...そして何も起こりません: SPIN は、このプロパティの証明とその否定の両方を見つけません。

なんで？

4

1 に答える 1

1

そのため、簡単に調べると、LTL プロパティを満たすことはおそらくありません。LTL プロパティには含まれて いますalwaysが、実行可能な実行の 1 つは、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

16 行目の<<<<<START OF CYCLE>>>>sr.pml ( :: 1 -> ...) は永久に実行されます。また、LTL には他にも障害があります。「./pan -a -i」を使用して SPIN 検索を実行し、最短のトレイルを見つけます。これは、探しているものを LTL が見つけられていないことを示しています。

于 2014-11-07T02:41:17.793 に答える