28e9566dc5
from Ori_B: There were a small number of changes needed from the tarball on spinroot.org: - The mkfile needed to be updated - Memory.h needed to not be included - It needed to invoke /bin/cpp instead of gcc -E - It depended on `yychar`, which our yacc doesn't provide. I'm still figuring out how to use spin, but it seems to do the right thing when testing a few of the examples: % cd $home/src/Spin/Examples/ % spin -a peterson.pml % pcc pan.c -D_POSIX_SOURCE % ./6.out (Spin Version 6.4.7 -- 19 August 2017) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid end states + State-vector 32 byte, depth reached 24, errors: 0 40 states, stored 27 states, matched 67 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.002 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 proctype user /tmp/Spin/Examples/peterson.pml:20, state 10, "-end-" (1 of 10 states) pan: elapsed time 1.25 seconds pan: rate 32 states/second |
||
---|---|---|
.. | ||
dstep.c | ||
flow.c | ||
guided.c | ||
main.c | ||
mesg.c | ||
mkfile | ||
msc_tcl.c | ||
pangen1.c | ||
pangen1.h | ||
pangen2.c | ||
pangen2.h | ||
pangen3.c | ||
pangen3.h | ||
pangen4.c | ||
pangen4.h | ||
pangen5.c | ||
pangen5.h | ||
pangen6.c | ||
pangen6.h | ||
pangen7.c | ||
pangen7.h | ||
pc_zpp.c | ||
ps_msc.c | ||
README | ||
reprosrc.c | ||
run.c | ||
sched.c | ||
spin.h | ||
spin.y | ||
spinlex.c | ||
structs.c | ||
sym.c | ||
tl.h | ||
tl_buchi.c | ||
tl_cache.c | ||
tl_lex.c | ||
tl_main.c | ||
tl_mem.c | ||
tl_parse.c | ||
tl_rewrt.c | ||
tl_trans.c | ||
vars.c | ||
version.h |
the latest version of spin is always available via: http://spinroot.com/spin/whatispin.html to make the sources compile with the mkfile on Plan 9 the following changes were made: omitted memory.h from spin.h changed /lib/cpp to /bin/cpp in main.c simplified non_fatal() in main.c to remove use of yychar