3

私は Windows OS を使用しており、Cygwin i で次のように入力wish -f ispin.tclして ispin インターフェイスを開きます。test.pml以下を含むファイルを開きます。

byte state = 2;

proctype A()
{   (state == 1) -> state = 3
}

proctype B()
{   state = state - 1
}

init
{   run A(); run B()
}

その後、シード = 123 でランダムな方法を使用して実行します。結果は問題なく出力に出力されます。

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting A with pid 1
  1:    proc  0 (:init::1) creates proc  1 (A)
  1:    proc  0 (:init::1) test.pml:12 (state 1)    [(run A())]
Starting B with pid 2
  2:    proc  0 (:init::1) creates proc  2 (B)
  2:    proc  0 (:init::1) test.pml:12 (state 2)    [(run B())]
  3:    proc  2 (B:1) test.pml:8 (state 1)  [state = (state-1)]
  4:    proc  1 (A:1) test.pml:4 (state 1)  [((state==1))]
  4:    proc  2 (B:1) terminates
  5:    proc  1 (A:1) test.pml:4 (state 2)  [state = 3]
  5:    proc  1 (A:1) terminates
  5:    proc  0 (:init::1) terminates
3 processes created

このモデルを検証しようとすると、問題が発生します。検証の結果は次のとおりです。

verification result:
spin -a  test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 3952
spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)

どうすればこれを解決できますか? インターネットで検索しましたが、役立つ情報が見つかりませんでした。

注：検証プロパティは変更していません： ispin_interface_verification_properties

4

1 に答える 1

5

上記のエラーの解決策は、ラップトップが 64 ビットであっても、32 ビット バージョンの Windows 用の Cygwinをインストールすることでした。これは、spin の実行ファイルがWindows 32-bit のみに存在するため、一致する必要があることがわかりました。

gccCygwin ( 、cpp、make)のインストール後、spin、ispinおよびtestファイルを新しい Cygwin フォルダー ( C:\cygwin\) に移動します。

他の変更を必要とせずにモデルを実行して再度検証しようとすると、エラーのない正しい出力が表示されます。

verification result:
spin -a  test.promela
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 6304
pan:1: assertion violated 0 (at depth 6)
pan: wrote test.promela.trail

(Spin Version 6.4.5 -- 1 January 2016)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

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

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.292   actual memory usage for states
   64.000   memory used for hash table (-w24)
    0.343   memory used for DFS stack (-m10000)
   64.539   total actual memory usage



pan: elapsed time 0.002 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
于 2016-02-28T01:27:40.553 に答える