| 1 | Distribution Update History of the SPIN sources |
| 2 | =============================================== |
| 3 | |
| 4 | ==== Version 3.0.0 - 12 August 1997 ==== |
| 5 | |
| 6 | A new release, a new V3.Updates file. See the end |
| 7 | of the V2.Updates file for the main changes between |
| 8 | the last version 2.9.7 and the new version 3.0.0. |
| 9 | |
| 10 | Spin Version 1 lasted from Jan. 1990 - Jan. 1995. |
| 11 | Spin Version 2 lasted from Jan. 1995 - August 1997. |
| 12 | |
| 13 | The shell script upgrade2 will take any version of |
| 14 | Spin between version 2.7 and 2.9 to version 3.0. |
| 15 | Upgrades from 3.0 forward will appear in a new shell |
| 16 | script upgrade3, to keep the file small. |
| 17 | |
| 18 | ==== Version 3.0.1 - 19 August 1997 ==== |
| 19 | |
| 20 | - on older PC's the hashing behavior could be substandard. |
| 21 | on those systems an int is often interpreted as a 16 bit, |
| 22 | instead of a 32-bit quantity. the fix made is to declare |
| 23 | the relevant variables as long integers instead of plain |
| 24 | integers. there is no visible difference for other systems. |
| 25 | - printf accidentily picked up a redundant newline in 3.0.0 |
| 26 | it is gone again. |
| 27 | - interactive use of spin models with rendez-vous statements |
| 28 | could get hung in some cases. |
| 29 | |
| 30 | ==== Version 3.0.2 - 24 August 1997 ==== |
| 31 | |
| 32 | - improved the fix for interactive use of rv's from 3.0.1 |
| 33 | - the parser now catches the use of 'run' to initialize |
| 34 | global variables as an error. |
| 35 | - the parser now catches the use of any initializer on |
| 36 | a formal parameter in a proctype as an error. |
| 37 | - addition of a new datatype to Promela: unsigned |
| 38 | usage: |
| 39 | unsigned name : 3; |
| 40 | declares 'name' to be a variable that can hold unsigned |
| 41 | values -- stored in 3 bits (i.e., values 0..7 inclusive). |
| 42 | values outside the declared range are truncated to the |
| 43 | range on assignments |
| 44 | - d_step may now appear inside and atomic and vice versa |
| 45 | - extra option -E to pass arguments to the C preprocessor |
| 46 | usage: |
| 47 | spin -E-Dfoo=faa filename |
| 48 | to redefined foo as faa in the filename |
| 49 | spin -Pmy_cpp -E-E filename |
| 50 | use my_cpp as the preprocessor (replacing cpp) and |
| 51 | pass it flag -E when it is called. |
| 52 | |
| 53 | ==== Version 3.0.3 - 8 September 1997 ==== |
| 54 | |
| 55 | - unsigned variables weren't cast correctly during |
| 56 | simulation runs -- |
| 57 | - warnings about variables being of too generous a type |
| 58 | are now only generated when the -v verbose option is set |
| 59 | - extra warnings, on use of channels, are now also |
| 60 | generated with spin -v -- still more with spin -v -g |
| 61 | - can now pass directives to the preprocessor with a simpler |
| 62 | spin option -D..., e.g., spin -DLOSS=1 spec |
| 63 | the earluer -E-D... also still works |
| 64 | - a few more additions to xspin303.tcl |
| 65 | |
| 66 | ==== Version 3.0.4 - 25 October 1997 ==== |
| 67 | |
| 68 | - now accepts truncated extensions of pan.trail |
| 69 | (often visible only as pan.tra) on PCs |
| 70 | - now recognizes compiler directive __FreeBSD__ |
| 71 | - redundant include file <malloc.h> deleted from main.c |
| 72 | - now properly initializes all channels hidden in typedef |
| 73 | structures |
| 74 | - made it possible to generate structural views of the |
| 75 | promela model, but tracking channel uses (more to come) |
| 76 | - added pc_zpp.c to the sources - used only on the pc |
| 77 | |
| 78 | ==== Version 3.0.5 - 5 November 1997 ==== |
| 79 | |
| 80 | - corrected bug in the builtin macro preprocessor of the |
| 81 | PC-version (only) of spin. if the first literal match |
| 82 | of the macro source failed to be a valid replacement string, |
| 83 | no further matches were tried on that line |
| 84 | - corrected bug in interactive simulation mode that could |
| 85 | cause a failure to return control to the user |
| 86 | |
| 87 | ==== Version 3.0.6 - 16 December 1997 ==== |
| 88 | |
| 89 | - a value that is truncated in an assignment to a variable |
| 90 | of a small type triggered an error message that sometimes |
| 91 | could cause xspin to miss a display update for the variable |
| 92 | values pannel. |
| 93 | - on a -c flag spin was a little too talkative, assuming also |
| 94 | a -v verbose flag for the final detail printed at the end of |
| 95 | a simulation run. |
| 96 | - fixed an error in the processing of logical OR in the presence |
| 97 | of the X operator in LTL formulae -- this only affected the |
| 98 | outcome of a translation if Spin was compiled with -DNXT |
| 99 | to enable the LTL next-time operator (this is not enabled by |
| 100 | default, because it jeopardizes compatibility with the partial |
| 101 | order reductions) |
| 102 | - a check for non-progress, in combination with provided clauses |
| 103 | on proctypes, could fail. the omission was that the never claim |
| 104 | process searched for its own provided clause, which should in |
| 105 | this case default to true. |
| 106 | - the restriction that the use of any provided clause voided the |
| 107 | partial order reduction was much too strict: it suffices to mark |
| 108 | all statements in only the proctype that is labeled with a |
| 109 | provided clause unsafe -- other processes are not affected. |
| 110 | - added new Test/pathfinder example to the Test directory, |
| 111 | illustrating the use of provided clauses |
| 112 | - the standard stutter extension on finite sequences is not |
| 113 | allowed to produce non-progress cycles, but in combination with |
| 114 | the weak-fairness option this erroneously could happen. |
| 115 | (stutter-extension on temporal claim matches is only applied |
| 116 | to standard acceptance properties, under runtime option -a) |
| 117 | - there was an error in the implementation of weak fairness |
| 118 | that could cause the algorithm to miss matching acceptance or |
| 119 | non-progress cycles with weak-fairness enabled. a small change |
| 120 | in the implementation of this option (incrementing the Choueka |
| 121 | counter values by 1) repairs this flaw. |
| 122 | |
| 123 | ==== Version 3.0.7 - 18 December 1997 ==== |
| 124 | |
| 125 | - the check on a self-loop, added in 3.0.6, unintentionally also |
| 126 | ruled out self-loops in never claims, which are harmless (e.g., |
| 127 | to allow for a finite prefix of 'true' propositions). |
| 128 | |
| 129 | ==== Version 3.0.8 - 2 January 1998 ==== |
| 130 | |
| 131 | - with fairness enabled, a process was considered to be temporarily |
| 132 | blocked while other processes performed a rv handshake. this |
| 133 | could cause a cycle to be reported as fair that normally would not |
| 134 | be considered as such. fairness rule 2 was updated to avoid this. |
| 135 | - an assignment beginning a dstep sequence was incorrectly considered |
| 136 | to be executable in the middle of a rendezvous handshake in progress |
| 137 | elsewhere. |
| 138 | |
| 139 | ==== Version 3.0.9 - 11 January 1998 ==== |
| 140 | |
| 141 | - rendezvous communications lacked an arrow in the new postscript |
| 142 | output generated with spin option -M |
| 143 | - new predefined channel name STDIN for reading a character from |
| 144 | the standard input as in: |
| 145 | chan STDIN; |
| 146 | short c; |
| 147 | do |
| 148 | :: STDIN?c -> |
| 149 | if |
| 150 | :: c == -1 -> /* EOF */ |
| 151 | break |
| 152 | :: else -> |
| 153 | printf("%c", c) |
| 154 | fi |
| 155 | od |
| 156 | - to match this, added support for recognizing character |
| 157 | symbols in Promela such as 'i', '\n', '\t', '\r', etc. |
| 158 | - fixed the bug that prevented weak fairness from being |
| 159 | turned off during verifications.... (bug introduced in 3.0.8) |
| 160 | - small improvements in error catching (mostly related to |
| 161 | illegal structure references) |
| 162 | |
| 163 | ==== Version 3.1.0 - 27 January 1998 ==== |
| 164 | |
| 165 | - all transitions from a local process state that is referenced |
| 166 | within the never claim (or ltl property) are now properly labeled |
| 167 | as unsafe in the partial order reduction |
| 168 | - a d_step that appears at the last statement in a proctype no longer |
| 169 | generates an error in the simulator |
| 170 | - the predefined variable _last is now updated correctly during the |
| 171 | verification process (thanks Pedro Merino for the examples) |
| 172 | - weak fairness is now considered incompatible with partial order reduction |
| 173 | in models that contain rendezvous operations (thanks Dennis Dams for |
| 174 | the example that revealed this) |
| 175 | |
| 176 | ==== Version 3.1.1 - 28 January 1998 ==== |
| 177 | |
| 178 | - fixed a goof in pc_zpp.c -- only visible in the precompiled PC |
| 179 | version. symptom: it would fail to expand some macros with the |
| 180 | builtin version of cpp. in particular, it would fail on the |
| 181 | testcase: Test/leader from the distribution (thanks Mike Ferguson). |
| 182 | |
| 183 | ==== Version 3.1.2 - 14 March 1998 ==== |
| 184 | |
| 185 | - added a Cut/Copy/Paste meny to the text window of xspin version 3.1.2 |
| 186 | (big convenience), plus a few smaller fixes |
| 187 | - the verifiers generated by spin have two extra run-time options: |
| 188 | -E to ignore all invalid endstate errors |
| 189 | -A to ignore all assert() violations |
| 190 | - added #include <strings.h> to pan.c |
| 191 | - main in pan.c is now properly typed 'int' instead of 'void' |
| 192 | - the following change, introduced in 2.9.0, was unnecessary |
| 193 | - assignments to channel variables can violate xr/xs assertions. |
| 194 | there is now a check to catch such violations |
| 195 | the check is removed: |
| 196 | when an xr channel variable is assigned to, it's old value is simply lost. |
| 197 | it was the old value (operations on the channel that the value pointed |
| 198 | to) that the xr/xs assertion applied to, not to the variable name as such. |
| 199 | operations on the new channel id that the variable now points to |
| 200 | are subject to the same xr/xs claims as the old one did. |
| 201 | - new argument to spin: |
| 202 | spin -N claimfile ... promelaspec |
| 203 | reads the never claim from 'claimfile' |
| 204 | (the main filename 'promelaspec' is always the last argument) |
| 205 | - new argument to spin |
| 206 | spin -C promelaspec |
| 207 | prints some channel access info on stdout, useful for producing |
| 208 | a structural view of the system |
| 209 | (used to be an added output in spin -v) |
| 210 | - fixed bug in pan.c that caused some states created during claim stutter |
| 211 | from not being removed from the dfs stack. should rarely have occured. |
| 212 | - all the above extensions are supported in Xspin 3.1.2 |
| 213 | - redesigned Xspin's LTL properties management dialogue panel |
| 214 | - fixed problem with hanging of long simulations on pc's |
| 215 | (a buffer overflow problem internal to windows95/nt) |
| 216 | |
| 217 | ==== Version 3.1.3 - 16 March 1998 ==== |
| 218 | |
| 219 | - small bug fix in sym.c -- reported too many variables as |
| 220 | unused on a spin -a -v spec |
| 221 | - small bug fix in xspin312.tcl -- replaced "else if" with "elseif" |
| 222 | - both bugs reported by Theo Ruys within hours after the release of 3.1.2 |
| 223 | thanks Theo! |
| 224 | |
| 225 | ==== Version 3.2.0 - 7 April 1998 ==== |
| 226 | |
| 227 | - a modest extension of the language: |
| 228 | there is now a procedure-like construct that should reduce the need |
| 229 | for macros. Promela 'inline' functions preserve linenumber |
| 230 | references in simulations (at least, that's the idea). |
| 231 | an inline definition look like this (appearing outside all proctypes) |
| 232 | |
| 233 | inline functionname(x, y) { |
| 234 | ...a promela fragment... |
| 235 | } |
| 236 | |
| 237 | a call looks like this -- and can appear wherever a statement can appear: |
| 238 | |
| 239 | functionname(4, a); |
| 240 | |
| 241 | the replacement text is inlined by the parser, with proper parameter |
| 242 | matching and replacement. |
| 243 | inlines can be recursive (one inline can call another), but not cyclic. |
| 244 | |
| 245 | there is still no local scope for variables. this means that the scope |
| 246 | of any local variable declared is always the entire proctype body -- |
| 247 | no matter where it is declared. |
| 248 | local variables may be declared at the start of an inline -- but such |
| 249 | variables have the same status as a local variable at the place of the call. |
| 250 | |
| 251 | - added an example to the Test directory, illustrating inlines (Test/abp) |
| 252 | |
| 253 | - timeout is no longer automatically enabled and available as a |
| 254 | user-selectable option during interactive simulation. it could cause |
| 255 | counter-intuitive behavior, e.g. when the timeout was used in an unless- |
| 256 | escape |
| 257 | - 'else' is now flagged as unexecutable when appropriate during interactive |
| 258 | simulations -- where possible it is offered as a choice so that an |
| 259 | execution can be forced in a given direction. |
| 260 | - small fixes and fiddles with xspin |
| 261 | |
| 262 | ==== Version 3.2.1 - 4 July 1998 ==== |
| 263 | |
| 264 | - added compile time directive HC, for a version of Wolper's hash-compact |
| 265 | algorithm. it can speed up the search, and reduce memory requirements, |
| 266 | with a relatively low probability of hash-collisions (or missed states). |
| 267 | this is a modification of exhaustive search where we store a 32-bit |
| 268 | hash-value in the hash-tables, as a compressed state vector. |
| 269 | the effective size of the compressed state-vector is the width of the |
| 270 | hash-table itself (controlled by the runtime -w parameter) plus 32 bits |
| 271 | (by default this is: 18+32 = 50 bits of information). |
| 272 | the hash-table entries have some additional overhead which pushes total |
| 273 | memory usage slightly higher -- but the memory reductions can be quite |
| 274 | substantial (depending, trivially, on the length of the state vector |
| 275 | without compression) |
| 276 | to enable: compile pan.c with -DHC (perferably combined with -DSAFETY) |
| 277 | - fixed fgets problem discovered by Theo Ruys |
| 278 | (problem: newlines could accidentily be added to the input text) |
| 279 | - fixed two bugs in dstep code generated in pan.c; improved error reporting |
| 280 | - fixed bug in processing of include files, when an ltl claim is used |
| 281 | |
| 282 | ==== Version 3.2.2 - 21 July 1998 ==== |
| 283 | |
| 284 | - generalized the hash-compact implementation |
| 285 | by default (compiling pan.c with -DHC) 6 bytes are stored: |
| 286 | 4 bytes from the first hash and 2 bytes from a second hash |
| 287 | this gives 32+16 = 48 bits of information, which should secure |
| 288 | a very low collision probability |
| 289 | alternatives are -DHC0 (for 32 bits) -DHC1 (for 40 bits) -DHC2 (48 bits) |
| 290 | and -DHC3 (56 bits). |
| 291 | - reversed the order in which the transitions in a never claim are |
| 292 | generated -- this tends to shorten the counter-examples generated |
| 293 | (by putting the 'true' self-loops that at the end of the list, rather |
| 294 | than at the beginning). Thanks to Dragan Bosnacki. |
| 295 | - fixed a bug in xspin.tcl that could cause the application to hang |
| 296 | when used on a PC (e.g., any simulation of leader...). |
| 297 | (this synchronization bug was introduced in 3.1.4.) |
| 298 | |
| 299 | ==== Version 3.2.3 - 1 August 1998 ==== |
| 300 | |
| 301 | - an atomic that ends with a jump into another |
| 302 | atomic sequence, now connects correctly without |
| 303 | breaking atomicity |
| 304 | - the choice of a rendezvous partner for send operations |
| 305 | wasn't random during simulations (when multiple targets |
| 306 | for the rendezvous are available). it is now. |
| 307 | - fix in xspin to avoid confusion between proctype names |
| 308 | with a common prefix, in rendering an automaton view |
| 309 | - fix in pc_zpp.c for occasional incorrect comment processing |
| 310 | and incorrect #define processing (affected the PC version only) |
| 311 | |
| 312 | ==== Version 3.2.4 - 10 January 1999 ==== |
| 313 | |
| 314 | modifications: |
| 315 | - replaced type "unsigned" in parameter to Malloc and emalloc |
| 316 | with "unsigned long long" to support 64 bit word size machines |
| 317 | (thanks to Judi Romijn's experiments at CWI) |
| 318 | (may not be recognized by non-ansi standard c-compilers) |
| 319 | extensions: |
| 320 | - added a runtime flag -J for both spin (simulations) and |
| 321 | for pan (verification runs), to specify that nested unless |
| 322 | clauses are to be evaluated in reverse order from the default |
| 323 | (to match java semantics of catch clauses) at the request |
| 324 | of Klaus Havelund. |
| 325 | - added runtime flags -qN and -B for spin (simulations) |
| 326 | -q4 suppresses printing output related to queue 4 |
| 327 | -B suppresses printing the final wrapups at the end of a run |
| 328 | - added runtime flag -v for pan (verification) to add filenames |
| 329 | to linenumbers in the listings of unreached states (xspin does |
| 330 | not support these extensions yet) |
| 331 | bug-fixes: |
| 332 | - a very long source statement could overflow an internal |
| 333 | buffer in pan.c, upon the generation of a trail-file. |
| 334 | (thanks for Klaus Havelund's experiments with a java->spin |
| 335 | translator) |
| 336 | - compilation with a vectorsize greater than 1024 could cause |
| 337 | the model checker to behave incorrectly in cases when receive |
| 338 | statements were used that received data into global variables |
| 339 | (instead of locals). this now works correctly. |
| 340 | - removed bug in the optimization code of the ltl-translation |
| 341 | algorithm -- it could remove untils in cases such as |
| 342 | p /\ (q U r) not only if p==r, but also if p appeared within r |
| 343 | - line numbers could be inaccurate if #if 0 ... #endif directives |
| 344 | were used inside inline declarations. corrected. |
| 345 | - fixed a bug in ltl translation due to a failure to recognize |
| 346 | 'true' to be part of any 'and' form -- should have been a rare |
| 347 | occurrence. |
| 348 | - fixed a bug that affected the use of rendezvous statements in |
| 349 | the guard of an escape clause of an unless |
| 350 | |
| 351 | ==== Version 3.3.0 - 1 June 1999 ==== |
| 352 | |
| 353 | - rearranged code to share code for identical cases |
| 354 | in pan.m and pan.b -- this reduces the file sizes by up |
| 355 | to 60% and similarly reduces compilation times for pan.c |
| 356 | - added pan.c compiler directive MEMLIM |
| 357 | compiling pan.c with -DMEMLIM=N will restrict memory use |
| 358 | to N Megabytes precisely; this is an alternative to the |
| 359 | existing limit -DMEMCNT=N which restricts to 2^N bytes |
| 360 | and gives less precise control. |
| 361 | - added new data declaration tag 'local' which can be used |
| 362 | wherever currently 'show' or 'hidden' can be used. |
| 363 | it allows one to identify global variables that are |
| 364 | effectively local (used by only 1 process) as data objects |
| 365 | of which manipulation is safe for partial order reductions. |
| 366 | there's no check for the validity of the tag during verification. |
| 367 | - automatically hide unused or write-only variables |
| 368 | option can be turned off with spin option -o2 |
| 369 | - eval() (used in receive statements to turn a variable into |
| 370 | a constant value) can now contain an arbitrary expression, |
| 371 | instead of just a name (request of Victor Bos). |
| 372 | - it is no longer an error to have multiple mtype definitions |
| 373 | (they are catenated internally) |
| 374 | - more verbose error-trails during guided simulations - in verbose |
| 375 | mode it now includes explicit mention of never claim moves, if |
| 376 | a never claim is involved |
| 377 | - added also an experimental option to generate code separately |
| 378 | for the main system and for the never claim - this makes |
| 379 | separate compilation possible. the option will be finetuned |
| 380 | and documented once it has settled. for the time being, they |
| 381 | are not listed in the usage listings. |
| 382 | - also added, but not enabled, fledgling support for a bisimulation |
| 383 | reduction algorithm that might be applied to never claims to |
| 384 | reduce their size (inspired by work of Kousha Etessami), |
| 385 | |
| 386 | - bugfixes (the first two found by Wenhui Zhang): |
| 387 | - in fairness option (could miss a fair cycle) |
| 388 | - in implementation of the -DMA option (could incorrectly |
| 389 | claim an intersection of the 1st dfs stack an declare a |
| 390 | cycle when none existed) |
| 391 | - in the conversion of ltl formulae to automata (could |
| 392 | occassionaly fail to match common subexpressions) |
| 393 | - bug fix in the runtime code for random receive, fixed |
| 394 | - fixed execution of atomics during interactive simulation |
| 395 | - fixed possibly erroneous marking as 'dead' variables used |
| 396 | to index a structure variable array |
| 397 | |
| 398 | - during interactive simulation, to avoid confusion, choices |
| 399 | between different *escapes* on a statement are no longer offered |
| 400 | in user menus, but are now always resolved by the simulator |
| 401 | - removed all uses of "long long" and replace with "long." |
| 402 | the former (temporarily used in 3.2.4) is not in ansi c, |
| 403 | and the latter will be interpreted correctly on 64bit machines |
| 404 | by a 64bit compiler. |
| 405 | - added better support for 64bit machines -- avoiding deteriorated |
| 406 | performance of the hashing algorithms (courtesy Doug McIlroy) |
| 407 | - the pc version could get the linenumber references wrong after |
| 408 | multiline comments - now repaired (courtesy Mike Ferguson) |
| 409 | - removed bug in xspin.tcl that prevented the selection of |
| 410 | bitstate hashing from the ltl properties manager panel |
| 411 | (courtesy Theo Ruys) |
| 412 | - added an option in xspin to exclude specific channels from the |
| 413 | msc displays (you have to know the channel number though) |
| 414 | - fixes in the interactive simulation model (courtesy Judi Romijn) |
| 415 | - d_steps and atomics now always run to completion without |
| 416 | prompting the user for intermediate choices that could break |
| 417 | the atomicity (and the semantics rules). |
| 418 | - unless escapes no longer reach inside d_steps (they do reach |
| 419 | inside atomics) |
| 420 | - merges sequences of safe or atomic steps -- a considerable speedup |
| 421 | this behavior can be disabled with spin option -o3 |
| 422 | - computes precondition for feasibility of rv - this option can be |
| 423 | enabled with spin option -o4 -- it seems of little use in practice |
| 424 | - dataflow analysis -- can be disabled with spin option -o1 |
| 425 | - partial evaluation to remove dead edges from verification model |
| 426 | (i.e., with a constant 'false' guard) |
| 427 | - added pan compile time option -DSC to enable new stack cycling option. |
| 428 | this will swap parts of deep stacks to a diskfile with only low overhead. |
| 429 | it needs no further user action to work -- the runtime -m flag |
| 430 | remains, but now simply sets the size of the part of the stack |
| 431 | that is in core (i.e., you need not set it explicitly unless you want to) |
| 432 | - added pan compile time option -DLC to optinally use hashcompacted stackstates |
| 433 | during Bitstate runs. it is slower by about 20-30%, but in cases |
| 434 | where -DSC is used (very deep stacks) it can safe a lot of extra memory. |
| 435 | for this reason -DSC always enables -DLC by default |
| 436 | |
| 437 | ==== Version 3.3.1 - 12 July 1999 ==== |
| 438 | |
| 439 | - fix in pangen2.h, to avoid a null-pointer reference |
| 440 | in the automata preparation routines. it can occur in some cases |
| 441 | where progress labels are used in combination with p.o. reduction |
| 442 | - fix for weak-fairness in combination with p.o. reduction and |
| 443 | unless/rendez-vous (courtesy Dragan Bosnacki) |
| 444 | - fix to prevent an infinite cycle during the weak-fairness based |
| 445 | verifications. (when both the 2nd and the 1st dfs stacks are |
| 446 | intersected with a non-zero choueka counter value, the search |
| 447 | used to continue - instead this should be treated as a regular |
| 448 | stack match) |
| 449 | - better feedback on spin -a when parts of the automaton are pruned |
| 450 | due to constant false guards |
| 451 | - added spin option -w (extra verbose) to force all variable |
| 452 | values to be printed at every execution step during simulations |
| 453 | |
| 454 | ==== Version 3.3.2 - 16 July 1999 ==== |
| 455 | |
| 456 | - correcting an initially erroneous fix in 3.3.1 that prevented |
| 457 | compilation alltogether for sources generated through xspin. (...) |
| 458 | (it left a reference to counters used in the weak fairness algorithm |
| 459 | in the code that had to be suppressed if weak fairness isn't used) |
| 460 | |
| 461 | ==== Version 3.3.3 - 21 July 1999 ==== |
| 462 | |
| 463 | - fix in the new code for dataflow analysis. in some cases a core-dump |
| 464 | could result if a particular control-flow structure was encountered |
| 465 | (courtesy Klaus Havelund) |
| 466 | - updated Xspin to 3.3.3 to deal with the new policy in 3.3 that printfs |
| 467 | during simulations are always indented by a number of tab-stops that |
| 468 | corresponds to the process number of the process that executes the |
| 469 | printf - this makes printfs from the same process line up in columns, |
| 470 | but it confused xspin. (fix courtesy of Theo Ruys) |
| 471 | |
| 472 | ==== Version 3.3.4 - 9 September 1999 ==== |
| 473 | |
| 474 | - new pan option -T to prevent an existing trail file from being |
| 475 | overwritten (useful if you run multiple copies of pan with |
| 476 | bitstate hashing and different -w parameters, to optimize chances |
| 477 | of finding errors fast -- the first run to write the trail file |
| 478 | then wins) |
| 479 | - small improvement in error reporting for use of special labels inside |
| 480 | atomic and d_step sequences |
| 481 | - small portability change to avoid problems with some compilers (e.g. |
| 482 | the ones used on plan9) |
| 483 | - increased some statically defined maxima (e.g. for the max length of |
| 484 | a single statement - now increased to 2K bytes to avoid problems with |
| 485 | machine generated Promela files) |
| 486 | |
| 487 | ==== Version 3.3.5 - 28 September 1999 ==== |
| 488 | |
| 489 | - two bug-fixes in the ltl->never claim conversion (with thanks to |
| 490 | Heikki Tauriainen for reporting them) |
| 491 | - increase in some static buffer sizes to allow for long |
| 492 | (typically machine generated) variable names |
| 493 | - removed some debugging printfs |
| 494 | |
| 495 | ==== Version 3.3.6 - 23 November 1999 ==== |
| 496 | |
| 497 | - two small extensions and 4 important bug fixes |
| 498 | |
| 499 | - added runtime option -t to pan; using pan -tsuf will |
| 500 | cause error trails to be written into spec.suf instead of |
| 501 | spec.trail (which remains the default) |
| 502 | - added a verbose output to the verification runs, to write |
| 503 | a line of output each time a new state in the never claim |
| 504 | is reached. this helps keeping track of progress in long |
| 505 | running verifications -- and helps to avoid false positives |
| 506 | (i.e., when most states in the never claim are unreached, |
| 507 | which is a strong indication that the LTL formula that |
| 508 | produced the claim isn't related to real behavior of the |
| 509 | system) |
| 510 | |
| 511 | - bug fix in the fairness algorithm (-f flag during verification) |
| 512 | that could cause false error reports to be generated |
| 513 | - bug fix in the stack cycling compile-time option to pan.c (-DSC) |
| 514 | which could cause erroneous behavior of the verifier |
| 515 | (both of these reported by Muffy Calder and Alice Miller) |
| 516 | - bug fix in the generation of never claims from LTL -- missing |
| 517 | parentheses around subexpressions in a guard |
| 518 | - fix to circumvent buggy behavior from gcc on Unix platforms |
| 519 | (its version of sbrk can return memory that is not properly |
| 520 | word aligned -- which causes memory faults in pan) |
| 521 | |
| 522 | ==== Version 3.3.7 - 6 December 1999 ==== |
| 523 | |
| 524 | - 3.3.6 introduced a bug that prevented the verifier code |
| 525 | from compiling unless fairness was enabled -- corrected in 3.3.7 |
| 526 | - fixed a minor problem with the as yet unadvertised separate |
| 527 | compilation option (compiling the program separately from |
| 528 | the claim to speed up verifications of multiple claims) |
| 529 | - fixed a bug in the simulation code that could make the |
| 530 | simulator miss executing statements. it could lead to |
| 531 | misleading traces for errors. (thanks to an example by Pim Kars) |
| 532 | |
| 533 | ==== Version 3.3.8 - 1 January 2000 ==== |
| 534 | |
| 535 | - fixed a bug in the simulation code that caused no output |
| 536 | to appear, for instance, when the traceback is done with |
| 537 | a guided simulation for the Test/loops testfile -- fixed |
| 538 | - fixed bug in the generation of ltl formula of the type: |
| 539 | <>[]p && []<>q && []<>r |
| 540 | traced to a mistake in the comparison of states in the |
| 541 | buchi automaton that could unjustly claim two states to |
| 542 | be identical even if they differed (reported by Hagiya) |
| 543 | - added a cast to (double) for manipulation of MEMLIM to |
| 544 | avoid problems with some compilers |
| 545 | - added a small optimization that rids the spec of repeated |
| 546 | sequential skip statements, or skips immediately following |
| 547 | printfs (these may be present in mechanically generated specs) |
| 548 | |
| 549 | ==== Version 3.3.9 - 31 January 2000 ==== |
| 550 | |
| 551 | - fixed several more bugs in the ltl -> buchi automata |
| 552 | conversion - found with a random testing method |
| 553 | described by Heikki Tauriainen. the method consists |
| 554 | of generating random ltl formula with a fixed number of |
| 555 | propositional symbols, with varying numbers of operators, |
| 556 | and generating random statespaces over the boolean |
| 557 | operands, up to preset maximum number of states. |
| 558 | we've done tests with three databases, consisting of: |
| 559 | - 27 handpicked standard ltl formulae with up to 4 |
| 560 | operands |
| 561 | - 5356 random ltl formulae with up to 10 temporal |
| 562 | operators and up to 3 operands |
| 563 | - 20577 ltl formulae with up to 3 temporal operators |
| 564 | and up to 3 operands |
| 565 | each formula was tested for 25 randomly generated statespaces |
| 566 | with up to 50 global states. |
| 567 | we checked spin's automata generation method against an |
| 568 | independent implementation by kousha etessami, and verified |
| 569 | that each of the tests either failed with both tools or |
| 570 | passed with both tools -- any difference pointed to a bug |
| 571 | in one of the two tools. |
| 572 | the fixes in spin version 3.3.9 are mostly related |
| 573 | to the use of the X (next operator -- which is normally |
| 574 | disabled but can be enabled by compiling the spin sources |
| 575 | with the extra compiler directive -DNXT) and V (the dual |
| 576 | of U) in long formula. |
| 577 | - used the opportunity to add in some more optimizations |
| 578 | that reduce the size of the automata that are produced |
| 579 | (which in many cases also speeds up the generation process). |
| 580 | the optimizations were inspired by kousha etessami's work. |
| 581 | (email: kousha@research.bell-labs.com) |
| 582 | |
| 583 | ==== Version 3.3.10 - 15 March 2000 ==== |
| 584 | |
| 585 | - this should be a final, stable release of spin |
| 586 | version 3.3, barring the unforeseen. |
| 587 | we'll move to 3.4.0 in a next round of extensions. |
| 588 | |
| 589 | - made the number of active processes a globally visible |
| 590 | read-only variable: _nr_pr |
| 591 | this makes it possible to start a process and then wait |
| 592 | for it to complete: |
| 593 | run A(); (_nr_pr == _pid+1); |
| 594 | useful for simulating function calls. |
| 595 | - the appearance of a timeout in the guard of a d_step |
| 596 | sequence was treated as an error - it is not treated |
| 597 | as a warning. (in the guard a timeout is ok) |
| 598 | - fixed rounding error in calculating the nr of bytes |
| 599 | to be stored in statevector with -DCOLLAPSE option. |
| 600 | in rare cases the roundoff error could result in |
| 601 | missed states when collapse was enabled. reported by |
| 602 | Dragan Bosnacki. |
| 603 | - improved ltl->buchi automata conversion some more |
| 604 | to be described in an upcoming paper by kousha. |
| 605 | - small update of xspin.tcl -- it failed to record spin |
| 606 | command line options in the advanced verification options |
| 607 | panel. reported by Theo Ruys. |
| 608 | |
| 609 | ==== Version 3.4.0 - 14 August 2000 ==== |
| 610 | |
| 611 | - fixed two remaining problems with the ltl conversion |
| 612 | algorithm, related to nested untils and the use of the next |
| 613 | operator (thanks again Heikki Tauriainen). |
| 614 | - deals better with renaming files for preprocessing -- no |
| 615 | longer relies on temporary files residing on the same |
| 616 | filesystem as the working directory |
| 617 | - added an alignment attribute for the State vector to force |
| 618 | gcc to align this structure on a wordboundary (on solaris |
| 619 | machines gcc apparently considers this optional). |
| 620 | - fixed two problems in the use of trace-assertions (could |
| 621 | fail when tracking actions on rendezvous channels) |
| 622 | - new xspin340.tcl that deals better with non-terminating |
| 623 | simulation runs on pcs. |
| 624 | - added support for property-based slicing, to be documented. |
| 625 | one example in the Test directory illustrates its use: the |
| 626 | wordcount example. |
| 627 | - added two examples (mobile[12]) that show how specifications |
| 628 | in the pi-calculus can be rendered in Promela (thanks Joachim |
| 629 | Parrow). |
| 630 | |
| 631 | ==== Version 3.4.1 - 15 August 2000 ==== |
| 632 | |
| 633 | - fixed problem with spin option -m -- it stopped working after |
| 634 | the upgrade to spin 3.3.0 a year ago. (Thanks Theo Ruys and Rui Hu). |
| 635 | - minor twiddles to avoid some spurious warnings from gcc on pan_ast.c |
| 636 | |
| 637 | ==== Version 3.4.2 - 28 October 2000 ==== |
| 638 | |
| 639 | - release 3.4.1 had some windows carriage returns in some of the |
| 640 | source files, which unix compilers don't like - removed |
| 641 | - two small fixes in the data dependency algorithm, e.g. to make sure |
| 642 | that an array index is never considered a def |
| 643 | - made the allignment attribute on the State struct GCC specific |
| 644 | (which it is -- used only on Solaris) |
| 645 | - the -o2 flag didn't work as advertised, fixed. |
| 646 | - fix to prevent problems with too liberal use of sequence brackets |
| 647 | which could cause a coredump in some cases |
| 648 | |
| 649 | ==== Version 3.4.3 - 22 December 2000 ==== |
| 650 | |
| 651 | - small bug fixes, related to the use of {...} for plain sequences |
| 652 | (other than for atomic or d_step sequences), and the use of |
| 653 | enabled to refer to the running process in simulation mode |
| 654 | |
| 655 | ==== Version 3.4.4 - 2 February 2001 ==== |
| 656 | |
| 657 | - fix of the trace assertion code in pan.c (there was a problem |
| 658 | when trace assertions were used in combination with rv operations) |
| 659 | - fix of marking of unreachable states (some reached states could |
| 660 | erroneously be reported as unreached in some cases) |
| 661 | |
| 662 | ==== Version 3.4.5 - 8 March 2001 ==== |
| 663 | |
| 664 | - one more bug found by Heikki Tauriainen - in the LTL -> Buchi |
| 665 | conversion algorithm. it was caused by an unjustified optimization |
| 666 | in tl_rewrt.c -- now commented out. |
| 667 | |
| 668 | ==== Version 3.4.6 - 29 March 2001 ==== |
| 669 | |
| 670 | - when using rendezvous channels, the compression mask was |
| 671 | not completely restored on backward moves during the search. |
| 672 | the correctness of the search was not affected, but the |
| 673 | number of reached states became larger than necessary |
| 674 | (up to twice as large as needed). bug fixed. |
| 675 | (found and reported by Vivek Shanbhag) |
| 676 | |
| 677 | ==== Version 3.4.7 - 23 April 2001 ==== |
| 678 | |
| 679 | - fixed a number of small bugs in xspin.tcl (now version 3.4.7) |
| 680 | (shaded out menu items were not enabled, errors on cancel of |
| 681 | simulation runs, etc.) |
| 682 | - pruned the number of unreached states reported, by removing |
| 683 | reports for internal states (marked ".(goto)" or "goto :b3") |
| 684 | - fixed bug in pid assignements on guided simulation for np-cycles |
| 685 | |
| 686 | ==== Version 3.4.8 - 22 June 2001 ==== |
| 687 | |
| 688 | - more small bug fixes |
| 689 | e.g., a problem with parameters on inline calls, if the name |
| 690 | of an actual parameter equals the name of another formal parameter |
| 691 | in the same inline; a typo in an 'attribute' annotation; some |
| 692 | missing parameters in rarely executed printf calls |
| 693 | |
| 694 | ==== Version 3.4.9 - 1 October 2001 ==== |
| 695 | |
| 696 | - two bug fixes: |
| 697 | - problem with xr/xs declarations for processes that can be |
| 698 | instatiated with multiple pids -- could lead to a coredump |
| 699 | - problem with treatment of merged statements in guided simulations. |
| 700 | could lead to a statement being printed twice when it only |
| 701 | occurred once. |
| 702 | |
| 703 | ==== Version 3.4.10 - 30 October 2001 ==== |
| 704 | |
| 705 | - two bug fixes: |
| 706 | - trace assertions were not working correctly, failing to |
| 707 | reliably generate matches for all channels within the scope |
| 708 | of an assertion. this was likely broken when statement merging |
| 709 | was first introduced in version 3.3 |
| 710 | - added protection against the use of pids outside the valid |
| 711 | range in remote references (i.e., less than 0 or over 255) |
| 712 | |
| 713 | ==== Version 3.4.11 - 17 December 2001 ==== |
| 714 | |
| 715 | - a bevy of small bug fixes: |
| 716 | - during verification, sorted send operations |
| 717 | (e.g., q!!m) were not reversed accurately, leading to |
| 718 | potentially inconsistent error trails |
| 719 | - 'else' was not interpreted correctly when it appeared |
| 720 | as the first statement of a d_step |
| 721 | - process death was not in all possible cases considered a safe |
| 722 | action, and thus could be deferred longer than necessary |
| 723 | - collapse did not in all cases generate the best compression |
| 724 | |
| 725 | ==== Version 3.4.12 - 18 December 2001 ==== |
| 726 | |
| 727 | - correcting a dumn coding error in 3.4.11 that made the |
| 728 | pan.c source uncompilable.. |
| 729 | |
| 730 | ==== Version 3.4.13 - 31 January 2002 ==== |
| 731 | |
| 732 | - new option -T, to suppress pid-dependent indenting of outputs |
| 733 | - new datatype 'pid' for storing return values from run expressions |
| 734 | |
| 735 | - improved reporting of unreached states for models with inlines. |
| 736 | - improved reporting of memory use for bitstate verification runs. |
| 737 | - fewer unused vars in pan.c for common modes of compilation. |
| 738 | - during simulation each line of output is now immediately flushed |
| 739 | - new restrictions on the use of 'run': max 1 run operator per |
| 740 | expression, and run cannot be combined with other conditionals. |
| 741 | this secures that if a run expression fails, because the max nr |
| 742 | of procs would be exceeded, the expression as a whole will have |
| 743 | no side-effects. |
| 744 | |
| 745 | - corrected bug in treatment of parameters to inlines |
| 746 | - corrected bug that showed up for some bizarre combinations |
| 747 | of constructs (d_step nested in atomic, embedded in loop) |
| 748 | sympton was that the spin parser would hang |
| 749 | - the maximum number of processes during simulation is now |
| 750 | equal to that during verification (255) - to prevent |
| 751 | runaway simulations. the exact number can be redefined |
| 752 | when spin is compiled, by adding a directive, e.g. -DMAXP=512 |
| 753 | similarly the max nr of message channels during simulation |
| 754 | can be set by compiling spin with a directive, e.g. -DMAXQ=512 |
| 755 | the bounds used during verification (255) cannot be changed. |
| 756 | |
| 757 | ==== Version 3.4.14 - 6 April 2002 ==== |
| 758 | |
| 759 | - added new spin option -uN to truncate a simulation run after |
| 760 | precisely N steps were taken. in combination with option -jM |
| 761 | this can select step M to N from a very long simulation |
| 762 | (say guided or random); example: spin -j10 -u20 spec |
| 763 | prints step 10 up to 20, but nothing else |
| 764 | |
| 765 | - corrected important bug introduced in 3.4.13 that caused a |
| 766 | core dump during verification runs. the bug was caused by |
| 767 | a poor attempt to correct reporting of unreached states |
| 768 | due to statement merging effects. |
| 769 | |
| 770 | - corrected compilation error for an unusual combination of |
| 771 | compiler directives |
| 772 | |
| 773 | ==== Version 3.4.15 - 1 June 2002 ==== |
| 774 | |
| 775 | - much improved hashfunctions, at the suggestion of Jan Hajek |
| 776 | from The Netherlands (the original implementor of the Approver |
| 777 | tool from the seventies). |
| 778 | this makes for better performance in both exhaustive searches |
| 779 | (fewer hashcollisions on standard hashtable, therefore often |
| 780 | faster), in bitstate and hashcompact searches (more coverage). |
| 781 | the old hashfunctions are reenabled if pan.c is compiled |
| 782 | with the new directive -DOHASH. the new functions are the default. |
| 783 | - improved reports of unreachable states, in the presence of |
| 784 | statement merging. |
| 785 | - small change in the indenting of printf output -- it now lines |
| 786 | up better with process columns in -c simulation output |
| 787 | - fewer compiler warnings |
| 788 | - some small fiddles with xspin to fix small problems |
| 789 | - giving up on maintaining the upgrade3 scripts -- they get too |
| 790 | long and they do not seem to be used much |
| 791 | |
| 792 | ==== Version 3.4.16 - 2 June 2002 ==== |
| 793 | |
| 794 | - a bug slipped in in 3.4.15, bitstate verification failed |
| 795 | - also increased the default memory limit on PCs to 64 Mb |
| 796 | |
| 797 | ==== Version 3.4.17 - 19 September 2002 ==== |
| 798 | |
| 799 | - added a function printm(x) to print the symbolic name of |
| 800 | an mtype constant. this is equivalent to printf("%e", x), |
| 801 | but can be more convenient. |
| 802 | - changed the structure of the never claim that is included |
| 803 | by default if pan.c is compiled for non-progress cycle |
| 804 | detection with directive -DNP |
| 805 | the change is to check first for a move to the accepting |
| 806 | state, rather than last. this reduces the length of |
| 807 | error trails that are generated, matching the earlier |
| 808 | change made in version 3.2.2, thanks again to Dragan Bosnacki |
| 809 | for pointing this out. |
| 810 | - rearranged the code for pan_ast.c so that it can be compiled |
| 811 | separately, rather than as an include file of pangen5.c |
| 812 | - a bug had been hiding in the -DCOLLAPSE memory compression |
| 813 | option that could in rare cases lead to states being missed |
| 814 | during a verification |
| 815 | the bug could be avoided with the optional -DJOINPROCS. |
| 816 | it is now permanently fixed by extending the nr of bytes |
| 817 | stored somewhat (the type of each process is now stored |
| 818 | explicitly in the compressed statevector, to avoid the |
| 819 | confusion that can result if two processes of the same |
| 820 | contents but with different types could be created with |
| 821 | the same pid, but as alternative options from the same |
| 822 | state -- a case found by Remco van Engelen. |
| 823 | the fix increases memory use slightly in some case (around |
| 824 | 10% in many test cases) but retains the greater part of |
| 825 | the memory compression benefit. if needed, the fix can |
| 826 | be disabled by compiling pan.c with -DNOFIX |
| 827 | - pan_ast.c is now a separately compiled file, just like |
| 828 | all the others, instead of being #included into pangen5.c |
| 829 | - more attempts to fix the accuracy of reachability reports |
| 830 | |
| 831 | ==== Version 3.5.0 - 1 October 2002 ==== |
| 832 | |
| 833 | - variable names starting with an underscore were mistreated |
| 834 | in the data flow analysis. |
| 835 | - this is meant to be a stable release of spin version 3, with |
| 836 | minor changes in contact-information for the new spinroot.com |
| 837 | website for all documentation, workshop information and |
| 838 | newsletters. |
| 839 | |
| 840 | ==== Version 3.5.1 - 11 November 2002 ==== |
| 841 | |
| 842 | - bug in parsing of remote label references, could cause a |
| 843 | core-dump of spin -a |
| 844 | - small additional improvements in reporting of unreachable |
| 845 | states - to more accurately take into account optimizations |
| 846 | made in the transition structure before verification starts |
| 847 | - noted incompatability of combining -DREACH and -DMA |
| 848 | |
| 849 | ==== Version 3.5.2 - 30 November 2002 ==== |
| 850 | |
| 851 | - slightly improved line number references in reporting syntax |
| 852 | errors within d_steps |
| 853 | - extension: remote references usually are written as: |
| 854 | proctypename[pid]@labelname |
| 855 | if there is only one instantiation of the proctype, then the |
| 856 | pid can more easily be figured out by Spin than by the user, |
| 857 | so it can, in these cases, now be omitted, making an anonymous |
| 858 | remote reference possible, as in: |
| 859 | proctypename@labelname |
| 860 | if there turn out to be multiple possible matches, Spin will |
| 861 | warn in simulation mode -- but not in verification mode. |
| 862 | (the additional check would probably be too consuming). |
| 863 | - during the execution of a d_step, spin would by default |
| 864 | still print out every execution step in simulations (under |
| 865 | the -p option). now it will only do so in verbose mode |
| 866 | (with also -v). |
| 867 | - if the last step in an atomic sequence was a rendezvous |
| 868 | send operation, atomicity would not reliably move with |
| 869 | the handshake to the receiver. this is fixed. |
| 870 | - the simulator used a confused method to help the user out |
| 871 | if the pid of a process was guessed incorrectly in a remote |
| 872 | reference operation. this is now done more sanely: if a |
| 873 | variable is used for the pid, the simulator now trusts that |
| 874 | it was set correctly -- the remote ref will simply fail with |
| 875 | an error warning if this is not the case. if the user specified |
| 876 | the pid with a fixed constant, the simulator will now always |
| 877 | add 1 to the number if the presence of a never claim is detected. |
| 878 | (this is because behind the scenes the pid's will move up one |
| 879 | slot to accomodate the claim -- this is always hidden from the |
| 880 | user -- allowing the user to assume that pids always start at 0). |
| 881 | |
| 882 | ==== Version 3.5.3 - 8 December 2002 ==== |
| 883 | |
| 884 | - slightly better error reporting when the nr of pars in a send |
| 885 | or run statement differs from the nr declared |
| 886 | - handling more cases of structure expansion (e.g., structure |
| 887 | reference inside other structure used as msg parameter) |
| 888 | |
| 889 | ==== Version 4.0.0 - 1 January 2003 ==== |
| 890 | |
| 891 | - Summary of the main changes that motivated the increase of the |
| 892 | main Spin version number from 3 to 4 |
| 893 | - added support for embedded C code, primarily to support |
| 894 | model extractors that can generate Spin models from C code |
| 895 | more easily now, but indirectly this extension also makes |
| 896 | all C data types and language elements available within |
| 897 | Spin models. a powerful extension - but with few safeguards |
| 898 | against erroneous use. read the documentation carefully. |
| 899 | - added a Breadth-First search option (compile pan.c with -DBFS) |
| 900 | this option works only for safety properties. it often uses |
| 901 | more memory and more time than the standard Depth-First search |
| 902 | mode that Spin uses, but it can find the shortest possible |
| 903 | error-trails more easily than with the dfs. |
| 904 | cycle detection is hard with bfs, so it's not supported yet. |
| 905 | all state compression modes are supported (bitstate, collapse, |
| 906 | hash-compact, mininized automata, etc.) |
| 907 | - a small number of bug fixes -- e.g., some unless constructs |
| 908 | gave compile-time errors in pan.c, some combinations of |
| 909 | compiler directives gave compiler errors, fewer unused vars |
| 910 | reported with some more rarely used combinations of compiler |
| 911 | directives. |
| 912 | - slightly rearranged the makefiles -- there is now a separate |
| 913 | shell script (make_pc) for windows and a makefile for unix |
| 914 | (make_unix). there's also a script for compiling a debuggable |
| 915 | version of spin with gcc and gdb (make_gcc). |
| 916 | by default these scripts and makefiles now enable the LTL next |
| 917 | operator. |
| 918 | - the call to sbrk() instead of malloc() on Unix is now no longer |
| 919 | the default -- it could cause large amounts of memory that on |
| 920 | Linux systems is pre-allocated to malloc, to be inaccessible. |
| 921 | - on Windows PC's the compiler directive -DPC to compile pan.c |
| 922 | source is no longer needed (it is only needed to compiler spin |
| 923 | itself) |
| 924 | |
| 925 | All further updates will appear in the new file: V4.Updates |