convert from svn repository: remove tags directory

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

Distribution Update History of the SPIN sources
===============================================

==== Version 2.0 - 1 January 1995 ====

The version published in the first printing of
``Design and Validation of Computer Protocols''
is nominally SPIN Version 1.0.

SPIN version 2.0 includes a partial order reduction
mode and many extensions and revisions that are
documented in the file Doc/WhatsNew.ps of the
distribution.  This file lists all updates
made to these sources after the first release.

===== 2.0.1 - 7 January 1995 ====

An automatic shell script `upgrades' in the main
SPIN directory will be maintained from now on.
For all future updates it will suffice to retrieve
just the upgrades file, and execute it in the Src
directory to apply all changes.  The tar file will
of course be kept up to date at all times as well.

Changes in this update:
1. MEMCNT can now grow larger than 2^31 - for those
   happy users that have a machine with more than
   a Gigabyte of main memory.
   (N.B. this fix was made and distributed before the
   upgrades file was started - so this one change isn't
   available in that way)
2. Change in the lexical analyzer to accept redundant
   text at the end of preprocessor directives, that
   some versions of cpp may produce.

===== 2.0.2 - 10 January 1995 ====

Two small updates to pangen1.h to avoid problems on
some systems when (1) compiling pan.c with profiling
enabled, or (2) when using the new predefined function
enabled() in combination with partial order reduction.

===== 2.0.3 - 12 January 1995 ====

At request, added a printout of the mapping from label
names as used in the Promela source to state numbers as
used in the verifier to spin option -d.
to see just this new part of the listing, say:
        spin -d spec | grep "^label"
first column is the keyword "label"
second column is the name of the label
third column is the state number assigned
last column is the name of the proctype in which the
label is used.
the same state numbers and transitions are
also used by the verifier, and can be printed as
before with:
        spin -a spec; cc -o pan pan.c; pan -d

===== 2.0.4 - 14 January 1995 ====

With the introduction of `else' a new opportunity for
silly syntax mistakes is created.  it is all too tempting
to write:
        if
        :: condition ->
                more
        :: else
                something
        fi
and forgot the statement separator that is required between
the `else' and `something'
this likely typo is easy to recognize, and is silently
repaired and accepted by the new lexical analyzer.

===== 2.0.5 - 17 January 1995 ====

transition labels for send and receive operations
now preserve all the information from the source text
(i.e., the symbolic names for all message parameters used).

===== 2.0.6 - 27 January 1995 ====

two fixes, both caught by Roberto Manione and Paola:
- deeply nested structures (more than two levels)
  could give syntax errors, and
- the transition label of an `else' statement wasn't
  always printed correctly in the traces.

===== 2.0.7 - 2 February 1995 ====

- another fix of the implementation of data structures
  to make references of deeply nested structure work
  the way they should
- removed suboptimal working of safety marking of
  atomic sequences.  reductions are now slightly
  larger in some cases.
- improved boundary checking of array indexing also
  slightly (made it more efficient for some cases)

===== 2.0.8 - 7 February 1995 ====

- adjusted line number counting slightly in spinlex.c
  to avoid annoying off-by-one errors.

===== 2.0.9 - 9 February 1995 ====

- removed a bug in the transition structures that are
  generated for d_steps. (small fix in pangen2.h)

===== 2.1 - 15 February 1995 ====

- removed two errors in the implementation of d_steps:
   one was related to the treatment of `else' during verification
   another related to the execution of d_steps in guided simulations
- improved the treatment of rendez-vous in SPIN verbose printings
   improves match with xspin; avoids misinterpretation of pids
- made mtype fields be interpreted uniformly in all SPIN modes
- added message sequence charts in xspin
- removed stutter-closedness checks from pangen2.h (no change
  in functionality, just replaced a dubious check with a more
  precise descriptive warning)

===== 2.1.1 - 17 February 1995 ====

- instantiated channels declared inside typedefs weren't
  properly initialized

===== 2.2 - 19 February 1995 ====

- main extension of functionality:
  added an interactive simulation mode (both in xspin and in spin itself)
  that will be described at greater length in Newsletter #4.
  also improved some of the printouts for verbose simulation runs.

- added a precompiler directive -DREACH to force exploration of
  all states reachable within N execution steps from the initial
  system state, when the search is deliberately truncated with -mN.
  normally such a truncated search does not give that guarantee.
  (note that if a state at level N-1 is also reachable from the
  initial state within 1 execution step, but it is reached via the
  longer path first in the DFS - then all successors via the shorter
  path would normally not be explored, because they succeed a
  previously visited state. with -DREACH we remember the depth at
  which a state was visited, and consider it unvisited when encountered
  on a shorter path.  not compatible with BITSTATE - for the obvious
  reason (no room to store the depth counts).

- fixed a bug in pangen[24].c that could cause an internal consistency check
  in the runtime verifiers to fail, and cause the run to terminate with
  the error `sv_save failed'

===== 2.2.1 - 23 February 1995 ====

- small refinements to interactive simulation mode (xspin and spin)

===== 2.2.2 - 24 February 1995 ====

- added missing prototype in 2.2.1, and fix parameter mistake in a
  function that was added in 2.2.1

===== 2.2.3 -  3 March 1995 ====

- bug fix in implementation of d_step (dstep.c)
  and some mild improvements in error reporting

===== 2.2.4 -  9 March 1995 ====

- made sure process numbers assigned by simulator
  are always the same as those assigned by the verifier
- by request: added a binary exclusive-or operator ('^')

===== 2.2.5 -  14 March 1995 ====

- removed error in treatment of `else' during random simulation.
  `else' was incorrectly considered to be executable also
  in the middle of a rendez-vous handshake. no more.

===== 2.2.6 -  21 March 1995 ====

- made sure that variable declarations are reproduced in
  the pan.c sources in the same order as they are given
  in the original promela specification.  this matters
  in cases where new variables are initialized with each
  others values.
- better error handling when a reference is made erroneously
  to an assumed element of an undeclared structure

===== 2.2.7 -  23 March 1995 ====

- catches more cases of blocking executions inside d_step
  sequences
- better handling of timeout, when using both blocking
  atomic sequences and never claims.  the behavior of the
  simulator and the verifier didn't always match in these
  cases.  it does now.

===== 2.2.8 -  30 March 1995 ====

- inside dstep sequences `else' wasn't translated correctly

===== 2.2.9 -  12 April 1995 ====

- removed a mismatch between spin and xspin in dataflow output
- clarified the scope of dataflow checks spin's -? response
- fixed a typo that could confuse pid assignments when -DNOCLAIM is used
- improved some of spin's outputs a little for xspin's benefit

===== 2.2.10 -  18 April 1995 ====

- removed a redundancy in the creation of channel templates
  during the generation of a verifier with spin option -a

===== 2.3.0 -  19 April 1995 ====

- an extension of functionality.  until now the simulator would execute
  a receive test (for instance: q?[var1,var2] ) erroneously with
  side-effects, possibly altering the values of the variables.
  any boolean condition in Promela, however, must be side-effect free
  and therefore the verifier had the correct implementation (no value
  transfers in a test of executability of this type)
  michael griffioen noted that the poll of a message in a channel was
  nonetheless usefull.  this leads to a new type of operation in Promela.
  pending more thorough documentation, here's an example of
  each of the existing ones:

  A.    q?var1,const,var2       - fifo receive (constants must be matched)
                                  if successful, the message is removed
                                  from the channel
  B.    q??var1,const,var       - random receive (as A., but from any slot
                                  that has a matching message, checked in
                                  fifo order) if successful, the message is
                                  removed from the channel
  C.    q?[var1,const,var2]     - boolean test of executability of type A receive.
  D.    q??[var1,const,var2]    - boolean test of executability of type B receive.
  E.    q?<var1,const,var2>     - fifo poll, exactly as A, but the message is
                                  not removed from the channel
  F.    q??<var1,const,var2>    - random receive poll, exactly as B, but message
                                  not removed from the channel

  there are still only two different ways to test the executability of a
  receive operation without side-effects (be it a normal receive or a poll
  operation)
  the two new operations of type E and F allow one to retrieve the contents
  of a message from a channel, without altering the state of the channel.
  all constant fields must of course still be matched, and if no variables
  are present, an operation of type E has the same effect as one of type C.
  (and similarly for types F and D)

===== 2.3.1 -  20 April 1995 ====

- slightly more conservative treatment for the change from 2.2.10
  some redundancy is caused by the spec, and now flagged as warnings.
  using a \ 5typedef structure that contains an initialized channel in
  a formal parameter list, for instance, is always reduncant and uses
  up channel templates in the verifier - without otherwise doing harm,
  but there is a limit (255) to the number of templates that can exist.
  the limit is now also checked and a warning is given when it is exceeded.

===== 2.3.2 -  25 April 1995 ====

- adjustment of output format of guided simulation to match a recent
  change in Xspin (better tracking of printfs in MSC's)

===== 2.3.3 -  29 April 1995 ====

- bit or bool variables cannot be hidden - this is now reported as a
  syntax error if attempted
- the reporting of the options during interactive simulations is
  improved - mysterious options, such as [ATOMIC] are now avoided better

===== 2.3.4 -  1 May 1995 ====

- added the keyword D_proctype as an alternative to proctype to
  indicate that all the corresponding processes are expected to
  be deterministic.  the determinism is not enforced, but it is
  checked by the verifier.  no other difference exists.  a simulation
  will not pick up violations of this requirement.

===== 2.3.5 -  13 May 1995 ====

- the check for enforcing determinism (2.3.4) was not placed
  correctly.  it is now.

===== 2.3.6 -  18 May 1995 ====

- removed bug in code generation for arrays of bools
- moved a debug-printf statement

===== 2.3.7 -  18 May 1995 ====

- removed bug in testing enabledness of run statements
  during interactive simulations

===== 2.3.8 -  19 May 1995 ====

- small change in bitstate mode.  the verifier checks if a
  new state is previously visited, or appears on the dfs stack.
  (information about presence in the stack is only needed to
   enforce the partial order reduction rules)
  in both cases (in bitstate mode) the check is done via hashing
  into a bitarray; with the array for the statespace much larger
  than the one for the stack.
  so far, if either match succeeded, the search was truncated.
  any match in the stack-array that is combined with no-match in
  the statespace array, however, is necessarily caused by a
  hash-collision (i.e., is a false match) and can be discarded.
  the coverage of bitstate runs should improve slightly by this
  change.  nothing else will be affected.

===== 2.4.0 -  22 May 1995 ====

- new functionality: there is a new option to SPIN that
  can be used in guided simulations (that is: in combination
  with the option -t, when following a error trail produced
  by one of the verifiers generated by SPIN)
  for very lengthy trails, it can take a while to reach an
  interesting point in the sequence.  by adding the option
  -jN one can now skip over the first N steps in the trail
  (more precisely: supress the printing during those steps)
  and quickly get to the interesting parts.
  for instance:
        spin -t -p -g -l -v -j1000 spec
  skips the first 1000 steps and prints the rest.
  caveat: if there are fewer than 1000 steps in the trail,
  only the last state of the trail gets printed.
- avoiding some more redundant printouts during guided simulations
  will also help to speed up the browsing of error trails with XSPIN
- the extension is supported in the new version of XSPIN as well
- the new version of XSPIN also supports BREAKPOINTS during
  all types of simulation
  breakpoints are supported via the MSC printf statements
  *     including a printf that starts with the prefix "MSC: "
        in a Promela Model will cause the remainder of the line
        printed to be included as a box inside the MSC charts
        maintined by XSPIN.
  *     if the remainder of such a line contains the capitalized word
        BREAK, the simulator will pause at that line and wait for
        the user to reactivate the run (single step or run)

===== 2.4.1 -  4 June 1995 ====

- added runtime option -e to verifiers produced by SPIN.
  with this option all errors encountered during the verification
  are saved in a trail file - up to the limit imposed by -cN
  (the default is one trail).  the first trail has the extension .trail,
  as before (which is also the only extension expected right now under
  the guided simulation option -t of SPIN). subsequent trails have
  extensions .trail1, .trail2, ... etc.
  use this option in combination with -cN
        using -c5 -e will produce the first 5 trails,
        using -c0 -e will produce all trails.
- modified Xspin to work also with the new Tcl7.4/Tk4.0, which is now
  in beta release.  the changes should not affect the working under
  the current version Tcl7.3/Tk3.6
- there is now a file called `version_nr' in the directory /netlib/spin
  on the distribution server.  the file contains just the version
  number from the currently distributed SPIN sources (avoids having to
  download larger files to find out if anything changed)
- added runtime option -hN to choose another than the default hash-function
  (useful in bitstate mode.  N must be an integer between 1 and 32)
- improved the implementation of the new runtime option -s (for selecting
  single-bit hashing instead of the default double-bit hashing)
  especially useful in combination with -hN for sequential multihashing
  techniques (iterative approximation of exhaustive searches for very large
  problem sizes)
- starting with this version of Xspin there will also be a separate upgrades
  script to keep the Tcl/Tk files up to date.

===== 2.4.2 -  11 June 1995 ====

- so far, variables were created and initialized in the simulator
  as late as possible:  upon the first reference.  a variable that
  is never referenced was therefore never created - which is some
  sense of economy.  however, if the local is initialized with an
  expression that includes references to other variables (local or
  global) then those other variables might well change value before
  the first reference to the initialized local is made - and thus
  the local might obtain an unexpected initial value.
  the error was caught by Thierry Cattel - and lazy variable creation
  is now abandoned.  the verifier is unaffected by this fix -- it
  already id the right thing (instant creation of all locals on process
  initialization).
- channels deeply hidden inside structures were not properly logged
  in the partial order reduction tables.  it could cause an abort of
  a verification run with the mysterious error "unknown q_id, q_cond."
  it works properly now.  error caught by Greg Duval.
- made a small change in output format (comments only) for remote
  references
- made the new runtim option -e (from version 2.4.1) also accessible
  from within XSPIN
- changed the MSC canvas in the simulation mode of XSPIn to no longer
  be self-scrolling (it defeated any attempt from the user to select
  other portions of the MSC to ponder, other than the tail, during a
  run).  also made the message transfer arrows wider - and added an
  option to replace the symbolic step numbers in the MSC's with source
  text.

===== 2.5 -  7 July 1995 ====

Fixes
- values of rendez-vous receives were printed incorrectly in printouts
  of spin simulation runs - this could confuse xspin; the symptom was that
  some rendez-vous send-recv arrows were not drawn in the MSC displays.
- rendez-vous operations that guarded escapes did not always execute
  properly in random simulations.
- in xspin, the boxes produced by an MSC printf could lose its text
  after the cursor would pass over it - that's no longer the case
- the use of a remote references used to disable the partial order
  reduction algorithm.  instead, such references now automatically label
  the transition that enters or exits from the corresponding process state
  as unsafe.  this suffices to preserve the use of the partial order
  reduction.  (proposed by Ratan Nalumasu.)

Small Changes
- added a print line in verbose output for process creations - as well
  as process terminations.  it will be used in a future version of xspin.
- made all xspin verification run timed - the user+system time info
  appears in the xspin logs
- on aborted verification runs, xspin will now also print the partial
  information gathered up to the point of the abort
- slightly changed the way aborts are handled in xspin
- never claims containing assignments (i.e., side-effects) can be useful
  in some cases.  spin will still generate warnings, but allows the user
  to ignore them (i.e., the exit status of spin is no longer affected)
- in simulation mode - xspin now pays attention to filenames and will not
  try to hilight lines in files that are not visible in the main text window
- added compile-time directive -DNOFAIR to allow compilation of a verifier
  if it is known that the weak-fairness option will not be used -- this
  avoids some memory overhead, and runs slightly faster.
  the fastest run can be obtained by compiling -DNOCOMP -DNOFAIR (turning
  off the state compression and the weak fairness related code)
  the most memory frugal run (apart from the effects of -DREDUCE) can be
  obtained by compiling with just -DNOFAIR (and leaving compression turned
  on by default)  note that memory consumed also goes up with the value
  provided for the -m option (the maximum depth of the stack)
- added a file Doc/Pan.Directives with an overview of all user definable
  compile-time directives of the above type.

Extension
- added a mechanism to define process priorities for use during random
  simulations - to make high priority processes more likely to execute
  than low priority processes.
  as alternatives to the standard:
        run pname(...)
        active proctype pname() { ... }
  you may now add a numeric execution priority:
        run pname(...) priority N
  and/or
        active proctype pname() priority N
  (with N a number >= 1)
  the default execution priority is 1; a higher number indicates a
  higher priority.  for instance, a priority 10 process is 10x more
  likely to execute than a priority 1 process, etc.
  the priority specified at the proctype declaration only affects the
  processes that are initiated through the `active' prefix
  a process instantiated with a run statement always gets the priority
  that is explicitly or implicitly specified there (the default is 1).
  the execution priorities have no effect during verification, guided,
  or interactive simulation.
- added an example specification file (Test/priorities) to verify the
  correct operation of the execution priorities

===== 2.5.1 -  12 July 1995 ====

- some tweaks to correct the last update (a simulation run could
  fail to terminate - and xspin could fail to detect the zero exit
  status of spin after warning messages are printed)

===== 2.6 -  16 July 1995 ====

- added a new option for executable verifiers - to compute the effective
  value range of all variables during executions.
  the option is enabled by compiling pan.c with the directive -DVAR_RANGES
  values are tracked in the range 0..255 only - to keep the memory
  and runtime overhead introduced by this feature reasonable.
  (the overhead is now restricted to roughly 40 bytes per variable -
   it would increase to over 8k per variable if extended to the full
   range of 16-bit integers)
- a new option in the validation panel to support the above extension
  was added
- xspin now supports compile-time option -DNOFAIR to produce faster
  verifiers when the weak fairness option is not selected
- added an example in directory Test to illustrate dynamic creation
  of processes (Test/erathostenes)
- removed an error message that attempted to warn when a data structure
  that contained an initialized channel was passed to a process as a
  formal parameter.  it leads to the creation of a redundant channel,
  but is otherwise harmless.
- changed the data types of some option flags from int to short

===== 2.6.1 -  18 July 1995 ====

- option -jN (introduced in version 2.4.0) -- to skip the verbose
  printouts for the first N execution steps -- now also works in
  random simulation mode.
  only process creations and terminations are still always printed
- channel names are no longer included in the -DVAR_RANGES output
  at least not by default (see version 2.6 - above)
  to still include them, generate the verifier in verbose mode
  as ``spin -a -v spec'' instead of the default ``spin -a spec''
- predefined variable _last was not quite implemented correctly
  in the verifier (the error was harmless, but if you tried to write
  specifications that included this construct, you may have had
  more trouble than necessary getting it to work properly)

===== 2.7.Beta -  24 July 1995 ====

Fixes
- when an atomic sequence blocks, the process executing that sequence
  loses control, and another process can run.  when all processes block,
  the predefined variable 'timeout' becomes true, and all processes again
  get a chance to execute.  if all processes still block - we have reached
  an end-state (valid or invalid, depending on how states are labeled).
  until now, timeout was allowed to become true before an atomically
  executing process could lose control - this is not strictly conform the
  semantics given above, and therefore no longer possible.
- it is now caught as a runtime error (in verification) if an attempt
  is made to perform a rendez-vous operation within a d_step sequence.
- it is also caught as an error if a 'timeout' statement is used inside
  a d_step sequence (it may be used as the first statement only)
- an else statement that appears jointly with i/o statements in
  a selection structure violates the rules of a partial order
  reduction.  a warning is now included if this combination is seen, both
  at compile-time and at run-time.  the combination should probably be
  prevented alltogether since its semantics are also not always clear.
- one more correction to the implementation of 'else' inside dsteps
  to avoid a possibly unjustified error report during verification
- a previously missed case of the appearance of multiple 'else' statements
  in selection structures is now caught and reported
- fixed a missing case were process numbers (_pid's) did not match
  between a verification run and a guided simulation run. (if a never
  claim was used, there could be an off-by-one difference.)
- rendez-vous operations are now offered as a choice in interactive
  simulation mode only when they are executable - as they should be
- the introduction of active proctypes in 2.5 introduced an obscure
  line-number problem (after the first active proctype in a model
  that contains initialized local vars, the line numbers could be
  off). it's fixed in this version.

Extensions
- The main extension added in this release is the inclusion of an
  algorithm, due to Gerth, Peled, Wolper and Vardi, for the translation
  from LTL formulae into Promela never claims.  The new options are
  supported both in SPIN directly, and from XSPIN's interface.

- added the option to specify an enabling condition for each
  proctype.  the syntax is as follows:
        proctype name(...) provided ( expression )
        {
                ...
        }
  where the expression is a general side-effect free expression
  that may contain constants, global variables, and it may contain
  the predefined variables timeout and _pid, but not other local
  variables or parameters, and no remote references.

  the proctype may be declared active or passive.  no enabling
  conditions can be specified on run statements unfortunately.
  the provided clauses take effect both during simulation runs
  and during verification runs.

- extended XSPIN with a barchart that can give a dynamic display
  of the relative fraction of the system execution that is used by
  each process.  modified the layout of the Simulation option panel,
  to make some of the runtime display panels optional.

- added a <Clear> button to most text windows (to clear the contents
  of the display)

- added <Larger> and <Smaller> scaling buttons to canvas displays
  (that is: the FSM view displays and the MSC display).  the buttons
  show up when the image is complete (e.g., when the message sequence
  chart has been completed) - so that it can be scaled to size as a
  whole.

- added new <Help> buttons, with matching explanations, to most display
  panels - and updated and extended the help menus.

===== 2.7 -  3 August 1995 ====

- fixed possible memory allignment problem on sun sytems
- several fine tunings of xspin
- made it possible to let the vectorsize get larger than 2^15 bytes
  to support very large models
- a provided clause has no effect inside d_step sequences, but it
  is looked at during atomic sequences.  this rule is now enforced
  equally in simulation and validation.
- the use of enabled() and pc_value() outside never claims now triggers
  a warning instead of an error message (i.e., it is now accepted).
  in models with synchronous channels, the use of enabled() still makes
  verification impossible (both random and interactive simulations will
  work though)
- added an option to `preserve' a message sequence chart across
  simulation runs (by default, all remnants of an old run are removed)

===== 2.7.1 -  9 August 1995 ====

- removed bug in the code that implements the compile time directive
  to verifier source -DNOFAIR, which was introduced in version 2.5,
  (and picked up starting with version 2.6 also via xspin).

===== 2.7.2 -  14 August 1995 ====

- the LTL formula parser accidentily swapped the arguments of U and V
  operators.  it does it correctly now.  the associativity of U and
  V now defaults to left-associative.
- arithmetic on channel id's was so far silently condoned.
  it is now flagged as an error.  it is still valid to say: c = d,
  if both c and d are declared as chan's, but d may no longer be
  part of an expression.
- unless operators now distribute properly to (only) the guard of
  d_step sequences (but not into the body of the d_step).

===== 2.7.3 -  15 August 1995 ====

- tweek in implementation of provided clauses - to make it possible
  to use `enabled()' inside them.

===== 2.7.4 -  25 September 1995 ====

- fixed a small omission in the implementation of dsteps
- allowed `else' to be combined with boolean channel references
  such as len and receive-poll
- added some compiler directives for agressively collapsing
  the size of state vectors during exhaustive explorations.
  this option is still experimental
- made some cosmetic changes in the look and feel of xspin

===== 2.7.5 -  7 October 1995 ====

- the value returned by a run statement triggered and
  unwarranted error report from spin, if assigned to a variable
- xspin didn't offer all possible choices in the menus, when
  used in interactive simulation mode
- somewhat more careful in closing file descriptors once they
  are no longer needed (to avoid running out on some systems)
- some small cosmetic changes in xspin (smaller arrows in the
  message sequence chart - to improve readability)

===== 2.7.6 -  8 December 1995 ====

- added a compiler directive PC to allow for compiling the
  SPIN sources for a PC.  (this is only needed in the makefile
  for spin itself - not for the pan.? files.)
  if you generate a y.tab.c file with yacc on a standard Unix
  machine, you must replace every occurrence of y.tab.[ch]
  with y_tab.[ch] in all the spin sources as well before compiling.
  some of the source file names also may need to be shortened.
- some syntax errors reported by spin fell between the cracks
  in xspin simulations.  they are now correctly reported in the
  simulation window and the log window.
- in interactive simulation mode - typing `q' is now a recognized
  way to terminate the session
- option -jN (skip output for the first N steps) now also works
  for interactive simulations.  the first N steps are then as in
  a random simulation.
- FSMview in xspin is updated to offer also the statemachine
  view for never claims - and to suppress the one for an init
  segment, if none is used
- fixed a bug in implementation of hidden structures - some of
  the references came out incorrectly in the pan.c code

===== 2.7.7 -  1 February 1996 ====

- made it possible to combine the search for acceptance cycles
  with one for non-progress cycles, to find cycles with at least
  one accepting state and no progress states.
  the combined search is compatible with -f (weak fairness).
  [note added at 2.8.0 -- this wasn't completely robust, and
   therefore undone in 2.8.0]
- added the explicit choice for the specification of a positive
  or a negative property in LTL interface to xspin
- fixed a bug in the ltl translator (it failed to produce the correct
  automaton for the right-hand side of an until-clause, if that clause
  contained boolean and-operators)
- in non-xspin mode, process states are now identified as <endstates>
  (where applicable) in the simulation trails
- it is now flagged as an error if a `run' statement is used
  inside a d_step sequence
- added two new options ( -i and -I ) for the generated verifiers
  (pan -i / pan -I).  recommended compilation of pan.c is with -DREACH
  for exhaustive mode (-DREACH has no effect on BITSTATE mode).
  option -i will search for the shortest path to an error.
  the search starts as before - but when an error is found, the
  search depth (-m) is automatically truncated to the length of that
  error sequence - so that only shorter sequences can now be
  found.  the last sequence generated will be the shortest one possible.
  option -I is more aggressive:  it halves the search depth
  whenever an error is found, to try to generate one that is at most
  half the length of the last generated one.
  if no errors are found at all, the use of -i or -I has no effect on
  the coverage of search performed (but the effect of using -DREACH
  is an increase in memory and time used, see the notes at version 2.2).

===== 2.7.8 -  25 February 1996 ====

Extensions
- a new runtime option on the verifiers produced by Spin is -q
  it enforces stricter conformance to what is promised in the book.
  by default, the verifiers produced by Spin require each process to have
  either terminated or be in a state labeled with an endstate-label, when
  the system as a whole terminates.   the book says that for such a state
  to be valid also all channels must be empty.  option -q enforces that
  stricter check (which is not always necessary).  the option was suggested
  by Pim Kars of Twente Univ., The Netherlands.
- `mtype' is now a real data-type, that can be used everywhere a `bit'
  `byte' `short' or `int' data-type is valid.
  variables of type `mtype' can be assigned symbolic values from the range
  declared in mtype range definitions (i.e.: mtype = { ... }; ).
  the value range of an mtype variable (global or local) remains equal
  to that of a `byte' variable (i.e., 0..255).
  for instance:
        mtype = { full, empty, half_full };
        mtype glass = empty;
  the extension was suggested by Alessandro Cimatti, Italy.
- the formfeed character (^L or in C-terms: \f) is now an acceptable
  white space character -- this makes it easier to produce printable
  promela documents straight from the source (also suggested by Cimatti).
- a new predefined and write-only (scratch) variable is introduced: _
  the variable can be assigned to in any context, but it is an error to
  try to read its value. for instance:
        q?_,_,_;        /* to remove a message from q */
        _ = 12;         /* assign a value to _ (not very useful) */
  the value of _ is not stored in the state-vector
  it may replace the need for the keyword `hidden' completely
  the syntax was suggested by Norman Ramsey (inspired by Standard ML)

Fixes
- the FSM-view mode in xspin wasn't very robust, especially when moving
  nodes, or changing scale.  it should be much better now.  button-1 or
  button-2 can move nodes around.  click button-1 at any edge to see
  its edge label (it no longer comes up when you hover over the edge -
  the magic point was too hard to find in many cases).
- fixed bug in processing of structure names, introduced in 2.7.5, caught
  by Thierry Cattel, France.
- trying to pass an array hidden inside a structure as a parameter
  to a process (in a run statement) was not caught as a syntax error
- trying to pass too many parameters in same also wasn't caught
- in interactive mode, the menus provided by xspin were sometimes
  incorrect for interactions in a rendez-vous system, caught by Pim Kars.

===== 2.8.0 -  19 March 1996 ====

- new version of the Spin sources that can be compiled, installed, and
  used successfully on PC systems running Windows95.
  (Because of remaining flaws in the latest Tcl/Tk 7.5/4.1 beta 3
   release, Xspin will not run on Windows 3.1 systems.  Spin itself
   however will work correctly on any platform.)
  to compile, you'll need the public domain version of gcc and yacc for PCs,
  (see README.spin under Related Software, for pointers on where to
  get these if you don't already have them)

  to use Spin on a PC, compile the Spin sources with directive -DPC
  (if you have no `make' utitility on the PC, simply execute the
  following three commands to obtain a spin.exe
        byacc -v -d spin.y
        gcc -DPC *.c -o spin
        coff2exe spin
  alternatively, use the precompiled spin.exe from the distribution
  (contained in the pc_spin280.zip file)

- small extension of xspin - lines with printf("MSC: ...\n") show up
  in xspin's graphical message sequence chart panel. the colors can now
  also be changed from the default yellow to red green or blue,
  respectively, as follows;
        printf("MSC: ~R ...\n")
        printf("MSC: ~G ...\n")
        printf("MSC: ~B ...\n")
  (suggested by Michael Griffioen, The Netherlands)
- small changes to improve portability and ANSI compliance of the C code
- compile-time option -DREDUCE (partial order reduction) is now the
  default type of verification.  both spin and xspin now use this default.
  to compile a verifier without using reduction, compile -DNOREDUCE
- missed case of syntax check for use of _ as lvalue corrected
- missed case of printing mtype values in symbolic form also corrected
- printfs no longer generate output during verification runs
  (this was rarely useful, since statements are executed in DFS search
  order and maybe executed repeatedly in seemingly bewildering order)
  a compile time directive -DPRINTF was added to suppress this change
  (this may be useful in debugging, but in little else)
  this relies on stdarg.h being available on your system - if not, compile
  Spin itself with -DPRINTF, and the new code will not be added.

===== 2.8.1 -  12 April 1996 ====

- we found a case where the partial order reduction method
  introduced in Spin version 2.0 was not compatible with
  the nested depth-first search method that Spin uses for
  cycle detection (i.e., runtime options -a and -l)
  the essence of the problem is that reachability properties
  are affected by the so-called `liveness proviso' from the
  partial order reduction method.  this `liveness proviso'
  acted on different states in the 1st and in the 2nd dfs,
  which could affect the basic reachability properties of states.
  the problem is corrected in 2.8.1.  as a side-effect of this
  upgrade, a few other problems with the implementation of the
  nested depth first searches were also corrected.  in some cases
  the changes do cause an increase of memory requirements.
  a new compiler directive -DSAFETY is added to make sure that
  more frugal verifiers can be produced if liveness is not required.
- other fixes - one small fix of interactive simulation mode -
  some small fixes to avoid compiler warnings in tl_parse.c -
  a fix in pangen3.h to avoid a compile-time error for a few
  cases of index bound-checking. small fixes in tl_buchi and
  tl_trans to correct treatment of "[]true" and "[]false"
- cosmetic changes to the xspin tcl/tk files

===== 2.8.2 -  19 April 1996 ====

- revised Doc/WhatsNew.ps to match the extensions in the
  current version of the software
- one more change to the algorithm for acceptance cycle detection
- changed filenames for multiple error-trails (to ease use on PCs)
  from spec.trail%d to spec%d.trail
- some small changes to improve portability

===== 2.8.3 -  23 April 1996 ====

- corrected a missed optimization in the new acceptance cycle detection
  algorithm from 2.8.[12]
- corrected a problem with blocking atomic sequences in pangen1.h
- added a predefined function predicate np_
  the value of np_ is true if the system is in a non-progress state
  and false otherwise.  (claim stutter doesn't count as non-progress.)
  np_ can only be used inside never claims, and if it is used all
  transitions into and out of progress states become visible/global
  under the partial order reduction
- background:
  the intended purpose of np_ is to support a more efficient check
  for the existence of non-progress cycles. (the efficient check we
  had was lost with the changes from 2.8.[12])  instead of the default
  check with runtime option -l, a more efficient method (under partial
  order reduction) is to use the never claim:
        never {
                /* non-progress: <>[] np_ */
                do
                :: skip
                :: np_ -> break
                od;
        accept: do
                :: np_
                od
        }
  and to perform a standard check for acceptance cycles (runtime
  option -a) -- the partial order reduction algorithm can optimize
  a search for the existence of acceptance cycles much better than
  one for non-progress cycles.
  a related advantage of searching for non-progress cycles with an
  LTL property is that the LTL formula (<>[] np_) can easily be
  combined with extra LTL properties, to built more sophisticated
  types of searches.

===== 2.8.4 -  25 April 1996 ====

- cycles are closed at a different point in the dfs with the change from
  2.8.[12], as a result, the cycle-point was no longer accurate - which
  could be confusing.  fixed
- all moves through progress states and accepting states within the program
  are visible under the partial order reduction rules.  it is unlikely that
  one would use extra accept labels in a program, if an LTL property or a
  never claim with accept labels is used, but just in case, this is covered.

===== 2.8.5 -  7 May 1996 ====

- process creation and process deletion are global actions
  they were incorrectly labeled as safe/local actions for the
  purposes of partial order reduction.  they are global, because
  the execution of either one can change the executability of
  similar actions in other processes
- didn't catch as an error when too many message parameters are
  specified in a receive test q?[...] (in verifications).
  it was reported in all other cases, just not for queue tests
  (the simulator reported it correctly, when flag -r is used)
- peculiar nestings of array and non-array structure elements
  could generate incorrect code
- with fairness enabled (-f), cycles were sometimes closed at the
  wrong place in the runtime verifiers.
- a variable initialized with itself could cause spin to go into
  an infinite loop.  the error is now caught properly.

===== 2.8.6 -  17 May 1996 ====

- timeout's weren't always marked as global actions in partial
  order reductions - they are now -- this can cause a small increase
  in the number of reached states during reduced searches
- fixed error that could cause a coredump on a remote reference
  during guided simulations (reported by Joe Lin, Bellcore)
- improved the efficiency of partial order search for acceptance
  cycles in bitstate mode. (for non-progress cycles, though, we still
  can't take much advantage of reduction during bitstate searches)
- fixed the error that caused the extent of a cycle not to be
  marked correctly in bitstate mode (the trails were always correct,
  but the cycle point was sometimes placed incorrectly)
- fixed error that could cause non-existent acceptance cycles to
  be produced in bitstate mode (hopefully the last aftershock from
  the correction of the cycle detection method in version 2.8.1)

===== 2.9.0 -  14 July 1996 ====

- Important Change:
  Spin now contains a predefined never claim template that captures
  non-progress as a standard LTL property (it is the template described
  under the notes for 2.8.3 above)
  this made it possible to unify the code for -a and -l;  it brings
  option -l (non-progress cycle detection) within the same automata
  theoretic framework as -a;  and it secures full compatibility of
  both options -a and -l with partial order reduced searches.

  compiled versions of pan.c now support *either* -a *or* -l, not both

  by default, the verifiers check for safety properties and standard
  buchi acceptance (option -a).
  to search for non-progress cycles (i.e., to *replace* option -a with
  option -l), compile the verifier with the new directive -DNP
- Xspin 2.9.0 supports this change, and makes it invisible to the user.

- the state vector length is now added explicitly into the state vector.
  in virtually all cases this is redundant, but it is safer.
  it can optionally be omitted from the state vector again (saving
  4 bytes of overhead per state) with the new compiler directive -DNOVSZ

- the verifiers didn't allow a d_step sequence to begin with a
  rendez-vous receive operation.  that's now fixed.

- change in the as-yet non-documented mode for extra agressive
  state compressions (added in version 2.7.4, not enabled yet for
  normal use - more information on this mode will come later)

- assignments to channel variables can violate xr/xs assertions.
  there is now a check to catch such violations

- updated the PC executable of xspin for the newer current version of
  gcc - updated the readme files to match the above changes

- added the code for handling the Next Operator from LTL.  the code is
  not yet enabled (to enable it, compile the sources with -DNXT added).
  note that when partial order reduction is used this operator cannot
  be used.  we'll figure out the appropriate warnings and then enable
  the code (i.e., when you use it, you must compile pan.c with -DNOREDUCE).
- in the process of this update, we also caught a bug in the translation
  of LTL formulae into never claims (affecting how the initial state of
  the claim was encoded).  the implementation has meanwhile been subjected
  to a more thorough check of the correctness of the translation -- using
  another model checker (cospan) as a sanity check. (both model checkers
  have passed the test)

===== 2.9.1 -  16 September 1996 ====

- no major changes - some purification and minor fixes
- updated email address for bug reports to bell-labs.com in
  all source files
- disallowed remote references inside d_step sequences
  (the verifier has no problem, but the simulator may
  resolve these differently can cause strange guided
  simulation results)
- provided some missing arguments to a routine in pangen1.c
  that could trigger compile time errors before
- improved the COLLAPSE modes to be slightly more frugal
- added explicit casts from shorts to ints to avoid warnings
  of some compilers...  also fixed a possible bad reference
  to the stack if an error is found in the first execution step
- fixed a case where the cycle-extent wasn't set correctly
  (found by stavros tripakis)
- write and rewrite just a single trail-file for options -[iI]
  (instead of numbered trails)
- fixed a bug in weak fairness cycle detection that had crept
  in with the overhaul from version 2.8
- fixed order of variable initialization in simulator (can
  make a difference if a local variable is initialized with
  the value of a parameter, which should now work correctly)
- expanded the number of options accessible through Xspin

===== 2.9.2 -  28 September 1996 ====

- with a -c0 flag, the 2.9.1 verifiers would still stop at the
  first error encountered, instead of ignoring all errors.
  has been corrected (-c0 means: don't stop at errors)
- corrected the instructions and the numbers in Test/README.tests
  for the current version of spin (for leader and pftp there are
  some small differences)

===== 2.9.3 -  5 October 1996 ====

- added a function eval() to allow casting a variable name into
  a constant value inside receive arguments.  this makes it possible
  to match a message field with a variable value, as in
        q?eval(_pid),par2,par3
  until now, only constant values could be matched in this way.
  note that in the above example the value of _pid does not change,
  but it guarantees that the receive is unexecutable unless the first
  message parameter is equal to the value of variable _pid
  eval() can be used for any message field - the argument must be a
  (local or global) variable reference (not be a general expression).
- in the process, discovered that global references inside the parameter
  list of send or receive statements would not be detected for the
  marking of safe and unsafe statements for the partial order reduction.
  this is now corrected - it may lead to a small increase in the number
  of reachable states under partial order reduction

===== 2.9.4 -  4 November 1996 ====

- the order of initialization of parameters and local variables after
  a process instantiation was incorrect in the verifier - this could
  be noticed when a local var was instantiated with a formal parameter
  inside the variable declaration itself (the verifier failed to do this).
- added a missing case for interpreting eval() in run.c (see 2.9.3)
- removed possible erroneous behavior during interactive simulations
  when a choice is made between multiple rendez-vous handshakes
- added SVDUMP compiler directive and some extra code to allow for the
  creation of a statespace dump into a file called sv_dump
- added an option in Xspin to redraw the layout of an FSM-view using
  the program 'dot' -- the option automatically enables itself if xspin
  notices that 'dot' is available on the host system (an extra button
  is created, giving the redraw option)

===== 2.9.5 -  18 February 1997 ====

- thoroughly revised -DCOLLAPSE -- it can now be used without
  further thought to reduce memory requirements of an exhaustive run
  by up to 80-90% without loss of information.  the price is an
  increase in runtime by 2x to 3x.
- added new compiler directives -DHYBRID_HASH and -DCOVEST
  (both for experimental use, see the Pan.Directives file)
- renamed file sv_dump (see 2.9.4) to 'spec'.svd, for compatibility
  with PCs
- removed spin's -D option (dataflow).  it was inaccurate, and
  took up more source code than warranted (300 lines in main.c and
  another 60 or so in Xspin)

===== 2.9.6 - 20 March 1997 ====

- bug fix -- for vectorsizes larger than 1024 the generated
  code from 2.9.5 contained an error in the backward execution
  of the transition for send operations.  (this did not
  affect the verification unless a compiler directive -DVECTORSZ=N
  with N>1024 was used -- which triggered an error-report)
- sometimes one may try typing 'pan -h' instead of 'pan -?'
  to get the options listing of the verifiers.  this now gives
  the expected response.
- previous versions of the spin Windows95 executable in pc_spin*.zip
  were compiled as 16-bit executable -- the current version is a
  32-bit executable.  the newer versions of tcl/tk actually care
  about the difference and will hang if you try to do a simulation
  run with one of the older spin executables installed...
- discrepancy in the stats on memory use reported at the end of a
  bitstate run corrected.
- new xspin295 file that corrects a problem when xspin is used on
  unix systems with a file name argument (it reported an undeclared
  function).

===== 2.9.7 - 18 April 1997 ====

- spin now recognizes a commandline option -P that can be used to
  define a different preprocessor.  the default behavior on Unix
  systems corresponds to:
        spin -P/lib/cpp [..other options..] model
  and on solaris systems:
        spin -P/usr/ccs/lib/cpp [..other options..] model
  (note, these two are the defaults, so these are just examples)
  use this option to define your own preprocessor for Promela++ variants
- bitstate mode can be made to hash over compressed state-vectors
  (using the byte-masking method).  this can improve the coverage
  in some cases. to enable, use -DBCOMP
- -DSVDUMP (see 2.9.4) now also works in -DBITSTATE mode
- added compiletime option -DRANDSTORE=33 to reduce the probability of
  storing the bits in the hasharray in -DBITSTATE mode to 33%
  give an integer value between 0 and 99 -- low values increase
  the amount of work done (time complexity) roughly by the reverse
  of the probability (i.e., by 5x for -DRANDSTORE=20), but they also
  increase the effective coverage for oversized systems. this can be
  useful in sequential bitstate hashing to improve accumulative coverage.
- combined the 3 readme-files into a single comprehensive README.

===== 3.0.0 - 29 April 1997 ====

- new additions to Spin's functionality that motivates upping the
  version number to 3.0:

        1. a new BDD-like state compression option based on
           the storage of reachable states in an automaton,
           combined with a checkpoint/recovery option for long runs.
           for the automata based compression, compiled -DMA=N
                with N the maximum length of the statevector in bytes
                expected (spin will complain if you guess too low)
           for checkpointing, compile -DW_XPT
                to get a checkpoint file written out every multiple
                of one million states stored
           for restarting a run from a checkpoint file, compile -DR_XPT

        2. addition of "event trace" definitions. for a description
           see Section 4 of the extended WhatsNew.ps

        3. addition of a columnated simulation output mode
           for raw spin that mimicks the view one could so
           far only obtain with through the intermediacy of
           xspin. to use, say:
                spin -c spec (or spin -t -c spec)
           there is one column per running process.  message send
           or receive events that cannot be associated with a process
           for any reason are printed in column zero.

        4. addition of a Postscript output option to spin.
           this can be used to create a postscript file for a message
           flow of a simulation, without needing the intervention of
           xspin (which can be slow).
                spin -M spec
           generates the message flow in file spec.ps
           also supported is:
                spin -t -M spec
           to convert an error trail into postscript form.

        5. addition of the ability in Xspin to automatically
           track variable values -- by prefixing their declaration
           in Promela with the keyword "show", e.g. "show byte cnt;"
           also added: automatic tracking of the state changes in
           the never claim, if present, during guided simulations
           (i.e., when inspecting an error.trail produced by the
           verifier)

        6. addition of an option to convert LTL formula stored in files.

        7. Xspin is now compatible with Windows95 and WindowsNT

smaller, changes
        - spin generates hints when the data-type of a variable is
          over-declared (i.e., it will detect the use of integers for
          storing booleans etc.)
        - the spin -d output for structure variables now includes the
          name of the structure declaration (as the 3rd field, which
          was unused in this case) to make the listings unambiguous.
          [change from Frank Weil]
        - spin -t can now take an argument.  without an argument
                spin -t spec opens spec.trail
                spin -t4 opens spec4.trail
          (multiple trails are generated with runtime option
                pan -c0 -e)
        - bugfix: local channels were not always restored correctly to
          their previous state on the reverse move of a process deletion
          in the verification (i.e., the deletion of the process to which
          those channels were local).
        - bugfix: stutter moves were only done in the 2nd dfs, to close
          cycles. this has to be done in both 1st and 2nd, to avoid missing
          the valid stutter extension of some finite behaviors
        - process death is now a conditionally safe action -- this partly
          reverses a decision made in version 2.8.5.
          the condition for safety is: this is the youngest process and
          there are fewer than the max nr of processes running.  this means
          that the action cannot enable any blocked run statements, although
          it may enable more process deaths (i.e., of processes that now
          become youngest).
          it does imply that a process dies as quickly as possible.  allowing
          them to also linger merely creates articifial execution scenarios
          where the number of active processes can grow without bound.
          compatibility with 2.8.5-2.9.7 on this issue can be forced by
          compiling pan.c with -DGLOB_ALPHA
        - atomics inside atomics or dsteps are now accepted by the parser,
          and ignored.
        - there is now a Syntax-Check option in Xspin
          [suggested by Klaus Havelund]
        - true and false are now predefined constants

Subsequent updates will appear in a new file: V3.Updates