X-Git-Url: http://git.lttng.org/?a=blobdiff_plain;ds=inline;f=verif%2FSpin%2FDoc%2FV2.Updates;fp=verif%2FSpin%2FDoc%2FV2.Updates;h=0000000000000000000000000000000000000000;hb=a219d12930979a81f43a3a3f5499b2bd00141a84;hp=bfca262081e78bb5fda33d7be537b6f1e920203c;hpb=31efe1f8304f09a4f4139c387a98d3215cd423c9;p=lttv.git diff --git a/verif/Spin/Doc/V2.Updates b/verif/Spin/Doc/V2.Updates deleted file mode 100755 index bfca2620..00000000 --- a/verif/Spin/Doc/V2.Updates +++ /dev/null @@ -1,1163 +0,0 @@ -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