如何在jspin中指定C庫的路徑？

Question

我使用jspin並試圖包括c_code表達式中stdio.h中庫：

c_code 
{ 
    #include <stdio.h> 
} 

不過，我得到以下錯誤：

spin: error: No file 'stdio.h' 

其中MinGW的安裝和它我已經檢查目錄有stdio.h裏面。因此，我想，這全是關於錯誤的路徑。如何在jspin中設置包含路徑？

Answer 1

嘗試：

c_decl { 
    \#include <stdio.h> 
} 

的\#是關鍵部分（Spinroot.com for c_decl）。此外，使用c_decl{}，因爲.h文件不包含代碼。

關於fprintf（）沒有顯示輸出;我不能說我知道原因。我試過你的特定代碼。下面是結果：

ebg@ebg$ rm /tmp/foo.bar 
ebg@ebg$ spin -a test.pml 
ebg@ebg$ gcc -o test pan.c 
ebg@ebg$ ./test 
hint: this search is more efficient if pan.c is compiled -DSAFETY 

(Spin Version 6.2.4 -- 21 November 2012) 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    - (none specified) 
    assertion violations + 
    acceptance cycles  - (not selected) 
    invalid end states + 

State-vector 12 byte, depth reached 2, errors: 0 
     3 states, stored 
     0 states, matched 
     3 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 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 


unreached in init 
    (0 of 2 states) 

pan: elapsed time 0 seconds 
ebg@ebg$ cat /tmp/foo.bar 
some str 

這裏是我使用的代碼：

c_decl { 
    \#include <stdio.h> 
} 

init { 
    c_code { 
    FILE *file; 

    file = fopen ("/tmp/foo.bar", "a+"); 
    fprintf (file, "%s", "some str"); 
    fclose (file); 
    } 
}