--- /dev/null
+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
projects / lttv.git / blobdiff