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
|
||
|---|---|---|
| .. | ||
| README | ||
| 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 | ||
| 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 | ||
README
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