1Distribution Update History of the SPIN sources 2=============================================== 3 4==== Version 6.0 - 5 December 2010 ==== 5 6The update history since 1989: 7 8 Version 0: Jan. 1989 - Jan. 1990 5.6K lines: original book version 9 Version 1: Jan. 1990 - Jan. 1995 7.9K lines: first version on netlib 10 Version 2: Jan. 1995 - Aug. 1997 6.1K lines: partial-order reduction 11 Version 3: Aug. 1997 - Jan. 2003 17.9K lines: bdd-like compression (MA) 12 Version 4: Jan. 2003 - Oct. 2007 28.2K lines: embedded c-code, bfs 13 Version 5: Oct. 2007 - Dec. 2010 32.8K lines: multi-core & swarm support 14 Version 6: Dec. 2010 - 36.8K lines: inline ltl formula, parallel bfs 15 Version 6.5.0: 2019 - 40.1K lines 16 17==== Version 6.0.0 - 5 December 2010 ==== 18 19the main improvements in Spin version 6 are: 20 21- support for inline specification of LTL properties: 22 Instead of specifying a never claim, you can now 23 specify LTL formulae directly inside a verification model. 24 Any number of named LTL formulae can be listed and named. 25 The formulae are converted by Spin into never claims in the background, 26 and you can choose which property should be checked for any run 27 using a new pan runtime parameter pan -N name. 28 Example: 29 ltl p1 { []<>p } 30 ltl p2 { <> (a > b) implies len(q) == 0 } 31 32 There are a few additional points to note: 33 - Inline LTL properties state *positive* properties to prove, i.e., 34 they do not need to be negated to find counter-examples. 35 (Spin performs the negation automatically in the conversions.) 36 - You can use any valid Promela syntax to specify the predicates 37 (state properties). See, for instance, the use of expressions (a>b) 38 and (len(q) == 0) in the examples above. 39 So it is no longer needed to introduce macros for propositional symbols. 40 - White space is irrelevant -- you can insert newlines anywhere in an LTL block 41 (i.e., in the part of the LTL formula between the curly braces). 42 - You can use textual alternatives to all temporal and some propositional operators. 43 This includes the terms always, eventually, until, weakuntil, 44 stronguntil, implies, equivalent, and release (the V operator), 45 which are now keywords. So the first formula (p1) above could also be 46 written as: 47 ltl p1 { 48 always 49 eventually p /* maybe some comment here */ 50 } 51 52- Improved scope rules: 53 So far, there were only two levels of scope for variable 54 declarations: global or proctype local. 55 Version 6 adopts more traditional block scoping rules: 56 for instance, a variable declared inside an inline definition or inside 57 an atomic or non-atomic block now has scope that is limited to that inline or block. 58 You can revert to the old scope rules by using spin -O (the capital letter Oh) 59 60- New language constructs: 61 There are two new language constructs, that can simplify the specification 62 of common constructs: 'for' and 'select'. Both are implemented as meta- 63 terms, which means that they are translated by the parser into existing 64 language constructs (using 'do' or 'if'). 65 66 The new 'for' construct has three different uses: 67 for (i : 1 .. 9) { 68 printf("i=%d\n", i) 69 } 70 simply prints the values from 1 through 9, meaning that the body of the 71 for is repeated once for each value in the range specified. 72 int a[10]; 73 for (i in a) { 74 printf("a[%d] = %d\n", i, a[i]) 75 } 76 is a way to repeat an fragment of code once for each element in an array. 77 In the example above, the printf will be executed once for each value from 78 0 through 9 (note that this is different from the first example). 79 This works for any array, independent of its type. 80 The last use of the for is on channels. 81 typedef utype { bin b; byte c; }; 82 chan c = [10] of { utype }; 83 utype x; 84 for (x in c) { 85 printf("b=%d c=%d\n", x.b, x.c) 86 } 87 which retrieves each message in the channel and makes it available for the 88 enclosed code. In this case, the channel (c above) must have been 89 declared with a single parameter, the type of which must match the variable 90 type specified in the for statement (the name before the 'in' keyword). 91 [Note that with the introduction of the new keyword 'in' some early 92 Spin models may now have syntax errors, if 'in' is used as a variable name.) 93 94 The second new language statement is 'select' and its use is illustrated 95 by this example: 96 int i; 97 select (i : 1..10); 98 printf("%d\n", i); 99 Select non-deterministically picks a value for i out of the range that 100 is provided. 101 102- Multiple never claims: 103 Other than multiple and named inline LTL properties, you can also include 104 multiple explicit (and named) never claims in a model. The name goes after 105 the keyword 'never' and before the curly brace. 106 As with inline LTL properties, the model checker will still only use one never 107 claim to perform a verification run, but you can choose on the 108 command line of pan which claim you want to use: pan -N name 109 110- Synchronous product of claims: 111 If multiple never claims are defined, you can use spin to 112 generate a single claim which encodes the synchronous product 113 of all never claims defined, using the new option: spin -e spec.pml 114 (this should rarely be needed). 115 116- Dot support: 117 A new option for the executable pan supports the generation of 118 the state tables in the format accepted by the dot tool from 119 graphviz: pan -D 120 The older ascii format remains available as pan -d. 121 122- Standardized output: 123 All filename / linenumber references are now in a new single standard 124 format, given as filename:linenumber, which allows postprocessing 125 tools to easily hotlink such references to the source. 126 This feature is exploited by the new replacement for xspin, called ispin 127 that will also be distributed soon. 128 129Smaller changes: 130 131- bugfix for line numbers being reported incorrectly in reachability reports 132- all filename linenumber references unified as filename:linenr 133 134==== Version 6.0.1 - 16 December 2010 ==== 135 136- fixed a bug in the implementation of the new 'for' and 'select' statements 137 where the end of the range could be one larger than intended. 138- extend the implementation of the new for and select meta-statements 139 to allow expressions for the start and end value of the ranges 140- when executing on Windowns without cygwin, better treatment of filenames 141 with backslashes, avoiding that the backslash is interpreted as an 142 escape in the pan.h source 143- fix small problem in generation of pan.h, avoiding the string intialization 144 ""-"" (when what is intended is "-"). remarkably, the C compiler does not 145 complain about the first version and merrily subtracts the two addresses 146 of the constant string "" and returns a 0... 147- prevented the ltl conversion algorithm to run in verbose mode when spin -a 148 is run with a -v flag (this produced a large amount of uninteresting output) 149- also a couple of updates to the new iSpin GUI -- so that it works better 150 on smaller screens, and also displays the automata view better (by adding 151 option -o3 in the pan.c generation, so that all transitions are visible 152 in the automata displayed.) 153 154==== Version 6.1.0 - 4 May 2011 ==== 155 156- removed calls to tmpfile(), which seems to fail on some Windows 7 systems 157- made it an error to have an 'else' statement combined with an i/o statement 158 when xs or xr assertions are used to strengthen the partial order reduction. 159 the 'else' would be equivalent to an 'empty()' call, which violates the 160 xr/xs rules and could make the partial order reduction unsound 161- avoid misinterpretation of U V an X characters when part of variable names 162 used in the new style of inline specification of ltl formula 163- improved treatment of remote references, under the new scope rules 164- some support for an experimental new version of bfs, not yet enabled 165- general code cleanup 166 167==== Version 6.2.0 - 4 May 2012 ==== 168 169- added a new algorithm for parallel breadth-first search, with support for 170 the verification of both safety and at least some liveness properties 171 more detail is available at http://spinroot.com/spin/multicore/bfs.html 172 173 the main new directive to enable parallel breadth-first search mode is 174 -DBFS_PAR 175 by default the storage mode that is used is hashcompact in a fixed size 176 table (using open addressing). 177 by default verification will continue as long as possible, but it can be 178 forced to stop when the table is filled to capacity by defining 179 -DSTOP_ON_FULL 180 storage can be changed from hashcompact to full statevector storage with 181 -DNO_HC 182 (although this is not really recommended) 183 you can also use bitstate hashing instead, by compiling with 184 -DBITSTATE 185 and (independently) you can use diskstorage to save some memory, with 186 -DBFS_DISK 187 but this has the disadvantage of making the verifier run slower, defeating 188 much of the benefit of the parallel search algorithm. 189 the default maximum length of a cycle for liveness violations is set to 10 190 steps; this can be changed by defining 191 -DL_BOUND=N 192 (which is safe, but should rarely be necessary -- setting it too large 193 reduces the accuracy of the search (see the spin2012 paper)). 194 195 when no compare and swap function __sync_bool_compare_and_swap is predefined 196 (e.g. cygwin when compiling with gcc) you can define: 197 -DNO_CAS 198 199 the new -DBFS_PAR mode cannot be combined with -DBCS, -DNP, or -DMA 200 201- some new language features to support modeling priority-based embedded software 202 (more detail on this at http://spinroot.com/spin/multicore/priority.html) 203 204 a new predefined local variable in proctypes: 205 _priority holds the current priority of the executing process 206 two new predefined functions: 207 get_priority(p) returns the priority of process p (p can be an expression) 208 set_priority(p, c) sets priority of process p to c (p and c can be expressions) 209 210 the use of these priority features cannot be combined with rendezvous statements 211 and it requires compilation with -DNOREDUCE 212 213 when process priorities are used (and the new mode is not disabled with -o6 214 see below) then only the highest priority enabled process can run 215 process priorities must be in the range 1..255 216 217- inlines can now contain a return statement, but it can be used only in a 218 few simple cases to return a single integer value 219 using this feature a single inline call can now be used on the right-hand side 220 of a simple assignment statement, for example 221 x = f(a,b); # works 222 but not in other contexts where one would normally expect a value to be returned, 223 like an expression) e.g., these cases do not work: 224 if :: (a > fct()) -> # does not work 225 if :: (fct()) -> # does not work 226 x = f(a,b) + g(x) # does not work 227 the return statement, being so restricted is of limited use, may therefore 228 disappear again in future versions 229 230- a label name can now appear also without a statement following it 231 (useful, for instance, to place a label at the end of the proctype or 232 sequence without having to add a dummy skip statement) 233 234- and else statement can now appear as the only option in an if or do 235 and then evaluates to 'true' -- this can be useful in some cases with 236 machine generated models 237 238- new spin options 239 spin option -o6 reverts to the old (pre 6.2.0) rules for interpreting 240 priority annotations 241 there's also a new experimental option -pp to improve the formatting of 242 a badly formatted spin model (e.g. machine generated). it is far from perfect 243 and the option may therefore disappear again in some future version 244 245- restructed how pan.h is generated, to make sure that it does not declare any 246 objects, only prototypes, datatypes, and structures -- this makes it possible 247 to include pan.h safely in other files as well 248 249- also made separate compilation of claims and code work again (if you don't know 250 what this means, it's best that you don't learn it either... it's an obscure 251 feature that almost nobody uses) 252 253- in bitstate mode the default size of the bitarray is now 16 MB (-w27), was 1MB (-w23) 254 255- in standard mode the default hashtable size is now -w24 (up from -w19) 256 257- bug fixes 258 the clang analyzer noted that the code in dstep.c left a local array buf 259 accessible via a global pointer (NextLab) also after the function returned. 260 corrected by declaring the local array as a static structure 261 similarly, removed some dead assignments in mesg.c flagged by clang. 262 263- cleaned up the scope rule enforcement a bit, so that top level local variable 264 declarations do not get any prefix -- simplifying the remote referencing 265 only declarations in inner-blocks or inlines are now affected, and get a scope 266 unique prefix (which is hidden from the user level in almost all cases) 267 268- corrected a problem noted on the spinroot forum that one could not use a 269 break statement inside the new 'for' construct (correction in spin.y and flow.c) 270 problem was that the break target was not defined early enough in the parsing 271 272- corrected a problem where label names were affected by the new scope rules, 273 causing some confusion with remote references and jumps 274 275- made the format of spin warning messages more consistent throughout the code 276 277- better recognition of invalid transition references in guided simulation 278 (scenario replay) in guided.c 279 280- statement merging is now disabled when proctype 'provided' clauses are used 281 282- corrected problem when an conditional expression was used in an argument to an inline 283 284- corrected problem when a remote reference was used as an array index inside an inline ltl formula 285 286- corrected the makefile to allow the use of multiple cores for parallel compilation 287 (using, for instance, "make -j 8") 288 289- now preventing assignments to the predefined local variable _pid (...) 290 291- fixed treatment of <-> or "equivalent" in ltl formula -- it wasn't always recognized correctly 292 293- some more general code cleanup 294 295==== Version 6.2.1 - 14 May 2012 ==== 296 297- first bug in 6.2: the new 'select' statement was broken and triggered a 298 syntax error 'misplaced break statement' -- fixed 299 300==== Version 6.2.2 - 6 June 2012 ==== 301 302- fixed bug in handling of the new 'set_priority' call. priorities were not 303 properly restored during the depth-first search, which could lead to 304 strange verification results. 305- fixed a bug that prevented use of parallel bfs in combination with collapse 306 compression. the combination isn't really recommended, but at least it 307 shouldn't crash of course... (the recommended mode for parallel bfs is 308 the default storage mode, which ias based on hashcompact, or bitstate). 309- added missing "extern YYSTYPE yylval;" in reprosrc.c, which prevented 310 compilation in some platforms 311- added warning against the use of hidden variables when using bfs 312- excluded run statements from statement merging, to secure correctness 313 when priority tags are used 314- omitted the message type field in datapackets exchanged with other cores 315 in parallel bfs mode, in those modes where the type field can be deduced 316 from other parts of the data, to reduce memory needed for the bfs queues 317 318==== Version 6.2.3 - 24 October 2012 ==== 319 320- fixed bug when using BFS_DISK in combination with BFS_PAR 321- fixed a bug when using process priorities, added initialization for the 322 priority to make sure it is set when a priority is not explicitly defined 323- fixed code when using COLLAPSE in combination with BFS_PAR 324- added warning when replaying an error-trail for a model with embedded c-code, 325 to make sure the user knows that the c-code fragments are not executed. 326 to replay an error-trail for models with embedded c-code only the compiled 327 pan.c file can be used (e.g., by executing ./pan -C) 328- no longer pointing to /lib/cpp for preprocessing, which dates to early 329 unix system; the default is to use gcc, or plain cpp 330- renamed global vars j2, j3 and j4 in pan.c to j2_spin, j3_spin and j4_spin 331 to avoid potential name clashes with embedded c-code fragments in models 332- added hints in bfs parallel mode at end of runs if the hash-table could 333 be resized in a new run, to improve performance 334- small additional speedups in BFS_PAR mode (finetuning the wait discipline 335 when switching from one generation of states to the next) 336- changed the default max nr of cores in BFS_PAR mode from 32 to 64 337- better memory alignment in BFS_PAR mode 338- other small fixes and minor code cleanup 339 340==== Version 6.2.4 - 10 March 2013 ==== 341 342- never claims generated from inline ltl formula are now automatically 343 added when replaying an error trial (so it will no longer say 'claim 344 ignored' in those cases) 345- improved treatment of the STDIN channel on linux systems 346- changed the format of never claims to improve error-trails 347 (by using an assertion in some cases instead of a goto to 348 the end of the claim -- this also includes changing 'if' into 'do' 349 in some cases, which may affect postprocessors that rely on the 350 older format) 351- changed parser to allow constant expressions in more places where 352 earlier only numeric constants were accepted (e.g., for active [...] 353 specifying the size of a channel, and the size of an array) 354- small improvements in memory use for parallel bfs mode (BFS_PAR) 355- added a BFS_NOTRAIL mode for parallel bfs, reducing memory use if 356 no counter-example error trail is expected 357- fixed bug in the evaluation of 'enabled(pid)' during verifications 358- fixed bug in implementation of weak-fairness algorithm, which could 359 in rare causes cause a fair cycle to go unreported. 360- improved calculation of hash-factor for very large bitstate spaces 361- fix bug introduced in 6.2.3 that gave a compiler error for -DBITSTATE 362- other minor code cleanup 363 364==== Version 6.2.5 - 4 May 2013 ==== 365 366- fixed bug when priorities are used and statement merging is enabled 367 (the default) -- this could cause state updates to get out of sync, 368 leading to a possible crash of the verifier. 369- added the keyword "const" to many of the constant array declarations, 370 to reassure static analyzers that printfs would not alter the contents 371 of these arrays 372- fixed bug in verifier in handling of priority based scheduling, which 373 could lead it to erroneously get process ids wrong; fixed problems 374 with the use of priorities when used in combination with ltl properties 375 or never claims; fixed a bug that could lead to a crash due to not 376 correctly storing backup values for priorities that are modified 377 dynamically with 'set_priority()' calls 378- more small changes to appease static source code analyzers 379- increased various buffer sizes to allow the parsing of larger ltl formula 380 381==== Version 6.2.6 - 17 February 2014 ==== 382 383- corrected bug in treatment of break statements hiding in unless constructs 384- corrected treatment of priorities (example by Mirtha Line Fernandez Venero) 385- added some new predefined routines to simplify integration with modex: 386 spin_malloc, spin_join, spin_mutex_free, spin_mutex_lock, spin_mutex_unlock, 387 and spn_mutex_init (not all of these may survive future updates) 388- added a new spin option -x to directly print the transition table for a model 389 (the option parses the model, generates pan.c, compiles it, and then 390 runs it with option -d) 391- ONE_L is now defined as 1L instead of (unsigned long) 1 to avoid a double 392 expansion of unsigned long to unsigned long long caused by a macro used 393 for compilation for 64-bit windows systems 394- mildly improved error reporting 395- doubled the size of the yacc parse stack (YYMAXSTACK), to support 396 parsing larger models 397 398==== Version 6.2.7 - 2 March 2014 ==== 399 400- another fix of enforcement of priorities during verification 401- fixed a bug in treatment of -DT_RAND and -DP_RAND that could 402 lead to the analyzer hanging in some cases 403 404==== Version 6.3.0 - 4 May 2014 ==== 405 406- A new minor version number because the Promela syntax rules changed. 407 A semi-colon at the end of the line is now optional. 408 this is implemented by having the lexical analyzer insert the 409 semi-colons automatically if they are missing. 410 Almost all models will still parse correctly, but the change can in 411 a few cases cause older models to trigger a syntax error if a 412 statement seperator is assumed in an unsuspected place, e.g., in the 413 middle of a multi-line expression. Avoid it by making sure a 414 multi-line boolean expression is always enclosed in round braces, 415 or by having the last token on a line be an operator. 416 For instance, these expressions will parse correctly: 417 if 418 :: (a 419 && b) -> ... 420 :: a && 421 b -> ... 422 fi 423 but these do not: 424 if 425 :: (a) // parser cannot see that the expression is incomplete 426 && (b) -> ... 427 :: a // same here 428 && b -> ... 429 fi 430 To revert to the old syntax rules, use spin option -o7 431 432- added 5 new options: 433 -run compile and run, verify safety properties 434 # Note the next four have been replaced in later versions, see 6.4.0 435 -runA compile and run, find acceptance cycles 436 -runAF compile and run, find weakly-fair acceptance cycles 437 -runNP compile and run, find non-progress cycles 438 -runNPF compile and run, find weakly-fair non-progress cycles 439 for instance: 440 spin -runA leader.pml 441 442- spin option -M changed: 443 replaced ps_msc.c with msc_tcl.c and with it changed the spin -M 444 option from generating scenarios in Postscript to generating them 445 as TclTk output. the new version of iSpin makes use of this as well. 446 By default the maximum length of the scenario generated is 1024 447 (equivalent to an option -u1024). To change it to a different 448 value, use the -u option (e.g., spin -u2048 -M leader.pml). 449 450- when using randomized searches (T_RAND, P_RAND, or RANDOMIZE, or pan_rand()) 451 the seed for the random number generator now also depends on the choice of -h 452 (i.e., the seed will change if you change the hashfunction used with ./pan -h) 453 454- added more support for verification of models extracted by Modex from 455 C code with pthread library calls embedded. 456 457- simplified the directory structure of the distribution somewhat by 458 combining all examples Spin models in a single directory Examples, 459 with subdirectories for specific subsets: LTL, Exercises, Book_1991 460 (the old subdirectories Samples, Test, and iSpin/ltl_examples are now gone) 461 462- bug fixes: 463 - another bug fix in treatment of priorities in verification runs 464 the priority tag in active proctype declarations was erroneously ignored 465 - fixed the accuracy of reporting the cycle-point in liveness errors 466 discovered in a breadth-first search with the piggyback algorithm 467 (courtesy Ioannis Filippidis, 4/2014) 468 - restored original settings for the piggyback algorithm, which restored 469 much of the cycle finding capabilities that were lost after version 6.2.2 470 - improved parser so that it can continue after the first syntax error 471 - improved accuracy of line numbers in traces (courtesy Akira Tanaka, 3/2014) 472 - prevented some compilation errors for unusual combinations of directives 473 - removed some warnings for printf statements with the wrong qualifiers 474 (e.g., %d for a long int, which should be %ld, etc.) 475 476==== Version 6.3.1 - 11 May 2014 ==== 477 478- big improvement in the handling of the new -run parameter to Spin 479 that will make it much easier to work with Spin. 480 all new functionality is now supported by the -run parameter alone, 481 so these four experimental options from 6.3.0 are no longer needed: 482 -runA,-runAF, -runNP, -runNPF 483 in the new setup, a -run parameter can be followed by any additional 484 settings and options that should be passed to either the compiler 485 (for compiling pan.c) or the ./pan verifier itself as runtime options. 486 the rule is that all parameters that preceed a -run argument are 487 interpreted by Spin itself for parsing the model; all parameters that 488 follow a -run parameter are passed down to compiler or verifier 489 for instance, to get the equivalent of -runNPF from 6.3.0, you can 490 now say: 491 spin -run -DNP -l -f spec.pml 492 to get an immediate run searching for weakly fair non-progress cycles 493 similarly, to optimize the compilation and reduce the run to a depth 494 of 3000 step, you would say: 495 spin -run -O2 -DNP -l -f -m3000 spec.pml 496 with this new setup you should in principle never have to compile 497 the pan.c source files manually, or invoke the verification manually. 498 if you want to redefine a macro used in the Spin model itself, you 499 can still pass that new definition directly to spin, by placing it 500 before the -run parameter, for instance: 501 spin -DMAX=24 -run -O2 -DNP -l -f -m3000 spec.pml 502 (assuming that macro MAX is used inside spec.pml) 503 504- new exercises and tutorials to match these changes in 505 http://spinroot.com/spin/Man/1_Exercises.html 506 http://spinroot.com/spin/Man/3_SpinGUI.html 507 http://spinroot.com/spin/Man/4_SpinVerification.html 508 509- bug fixes: 510 - in simulations, dynamically changing process priorities did not always 511 work correctly. now fixed 512 - additional corrections to the line number reporting in simulations 513 514==== Version 6.3.2 - 17 May 2014 ==== 515 516- this update makes all new spin options work correctly, 517 and can be compiled cleanly, on Linux, Windows PCs, and 518 Mac's, and it supports all new Modex options for direct 519 verification of C source code (http://spinroot.com/modex) 520 521- other updates and fixes: 522 - assigning to the reserved predefined variables (_last, 523 _p, _pid, _nr_qs, _nr_pr) is now intercepted correctly 524 - assigning to _priority now works correctly also in simulations 525 526- new features: 527 - you can now initialize an array of integers with a list 528 in proctypes, and in global declarations (but not yet 529 if the array is declared inside an inline definition) 530 for instance: int a[4] = { 3, 1, 4, 1 } 531 all initialization values must be constants 532 - parser improved so that it can allow the use of variables 533 or channels named 'in' -- without causing a conflict with 534 the token 'in' from for-statements 535 - process priorities now work in simulation the same as in 536 verification -- you can revert to the old behavior with -o7 537 538- for this version added a Mac executable to the distribution 539 (no guarantees that future versions will also have this though) 540 541==== Version 6.4.0 - 19 September 2014 ==== 542 543- main new features: 544 545 - new ./pan runtime option flag -hash to randomly generate a hash polynomial, 546 for instance to separate multiple runs with bitstate hashing better. 547 the seed for the random number generator determines what polynomial 548 is going to be generated (same seed means same polynomial). the seed 549 can be changed with ./pan option -RSn where n is any positive integer 550 e.g., obtained from a Unix/Linux system call 'rand.' 551 for instance ./pan -RS`rand` -hash # using backquotes around rand 552 553 - extended the number of features that is supported in combination with 554 the new spin runtime options that were introduced in 6.3.0 555 four main types of spin (not pan) options are now supported: 556 557 spin [..options1..] -run [..options2..] modelname.pml 558 spin [..options1..] -replay [..options2..] modelname.pml 559 spin [..options1..] -biterate [..options2..] modelname.pml 560 spin [..options1..] -swarmN,M [..options2..] modelname.pml 561 562 other parse-time (options1) or runtime (options2) options can be 563 passed along as shown above, and as explained below: 564 565 o parse-time options are placed *before* the mode flag (-run, -replay, etc.) 566 567 o compile-time and run-time options are placed *after* the mode flag. 568 this can include compiler directives to be used to compile pan.c 569 (which happens in the background), or to execute the resulting ./pan 570 executable (which now also happens automatically). 571 572 note 1: when you use this command: 573 spin -DX=2 -m -run -DSAFETY -m100 modelname 574 compiler directive -DX=2 is used in the preprocessing of the model, and 575 compiler directive -DSAFETY is used to compile the resulting pan.c. 576 and further, the first -m argument is interpreted by spin, and the 577 second -m100 argument is interpreted by ./pan 578 579 note 2: the new options make use of gcc, which is assumed to be 580 installed on your system, so on Windows systems this is unlikely 581 to work unless you also have cygwin with gcc installed. you can 582 change the compiler to be used by compiling the spin sources with 583 a different choice for -DCPP (e.g., "-DCPP=clang -E -x c" might work) 584 when using the new options on a Windows system with gcc may also 585 doom you to 32-bit pan executables, which will limit the size of 586 memory you can allocate for a search to 2GB. using linux is recommended. 587 588 explanation of the use of the spin -replay option: 589 this option can be used to replay an existing error trail-file 590 (e.g., found with an earlier spin -run) 591 if the model contains embedded c-code, the ./pan executable is used 592 for the replay; otherwise spin itself is used for the replay. 593 note that ./pan recognizes different runtime options than spin itself 594 so it can matter which of these two cases applies for [..options2..] 595 you can of course always still fall back on the old 596 spin -t -p modelname.pml 597 method for models withnout embedded C code, or the ./pan -r method for 598 models with embedded C code. 599 600 explanation of the use of the spin -run option: 601 a synonym of this option is -search -- it behaves identical to -run. 602 this option is used to generate a verifier (pan.c), compile it, and 603 execute it run, all without further user intervention. 604 new options that can be used in the [..options2..] part include: 605 -bfs to perform a breadth-first search 606 -bfspar to perform a parallel breadth-first search 607 -bcs to use the bounded-context-switching algorithm 608 -bitstate or -bit, to use bitstate storage 609 -link file.c to link the pan.c to file.c in the compilation 610 -collapse to use collapse state compression 611 -hc to use hashcompact storage 612 -noclaim to ignore all ltl and never claims 613 -p_permute to use process scheduling order permutation 614 -p_rotateN to use process scheduling order rotation by N (default 0) 615 -p_reverse to use process scheduling order reversal 616 -ltl p to verify the ltl property named p 617 -safety to compile for safety properties only (default is liveness+safety) 618 -i to use the dfs iterative shortening algorithm 619 -a to search for acceptance cycles (and compile correspondingly) 620 -l to search for non-progress cycles (and compile correspondingly) 621 622 explanation of the use of the new spin -biterate option: 623 uses bitstate compilation plus iterative search refinement for the 624 execution of ./pan with hashtable size increasing step by step 625 from -w18 upto -w35 -- until an error is found. 626 this performs 18 runs sequentially, with the first runs executing 627 very fast -- thus making it likely that errors are found very quickly 628 each new run increases precision and runtime, until the max is reached 629 630 explanation of the use of the new spin -swarmN,M option: 631 the most advanced new search mode -- only for use on larger multi-core 632 systems (e.g., 16 cores and up). 633 this option performs N runs in parallel and increments -w every M runs 634 for each run performed several other parameters are also randomized 635 (e.g., the hash function used, process scheduling decisions, transition 636 ordering, etc. similar to what the swarm preprocessor would do) 637 638 the default value for N is 10, and the default for M is 1 639 640 the swarm option makes use of a new compiler directive for pan.c files 641 called -DPERMUTED that allows for more extensive options for process 642 scheduling randomization (p_rotate, p_reverse, and p_permute, see below) 643 644 spin -swarmN,M will use the following compilation directives and 645 runtime parameters (most of this is meant to be internal to Spin, 646 but listed here for completeness as background information). 647 (the new options below are probably not too useful when used separately) 648 649 swarm compilation adds: 650 -DBITSTATE -DPUTPID and -DPERMUTED (a new directive, see below) 651 -DSAFETY unless there is also -a or -l parameter in [..options2..] 652 -DNOFAIR unless there is a -f parameter or there is no -a or -l 653 654 runtime flags used (with randomized arguments): 655 -w18 unless there already is a -w argument, then use that as starting point 656 -i_reverse envoked on some of the runs, to change initialization orders of processes 657 -t_reverse envoked on some of the runs, to reverse transition orders 658 unless -DT_RAND or -DT_REVERSE are defined 659 -h0 unless there already is a -hN argument, then use that as starting point 660 or if the user specified -hash, then do not use -h 661 -k1 unless there already is a -k argument, then use that as starting point 662 -p_rotate0 unless there already is a different -p_rotateN argument, 663 unless there is a -p_permute argument, then do not use 664 -RSn using internal choice for n, overrides a user-defined argument 665 -a unless there is already a -a or -l argument 666 or there is a -DNOCLAIM directive 667 or there are no accept-state labels in the model or ltl formula 668 669 the swarm option varies these parameters across all parallel runs: 670 -w every Nth iteration (from -swarmN,M): 18..35 671 -h every run 0..499 (unless the user defined -hash) 672 -p_rotate every run 0..255 (unless suppressed by p_normal or p_reverse) 673 -k every run 1..3 674 -T every run 0..1 675 -P every run 0..3 676 -RSn every run 677 -p_reverse is enabled on every 5th run, but overriden by -P0/1 678 in half the cases (overrides p_rotate if selected) 679 -p_normal to revert to normal process scheduling at least once ever 6 runs 680 681 the new -DPERMUTED directive enables a set of new runtime options to pan 682 that support how the process scheduling selecting can be modified during the search: 683 684 -p_permute -- to randomly permute the processes (the default) 685 -p_rotate -- to rotate the process ready queue 1 slot 686 -p_rotateN -- to rotate the process ready queue N slots 687 (using -p_rotate0 will have no effect of course) 688 -p_reverse -- to reverse order for all processes 689 -p_normal -- perform process scheduling as if -DPERMUTED was not defined 690 691 if more than one of these options is used, the last one wins. 692 if -DPERMUTED is defined and none of these flags are used 693 the default process scheduling order is -p_permute 694 note that using -DPERMUTED adds overhead and slows down a search, which is only 695 reasonable when used in combination with the swarm randomizations 696 697- two additional pan runtime options were added that can affect process 698 scheduling and transition selection orders: 699 -i_reverse -- reverse the initialization order of all processes declared 'active' 700 -t_reverse -- reverse the order of transition selections 701 702- other smaller additions: 703 - extended the number of builtin hash-polynomials (selected via -hN) from 32 to 100 704 - can now place ltl formula anywhere in a Promela file -- it does not need 705 to appear after all symbols that are referenced in the formula have been 706 declared (the parser will now always defer processing until the entire 707 specification has been parsed) 708 - added a quick sanity check to parsing of ltl formula, to catch some common mistakes. 709 710- some fixes: 711 - removed some false warnings about duplicate label declarations 712 - added -std=gnu99 to calls to the gcc compiler an preprocessor 713 to make sure that // comments in Promela specifications are recognized 714 - removed pc_zpp.c -- the builtin preprocessor used when compiled with -DPC 715 the original reason for adding this was to avoid a command window 716 from flashing on the screen when an external preprocessor was 717 called from within xspin. that problem no longer seems to exist, and 718 so this restricted version of the preprocessor is no longer needed 719 - small improvements in typechecking in receive statements 720 - improved the look of message sequence charts generated with spin -M 721 - fewer compiler warnings when using models with priorities 722 - deprecated flag ./pan -s now removed (sam as ./pan -k1) 723 - fixed bug in implementation of bounded context switching code (-DBCS) 724 that could cause states to be restored incorrectly 725 - removed the mapping of type long to long long on windows pcs (-DPC) 726 - improved parsing for very large models, saving about 20% of cpu-time, 727 by switching from unsorted to sorted linked lists in a few places 728 - a few more bug fixes in the implementation of support for dynamically 729 changing priorities 730 - fixed a bug in replay of error trails for ltl formula, for models where 731 multiple formula are used, to make sure that the formula are parsed 732 in the same way for verification and for replay. 733 734- new or renamed compilation directives 735 - -DREVERSE (gone) to reverse process selection order is renamed to 736 -DP_REVERSE to make it more symmetric with the older 737 -DT_REVERSE used to reverse the transition selection order 738 - the new directive -DPERMUTED overrides -DP_REVERSE if both are used 739 740==== Version 6.4.1 - 5 October 2014 ==== 741 742- two small fixes to 6.4.0 743 - the new -run -biterate options wasn't working correctly 744 745 - on windows32 and windows64 versions, suppressed logos from gcc 746 and improved method for detecting whether gcc.exe is a symbolic 747 link or not 748 749==== Version 6.4.2 - 8 October 2014 ==== 750 751- restored the correct behavior for a standalone -run argument 752 (i.e., without -swarm or -biterate), which should perform a single 753 compilation and execution of the ./pan verifier 754- less chatter on stdout for executed background commands 755 (you can restore this by adding -v or -w -- if you use -w the 756 commands generated for -biterate or -swarm are shown, but not 757 executed) 758 759==== Version 6.4.3 - 16 December 2014 ==== 760 761- added definition of tas() function for powerpc64, courtesy of srirajpaul (Rice CAF group) 762- corrected parsing unsigned int variables in c_state declarations 763- allow use of a variable name in an array bound, provided that variable 764 is an initialized scalar - generats a warning when this is used 765- made sure ltl formula are parsed the same way on replay of an error 766 trail as when generating a verifier 767- improved matching of labels if the same labelname is used in multiple scopes 768 (e.g., different inlines) 769- fewer issues with WindowsPC compiled versions 770- the label "accept_all" in neverclaims is no longer treated as an indication 771 of a check that requires cycle detection 772- presence of -bfs will now preclude addition of -a flag in auto-generated runs 773- fixed limit that was set too short when reproducing an MSC from an error-trail 774 with spin option -M 775- small improvement in replays of error-trails with ./pan -r 776- improved support for Modex generated models 777- now handles select statements in preprocessor (spinlex.c) rather than in the 778 grammar -- replaces it with a true non-deterministic choice for relatively 779 small ranges (1..32 entries), rather than a non-deterministically terminated 780 do-loop, for simpler error trails 781- fixed some minor type inaccuracies 782 783==== Version 6.4.4 - 1 November 2015 ==== 784 785- when compiletime option -DNP is defined after a -run flag, the runtime 786 option -l is now added, if missing. 787- removed the dummy definition of yywrap() 788- added make32 for 32-bit linux builds (make -f make32) 789- improved printing of mtype values in trace replay with pan 790- improved support for cond_wait, cond_signal, and mutex_init 791 for models extracted by modex (not meant to be called directly) 792- improved replay of error traces when -DPERMUTED is used 793- improved verbose output for -DPERMUTED options 794- added 64-bit murmurhash function as an alternative on 64-bit systems 795 it is enabled by compiling pan.c with an additional -DMURMUR directive 796- replaced call srandom() with srand() and replaced random() with rand() 797- added p_randrot to the set of options supported by -DPERMUTED for 798 rotating the process scheduling list by a random amount (see 6.4.0) 799- added a runtime option (for pan.c) called -rhash to generated a 800 random hash-polynomial for the run (as determined by the seed for the 801 random number generator, which can be changed with runtime option -RSnnn) 802 if no seed is selected with -RS, then time is used to seed the random 803 number generator. Compile pan.c with -DRHASH to enable this option. 804 If -DRHASH is defined it will also enable directive -DPERMUTED. 805 see VMCAI2016 paper for examples of its use in cloud / swarm verification. 806- removed the warning "this search is more efficient if compiled with -DSAFETY" 807- improved spin replay of error-traces for models using process priorities 808 together with ltl properties or never claims 809- added support for using c_expr inside ltl formula 810- made select ( name : constant .. constant-expression ) work again, 811 e.g. so that you can again say: select (i : 0 .. N-1) 812- other minor fixes and improvements throughout 813 814==== Version 6.4.5 - 1 January 2016 ==== 815 816- The first version of Spin that is released under a standard 817 BSD 3-Clause open source license. This was possible thanks to 818 the transfer of the copyright on all Spin sources from 819 Alcatel-Lucent (the successor to AT&T in ownership of Bell Labs), 820 to me on 30 December 2015. This release also comes 25 years 821 after the very first source release of Version 1.0 in Jan. 1991. 822 Since the license is now standard, and no longer Lucent specific, 823 the Spin sources and executables are now more easily packaged 824 for distribution in other open source systems, e.g., Ubuntu. 825 826- other minor updates, e.g. to remove a sanity check that caused 827 inline ltl formulae like ltl { true U (true U true) } to 828 be flagged as incorrect, and the correction of an incorrectly 829 bracketed expression in function spin_cond_wait, which is 830 used by the modex model extractor. 831 832==== Version 6.4.6 - 2 December 2016 ==== 833 834- fixed bug in treatment of select() statement, when used inside 835 and inline definition. 836- made it an error to use 'run' to initialize a variable inside 837 a declaration. 838- small fixes in d_step.c, run.c, pangen2,c, and main.c (missing 839 parentheses around subexpressions with a binary operators). 840- small improvements in the makefile 841- fix in mesg.c to allow recv poll operators on rhs of 842 assignments (erroneously flagged before as a side-effect) 843- prefixed some more generated variables in pan.c to 844 avoid name-clashes (_nstates, _endstateN, _startN) 845- prevented possible compiler warnings on definition of 846 a recently added function spin_join() 847- added new function mutex_destroy to support modex 848 conversions from C to Promela 849- fixed typo in BFS_PAR print statement (Seperate->Separate) 850- fixed flaw in generation of BFS_PAR code, preventing 851 compiler warnings 852- made hash function inside sym.c return an unsigned int 853 854==== Version 6.4.7 - 19 August 2017 ==== 855 856- fixed a bug in the parsing of for (...) statements if 857 initialized variable declarations appear in the body of the loop 858- optimization in interpreting the swarm option, by avoiding 859 unnecessary recompilations, plus other small fixes in the 860 generation of parameter values for -k and -w with swarms 861- added runtime option -W to suppress recompilation of pan if 862 the executable already exists 863- fixed bug in printing the value of a random seed at the end of 864 a randomized run 865- added compilation warning if both -DNP and -DNOCLAIM are used 866 (in that case -DNP is assumed to override -DNOCLAIM) 867- fixed a bug in the parsing of select (...) statements that could 868 cause unwarranted syntax errors when larger ranges are used 869- switched to executables for Windows PCs that do not require 870 a cygwin installation (using mingw32 and mingw64 bit compilations) 871 872==== Version 6.4.8 - 2 March 2018 ==== 873 874- fixed bug in 6.4.7 that prevented spin -run from working correctly. 875- improved explanation of spin swarm options 876- added -noreduce option to work with -run (same as -DNOREDUCE) 877- added -dfspar option to work with -run (same as -DNCORE=4) 878- added -np option to work with -run (same as -DNP) 879- extended -biterate option to -biterateN,M (similar to -swarmN,M) 880- added -rhash option to work with -run (-DPERMUTED, enables random 881 selection of process scheduling randomization) 882- added -W option to work with -run, to prevent recompilation of ./pan 883- cleaned up makefile a bit 884- added support of named mtype declarations 885 (see new mtype manual page online); backward compatible with use of 886 unnamed mtypes as before 887- fixed small problems with -DNP is used and also erroneously -DNOCLAIM 888- improved error reporting, eliminated some more compiler warnings on pan.c 889 890==== Version 6.4.9 - 17 December 2018 ==== 891 892- fixed bug where on replay of a trail with -l option the local variable 893 values were not included in the final state listings 894- on Windows systems, redirect error output from gcc test better 895- now correctly turning off statement merging when remote variables are used 896- changed internal variable name 'this' into '_this' to prevent name conflicts 897 when linking to C++ code 898- added warning that liveness checking with both -DMA and partial order 899 reduction enabled can lead to incompleteness 900- added compiler directive INIT_STATE for pan.c that calls a new routine 901 called init_state(now) in pangen3.h to perform the initializations. 902 this routine can now also be called from within embedded code, if needed. 903- other more cosmetic small changes to prevent compiler warnings 904- improved treatment of missing semi-colons slightly 905- corrected an (unlikely) initialization problem for local variables in inlines 906 907 908==== Version 6.5.0 -- 1 July 2019 ==== 909 910- source code distribution of Spin and a couple of related tools 911 moved to GitHub (www.github.com/nimble-code) 912- the lgtm scans of the Spin sources on github prompted some more 913 code cleanup efforts, to get closer to a squeaky clean scan. 914 some of the lgtm/semmle alerts are cosmetic, e.g., warning 915 about short global variable names like 'run' or 'rdy'. in 916 6.5.0 many of these are replaced with longer names. these small 917 cosmetic changes have touched many files. 918- some further standardazation of the makefile (courtesy Tom Lee) 919- you can now install spin on Debian/Ubuntu systems with a straight 920 apt-get update; apt-get install spin (also courtesy Tom Lee) 921- update to make it possible to convert arbitrary length ltl formula 922 (i.e., long texts of the formula -- but complex formula could of course 923 still require too much computation to convert efficiently) 924- better use of quotes in preprocessing command 925- corrected scope issue found by coverity 926- increased sizes of some buffers to avoid overflow 927- removed a check that prevented mtype definitions on structure elements 928- removed unused variables and unused labels 929- made the count for errors an insigned long, instead of signed int 930- moved a few more extern declarations to the top of each file 931