+++ /dev/null
-Distribution Update History of the SPIN sources
-===============================================
-
-==== Version 3.0.0 - 12 August 1997 ====
-
-A new release, a new V3.Updates file. See the end
-of the V2.Updates file for the main changes between
-the last version 2.9.7 and the new version 3.0.0.
-
-Spin Version 1 lasted from Jan. 1990 - Jan. 1995.
-Spin Version 2 lasted from Jan. 1995 - August 1997.
-
-The shell script upgrade2 will take any version of
-Spin between version 2.7 and 2.9 to version 3.0.
-Upgrades from 3.0 forward will appear in a new shell
-script upgrade3, to keep the file small.
-
-==== Version 3.0.1 - 19 August 1997 ====
-
-- on older PC's the hashing behavior could be substandard.
- on those systems an int is often interpreted as a 16 bit,
- instead of a 32-bit quantity. the fix made is to declare
- the relevant variables as long integers instead of plain
- integers. there is no visible difference for other systems.
-- printf accidentily picked up a redundant newline in 3.0.0
- it is gone again.
-- interactive use of spin models with rendez-vous statements
- could get hung in some cases.
-
-==== Version 3.0.2 - 24 August 1997 ====
-
-- improved the fix for interactive use of rv's from 3.0.1
-- the parser now catches the use of 'run' to initialize
- global variables as an error.
-- the parser now catches the use of any initializer on
- a formal parameter in a proctype as an error.
-- addition of a new datatype to Promela: unsigned
- usage:
- unsigned name : 3;
- declares 'name' to be a variable that can hold unsigned
- values -- stored in 3 bits (i.e., values 0..7 inclusive).
- values outside the declared range are truncated to the
- range on assignments
-- d_step may now appear inside and atomic and vice versa
-- extra option -E to pass arguments to the C preprocessor
- usage:
- spin -E-Dfoo=faa filename
- to redefined foo as faa in the filename
- spin -Pmy_cpp -E-E filename
- use my_cpp as the preprocessor (replacing cpp) and
- pass it flag -E when it is called.
-
-==== Version 3.0.3 - 8 September 1997 ====
-
-- unsigned variables weren't cast correctly during
- simulation runs --
-- warnings about variables being of too generous a type
- are now only generated when the -v verbose option is set
-- extra warnings, on use of channels, are now also
- generated with spin -v -- still more with spin -v -g
-- can now pass directives to the preprocessor with a simpler
- spin option -D..., e.g., spin -DLOSS=1 spec
- the earluer -E-D... also still works
-- a few more additions to xspin303.tcl
-
-==== Version 3.0.4 - 25 October 1997 ====
-
-- now accepts truncated extensions of pan.trail
- (often visible only as pan.tra) on PCs
-- now recognizes compiler directive __FreeBSD__
-- redundant include file <malloc.h> deleted from main.c
-- now properly initializes all channels hidden in typedef
- structures
-- made it possible to generate structural views of the
- promela model, but tracking channel uses (more to come)
-- added pc_zpp.c to the sources - used only on the pc
-
-==== Version 3.0.5 - 5 November 1997 ====
-
-- corrected bug in the builtin macro preprocessor of the
- PC-version (only) of spin. if the first literal match
- of the macro source failed to be a valid replacement string,
- no further matches were tried on that line
-- corrected bug in interactive simulation mode that could
- cause a failure to return control to the user
-
-==== Version 3.0.6 - 16 December 1997 ====
-
-- a value that is truncated in an assignment to a variable
- of a small type triggered an error message that sometimes
- could cause xspin to miss a display update for the variable
- values pannel.
-- on a -c flag spin was a little too talkative, assuming also
- a -v verbose flag for the final detail printed at the end of
- a simulation run.
-- fixed an error in the processing of logical OR in the presence
- of the X operator in LTL formulae -- this only affected the
- outcome of a translation if Spin was compiled with -DNXT
- to enable the LTL next-time operator (this is not enabled by
- default, because it jeopardizes compatibility with the partial
- order reductions)
-- a check for non-progress, in combination with provided clauses
- on proctypes, could fail. the omission was that the never claim
- process searched for its own provided clause, which should in
- this case default to true.
-- the restriction that the use of any provided clause voided the
- partial order reduction was much too strict: it suffices to mark
- all statements in only the proctype that is labeled with a
- provided clause unsafe -- other processes are not affected.
-- added new Test/pathfinder example to the Test directory,
- illustrating the use of provided clauses
-- the standard stutter extension on finite sequences is not
- allowed to produce non-progress cycles, but in combination with
- the weak-fairness option this erroneously could happen.
- (stutter-extension on temporal claim matches is only applied
- to standard acceptance properties, under runtime option -a)
-- there was an error in the implementation of weak fairness
- that could cause the algorithm to miss matching acceptance or
- non-progress cycles with weak-fairness enabled. a small change
- in the implementation of this option (incrementing the Choueka
- counter values by 1) repairs this flaw.
-
-==== Version 3.0.7 - 18 December 1997 ====
-
-- the check on a self-loop, added in 3.0.6, unintentionally also
- ruled out self-loops in never claims, which are harmless (e.g.,
- to allow for a finite prefix of 'true' propositions).
-
-==== Version 3.0.8 - 2 January 1998 ====
-
-- with fairness enabled, a process was considered to be temporarily
- blocked while other processes performed a rv handshake. this
- could cause a cycle to be reported as fair that normally would not
- be considered as such. fairness rule 2 was updated to avoid this.
-- an assignment beginning a dstep sequence was incorrectly considered
- to be executable in the middle of a rendezvous handshake in progress
- elsewhere.
-
-==== Version 3.0.9 - 11 January 1998 ====
-
-- rendezvous communications lacked an arrow in the new postscript
- output generated with spin option -M
-- new predefined channel name STDIN for reading a character from
- the standard input as in:
- chan STDIN;
- short c;
- do
- :: STDIN?c ->
- if
- :: c == -1 -> /* EOF */
- break
- :: else ->
- printf("%c", c)
- fi
- od
-- to match this, added support for recognizing character
- symbols in Promela such as 'i', '\n', '\t', '\r', etc.
-- fixed the bug that prevented weak fairness from being
- turned off during verifications.... (bug introduced in 3.0.8)
-- small improvements in error catching (mostly related to
- illegal structure references)
-
-==== Version 3.1.0 - 27 January 1998 ====
-
-- all transitions from a local process state that is referenced
- within the never claim (or ltl property) are now properly labeled
- as unsafe in the partial order reduction
-- a d_step that appears at the last statement in a proctype no longer
- generates an error in the simulator
-- the predefined variable _last is now updated correctly during the
- verification process (thanks Pedro Merino for the examples)
-- weak fairness is now considered incompatible with partial order reduction
- in models that contain rendezvous operations (thanks Dennis Dams for
- the example that revealed this)
-
-==== Version 3.1.1 - 28 January 1998 ====
-
-- fixed a goof in pc_zpp.c -- only visible in the precompiled PC
- version. symptom: it would fail to expand some macros with the
- builtin version of cpp. in particular, it would fail on the
- testcase: Test/leader from the distribution (thanks Mike Ferguson).
-
-==== Version 3.1.2 - 14 March 1998 ====
-
-- added a Cut/Copy/Paste meny to the text window of xspin version 3.1.2
- (big convenience), plus a few smaller fixes
-- the verifiers generated by spin have two extra run-time options:
- -E to ignore all invalid endstate errors
- -A to ignore all assert() violations
-- added #include <strings.h> to pan.c
-- main in pan.c is now properly typed 'int' instead of 'void'
-- the following change, introduced in 2.9.0, was unnecessary
- - assignments to channel variables can violate xr/xs assertions.
- there is now a check to catch such violations
- the check is removed:
- when an xr channel variable is assigned to, it's old value is simply lost.
- it was the old value (operations on the channel that the value pointed
- to) that the xr/xs assertion applied to, not to the variable name as such.
- operations on the new channel id that the variable now points to
- are subject to the same xr/xs claims as the old one did.
-- new argument to spin:
- spin -N claimfile ... promelaspec
- reads the never claim from 'claimfile'
- (the main filename 'promelaspec' is always the last argument)
-- new argument to spin
- spin -C promelaspec
- prints some channel access info on stdout, useful for producing
- a structural view of the system
- (used to be an added output in spin -v)
-- fixed bug in pan.c that caused some states created during claim stutter
- from not being removed from the dfs stack. should rarely have occured.
-- all the above extensions are supported in Xspin 3.1.2
-- redesigned Xspin's LTL properties management dialogue panel
-- fixed problem with hanging of long simulations on pc's
- (a buffer overflow problem internal to windows95/nt)
-
-==== Version 3.1.3 - 16 March 1998 ====
-
-- small bug fix in sym.c -- reported too many variables as
- unused on a spin -a -v spec
-- small bug fix in xspin312.tcl -- replaced "else if" with "elseif"
-- both bugs reported by Theo Ruys within hours after the release of 3.1.2
- thanks Theo!
-
-==== Version 3.2.0 - 7 April 1998 ====
-
-- a modest extension of the language:
- there is now a procedure-like construct that should reduce the need
- for macros. Promela 'inline' functions preserve linenumber
- references in simulations (at least, that's the idea).
- an inline definition look like this (appearing outside all proctypes)
-
- inline functionname(x, y) {
- ...a promela fragment...
- }
-
- a call looks like this -- and can appear wherever a statement can appear:
-
- functionname(4, a);
-
- the replacement text is inlined by the parser, with proper parameter
- matching and replacement.
- inlines can be recursive (one inline can call another), but not cyclic.
-
- there is still no local scope for variables. this means that the scope
- of any local variable declared is always the entire proctype body --
- no matter where it is declared.
- local variables may be declared at the start of an inline -- but such
- variables have the same status as a local variable at the place of the call.
-
-- added an example to the Test directory, illustrating inlines (Test/abp)
-
-- timeout is no longer automatically enabled and available as a
- user-selectable option during interactive simulation. it could cause
- counter-intuitive behavior, e.g. when the timeout was used in an unless-
- escape
-- 'else' is now flagged as unexecutable when appropriate during interactive
- simulations -- where possible it is offered as a choice so that an
- execution can be forced in a given direction.
-- small fixes and fiddles with xspin
-
-==== Version 3.2.1 - 4 July 1998 ====
-
-- added compile time directive HC, for a version of Wolper's hash-compact
- algorithm. it can speed up the search, and reduce memory requirements,
- with a relatively low probability of hash-collisions (or missed states).
- this is a modification of exhaustive search where we store a 32-bit
- hash-value in the hash-tables, as a compressed state vector.
- the effective size of the compressed state-vector is the width of the
- hash-table itself (controlled by the runtime -w parameter) plus 32 bits
- (by default this is: 18+32 = 50 bits of information).
- the hash-table entries have some additional overhead which pushes total
- memory usage slightly higher -- but the memory reductions can be quite
- substantial (depending, trivially, on the length of the state vector
- without compression)
- to enable: compile pan.c with -DHC (perferably combined with -DSAFETY)
-- fixed fgets problem discovered by Theo Ruys
- (problem: newlines could accidentily be added to the input text)
-- fixed two bugs in dstep code generated in pan.c; improved error reporting
-- fixed bug in processing of include files, when an ltl claim is used
-
-==== Version 3.2.2 - 21 July 1998 ====
-
-- generalized the hash-compact implementation
- by default (compiling pan.c with -DHC) 6 bytes are stored:
- 4 bytes from the first hash and 2 bytes from a second hash
- this gives 32+16 = 48 bits of information, which should secure
- a very low collision probability
- alternatives are -DHC0 (for 32 bits) -DHC1 (for 40 bits) -DHC2 (48 bits)
- and -DHC3 (56 bits).
-- reversed the order in which the transitions in a never claim are
- generated -- this tends to shorten the counter-examples generated
- (by putting the 'true' self-loops that at the end of the list, rather
- than at the beginning). Thanks to Dragan Bosnacki.
-- fixed a bug in xspin.tcl that could cause the application to hang
- when used on a PC (e.g., any simulation of leader...).
- (this synchronization bug was introduced in 3.1.4.)
-
-==== Version 3.2.3 - 1 August 1998 ====
-
-- an atomic that ends with a jump into another
- atomic sequence, now connects correctly without
- breaking atomicity
-- the choice of a rendezvous partner for send operations
- wasn't random during simulations (when multiple targets
- for the rendezvous are available). it is now.
-- fix in xspin to avoid confusion between proctype names
- with a common prefix, in rendering an automaton view
-- fix in pc_zpp.c for occasional incorrect comment processing
- and incorrect #define processing (affected the PC version only)
-
-==== Version 3.2.4 - 10 January 1999 ====
-
-modifications:
-- replaced type "unsigned" in parameter to Malloc and emalloc
- with "unsigned long long" to support 64 bit word size machines
- (thanks to Judi Romijn's experiments at CWI)
- (may not be recognized by non-ansi standard c-compilers)
-extensions:
-- added a runtime flag -J for both spin (simulations) and
- for pan (verification runs), to specify that nested unless
- clauses are to be evaluated in reverse order from the default
- (to match java semantics of catch clauses) at the request
- of Klaus Havelund.
-- added runtime flags -qN and -B for spin (simulations)
- -q4 suppresses printing output related to queue 4
- -B suppresses printing the final wrapups at the end of a run
-- added runtime flag -v for pan (verification) to add filenames
- to linenumbers in the listings of unreached states (xspin does
- not support these extensions yet)
-bug-fixes:
-- a very long source statement could overflow an internal
- buffer in pan.c, upon the generation of a trail-file.
- (thanks for Klaus Havelund's experiments with a java->spin
- translator)
-- compilation with a vectorsize greater than 1024 could cause
- the model checker to behave incorrectly in cases when receive
- statements were used that received data into global variables
- (instead of locals). this now works correctly.
-- removed bug in the optimization code of the ltl-translation
- algorithm -- it could remove untils in cases such as
- p /\ (q U r) not only if p==r, but also if p appeared within r
-- line numbers could be inaccurate if #if 0 ... #endif directives
- were used inside inline declarations. corrected.
-- fixed a bug in ltl translation due to a failure to recognize
- 'true' to be part of any 'and' form -- should have been a rare
- occurrence.
-- fixed a bug that affected the use of rendezvous statements in
- the guard of an escape clause of an unless
-
-==== Version 3.3.0 - 1 June 1999 ====
-
-- rearranged code to share code for identical cases
- in pan.m and pan.b -- this reduces the file sizes by up
- to 60% and similarly reduces compilation times for pan.c
-- added pan.c compiler directive MEMLIM
- compiling pan.c with -DMEMLIM=N will restrict memory use
- to N Megabytes precisely; this is an alternative to the
- existing limit -DMEMCNT=N which restricts to 2^N bytes
- and gives less precise control.
-- added new data declaration tag 'local' which can be used
- wherever currently 'show' or 'hidden' can be used.
- it allows one to identify global variables that are
- effectively local (used by only 1 process) as data objects
- of which manipulation is safe for partial order reductions.
- there's no check for the validity of the tag during verification.
-- automatically hide unused or write-only variables
- option can be turned off with spin option -o2
-- eval() (used in receive statements to turn a variable into
- a constant value) can now contain an arbitrary expression,
- instead of just a name (request of Victor Bos).
-- it is no longer an error to have multiple mtype definitions
- (they are catenated internally)
-- more verbose error-trails during guided simulations - in verbose
- mode it now includes explicit mention of never claim moves, if
- a never claim is involved
-- added also an experimental option to generate code separately
- for the main system and for the never claim - this makes
- separate compilation possible. the option will be finetuned
- and documented once it has settled. for the time being, they
- are not listed in the usage listings.
-- also added, but not enabled, fledgling support for a bisimulation
- reduction algorithm that might be applied to never claims to
- reduce their size (inspired by work of Kousha Etessami),
-
-- bugfixes (the first two found by Wenhui Zhang):
- - in fairness option (could miss a fair cycle)
- - in implementation of the -DMA option (could incorrectly
- claim an intersection of the 1st dfs stack an declare a
- cycle when none existed)
- - in the conversion of ltl formulae to automata (could
- occassionaly fail to match common subexpressions)
- - bug fix in the runtime code for random receive, fixed
- - fixed execution of atomics during interactive simulation
- - fixed possibly erroneous marking as 'dead' variables used
- to index a structure variable array
-
-- during interactive simulation, to avoid confusion, choices
- between different *escapes* on a statement are no longer offered
- in user menus, but are now always resolved by the simulator
-- removed all uses of "long long" and replace with "long."
- the former (temporarily used in 3.2.4) is not in ansi c,
- and the latter will be interpreted correctly on 64bit machines
- by a 64bit compiler.
-- added better support for 64bit machines -- avoiding deteriorated
- performance of the hashing algorithms (courtesy Doug McIlroy)
-- the pc version could get the linenumber references wrong after
- multiline comments - now repaired (courtesy Mike Ferguson)
-- removed bug in xspin.tcl that prevented the selection of
- bitstate hashing from the ltl properties manager panel
- (courtesy Theo Ruys)
-- added an option in xspin to exclude specific channels from the
- msc displays (you have to know the channel number though)
-- fixes in the interactive simulation model (courtesy Judi Romijn)
- - d_steps and atomics now always run to completion without
- prompting the user for intermediate choices that could break
- the atomicity (and the semantics rules).
- - unless escapes no longer reach inside d_steps (they do reach
- inside atomics)
-- merges sequences of safe or atomic steps -- a considerable speedup
- this behavior can be disabled with spin option -o3
-- computes precondition for feasibility of rv - this option can be
- enabled with spin option -o4 -- it seems of little use in practice
-- dataflow analysis -- can be disabled with spin option -o1
-- partial evaluation to remove dead edges from verification model
- (i.e., with a constant 'false' guard)
-- added pan compile time option -DSC to enable new stack cycling option.
- this will swap parts of deep stacks to a diskfile with only low overhead.
- it needs no further user action to work -- the runtime -m flag
- remains, but now simply sets the size of the part of the stack
- that is in core (i.e., you need not set it explicitly unless you want to)
-- added pan compile time option -DLC to optinally use hashcompacted stackstates
- during Bitstate runs. it is slower by about 20-30%, but in cases
- where -DSC is used (very deep stacks) it can safe a lot of extra memory.
- for this reason -DSC always enables -DLC by default
-
-==== Version 3.3.1 - 12 July 1999 ====
-
-- fix in pangen2.h, to avoid a null-pointer reference
- in the automata preparation routines. it can occur in some cases
- where progress labels are used in combination with p.o. reduction
-- fix for weak-fairness in combination with p.o. reduction and
- unless/rendez-vous (courtesy Dragan Bosnacki)
-- fix to prevent an infinite cycle during the weak-fairness based
- verifications. (when both the 2nd and the 1st dfs stacks are
- intersected with a non-zero choueka counter value, the search
- used to continue - instead this should be treated as a regular
- stack match)
-- better feedback on spin -a when parts of the automaton are pruned
- due to constant false guards
-- added spin option -w (extra verbose) to force all variable
- values to be printed at every execution step during simulations
-
-==== Version 3.3.2 - 16 July 1999 ====
-
-- correcting an initially erroneous fix in 3.3.1 that prevented
- compilation alltogether for sources generated through xspin. (...)
- (it left a reference to counters used in the weak fairness algorithm
- in the code that had to be suppressed if weak fairness isn't used)
-
-==== Version 3.3.3 - 21 July 1999 ====
-
-- fix in the new code for dataflow analysis. in some cases a core-dump
- could result if a particular control-flow structure was encountered
- (courtesy Klaus Havelund)
-- updated Xspin to 3.3.3 to deal with the new policy in 3.3 that printfs
- during simulations are always indented by a number of tab-stops that
- corresponds to the process number of the process that executes the
- printf - this makes printfs from the same process line up in columns,
- but it confused xspin. (fix courtesy of Theo Ruys)
-
-==== Version 3.3.4 - 9 September 1999 ====
-
-- new pan option -T to prevent an existing trail file from being
- overwritten (useful if you run multiple copies of pan with
- bitstate hashing and different -w parameters, to optimize chances
- of finding errors fast -- the first run to write the trail file
- then wins)
-- small improvement in error reporting for use of special labels inside
- atomic and d_step sequences
-- small portability change to avoid problems with some compilers (e.g.
- the ones used on plan9)
-- increased some statically defined maxima (e.g. for the max length of
- a single statement - now increased to 2K bytes to avoid problems with
- machine generated Promela files)
-
-==== Version 3.3.5 - 28 September 1999 ====
-
-- two bug-fixes in the ltl->never claim conversion (with thanks to
- Heikki Tauriainen for reporting them)
-- increase in some static buffer sizes to allow for long
- (typically machine generated) variable names
-- removed some debugging printfs
-
-==== Version 3.3.6 - 23 November 1999 ====
-
-- two small extensions and 4 important bug fixes
-
-- added runtime option -t to pan; using pan -tsuf will
- cause error trails to be written into spec.suf instead of
- spec.trail (which remains the default)
-- added a verbose output to the verification runs, to write
- a line of output each time a new state in the never claim
- is reached. this helps keeping track of progress in long
- running verifications -- and helps to avoid false positives
- (i.e., when most states in the never claim are unreached,
- which is a strong indication that the LTL formula that
- produced the claim isn't related to real behavior of the
- system)
-
-- bug fix in the fairness algorithm (-f flag during verification)
- that could cause false error reports to be generated
-- bug fix in the stack cycling compile-time option to pan.c (-DSC)
- which could cause erroneous behavior of the verifier
- (both of these reported by Muffy Calder and Alice Miller)
-- bug fix in the generation of never claims from LTL -- missing
- parentheses around subexpressions in a guard
-- fix to circumvent buggy behavior from gcc on Unix platforms
- (its version of sbrk can return memory that is not properly
- word aligned -- which causes memory faults in pan)
-
-==== Version 3.3.7 - 6 December 1999 ====
-
-- 3.3.6 introduced a bug that prevented the verifier code
- from compiling unless fairness was enabled -- corrected in 3.3.7
-- fixed a minor problem with the as yet unadvertised separate
- compilation option (compiling the program separately from
- the claim to speed up verifications of multiple claims)
-- fixed a bug in the simulation code that could make the
- simulator miss executing statements. it could lead to
- misleading traces for errors. (thanks to an example by Pim Kars)
-
-==== Version 3.3.8 - 1 January 2000 ====
-
-- fixed a bug in the simulation code that caused no output
- to appear, for instance, when the traceback is done with
- a guided simulation for the Test/loops testfile -- fixed
-- fixed bug in the generation of ltl formula of the type:
- <>[]p && []<>q && []<>r
- traced to a mistake in the comparison of states in the
- buchi automaton that could unjustly claim two states to
- be identical even if they differed (reported by Hagiya)
-- added a cast to (double) for manipulation of MEMLIM to
- avoid problems with some compilers
-- added a small optimization that rids the spec of repeated
- sequential skip statements, or skips immediately following
- printfs (these may be present in mechanically generated specs)
-
-==== Version 3.3.9 - 31 January 2000 ====
-
-- fixed several more bugs in the ltl -> buchi automata
- conversion - found with a random testing method
- described by Heikki Tauriainen. the method consists
- of generating random ltl formula with a fixed number of
- propositional symbols, with varying numbers of operators,
- and generating random statespaces over the boolean
- operands, up to preset maximum number of states.
- we've done tests with three databases, consisting of:
- - 27 handpicked standard ltl formulae with up to 4
- operands
- - 5356 random ltl formulae with up to 10 temporal
- operators and up to 3 operands
- - 20577 ltl formulae with up to 3 temporal operators
- and up to 3 operands
- each formula was tested for 25 randomly generated statespaces
- with up to 50 global states.
- we checked spin's automata generation method against an
- independent implementation by kousha etessami, and verified
- that each of the tests either failed with both tools or
- passed with both tools -- any difference pointed to a bug
- in one of the two tools.
- the fixes in spin version 3.3.9 are mostly related
- to the use of the X (next operator -- which is normally
- disabled but can be enabled by compiling the spin sources
- with the extra compiler directive -DNXT) and V (the dual
- of U) in long formula.
-- used the opportunity to add in some more optimizations
- that reduce the size of the automata that are produced
- (which in many cases also speeds up the generation process).
- the optimizations were inspired by kousha etessami's work.
- (email: kousha@research.bell-labs.com)
-
-==== Version 3.3.10 - 15 March 2000 ====
-
-- this should be a final, stable release of spin
- version 3.3, barring the unforeseen.
- we'll move to 3.4.0 in a next round of extensions.
-
-- made the number of active processes a globally visible
- read-only variable: _nr_pr
- this makes it possible to start a process and then wait
- for it to complete:
- run A(); (_nr_pr == _pid+1);
- useful for simulating function calls.
-- the appearance of a timeout in the guard of a d_step
- sequence was treated as an error - it is not treated
- as a warning. (in the guard a timeout is ok)
-- fixed rounding error in calculating the nr of bytes
- to be stored in statevector with -DCOLLAPSE option.
- in rare cases the roundoff error could result in
- missed states when collapse was enabled. reported by
- Dragan Bosnacki.
-- improved ltl->buchi automata conversion some more
- to be described in an upcoming paper by kousha.
-- small update of xspin.tcl -- it failed to record spin
- command line options in the advanced verification options
- panel. reported by Theo Ruys.
-
-==== Version 3.4.0 - 14 August 2000 ====
-
-- fixed two remaining problems with the ltl conversion
- algorithm, related to nested untils and the use of the next
- operator (thanks again Heikki Tauriainen).
-- deals better with renaming files for preprocessing -- no
- longer relies on temporary files residing on the same
- filesystem as the working directory
-- added an alignment attribute for the State vector to force
- gcc to align this structure on a wordboundary (on solaris
- machines gcc apparently considers this optional).
-- fixed two problems in the use of trace-assertions (could
- fail when tracking actions on rendezvous channels)
-- new xspin340.tcl that deals better with non-terminating
- simulation runs on pcs.
-- added support for property-based slicing, to be documented.
- one example in the Test directory illustrates its use: the
- wordcount example.
-- added two examples (mobile[12]) that show how specifications
- in the pi-calculus can be rendered in Promela (thanks Joachim
- Parrow).
-
-==== Version 3.4.1 - 15 August 2000 ====
-
-- fixed problem with spin option -m -- it stopped working after
- the upgrade to spin 3.3.0 a year ago. (Thanks Theo Ruys and Rui Hu).
-- minor twiddles to avoid some spurious warnings from gcc on pan_ast.c
-
-==== Version 3.4.2 - 28 October 2000 ====
-
-- release 3.4.1 had some windows carriage returns in some of the
- source files, which unix compilers don't like - removed
-- two small fixes in the data dependency algorithm, e.g. to make sure
- that an array index is never considered a def
-- made the allignment attribute on the State struct GCC specific
- (which it is -- used only on Solaris)
-- the -o2 flag didn't work as advertised, fixed.
-- fix to prevent problems with too liberal use of sequence brackets
- which could cause a coredump in some cases
-
-==== Version 3.4.3 - 22 December 2000 ====
-
-- small bug fixes, related to the use of {...} for plain sequences
- (other than for atomic or d_step sequences), and the use of
- enabled to refer to the running process in simulation mode
-
-==== Version 3.4.4 - 2 February 2001 ====
-
-- fix of the trace assertion code in pan.c (there was a problem
- when trace assertions were used in combination with rv operations)
-- fix of marking of unreachable states (some reached states could
- erroneously be reported as unreached in some cases)
-
-==== Version 3.4.5 - 8 March 2001 ====
-
-- one more bug found by Heikki Tauriainen - in the LTL -> Buchi
- conversion algorithm. it was caused by an unjustified optimization
- in tl_rewrt.c -- now commented out.
-
-==== Version 3.4.6 - 29 March 2001 ====
-
-- when using rendezvous channels, the compression mask was
- not completely restored on backward moves during the search.
- the correctness of the search was not affected, but the
- number of reached states became larger than necessary
- (up to twice as large as needed). bug fixed.
- (found and reported by Vivek Shanbhag)
-
-==== Version 3.4.7 - 23 April 2001 ====
-
-- fixed a number of small bugs in xspin.tcl (now version 3.4.7)
- (shaded out menu items were not enabled, errors on cancel of
- simulation runs, etc.)
-- pruned the number of unreached states reported, by removing
- reports for internal states (marked ".(goto)" or "goto :b3")
-- fixed bug in pid assignements on guided simulation for np-cycles
-
-==== Version 3.4.8 - 22 June 2001 ====
-
-- more small bug fixes
- e.g., a problem with parameters on inline calls, if the name
- of an actual parameter equals the name of another formal parameter
- in the same inline; a typo in an 'attribute' annotation; some
- missing parameters in rarely executed printf calls
-
-==== Version 3.4.9 - 1 October 2001 ====
-
-- two bug fixes:
- - problem with xr/xs declarations for processes that can be
- instatiated with multiple pids -- could lead to a coredump
- - problem with treatment of merged statements in guided simulations.
- could lead to a statement being printed twice when it only
- occurred once.
-
-==== Version 3.4.10 - 30 October 2001 ====
-
-- two bug fixes:
- - trace assertions were not working correctly, failing to
- reliably generate matches for all channels within the scope
- of an assertion. this was likely broken when statement merging
- was first introduced in version 3.3
- - added protection against the use of pids outside the valid
- range in remote references (i.e., less than 0 or over 255)
-
-==== Version 3.4.11 - 17 December 2001 ====
-
-- a bevy of small bug fixes:
-- during verification, sorted send operations
- (e.g., q!!m) were not reversed accurately, leading to
- potentially inconsistent error trails
-- 'else' was not interpreted correctly when it appeared
- as the first statement of a d_step
-- process death was not in all possible cases considered a safe
- action, and thus could be deferred longer than necessary
-- collapse did not in all cases generate the best compression
-
-==== Version 3.4.12 - 18 December 2001 ====
-
-- correcting a dumn coding error in 3.4.11 that made the
- pan.c source uncompilable..
-
-==== Version 3.4.13 - 31 January 2002 ====
-
-- new option -T, to suppress pid-dependent indenting of outputs
-- new datatype 'pid' for storing return values from run expressions
-
-- improved reporting of unreached states for models with inlines.
-- improved reporting of memory use for bitstate verification runs.
-- fewer unused vars in pan.c for common modes of compilation.
-- during simulation each line of output is now immediately flushed
-- new restrictions on the use of 'run': max 1 run operator per
- expression, and run cannot be combined with other conditionals.
- this secures that if a run expression fails, because the max nr
- of procs would be exceeded, the expression as a whole will have
- no side-effects.
-
-- corrected bug in treatment of parameters to inlines
-- corrected bug that showed up for some bizarre combinations
- of constructs (d_step nested in atomic, embedded in loop)
- sympton was that the spin parser would hang
-- the maximum number of processes during simulation is now
- equal to that during verification (255) - to prevent
- runaway simulations. the exact number can be redefined
- when spin is compiled, by adding a directive, e.g. -DMAXP=512
- similarly the max nr of message channels during simulation
- can be set by compiling spin with a directive, e.g. -DMAXQ=512
- the bounds used during verification (255) cannot be changed.
-
-==== Version 3.4.14 - 6 April 2002 ====
-
-- added new spin option -uN to truncate a simulation run after
- precisely N steps were taken. in combination with option -jM
- this can select step M to N from a very long simulation
- (say guided or random); example: spin -j10 -u20 spec
- prints step 10 up to 20, but nothing else
-
-- corrected important bug introduced in 3.4.13 that caused a
- core dump during verification runs. the bug was caused by
- a poor attempt to correct reporting of unreached states
- due to statement merging effects.
-
-- corrected compilation error for an unusual combination of
- compiler directives
-
-==== Version 3.4.15 - 1 June 2002 ====
-
-- much improved hashfunctions, at the suggestion of Jan Hajek
- from The Netherlands (the original implementor of the Approver
- tool from the seventies).
- this makes for better performance in both exhaustive searches
- (fewer hashcollisions on standard hashtable, therefore often
- faster), in bitstate and hashcompact searches (more coverage).
- the old hashfunctions are reenabled if pan.c is compiled
- with the new directive -DOHASH. the new functions are the default.
-- improved reports of unreachable states, in the presence of
- statement merging.
-- small change in the indenting of printf output -- it now lines
- up better with process columns in -c simulation output
-- fewer compiler warnings
-- some small fiddles with xspin to fix small problems
-- giving up on maintaining the upgrade3 scripts -- they get too
- long and they do not seem to be used much
-
-==== Version 3.4.16 - 2 June 2002 ====
-
-- a bug slipped in in 3.4.15, bitstate verification failed
-- also increased the default memory limit on PCs to 64 Mb
-
-==== Version 3.4.17 - 19 September 2002 ====
-
-- added a function printm(x) to print the symbolic name of
- an mtype constant. this is equivalent to printf("%e", x),
- but can be more convenient.
-- changed the structure of the never claim that is included
- by default if pan.c is compiled for non-progress cycle
- detection with directive -DNP
- the change is to check first for a move to the accepting
- state, rather than last. this reduces the length of
- error trails that are generated, matching the earlier
- change made in version 3.2.2, thanks again to Dragan Bosnacki
- for pointing this out.
-- rearranged the code for pan_ast.c so that it can be compiled
- separately, rather than as an include file of pangen5.c
-- a bug had been hiding in the -DCOLLAPSE memory compression
- option that could in rare cases lead to states being missed
- during a verification
- the bug could be avoided with the optional -DJOINPROCS.
- it is now permanently fixed by extending the nr of bytes
- stored somewhat (the type of each process is now stored
- explicitly in the compressed statevector, to avoid the
- confusion that can result if two processes of the same
- contents but with different types could be created with
- the same pid, but as alternative options from the same
- state -- a case found by Remco van Engelen.
- the fix increases memory use slightly in some case (around
- 10% in many test cases) but retains the greater part of
- the memory compression benefit. if needed, the fix can
- be disabled by compiling pan.c with -DNOFIX
-- pan_ast.c is now a separately compiled file, just like
- all the others, instead of being #included into pangen5.c
-- more attempts to fix the accuracy of reachability reports
-
-==== Version 3.5.0 - 1 October 2002 ====
-
-- variable names starting with an underscore were mistreated
- in the data flow analysis.
-- this is meant to be a stable release of spin version 3, with
- minor changes in contact-information for the new spinroot.com
- website for all documentation, workshop information and
- newsletters.
-
-==== Version 3.5.1 - 11 November 2002 ====
-
-- bug in parsing of remote label references, could cause a
- core-dump of spin -a
-- small additional improvements in reporting of unreachable
- states - to more accurately take into account optimizations
- made in the transition structure before verification starts
-- noted incompatability of combining -DREACH and -DMA
-
-==== Version 3.5.2 - 30 November 2002 ====
-
-- slightly improved line number references in reporting syntax
- errors within d_steps
-- extension: remote references usually are written as:
- proctypename[pid]@labelname
- if there is only one instantiation of the proctype, then the
- pid can more easily be figured out by Spin than by the user,
- so it can, in these cases, now be omitted, making an anonymous
- remote reference possible, as in:
- proctypename@labelname
- if there turn out to be multiple possible matches, Spin will
- warn in simulation mode -- but not in verification mode.
- (the additional check would probably be too consuming).
-- during the execution of a d_step, spin would by default
- still print out every execution step in simulations (under
- the -p option). now it will only do so in verbose mode
- (with also -v).
-- if the last step in an atomic sequence was a rendezvous
- send operation, atomicity would not reliably move with
- the handshake to the receiver. this is fixed.
-- the simulator used a confused method to help the user out
- if the pid of a process was guessed incorrectly in a remote
- reference operation. this is now done more sanely: if a
- variable is used for the pid, the simulator now trusts that
- it was set correctly -- the remote ref will simply fail with
- an error warning if this is not the case. if the user specified
- the pid with a fixed constant, the simulator will now always
- add 1 to the number if the presence of a never claim is detected.
- (this is because behind the scenes the pid's will move up one
- slot to accomodate the claim -- this is always hidden from the
- user -- allowing the user to assume that pids always start at 0).
-
-==== Version 3.5.3 - 8 December 2002 ====
-
-- slightly better error reporting when the nr of pars in a send
- or run statement differs from the nr declared
-- handling more cases of structure expansion (e.g., structure
- reference inside other structure used as msg parameter)
-
-==== Version 4.0.0 - 1 January 2003 ====
-
-- Summary of the main changes that motivated the increase of the
- main Spin version number from 3 to 4
-- added support for embedded C code, primarily to support
- model extractors that can generate Spin models from C code
- more easily now, but indirectly this extension also makes
- all C data types and language elements available within
- Spin models. a powerful extension - but with few safeguards
- against erroneous use. read the documentation carefully.
-- added a Breadth-First search option (compile pan.c with -DBFS)
- this option works only for safety properties. it often uses
- more memory and more time than the standard Depth-First search
- mode that Spin uses, but it can find the shortest possible
- error-trails more easily than with the dfs.
- cycle detection is hard with bfs, so it's not supported yet.
- all state compression modes are supported (bitstate, collapse,
- hash-compact, mininized automata, etc.)
-- a small number of bug fixes -- e.g., some unless constructs
- gave compile-time errors in pan.c, some combinations of
- compiler directives gave compiler errors, fewer unused vars
- reported with some more rarely used combinations of compiler
- directives.
-- slightly rearranged the makefiles -- there is now a separate
- shell script (make_pc) for windows and a makefile for unix
- (make_unix). there's also a script for compiling a debuggable
- version of spin with gcc and gdb (make_gcc).
- by default these scripts and makefiles now enable the LTL next
- operator.
-- the call to sbrk() instead of malloc() on Unix is now no longer
- the default -- it could cause large amounts of memory that on
- Linux systems is pre-allocated to malloc, to be inaccessible.
-- on Windows PC's the compiler directive -DPC to compile pan.c
- source is no longer needed (it is only needed to compiler spin
- itself)
-
-All further updates will appear in the new file: V4.Updates
projects / lttv.git / blobdiff