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? - fifo poll, exactly as A, but the message is not removed from the channel F. q?? - 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 typedef 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 button to most text windows (to clear the contents of the display) - added and 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 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 (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