如何在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); 
    } 
}