+++ /dev/null
-Distribution Update History of the SPIN sources
-===============================================
-
-==== Version 4.0.0 - 1 January 2003 ====
-
-See the end of the V3.Updates file for the main changes
-between the last version 3.5.3 and version 4.0.0.
-A glimpse of the Spin update history since 1989:
-
- Version 0: Jan. 1989 - Jan. 1990 5.6K lines: book version
- Version 1: Jan. 1990 - Jan. 1995 7.9K lines: first version on netlib
- Version 2: Jan. 1995 - Aug. 1997 6.1K lines: partial-order reduction
- Version 3: Aug. 1997 - Jan. 2003 17.9K lines: bdd-like compression (MA)
- Version 4: Jan. 2003 - 28.2K lines: embedded c-code, bfs
-
-==== Version 4.0.1 - 7 January 2003 ====
-
-- the rule that one cannot combine a run operator
- in an expression with any other type of boolean
- or arithmetic operator within the same expression
- is now enforced.
-- bfs now produces the usual stats upon finding
- and error; and it now supports the -e option.
-- extended bfs to deal also with safety properties
- specified in never claims and trace assertions.
- unlike the regular dfs search, the bfs search cannot
- handle the use of atomic sequences inside never claims.
- it will issue a warning, and will abort, if it sees this.
- unless constructs, d_steps, etc. should all work also
- within never claims
- a warning is issued if accept labels are found inside
- the never claim (to warn that the bfs search is restricted
- to safety properties only).
- the never claim does always work to restrict the search
- space to the part that is covered by the claim.
-- fixed bug in simulation mode, where atomicity was not
- always correctly preserved across rv actions from one
- atomic chain to another (if the sender action was the
- last statement in an atomic sequence) reported by Judi Romijn.
-- added the BFS option also in the advanced verification
- options panel of xspin401.tcl
-
-==== Version 4.0.2 - 6 March 2003 ====
-
-- removed a long-standing bug in the marking of transitions
- for partial order reduction:
- the guard statement of an atomic or d_step sequence within
- which a non-atomic,atomic,or d_step sequence is nested did
- not always get the proper tag
- if the tag assigned was local and it should have been global,
- the p.o. reduction algorithm could make an invalid reduction.
- such a case can indirectly be constructed if an atomic sequence
- contains an call of an inline function as the first statement.
- (this case was found by Bram de Wachter)
-- removed reliance on tmpnam() in main.c -- gcc complains about
- it allowing a race condition on the use of the name returned.
- we now use fixed local names for the temporary files.
- there could be a problem now if two users run spin within the
- same directory simultaneously -- but that problem already
- exists with xspin as well (pan.tmp and pan.pre) and is
- easily avoided. (if needed, we could add a locking mechanism
- at some point, but this seems overkill for the time being.)
-- the -m option now works the same in breadth-first search as it
- does in depth-first search. there's less of a strict reason
- to cutoff the search at the -m depth with bfs, since the
- stack is not pre-allocated in this case; it grows dynamically.
- by setting -m to a very large number, one can therefore just
- let the verifier proceed until it exhausts memory, or finishes
- (that is to recreate the earlier behavior when needed).
-- increased the size of some internal arrays a bit to better
- accomodate the use of very long identifier or structure names.
-- much improved rule for creating and locating error trail files:
- if possible, the trail file is created by appending .trail
- to the filename of the source model
- some older operating systems don't like it if the filename
- for the source model already contains a period, so if a
- failure is detect, a second attempt is now made by stripping
- the existing . extesion (e.g., .pml) and replacing it with
- .trail (some os's also truncate this to .tra, which is also
- accepted).
-
-==== Version 4.0.3 - 3 April 2003 ====
-
-- no verbose steps printed for never claim in guided simulations
- unless -v is given as a commandline argument
- state changes in the never claim are still printed, but with
- the already existing separate output ("Never claim moves to...")
-- new spin command-line option -I, to reproduce a version of the
- specification after preprocessing and inlining operations are
- done. the reproduced code is not complete: declarations and
- process parameters are skipped, some internally generated labels
- and jumps (e.g., replacing break statements) also become visible.
- the version is intended only to show what the effect of inlining
- and preprocessing is.
-- change in sched.c to suppres printing of final value of variables
- marked 'show' -- this looks like an assignment, which is confusing.
-- small fixes in xspin, which is now xspin402.tcl
-- in guided simulation mode, when a claim from an ltl property is
- present, the simulator's pid nrs did not always agree with the
- verifiers numbers -- this could lead to the wrong name for a
- process being printed in the simulation trails.
-
-==== Version 4.0.4 - 12 April 2003 ====
-
-- there was a bug in 4.0.3 that prevented successful compilation
- of pan.c (and unbalanced endif, caused by a missing newline
- character in pangen1.h on line 3207)
-- there was a maximum of 128 variables that could be changed per
- atomic sequence, this is now 512.
-
-==== Version 4.0.5 - 29 May 2003 ====
-
-- correction in the reporting of process id's during guided simulation.
- the numbers could be off by one when never claims are used.
- (just a reporting problem, the run itself was always correct)
-- increased bounds on the length of strings passed as preprocessor
- commands
-- explicit cast of return value ot strlen to int, to keep compilers
- happier
-- fixed subtle bug in the fairness option (reported by Dragan
- Bosnacki). with fairness enabled, standard claim stutter could
- in special cases cause a false acceptance cycle to be reported
- (i.e., a cycle not containing an accepting state).
- for compatibility, the old behavior can still be obtained by
- compiling the pan.c verifiers with -DOLDFAIR. the default is
- the fixed algorithm.
-- restricted the maximum length of a string in the lookup table
- for c_code segments to 1024 characters. this table is only used
- to print out the code segment in error traces -- so the truncation
- is cosmetic, not functional. it avoids compiler complaints about
- excessively long strings though (which could prevent compilation).
-- improved error reporting when a value outside the range of the
- target data type is passed as an parameter in a run statement
-
-==== Version 4.0.6 - 29 May 2003 ====
-
-- the fix of the fairness option wasn't quite right.
- directive -DOLDFAIR is gone again, and the real fix
- is now in place.
-
-==== Version 4.0.7 - 1 August 2003 ====
-
-.------------------------------------------------------.
-| Version 4.0.7 is the version of Spin that is |
-| described in the Spin book (Addison-Wesley 2003) |
-| and that is used for all examples there |
-| http://spinroot.com/spin/Doc/Book_extras/index.html |
-.------------------------------------------------------.
-
-- added (really restored) code for allowing separate
- compilation of pan.c for model and claim
- two new (previously undisclosed) commandline
- options -S1 and -S2 -- usage documented in the new book
-
-- if it is detected that a c_expr statement definitely has
- side effects, this now triggers a fatal error.
-
-- complains about more than 255 active processes
- being declared in active prefix
-
-- fix in -A option: removed bug in handling of eval()
-
-- cosmetic changes:
- endstate and end-state are now spelled 'end state' as
- preferred by Websters dictionary (...)
- hash-array, hash-table, and never-claim similarly
- are now spelled without hyphens
-
-- improved error replay for models with embedded c code
-
-- the -m option is no longer automatically set in guided
- simulation runs.
-
-- change spin.h to allow it to be included twice without
- ill effects (happens in y.tab.c, generated from spin.y)
-
-- updated the make_gcc file for newer versions if cygwin
-
-==== Version 4.1.0 - 4 December 2003 ====
-
-- new spin option -h, when used it will print out the
- seed number that was used for the random number
- generator at the end of a simulation run -- useful
- when you have to reproduce a run precisely, but forgot
- to set an explicit seed value with option -n
-
-- c_track now has an optional extra argument, to be
- documented - the extra qualifier cannot be used with BFS
- (spin.h, spin.y, spinlex.c, pangen4.c, ...)
-
-- the documentation (book p. 41) says that unsigned data
- can use a width specifier up to 32 bits -- it actually
- only worked up to 31 bits. it now works as advertised.
- fix courtesy of Doug McIlroy. (vars.c)
-
-- when trying to compile a model without initialized
- channels, a confusing compiler error would result.
- now avoided (spin.y, pangen1.c)
-
-- there is no longer a default maximum memory arena
- on verifications, that would apply in the absence of
- an explicit -DMEMCNT or -DMEMLIM setting (the default
- was 256 Mb).
-
-- some more fixes to account for 64bit machines, courtesy
- of C. Scott Ananian.
-
-- from Dominik Brettnacher, some instructions on compiling Spin
- on a Mac under OS X, added to the installation README.html
- file.
-
-- so far you could not use a -w parameter larger than
- 31 during bitstate search -- this effectively limited
- the max bitarray to about 512Mb. the max is now -w32
- which extends this to 1Gb (i.e., 4 10^9 bits).
- (really should be allowed to go higher, but wordsize
- gets in the way for now.)
-
-- suppressed a redundant 'transition failed' message
- that could occur during guided simulations (guided.c)
-
-- fixed a long standing bug that could show up if the last
- element of an atomic sequence was itself a sub-sequence
- (e.g., defined as an inline or as an unless stmnt).
- in those cases, atomicity could be lost before the
- last statement (sequence) completed. (flow.c)
-
-- fixed two long standing bugs in parsing of
- nested unless structures. the bug showed up in
- a double nested unless that is itself embedded in a
- non-atomic block. symptom was that some code became
- unreachable (thanks to Judi Romijn for the example).
- goto statements that survived state machine optimization
- also did not properly get tagged with escape options.
-
-- also fixed a bug in handling excessively long assertion
- strings (larger than 999 characters) during verification
-
-- revised the way that c_track is implemented (the points
- where c_update and c_revert are called) to make it a
- little easier to maintain
-
-- removed some no longer used code from pangen1.h
-
-- fixed bug in treatment of rendezvous statements in BFS mode
-
-- xspin408.tcl update: compiler errors are now printed in the
- log window, as they should have been all along...
- (courtesy Doug McIlroy)
-
-==== Version 4.1.1 - 2 January 2004 ====
-
-- extended bitstate hashing on 32-bit machines to work correctly
- with -w arguments up to and including -w34 (courtesy Peter Dillinger)
-- reduced amount of memory allocated to dfs stack in bitstate
- mode to something more reasonable (it's accessed through a
- hash function -- now related to the maxdepth, not the -w
- parameter
-- fixed bug that could cause problem with very long assertions
- (more than 256 characters long)
-
-- in xspin411, verbose mode during verifications is now default
- (it adds line numbers reached in the never claim to the output)
-- small fixes to the search capability in most text windows
-
-==== Version 4.1.2 - 21 February 2004 ====
-
-- fixed bug in support for notrace assertions (the pan.c would
- not compile if a notrace assertion was defined)
-- fixed unintended feature interaction between bitstate search
- and the -i or -I runtime flags for finding the shortest
- counter-example
-- some cosmetic changes to ease the life of static analyzers
-- fixed implementation of Jenkins function to optionally
- skip a semi-compression of the statevector -- to increase speed
- (pointed out by Peter Dillinger)
-- fixed bug in resetting memory stack arena that could show up
- in iterative verification runs with pan -R argument
- (also found by Peter Dillinger)
-- new version of xspin 4.1.2, with a better layout of some
- of the panels
-
-==== Version 4.1.3 - 24 April 2004 ====
-
-- changed from using "cpp" by default to using "gcc -E -x c"
- given that most users/systems have gcc anyway to compile c programs
- and not all systems have cpp in a fixed place.
- there should be no visible effect of this change.
-
-- a rendezvous send operation inside an atomic sequence was
- incorrectly accepted as a candidate for merging with subsequent
- statements in the atomic sequence. it is the only type of statement
- that can cause loss of atomicity (and a switch to another process)
- when *executable* (rather than when blocking, as is the case for
- all other types of statements, including asynchronous sends).
- this is now fixed, such that if there is at least one rv channel
- in the system, send operations inside atomic sequences cannot
- be merged with any other statement
- (in general, we cannot determine statically if a send operation
- targets an rv channel or an asynchronous channel, so we can only
- safely allow the merging if there are no rv channels at all).
- this can cause a small increase in the number of stored states
- for models with rendezvous cannels
-
-- counter-examples produced for liveness properties (non-progress or
- acceptance cycles) often contained one step too many -- now fixed
-
-- added check for reuse of varnames in multiple message fields
- i.e., q?x,x is not allowed (would cause trouble in the verifier)
-
-- added a warning against using a remote reference to a label
- that is declared inside an atomic or d_step sequence -- such
- labels are always invisible to the never claim (since the
- executing of the sequence containing the label is meant to be
- indivisible), which can cause confusion.
-
-- "StackOnly" can be used as an alternative to "UnMatched" when used
- as the optional 3rd argument a c_track primitive (see Spin2004 paper)
-
-==== Version 4.2.0 - 27 June 2004 ====
-
-- main.c now recognizes __OpenBSD__ and treats it the same as __FreeBSD__
-
-- general cleanup of code (removing some ifdefs etc)
-
-- allow reuse of varnames in multiple message fields (see 4.1.3) if
- var is an array variable (e.g., using different elements)
-
-- deleted support for directive -DCOVEST -- replaced with -DNOCOVEST
-
-- deleted support for directive -DHYBRID_HASH
-
-- deleted support for directive -DOHASH, -DJHASH, -DEXTENDED
- added -DMM for an experimental/debugging mode (non-documented)
-
-- replaced Jenkins' original hashfunction with an extended version
- contributed by Peter Dillinger.
- it uses more of the information to generate multiple pseudo hash values
- (multi-hashing with anywhere from 1,2,... hash-functions)
-
-- added runtime verifier flag -k to support multi-hashing in Bitstate mode.
- pan -k2 reproduces the default behavior, with 2 bits set per state.
- pan -k1 is the same as the old pan -s (which also still works).
- (as also first suggested by Dillinger and Manolios from Georgia Tech.)
-
-- some more useful hints are generated at the end of each bitstate
- run about possible improvements in coverage, based on the results
- obtained in the last run.
-
-- updated xspin420.tcl to match the above changes in verification options.
-
-==== Version 4.2.1 - 8 October 2004 ====
-
-- improvement of BFS mode for partial order reduction, thanks to
- Dragan Bosnacki
-- fewer redundant declarations and fewer complaints from static analyzers
-- a d_step could under some circumstances interfere with a rendezvous
- in progress (e.g., when the d_step started with an if statement, or
- when it started with a send or receive rather then a straight guard
- condition (i.e., an expression). this now works as it should.
-- 4.2.0 attempted to make support for coverage estimates the default.
- this, however, means that on some systems the pan.c source has to be
- compiled with an additional -lm flag (for the math library)
- coverage estimates had to be turned off explicitly by compiling with
- -DNOCOVEST
- in 4.2.1 the earlier default is restored, meaning that you have to
- specify -DCOVEST to get the coverage estimates (and presumably you
- will then know to compile also with -lm)
-- fixed bug that caused an internal name conflict on the verification
- of the mobile1 model from the Test distribution
-- fixed a problem that prevented having more than 127 distinct proctypes
- the max is now 255, the same as the max number of running processes.
-- fix to restore bitstate hashing to work on 64-bit machines
- we still only compute a 32-bit hash; the largest usable bitstate
- hash-array remains 2^35 bits (i.e., 2^32 bytes or 4 Gigabytes).
- (the maximum on 32-bit machines remains -w34 or 2 Gigabytes)
- for 64-bit mode, we will extend this soon to take advantage of
- larger memory sizes available on those machines. [see 4.2.5]
-- the default number of hash-functions used in bitstate hashing
- is now 3 (equivalent to a runtime option -k3), which gives slightly
- better coverage in most cases
-
-==== Version 4.2.2 - 12 December 2004 ====
-
-- verifiers now can be compiled with -DRANDOMIZE (for dfs mode only)
- to achieve that transitions within each process are explored in
- random, rather than fixed, order. the other in which processes are
- explored remains fixed, with most recently created process explored
- first (if we can think of a good way of supporting random mode
- for this, we may add this later). if there is an 'else' transition
- among the option, no randomization is done (since 'else' currently
- must be explored as the last option in a set, to work correctly).
- this option can be useful to get more meaningful coverage of very
- large states that cannot be explored exhaustively.
- the idea for this option is Doron Peled's.
-- fixed a limitation in the pan.c verifiers that prevented the use
- of channels with more than 256 slots. this should rarely be an
- issue, since very large asynchronous channels are seldomly useful
- in verifications, but it might as well work.
-- fix to avoid a compiler complaint about a missing prototype when
- compiling pan.c with -DBFS
-- renamed error message about us of hidden arrays in parameter list
- to the more accurate description 'array of structures'
-
-==== Version 4.2.3 - 5 February 2005 ====
-
-- _pid and _ are no longer considered global for partial order reduction
-- fixed bug that could lead to the error "confusing control structure"
- during guided simulations (replay of error trails)
-- fixed problem where an error trail could be 1 step too long for
- invalid endstate errors
-- added experimental 64-bit hash mode for 64-bit machines,
- compile pan.c in bitstate mode with the additional directive -DHASH64
- the code is by Bob Jenkins: http://burtleburtle.net/bob/c/lookup8.c
- [placeholder for a later extension for 64 bit machines]
-
-==== Version 4.2.4 - 14 February 2005 ====
-
-- added missing newline after #ifdef HASH64 -- introduced in 4.2.3
- this caused a compiler warning when compiling pan.c in -DBITSTATE mode
-- a terminating run ending in an accept state was not stutter extended
- unless a never claim was defined. this now works also without a
- never claim, provided that a search for acceptance cycles is performed.
- in the absence of a never claim the corresponding error type is
- called a 'accept stutter' sequence (to distinguish it from 'claim stutter')
- (bug report from Alice Miller)
- the extension is disabled if the compiler directive -DNOSTUTTER is used,
- just like for the normal claim stutter extension rule
-- added support for using -DSC on file sizes larger than 2Gb (courtesy Hendrik Tews)
-- in simulation mode, the guard statement of a d_step sequence was not
- subject to escape clauses from a possible unless statement, contrary to the
- language spec. in verification mode this did work correctly; simulation mode fixed.
- (courtesy Theo Ruys and David Guaspari)
-- added warning for use of an 'unless' construct inside a d_step sequence
-
-==== Version 4.2.5 - 2 April 2005 ====
-
-- the default bitstate space size is now 1 Mb (was 512K)
-- the default hashtable size in exhaustive mode is now 512K slots (was 256K)
-- fixed memory leak that can bite in very long simulation runs
- (courtesy Hendrik Tews)
-- now turns off dataflow optimization (setting dead variables to 0)
- when remote variable references are used. (this is a little bit of
- overkill, since we'd only need to turn it off for the variables
- that are being monitored from the never claim, but it is simple and safe)
-- you can now compile pan.c with -DHASH64 to invoke a 64bit Jenkins hash,
- (enabled by default on 64bit machines) or disable it by compiling with -DHASH32
- (which is the default on 32bit machines)
- the 64-bit version of Spin (and of the pan.c files it generates) has now been
- fully tested; this means that we can now use more than 4 Gbyte of memory, both
- in full state and in bitstate mode.
-- added pan runtime options -M and -G (inspired by the work of Peter Dillinger
- and Panagiotis Manolios on 3Spin), with a simple implementation.
- (the code for pangen1.h actually got smaller in this update).
-
- these two new options are available in bitstate mode only and allow the user to
- define a bitstate hash array that is not necessarily equal to a power of two.
- if you use -M or -G, then this overrides any other setting you may have
- used for -w. for example:
- pan -M5 will use a hash array of 5 Megabytes
- pan -G7 will use a hash array of 7 Gigabytes.
- use this instead of -w when the hash array cannot be a power of 2 bytes large.
- pan -M4 is technically the same as pan -w25 in that it will allocate
- a hash array of 4 Megabytes (2^(25-3) bytes), but it can be slower
- because indices into the hash-array are now computed with a modulo operator
- instead of with faster bit masks and bit shifts. similarly,
- pan -G1 is technicall the same as pan -M1024 or pan -w33
- whether the use of -M and -G is slower than -w depends on your compiler.
- many modern compilers (e.g. gcc and microsoft visual studio) will automatically
- optimize the hash array access anyway when it effectively is a power
- of two large (i.e., independent of whether you use -w25 or -M4).
- in a small set of tests on a 2.5 GHz machine, using both gcc and the MS
- compilers, no meaningful difference in speed when using -M or -G could be
- measured, compared with -w (not even for non powers of two hash array sizes).
- (the difference in runtime was in the order of 3 to 4%).
-
-==== Version 4.2.6 - 27 October 2005 ====
-
-- mostly small fixes -- one bug fix for reading error trails on 64bit machines
- (courtesy Ignacy Gawedzki)
-- the full tar file now creates all files into a single common directory named
- Spin, which will simplify keep track of versions and updates
-- small update of xspin as well (now xspin4.2.6)
- the main change in xspin is that on startup it will now look for a file with
- the same name as the filename argument given (which is typically the name of
- the file with the Promela model in it) with extension .xsp
- so when executing "xspin model" the command will look for a file "model.xsp".
- xspin will read this file (if present) for commands to execute upon startup.
- (very useful for demos!)
- commands must start with either "X:" or "L:"
- an L: command must be followed by a number, which is used to set the number of
- lines that should be visible in the command log window
- an X: command can be followed by any shell command, that xspin will now execute
- automatically, with the output appearing in the command log window
- an example .xsp file:
-
-X: spin -a model
-L: 25
-X: nice gcc -DMEMLIM=1000 -DCOLLAPSE -DSAFETY -DREACH -o pan pan.c
-X: nice time -p ./pan -i -m150
-X: spin -t -c -q3 model
-X: cp model.trail pan_in.trail
-
-==== Version 4.2.7 - 23 June 2006 ====
-
-- change in pc_zpp.c, courtesy of Sasha Ivanov, to fix an incorrect order of
- preprocessing directives -- scanning "if" before "ifdef" and "ifndef"
-
-- all 3 very dubious types of statements in the following model were erroneously
- accepted by Spin version 4.2.6 and predecessors.
- they no longer are -- courtesy of the class of 2006 @ Caltech CS
- active proctype X() {
- chan q = [2] of { int, int };
-
- _nr_pr++; /* change the number of processes... */
- _p = 3; /* change the state of process X.... */
- q!2(run X()); /* something really devious with run */
- }
-
-- added the compiler directive __NetBSD__
-
-- the vectorsize is now always stored in an unsigned long, to avoid
- some obscure bugs when the size is chosen too small
-
-- fix in the parsing of LTL formulae with spin -f to make sure that
- unbalanced braces are always detected
-
-- added warning against use of rendezvous in BFS mode -- which cannot
- guarantee that all invalid endstates will be preserved
-
-- minor things: make_pc now defaults to gcc instead of cl (the microsoft
- visual studio compiler)
-
-- xspin4.2.7 disables some bindings that seem to be failing
- consistently now on all platforms, although the reason is unclear
- (this occurs in the automata view and the msc views, which are supposed
- to track states or execution steps to source lines in the main text
- window -- instead these bindings, if enabled, now seem to hang the gui)
-
-==== Version 4.2.8 - 6 January 2007 ====
-
-- added optimizations in cycle search described by Schwoon & Esparza 2005,
- in 'a note on on-the-fly verification algorithms' and in
- Gastin, Moro, and Zeitoun 2004, 'Minimization of counter-examples in Spin'
- to allow for early detection of acceptance cycles, if a state is found
- on the stack that is accepting, while still in the 1st dfs. the version
- also mentioned in Schwoon & Esparza -- for the case where the source state
- of such a transition is accepting -- is also included.
-
-- eleminated many of the #ifdef PC directives that distinguished between
- use of y.tab.h and y_tab.h which is no longer needed with the newer
- versions if yacc on cygwin (e.g., bison yacc)
-
-- the use of a non-local x[rs] assertion is now fatal
-
-- fixed small problem where scheduler could lose track of a process during
- simulations
-
-- small rewrites for problems spotted by static analyzers
-
-- restored correct working of separate compilation option (-S[12])
-
-- fixed initialization problem with local variables (making sure that
- a local can be initialized with a parameter or with the value of a
- previously declared and initialized local
-
-- emalloc now returns NULL when 0 bytes are requested (robert shelton 10/20/06)
-
-- using _stat instead of stat on WIN32 platforms for compatibility with cl.exe
-
-- avoided a problem with non-writable strings, in pan.c
-
-- renamed QPROVISO to Q_PROVISO in preparation for related updates in 4.3.0
-
-- fixed problem with the final transition of an error trail sometimes
- not appearing in the trail file (alex groce)
-
-==== Version 4.2.9 - 8 February 2007 ====
-
-- the optimization for cycle search from 4.2.8 wasn't complete -- it could cause
- annoying messages to show up, and the start of a cycle not being identified
- in all cases (Moti Ben-Ari) -- it now works they way it was intended
-
-- made it possible to compile pan.c with visual studio, provided that -DWIN32 or
- -DWIN64 are included in the compiler directives; see make_pc for an example.
- without this, file creat calls would crash the application -- because the windows
- implementation of this call uses its own set of flags...
-
-- the spin parser now flags all cases where the wrong number of parameters
- is specified in a run statement (as suggested by Klaus Havelund)
-
-- it is now possible to use a c_expr inside an expression, e.g. as in
- x[ c_expr { 4 } ] = 3 or x[ c_expr { f() } ] (Rajeev Joshi)
-
-- a new option for ./pan when embedded C code is used: -S to replay the
- error trace without printing anything other than the user-defined printfs
- from the model itself or from inside c_code fragments - (Rajeev Joshi)
-
-==== Version 4.3.0 - 22 June 2007 ====
-
-- bug fix (thank you Claus Traulsen) for goto jumps from one atomic
- sequence into another. if the first was globally safe, but the second
- was not, then an erroneous partial-order reduction was possible
-- small changes based on static analyzer output, to increase robustness
-- smaller pan.c files generated if huge arrays are part of the model
-- more accurate reporting of statecounts in bitstate liveness mode
-- better portability for compilation with visual studio
-- likely to be the last spin version 4 release -- the next should be 5.0
- which supports safety and liveness verification on multi-core systems
-
-==== Version 5.0 - 26 October 2007 ====
-
-- lots of small changes to make the sources friendlier to static analyzers,
- like coverity, klocwork, codesonar, and uno, so that they find fewer things
- to warn about
-- improved check for a match of the number of operands specified to a run
- operator with the number of formal parameters specified for the proctype
- (courtesy an example by Klaus Havelund)
-- memory counts are now printed properly as MB quantities (divided by
- 1024*1024 instead of 1,000,000)
-- more accurate treament of atomic sections that contain goto statements,
- when they jump into a different atomic section (especially when the two
- atomics have different properties under partial order reduction)
- (courtesy and example by Claus Traulsen)
-- improvement treatment of run statements for processes that initialize
- local variables with global expressions. in these cases the run
- statement itself is now recognized as global -- otherwise it can still
- be treated as local under partial order reduction rules
-- improved treatment of variable update printing when xspin is used.
- before, large structures were always full printed on every step, which
- could slow down xspin significantly -- this now happens only if there
- was a change of at least one of the values printed.
-
- Additions:
-- support for use of multi-core systems, for both safety and liveness
- properties. see: http://www.spinroot.com/spin/multicore/
-- added the time of a run in seconds as part of all outputs, and in many
- cases also the number of new states reached per second
-
-- new compile-time directives for pan.c supported in Version 5.0 include:
- NCORE, SEP_STATE, USE_DISK, MAX_DSK_FILE, FULL_TRAIL, T_ALERT
- and for more specialized use:
- SET_SEG_SIZE, SET_WQ_SIZE, C_INIT, SHORT_T, ONESECOND
- the following three can be left unspecified unless prompted by pan itself
- on a first trial run:
- VMAX, PMAX, QMAX,
- the use of all the above directives is explained in
- http://www.spinroot.com/spin/multicore/V5_Readme.html
- for typical multi-core applications only the use of -DNCORE=N is
- typically needed
-- a small number of other new directives is not related to the use of
- multicore verifications - their use is also explained (at the very
- bottom of) the V5_Readme.html file mentioned above. they are:
- FREQ, NUSCC, BUDGET, THROTTLE, LOOPSTATE, NO_V_PROVISO
projects / lttv.git / blobdiff