1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
|
<html>
<body bgcolor=#ffffff>
<head>
<title>Pan Verification Options</title>
</head>
<table cols=3 width=100%>
<tr>
<td valign=top><h3>
<a href="index.html">Pan</a></h3></td>
<td valign=top align=center><h3>Verification Options</h3></td>
<td valign=top align=right><h3>Overview</h3>
</td></tr>
</table>
<p><b><tt>NAME</tt></b>
<br>
pan - <i>Spin</i> generated source for a model-specific verifier.
<p><b><tt>DESCRIPTION</tt></b>
<br>
Overview of options that are available with the verifiers
generated by <i>Spin</i> with <i>Spin</i>'s run-time
option <b>-a</b>. 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.
<ul>
<li> A - <a href="#A">Run-Time Options</a></li>
<li> B - <a href="#B">Compile-Time Options</a></li>
<li> C - <a href="#C"><i>Pan</i>'s output format</li>
</ul>
<font color=blue</font><b>
See <a href="http://www.spinroot.com/spin/multicore/V5_Readme.html">V5_Readme</a>
for options specific to multi-core verifications with version 5.0 and later.</b></font>
<h3><tt><a name="A">Run-Time Options for <i>Pan</i> </a></tt></h3>
<ul>
<li>
<b>-A</b>
<br>suppress the reporting of assertion violations (see also <b>-E</b>)
<li>
<b>-a</b>
<br>find acceptance cycles (available if compiled <i>without</i> <b>-DNP</b>)
<b>-B</b>
<br>reserved
<li>
<b>-b</b>
<br>bounded search mode, makes it an error to exceed the search depth, triggering
and error trail
<li>
<b>-C</b>
<br>
for models with embedded C code, reproduce error trail in columnated format
<li>
<b>-c</b><i>N</i>
<br>
stop at <i>N</i>th error (defaults to first error if <i>N</i> is absent)
<li>
<b>-d</b>
<br>print state tables and stop (-d -d or -d -d -d will print versions of the
state tables before additional optimizations are applied)
<li>
<b>-E</b>
<br>suppress the reporting of invalid endstate errors (see also <b>-A</b>)
<li>
<b>-e</b>
<br>create trails for all errors encountered (default is first one only)
<li>
<b>-F</b><i>filename</i>
<br>when compiled with -DSC, names the file to be used for the stack data
<li>
<b>-f</b>
<br>add weak fairness (to <b>-a</b> or <b>-l</b>)
<li>
<b>-g</b>
<br>for models with embedded C code, reproduce error trail with msc gui support
<li>
<b>-h</b><i>N</i>
<br>choose another hash-function, with <i>N</i>: 1..32 (defaults to 1)
<li>
<b>-I</b>
<br>like <b>-i</b>, but approximate and faster
<li>
<b>-i</b>
<br>search for shortest path to error (causes an increase of complexity)
<li>
<b>-J</b>
<br>reverse the evaluation order of nested unless statements (to conform
to the one used in Java)
<li>
<b>-k</b><i>N</i>
<br>set the number of hashfunctions used in bitstate hashing mode to <i>N</i>
(bitstate mode)
The default is k=2. This option was introduced in version 4.2.0.
<li>
<b>-L</b><i>N</i>
when compiled -DSCHED, sets a restriction on the max nr of context
switches to <i>N</i> (default 10). Introduced in version 5.1.5.
<li>
<b>-l</b>
<br>find non-progress cycles (requires compilation with <b>-DNP</b>)
<li>
<b>-M</b><i>N</i>
<br>use N Megabytes for bitstate hash array (bitstate mode)
<li>
<b>-G</b><i>N</i>
<br>use N Gigabytes for bitstate hash array (bitstate mode)
<li>
<b>-m</b><i>N</i>
<br>set max search depth to <i>N</i> steps (default <i>N</i>=10000)
<li>
<b>-n</b>
<br>no listing of unreached states at the end of the run
<li>
<b>-N</b> <i>n</i>
<br>if more than one LTL property or never claim is defined,
use the n-th one. Instead of <i>n</i> also the name of the
claim or the LTL property can be used. If only one claim/property
appears, or if none are used, then this option is not available.
<li>
<b>-P</b><i>N</i>
<br>for models with embedded C code, reproduce trail, but print
only steps from the process with pid <i>N</i>
<li>
<b>-Q</b><i>N</i>
<br>set time-limit on execution of N minutes (not in multicore mode)
<li>
<b>-q</b>
<br>require empty channels in valid endstates
<li>
<b>-RS</b><i>N</i>
<br>Use <i>N</i> as a seed for the random number generator.
<br>Can be used in combination with compilation directives <b>-DT_RAND</b> and <b>-DP_RAND</b>
(defined under experimental options below) to randomize the search process.
<i>N</i> can be any non-negative integer value.
<li>
<b>-r</b>, <b>-P</b>, <b>-C</b>
<br>for models with embedded C code, play back error trail (optionally followed
by the name of a trailfile, as the next argument)
<li>
<b>-r</b><i>N</i>
<br>play back error trail numbered N
<li>
<b>-r</b> <i>filename</i>
<br>play back error trail stored in filename (works also with options
<b>-C</b>, <b>-P</b><i>N</i>, <b>-g</b> and <b>-S</b>).
<li>
<b>-S</b>
<br>for models with embedded C code, replay in silent mode, printing only
the output from the user-defined printf statements in the model
<li>
<b>-s</b>
<br>use 1-bit hashing (default is 2-bit hashing, assumes compilation <b>-DBITSTATE</b>).
In version 4.2.0 and later, the option -s is equivalent to -k1.
<li>
<b>-T</b>
<br>create trail files in read-only mode (see also -x)
<li>
<b>-t</b><i>suff</i>
<br>instead of .trail use .suf on trailfiles
<li>
<b>-U</b>
<br>reserved
<li>
<b>-V</b>
<br>prints the <i>Spin</i> version number, and shows how the
pan.c was compiled, then stops.
<li>
<b>-v</b>
<br>verbose mode
<li>
<b>-W</b>
<br>reserved
<li>
<b>-w</b><i>N</i>
<br>use a hashtable of 2^<i>N</i> entries(defaults to <b>-w</b><i>23</i>
in bitstate mode and <b>-w</b><i>19</i> in exhaustive search mode)
<li>
<b>-X</b>
<br>print all stderr output onto stdout instead
<li>
<b>-x</b>
<br>do not overwrite an existing trail file
<li>
<b>-Y</b> and <b>-Z</b>
<br>reserved
<li>
<b>-z</b><i>N</i> <tt>[Version 5 and later]</tt>
<br>Set handoff depth for multi-core search to N (default is 20).
</ul>
<h3><tt><a name="B">B </a>Compile Time Options for <i>Spin</i> and <i>Pan</i></tt></h3>
The directives are grouped in eight sets, depending on
their main purpose.
<ul><ul><tt>
<li> <a href="#D0">For Compiling <i>Spin</i> itself</a>
<li> <a href="#D1">Parameters Supported by Xspin</a>
<li> <a href="#D2">Related to Partial Order Reduction</a>
<li> <a href="#D3">To Increase Speed</a>
<li> <a href="#D4">To Reduce Memory Use</a>
<li> <a href="#D5">For Use When Prompted by <i>Pan</i></a>
<li> <a href="#D6">For Debugging <i>Spin</i> Verifiers</a>
<li> <a href="#D7">For Experimental Use</a>
</tt></ul></ul>
There are four directives that can be used for
compiling the <i>Spin</i> sources itself. These should never
be needed by <i>Spin</i> users, only (once) by someone
recompiling and installing <i>Spin</i> from its sources.
<p><hr><center>
<b><tt><a name="D0">Directives for Compiling <i>Spin</i> itself</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr>
<td><tt>NXT</tt></td>
<td><tt>if defined, the NEXT operator X can be used
in LTL formulae; risky, not compatible with partial
order reductions</tt></td>
</tr><tr>
<td><tt>PC</tt></td>
<td valign=top><tt>required when compiling <i>Spin</i> on a PC</tt></td>
</tr><tr>
<td><tt>PRINTF</tt></td>
<td valign=top><tt>if defined, printf statements in the model are enabled
during the verification process (not recommended)</tt></td>
</tr><tr>
<td><tt>SOLARIS</tt></td>
<td valign=top><tt>required when compiling <i>Spin</i> on a Solaris system</tt></td>
</tr>
</table>
<p>
The next tables give optional directives for compiling
the verifiers that are generated by <i>Spin</i>. 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:
<ul><pre>
$ spin -a spec
$ cc -o pan -DNOBOUNDCHECK pan.c
</pre></ul>
Each directive modifies the default behavior of the verifier
to achieve a specific effect noted in the tables below.
<p><hr><center>
<b><tt><a name="D1">Directives Supported by <i>Xspin</i></a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>BITSTATE</tt></td>
<td><tt>use supertrace/bitstate instead of exhaustive exploration</tt></td>
</tr>
<tr><td><tt>MEMCNT=N</tt></td>
<td><tt>sets upperbound to the amount of memory that can be allocated
usage, e.g.: -DMEMCNT=20 for a maximum of 2^20 bytes.
<br>Use of MEMLIM is preferred.</tt></td>
</tr>
<tr><td><tt>MEMLIM=N</tt></td>
<td><tt>sets upperbound to the true number of Megabytes that can be
allocated; usage, e.g.: -DMEMLIM=200 for a maximum of 200 Megabytes
(meant to be a simple alternative to MEMCNT)
</tt></td>
</tr>
<tr><td><tt>NOCLAIM</tt></td>
<td><tt>exclude the never claim from the verification, if present</tt></td>
</tr>
<tr><td><tt>NOFAIR</tt></td>
<td><tt>disable the code for weak-fairness (is faster)</tt></td>
</tr>
<tr><td><tt>NOREDUCE</tt></td>
<td><tt>disables the partial order reduction algorithm</tt></td>
</tr>
<tr><td><tt>NP</tt></td>
<td><tt>enable non-progress cycle detection (option -l),
replacing option -a for acceptance cycle detection</tt></td>
</tr>
<tr><td><tt>PEG</tt></td>
<td><tt>add complexity profiling (transition counts)</tt></td>
</tr>
<tr><td><tt>SAFETY</tt></td>
<td><tt>optimize for the case where no cycle detection is needed
(faster, uses less memory, disables both -l and -a)</tt></td>
</tr>
<tr><td><tt>VAR_RANGES</tt></td>
<td><tt>compute the effective value range of variables
(restricted to the interval 0..255)</tt></td>
</tr>
<tr><td><tt>CHECK</tt>
<td><tt>generate debugging information (see also DEBUG)</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D2">Directives Related to Partial Order Reduction</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>CTL</tt></td>
<td><tt>allow only those reductions that are consistent with
branching time logics like CTL (i.e., the persistent
set contains either one or all transitions)</tt></td>
</tr>
<tr><td><tt>GLOB_ALPHA</tt></td>
<td><tt>consider process death a global action (for compatibility
with versions of Spin between 2.8.5 and 2.9.7)</tt></td>
</tr>
<tr><td><tt>NIBIS</tt></td>
<td><tt>apply a small optimization of partial order reduction
(sometimes faster, sometimes not...)</tt></td>
</tr>
<tr><td><tt>NOREDUCE</tt></td>
<td><tt>disables the partial order reduction algorithm</tt></td>
</tr>
<tr><td><tt>XUSAFE</tt></td>
<td><tt>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)</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D25">Other Main Search and Compilation Modes</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>BFS</tt></td>
<td><tt>use breadth-first, instead of depth-first search</tt></td>
</tr>
<tr><td><tt>BFS_DISK</tt></td>
<td><tt>in BFS mode, store some of the data on disk</tt></td>
</tr>
<tr><td><tt>BFS_DSK_LIMIT=N</tt></td>
<td><tt>in BFS mode, max number of states stored per diskfile, default 1 million</tt></td>
</tr>
<tr><td><tt>BFS_LIMIT=N</tt></td>
<td><tt>in BFS mode, point beyond which states move to disk, default 100,0000</tt></td>
</tr>
<tr><td><tt>CYGWIN</tt></td>
<td><tt>compile pan.c for 32-bit cygwin</tt></td>
</tr>
<tr><td><tt>WIN32</tt></td>
<td><tt>compile pan.c for 32-bit Windows</tt></td>
</tr>
<tr><td><tt>WIN64</tt></td>
<td><tt>compile pan.c for 64-bit Windows</tt></td>
</tr>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D3">Directives to Increase Speed</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>NOBOUNDCHECK</tt></td>
<td><tt>don't check array bound violations (faster)</tt></td>
</tr>
<tr><td><tt>NOCOMP</tt></td>
<td><tt>don't compress states with fullstate storage
(faster, but not compatible with liveness unless -DBITSTATE)</tt></td>
</tr>
<tr><td><tt>NOFAIR</tt></td>
<td><tt>disable the code for weak-fairness (is faster)</tt></td>
</tr>
<tr><td><tt>NOSTUTTER</tt></td>
<td><tt>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</tt></td>
</tr>
<tr><td><tt>SAFETY</tt></td>
<td><tt>optimize for the case where no cycle detection is needed
(faster, uses less memory, disables both -l and -a)</tt></td>
</tr>
<tr><td><tt>SFH<br><font color=blue>version 5</font></tt></td>
<td><tt>faster verification of safety properties, sets also NOCOMP
(faster, uses slightly more memory, disables both -l and -a)</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D4">Directives to Reduce Memory Use</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>BITSTATE</tt></td>
<td><tt>use supertrace/bitstate instead of exhaustive exploration</tt></td>
</tr>
<tr><td><tt>COLLAPSE</tt></td>
<td><tt>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)</tt></td>
</tr>
<tr><td><tt>FULL_TRAIL<br><font color=blue>version 5</font></tt></td>
<td><tt>leaving this directive out significantly reduces memory in
multi-core mode, but reduces error-trails to a suffix of the full trail
only. adding it restores the capability to generate full error trails.
<br>Only relevant in mult-core verfications; no effect elsewhere.</tt></td>
</tr>
<tr><td><tt>HC</tt></td>
<td><tt>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.</tt></td>
</tr>
<tr><td><tt>MA=N</tt></td>
<td><tt>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)</tt></td>
</tr>
<tr><td><tt>MEMCNT=N</tt></td>
<td><tt>set upperbound to the amount of memory that can be allocated
usage, e.g.: -DMEMCNT=20 for a maximum of 2^20 bytes</tt></td>
</tr>
<tr><td><tt>MEMLIM=N</tt></td>
<td><tt>set upperbound to the true number of Megabytes that can be
allocated; usage, e.g.: -DMEMLIM=200 for a maximum of 200 Megabytes
(meant to be a simple alternative to MEMCNT)</tt></td>
</tr>
<tr><td><tt>SC</tt></td>
<td><tt>enables stack cycling. this will swap parts of a very long
search stack to a diskfile during verifications. the runtime flag -m
for setting the size of the search stack still remains, but now
sets the size of the part of the stack that remains in core.
it is meant for rare applications where the search stack is many
millions of states deep and eats up the majority of the memory
requirements.</tt></td>
</tr>
<tr><td><tt>SPACE</tt></td>
<td><tt>optimize for space not speed</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D5">Directives Reserved for Use When Prompted by <i>Pan</i></a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>NFAIR=N</tt></td>
<td><tt>allocates memory for enforcing weak fairness
usage, e.g.: -DNFAIR=3 (default is 2)</tt></td>
</tr>
<tr><td><tt>VECTORSZ=N</tt></td>
<td><tt>allocates memory (in bytes) for state vector
usage, e.g.: -DVECTORSZ=2048 (default is 1024)</tt></td>
</tr>
<tr><td><tt>VMAX=N<br><font color=blue>version 5</font></tt></td>
<td><tt>allocates memory (in bytes) for state vector
queues in Multicore mode, e.g.: -DVMAX=500 (default is 256)
(Can also safely be ignored -- but optimizing the values can
increase the number of states that can be accomodated in the
handoff queues)
</tt></td>
</tr>
<tr><td><tt>PMAX=N<br><font color=blue>version 5</font></tt></td>
<td><tt>allocates memory (in bytes) for process structures inside
queues in Multicore mode, e.g.: -DPMAX=32 (default is 16)
(Can also safely be ignored -- but optimizing the values can
increase the number of states that can be accomodated in the
handoff queues)
</tt></td>
</tr>
<tr><td><tt>QMAX=N<br><font color=blue>version 5</font></tt></td>
<td><tt>allocates memory (in bytes) for chan structures inside
queues in Multicore mode, e.g.: -DQMAX=32 (default is 16)
(Can also safely be ignored -- but optimizing the values can
increase the number of states that can be accomodated in the
handoff queues)
</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D6">Directives For Debugging <i>Pan</i> Verifiers</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>CHECK</tt></td>
<td><tt>more frugal debugging printouts (see also -DVERBOSE)</tt></td>
</tr>
<tr><td><tt>SDUMP</tt></td>
<td><tt>if used in addition to CHECK: adds ascii dumps of state vectors
to verbose output (i.e., an ascii version of SVDUMP)</tt></td>
</tr>
<tr><td><tt>SVDUMP</tt></td>
<td><tt>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)</tt></td>
</tr>
<tr><td><tt>VERBOSE</tt></td>
<td><tt>adds elaborate debugging printouts (see also -DCHECK)</tt></td>
</tr>
</table>
<p><hr><center>
<b><tt><a name="D7">Directives For Experimental Use</a></tt></b>
</center><hr><p>
<table cols=2 border="2">
<tr><td><tt>ALIGNED</tt></td>
<td><tt>on some platforms, to avoid complaints from the runtime system
about unaligned data access</tt></td>
</tr>
<tr><td><tt>FREQ=N<br><font color=blue>version 5</font></tt></td>
<td><tt>changes the frequency of snapshot updates during a run
from once every 1000000 states to once every N states</tt></td>
</tr>
<tr><td><tt>HASH32</tt><br><font color=blue>version 5</font></td>
<td><tt>force the use of 32-bit hash (on 64-bit machine)</tt></td>
</tr>
<tr><td><tt>HASH64</tt><br><font color=blue>version 5</font></td>
<td><tt>force the use of 64-bit hash (on 32-bit machine)</tt></td>
</tr>
<tr><td><tt>JOINPROCS</tt></td>
<td><tt>a variant of collapse</tt></td>
</tr>
<tr><td><tt>LC</tt></td>
<td><tt>to be used in combination with BITSTATE hashing only.
it is automatically enabled when -DSC is used in BITSTATE mode.
LC forces the use of hashcompact compression for stackstates
(instead of the dedault which is full-state storage for states
while they are on the search stack, even in bitstate mode).
it slows down the search, but can save memory. it uses 4 bytes
per state (giving very low probability of collision).
</tt></td>
</tr>
<tr><td><tt>NO_FAST_C</tt><br><font color=blue>version 5</font></td>
<td><tt>supress loop unrolling in compress() function</tt></td>
</tr>
<tr><td><tt>NO_RESIZE</tt><br><font color=blue>version 5</font></td>
<td><tt>suppress automatic resize of hashtable (bitstate mode)</tt></td>
</tr>
<tr><td><tt>NOVSZ</tt></td>
<td><tt>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</tt></td>
</tr>
<tr><td><tt>NSUCC<br><font color=blue>version 5</font></tt></td>
<td><tt>computes the average fanout of states in the statespace
and prints a summary at the end of the run</tt></td>
</tr>
<tr><td><tt>ON_EXIT=fct()</tt><td>
<td><tt>optional function to call just before pan exits</tt></td>
</tr>
<tr><td><tt>P_RAND=N</tt><br><font color=blue>version 5.2.5</font></td>
<td><tt>randomize order in which processes are scheduled, using (optional) seed N
<br>the seed can also be set (or changed) with <i>pan</i> runtime option <b>-RS</b><i>N</i>
<br>the value provided can be any non-negative integer
<br>(See also T_RAND)</tt></td>
</tr>
<tr><td><tt>PRINTF</tt></td>
<td><tt>enables printfs during verification runs (Version 2.8
and later -- earlier versions always left these enabled)</tt></td>
</tr>
<tr><td><tt>PUTPID</tt><br><font color=blue>version 5.1.5</font></td>
<td><tt>include the process pid number in trailfile names</tt></td>
</tr>
<!---
<tr><td><tt>RANDOMIZE=N</tt><br><font color=blue>version 5.1.5</font></td>
<td><tt>randomize order in which transitions are explored, using (optional) seed N
<br><b>NB: replaced with T_RAND and P_RAND in version 5.2.5</b></tt></td>
</tr>
--->
<tr><td><tt>RANDSTORE</tt></td>
<td><tt>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</tt></td>
</tr>
<tr><td><tt>REACH</tt></td>
<td><tt>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.)</tt></td>
</tr>
<tr><td><tt>REVERSE</tt><br><font color=blue>version 5.1.4</font></td>
<td><tt>reverse the order in which process interleavings are explored
<br>(see also T_RAND, P_RAND, SCHED, and T_REVERSE</tt></td>
</tr>
<tr><td><tt>R_XPT</tt></td>
<td><tt>in combination with MA, restart a verification run from the
last checkpoint file written, can be combined with W_XPT</tt></td>
</tr>
<tr><td><tt>SCHED</tt><br><font color=blue>version 5.1.5</font></td>
<td><tt>restrict the maximum number of process context switches (using pan runtime option -L)</tt></td>
</tr>
<tr><td><tt>T_RAND=N</tt><br><font color=blue>version 5.2.5</font></td>
<td><tt>randomize order in which transitions are explored, using (optional) seed N
<br>the seed can also be set (or changed) with <i>pan</i> runtime option <b>-RS</b><i>N</i>
<br>the value provided can be any non-negative integer
<br>(See also P_RAND)</tt></td>
</tr>
<tr><td><tt>T_REVERSE</tt><br><font color=blue>version 5.1.5</font></td>
<td><tt>reverse order in which transitions are explored (See also T_RAND, and REVERSE)</tt></td>
</tr>
<tr><td><tt>W_XPT=N</tt></td>
<td><tt>in combination with MA, write checkpoint files every multiple
of N states stored</tt></td>
</tr>
<tr><td><tt>ZAPH</tt></td>
<td><tt>in bitstate mode, reset the hash array to empty
each time it becomes half full</tt></td>
</tr>
</table>
<h3><a name="C">C </a><i>Pan</i>'s Output Format</h3>
A typical printout of a verification run is as follows:
<ul><pre>
$ pan
<a href="#L1">(Spin Version 3.0 -- 21 July 1997)</a>
<a href="#L2">+ Partial Order Reduction</a>
<a href="#L3">Full statespace search for:</a>
<a href="#L4">never-claim - (none specified)</a>
<a href="#L5">assertion violations +</a>
<a href="#L6">acceptance cycles - (not selected)</a>
<a href="#L7">invalid endstates +</a>
<a href="#L8">State-vector 32 byte, depth reached 13, errors: 0</a>
<a href="#L9">74 states, stored</a>
<a href="#L10">30 states, matched</a>
<a href="#L11">104 transitions (= stored+matched)</a>
<a href="#L12">1 atomic steps</a>
<a href="#L13">hash conflicts: 2 (resolved)</a>
<a href="#L14">(max size 2^18 states)</a>
<a href="#L15">1.533 memory usage (Mbyte)</a>
<a href="#L16">unreached in proctype ProcA</a>
<a href="#L16">line 7, state 8, "Gaap = 4"</a>
<a href="#L16">(1 of 13 states)</a>
<a href="#L16">unreached in proctype :init:</a>
<a href="#L16">line 21, state 14, "Gaap = 3"</a>
<a href="#L16">line 21, state 14, "Gaap = 4"</a>
<a href="#L16">(1 of 19 states)</a>
</pre></ul>
This is what each line in this listing means:
<pre><i> <a name="L1">(Spin Version 3.0 -- 21 July 1997)</a>
</pre></i>
Identifies the version of <i>Spin</i> that generated the
pan.c source from which this verifier was compiled.
<pre><i> <a name="L2">+ Partial Order Reduction</a>
</pre></i>
The 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 .
<pre><i> <a name="L3">Full statespace search for:</a>
</pre></i>
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.
<pre><i> <a name="L4">never-claim</a> - (none specified)
</pre></i>
The minus sign indicates that no <b>never</b>
claim, or LTL fomrula was used for this run. If a <b>never</b>
claim was part of the model, it could have been suppressed with
the compiler directive -DNOCLAIM .
<pre><i> <a name="L5">assertion violations</a> +
</pre></i>
The plus indicates that the search checked for violations of
user specified assertions, which is the default.
<pre><i> <a name="L6">acceptance cycles</a> - (not selected)
</pre></i>
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 <b>-a</b> or compilation with -DNP
combined with the run-time option <b>-l</b>.
<pre><i> <a name="L7">invalid endstates</a> +
</pre></i>
The plus indicates that a check for invalid endstates was
done (i.e., for absence of deadlocks).
<pre><i> <a name="L8">State-vector 32 byte, depth reached 13, errors: 0</a>
</pre></i>
The 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.
<pre><i> <a name="L9">74 states, stored</a>
</pre></i>
A total of 74 unique global system states were stored in the
statespace (each represented effectively by a vector of 32 bytes).
<pre><i> <a name="L10">30 states, matched</a>
</pre></i>
In 30 cases did the search return to a previously visited state
in the search tree.
<pre><i> <a name="L11">104 transitions (= stored+matched)</a>
</pre></i>
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.
<pre><i> <a name="L12">1 atomic steps</a>
</pre></i>
One of the transitions was part of an atomic sequence, all
others were outside atomic sequences.
<pre><i> <a name="L13">hash conflicts: 2 (resolved)</a>
</pre></i>
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.
<pre><i> <a name="L14">(max size 2^18 states)</a>
</pre></i>
The (perhaps default) argument that was specified for the size
of the hash-table was 2^18; equivalent to a run-time option <b>-w18</b>.
<pre><i> <a name="L15">1.533 memory usage (Mbyte)</a>
</pre></i>
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
<b>-m</b> and <b>-w</b>,
which could in this case, with only 74 reachable states of 32
bytes each, considerably reduce memory use.
<pre><i> <a name="L16">unreached in proctype ProcA</a>
line 7, state 8, "Gaap = 4"
(1 of 13 states)
unreached in proctype :init:
line 21, state 14, "Gaap = 3"
(1 of 19 states)
</pre></i>
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).
<hr>
<table cols=3 width=100%>
<tr>
<tr>
<td valign=top>
<a href="index.html">Spin Online References</a><br>
<a href="promela.html">Promela Manual Index</a><br>
<a href="http://spinroot.com/spin/">Spin HomePage</a>
</td>
<td valign=top align=center></td>
<td valign=top align=right>
<font size="3"><b><tt>(Page Updated: 10 July 2011)</tt></font></b></td></tr>
</table>
</body>
</html>
|
