Overview |
Verification Options |
Pan |
NAME
pan - Spin generated source for a model-specific verifier.
DESCRIPTION
Overview of options that are available with the verifiers
generated by Spin with Spin's run-time
option -a. There are two groups of options: those that
are available after the verifier source in pan.c has been compiled,
and those that are available at compilation time.
The reason for the split is that knowledge of some options at
compile time can be used to produce a more efficient verification
system.
Attached is also a brief explanation of the numbers that are
printed by the verifiers at the end of a run.
NXT | if defined, the NEXT operator X can be used in LTL formulae; risky, not compatible with partial order reductions |
PC | required when compiling Spin on a PC |
PRINTF | if defined, printf statements in the model are enabled during the verification process (not recommended) |
SOLARIS | required when compiling Spin on a Solaris system |
The next tables give optional directives for compiling the verifiers that are generated by Spin. Traditionally these are stored in a file named pan.c (with a number of dependent files). Usage of the directives below is always optional, and typically of the form:
$ spin -a spec $ cc -o pan -DNOBOUNDCHECK pan.cEach directive modifies the default behavior of the verifier to achieve a specific effect noted in the tables below.
BITSTATE | use supertrace/bitstate instead of exhaustive exploration |
MEMCNT=N | set upperbound to the amount of memory that can be allocated usage, e.g.: -DMEMCNT=20 for a maximum of 2^20 bytes |
NOCLAIM | exclude the never claim from the verification, if present |
NOFAIR | disable the code for weak-fairness (is faster) |
NOREDUCE | disables the partial order reduction algorithm |
NP | enable non-progress cycle detection (option -l), replacing option -a for acceptance cycle detection |
PEG | add complexity profiling (transition counts) |
SAFETY | optimize for the case where no cycle detection is needed (faster, uses less memory, disables both -l and -a) |
VAR_RANGES | compute the effective value range of variables (restricted to the interval 0..255) |
CHECK | generate debugging information (see also DEBUG) |
CTL | allow only those reductions that are consistent with branching time logics like CTL (i.e., the persistent set contains either one or all transitions) |
GLOB_ALPHA | consider process death a global action (for compatibility with versions of Spin between 2.8.5 and 2.9.7) |
NIBIS | apply a small optimization of partial order reduction (sometimes faster, sometimes not...) |
NOREDUCE | disables the partial order reduction algorithm |
XUSAFE | disable validity checks of x[rs] assertions (faster, and sometimes useful if the check is too strict, e.g. when channels are passed around as process parameters) |
NOBOUNDCHECK | don't check array bound violations (faster) |
NOCOMP | don't compress states with fullstate storage (faster, but not compatible with liveness unless -DBITSTATE) |
NOFAIR | disable the code for weak-fairness (is faster) |
NOSTUTTER | disable stuttering rules (warning: changes semantics) stuttering rules are the standard way to extend a finite execution sequence into and infinite one, to allow for a consistent interpretation of B\(u"chi acceptance rules |
SAFETY | optimize for the case where no cycle detection is needed (faster, uses less memory, disables both -l and -a) |
BITSTATE | use supertrace/bitstate instead of exhaustive exploration |
HC | a state vector compression mode; collapses state vector sizes down to 32+16 bits and stores them in conventional hash-table (a version of Wolper's hash-compact method -- new in version 3.2.2.) Variations: HC0, HC1, HC2, HC3 for 32, 40, 48, or 56 bits respectively. The default is equivalent to HC2. |
COLLAPSE | a state vector compression mode; collapses state vector sizes by up to 80% to 90% (see Spin97 workshop paper) variations: add -DSEPQS or -DJOINPROCS (off by default) |
MA=N | use a minimized DFA encoding for the state space, similar to a BDD, assuming a maximum of N bytes in the state-vector (this can be combined with -DCOLLAPSE for greater effect in cases when the original state vector is long) |
MEMCNT=N | set upperbound to the amount of memory that can be allocated usage, e.g.: -DMEMCNT=20 for a maximum of 2^20 bytes |
NFAIR=N | allocates memory for enforcing weak fairness usage, e.g.: -DNFAIR=3 (default is 2) |
VECTORSZ=N | allocates memory (in bytes) for state vector usage, e.g.: -DVECTORSZ=2048 (default is 1024) |
VERBOSE | adds elaborate debugging printouts |
CHECK | more frugal debugging printouts |
SVDUMP | if defined, adds an option -pN to the runtime verifiers to produce a file sv_dump at the end of the run, with a binary representation of all states, using a fixed size of N bytes per state. (see also SDUMP below) |
SDUMP | if used in addition to CHECK: adds ascii dumps of state vectors to verbose output (i.e., an ascii version of SVDUMP) |
BCOMP | when in BITSTATE mode, this computes hash functions over the compressed state-vector (compressed with byte-masking) in some cases, this can improve the coverage |
COVEST | compiles in extra code for giving a coverage estimate at the end of BITSTATE runs, defined by Uli Stern. must compile pan.c with -lm in this case |
HYBRID_HASH | can shave a word (4 bytes) from every state vector, in 25% of the cases... when the state vector is 1 byte longer than a multiple of 4 the memory allocator ends up adding 3 dummy bytes to secure memory alignment. to avoid this, the HYBRID_HASH mode will take away 1 byte from the state vector, and use it as part of the hash -- this causes more collisions, but preserves correct exhaustive exploration - and saves 4 bytes per stored state in memory... |
NOVSZ | risky - removes 4 bytes from state vector - its length field. in most cases this is redundant - so when memory is tight in fullstate storage, try this mode. if the number of states stored changes when -DNOVSZ is used, the information wasn't redundant... (safety checks will still be valid, but liveness checks may then fail) NOVSZ cannot be combined with COLLAPSE |
PRINTF | enables printfs during verification runs (Version 2.8 and later -- earlier versions always left these enabled) |
RANDSTORE | when in BITSTATE mode, use for instance -DRANDSTORE=33 to reduce the probability of storing the bits in the hasharray to 33%. the value assigned must be between 0 and 99 low values increase the amount of work done (time complexity) and increase the effective coverage for large state spaces. most useful in sequential bitstate hashing runs to improve the accumulative coverage of all runs significantly |
REACH | guarantee absence of errors within the -m depth-limit (described in more detail in Newsletter 4 and in the V2.Updates notes for Version 2.2.) |
W_XPT=N | in combination with MA, write checkpoint files every multiple of N states stored |
R_XPT | in combination with MA, restart a verification run from the last checkpoint file written, can be combined with W_XPT |
$ pan (Spin Version 3.0.alpha -- 21 July 1997) + Partial Order Reduction Full statespace search for: never-claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid endstates + State-vector 32 byte, depth reached 13, errors: 0 74 states, stored 30 states, matched 104 transitions (= stored+matched) 1 atomic steps hash conflicts: 2 (resolved) (max size 2^18 states) 1.533 memory usage (Mbyte) unreached in proctype ProcA line 7, state 8, "Gaap = 4" (1 of 13 states) unreached in proctype :init: line 21, state 14, "Gaap = 3" line 21, state 14, "Gaap = 4" (1 of 19 states)This is what each line in this listing means:
(Spin Version 3.0.alpha -- 21 July 1997)Identifies the version of Spin that generated the pan.c source from which this verifier was compiled.
+ Partial Order ReductionThe plus sign means that the default partial order reduction algorithm was used. A minus sign would indicate compilation for exhaustive, non-reduced, verification with option -DNOREDUCE .
Full statespace search for:Indicates the type of search. The default is a full statespace search. Large models can also be verified with a Bitstate search, which is approximate.
never-claim - (none specified)The minus sign indicates that no never claim, or LTL fomrula was used for this run. If a never claim was part of the model, it could have been suppressed with the compiler directive -DNOCLAIM .
assertion violations +The plus indicates that the search checked for violations of user specified assertions, which is the default.
acceptance cycles - (not selected)The minus indicates that the search did not check for the presence of acceptance or non-progress cycles. To do so would require a run-time option -a or compilation with -DNP combined with the run-time option -l.
invalid endstates +The plus indicates that a check for invalid endstates was done (i.e., for absence of deadlocks).
State-vector 32 byte, depth reached 13, errors: 0The complete description of a global system state required 32 bytes of memory (per state). The longest depth-first search path contained 13 transitions from the root of the tree (i.e., from the initial system state). No errors were found in this search.
74 states, storedA total of 74 unique global system states were stored in the statespace (each represented effectively by a vector of 32 bytes).
30 states, matchedIn 30 cases did the search return to a previously visited state in the search tree.
104 transitions (= stored+matched)A total of 104 transitions were explored in the search, which can serve as a statistic for the amount of work that has been performed to complete the verification.
1 atomic stepsOne of the transitions was part of an atomic sequence, all others were outside atomic sequences.
hash conflicts: 2 (resolved)In 2 cases the default hashing scheme (a weaker version than what is used in bitstate hashing) encountered a collision, and had to place the states into a linked list in the hash-table.
(max size 2^18 states)The (perhaps default) argument that was specified for the size of the hash-table was 2^18; equivalent to a run-time option -w18.
1.533 memory usage (Mbyte)Total memory usage was 1.533 Megabytes, including the stack, the hashtable, and all related data structures. Memory use would go down for smaller than the default choices for run-time options -m and -w, which could in this case, with only 74 reachable states of 32 bytes each, considerably reduce memory use.
unreached in proctype ProcA line 7, state 8, "Gaap = 4" (1 of 13 states) unreached in proctype :init: line 21, state 14, "Gaap = 3" (1 of 19 states)A listing of the state numbers and approximate line numbers for the basic statements in the specification that were not reached. Since this is a full statespace search that ran to completion this means that these transitions are effectively unreachable (dead code).
Spin Online References Promela Manual Index Spin HomePage |
(Page Updated: 10 August 1997) |