自旋：錯誤，生成此pan.c自旋的版本假定不同的字長（4-異8）

Question

我使用Windows O.S和Cygwin的i型：wish -f ispin.tcl打開ispin接口。 我打開一個文件​​其中包含：

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) 

我該如何解決這個問題？我在互聯網上搜索，但我找不到幫助我的東西。

注：我並沒有改變任何驗證屬性：

Answer 1

解決上述錯誤是安裝Cygwin for 32-bit versions of Windows即使我的筆記本電腦是64位。這是因爲executable of spin只存在於Windows 32位，所以他們一定要配合我的理解。

安裝Cygwin的（gcc，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"