convert from svn repository: remove tags directory

[lttv.git] / trunk / verif / Spin / Doc / V4.Updates

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