Spinroot

blackhorse

Member

Registered: 2011-06-22

Posts: 3

About instructions of files in SPIN sources

Hello, I wonder if there are any instructions about the function of files in the SPIN source distribution.
Thanks.

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Re: About instructions of files in SPIN sources

the files are explained in the book, but for a short synopsis:
pan.h has data structure definitions and macros
pan.c contains the generic model checking algorithms and storage modes
pan.t contains the automata specficications for all proctypes
pan.m has the details of the forward transitions, and pan.b has the details of the backward transitions that can undo the effect of the forward moves (this allows for compact representation of the search stack which then only needs to contain delta-information and not full state descriptors in many cases)
hope this helps

blackhorse

Member

Registered: 2011-06-22

Posts: 3

Re: About instructions of files in SPIN sources

Thanks a lot:)
[quote=spinroot]the files are explained in the book, but for a short synopsis:
pan.h has data structure definitions and macros
pan.c contains the generic model checking algorithms and storage modes
pan.t contains the automata specficications for all proctypes
pan.m has the details of the forward transitions, and pan.b has the details of the backward transitions that can undo the effect of the forward moves (this allows for compact representation of the search stack which then only needs to contain delta-information and not full state descriptors in many cases)
hope this helps[/quote]