| 1 | Distribution Update History of the SPIN sources |
| 2 | =============================================== |
| 3 | |
| 4 | ==== Version 2.0 - 1 January 1995 ==== |
| 5 | |
| 6 | The version published in the first printing of |
| 7 | ``Design and Validation of Computer Protocols'' |
| 8 | is nominally SPIN Version 1.0. |
| 9 | |
| 10 | SPIN version 2.0 includes a partial order reduction |
| 11 | mode and many extensions and revisions that are |
| 12 | documented in the file Doc/WhatsNew.ps of the |
| 13 | distribution. This file lists all updates |
| 14 | made to these sources after the first release. |
| 15 | |
| 16 | ===== 2.0.1 - 7 January 1995 ==== |
| 17 | |
| 18 | An automatic shell script `upgrades' in the main |
| 19 | SPIN directory will be maintained from now on. |
| 20 | For all future updates it will suffice to retrieve |
| 21 | just the upgrades file, and execute it in the Src |
| 22 | directory to apply all changes. The tar file will |
| 23 | of course be kept up to date at all times as well. |
| 24 | |
| 25 | Changes in this update: |
| 26 | 1. MEMCNT can now grow larger than 2^31 - for those |
| 27 | happy users that have a machine with more than |
| 28 | a Gigabyte of main memory. |
| 29 | (N.B. this fix was made and distributed before the |
| 30 | upgrades file was started - so this one change isn't |
| 31 | available in that way) |
| 32 | 2. Change in the lexical analyzer to accept redundant |
| 33 | text at the end of preprocessor directives, that |
| 34 | some versions of cpp may produce. |
| 35 | |
| 36 | ===== 2.0.2 - 10 January 1995 ==== |
| 37 | |
| 38 | Two small updates to pangen1.h to avoid problems on |
| 39 | some systems when (1) compiling pan.c with profiling |
| 40 | enabled, or (2) when using the new predefined function |
| 41 | enabled() in combination with partial order reduction. |
| 42 | |
| 43 | ===== 2.0.3 - 12 January 1995 ==== |
| 44 | |
| 45 | At request, added a printout of the mapping from label |
| 46 | names as used in the Promela source to state numbers as |
| 47 | used in the verifier to spin option -d. |
| 48 | to see just this new part of the listing, say: |
| 49 | spin -d spec | grep "^label" |
| 50 | first column is the keyword "label" |
| 51 | second column is the name of the label |
| 52 | third column is the state number assigned |
| 53 | last column is the name of the proctype in which the |
| 54 | label is used. |
| 55 | the same state numbers and transitions are |
| 56 | also used by the verifier, and can be printed as |
| 57 | before with: |
| 58 | spin -a spec; cc -o pan pan.c; pan -d |
| 59 | |
| 60 | ===== 2.0.4 - 14 January 1995 ==== |
| 61 | |
| 62 | With the introduction of `else' a new opportunity for |
| 63 | silly syntax mistakes is created. it is all too tempting |
| 64 | to write: |
| 65 | if |
| 66 | :: condition -> |
| 67 | more |
| 68 | :: else |
| 69 | something |
| 70 | fi |
| 71 | and forgot the statement separator that is required between |
| 72 | the `else' and `something' |
| 73 | this likely typo is easy to recognize, and is silently |
| 74 | repaired and accepted by the new lexical analyzer. |
| 75 | |
| 76 | ===== 2.0.5 - 17 January 1995 ==== |
| 77 | |
| 78 | transition labels for send and receive operations |
| 79 | now preserve all the information from the source text |
| 80 | (i.e., the symbolic names for all message parameters used). |
| 81 | |
| 82 | ===== 2.0.6 - 27 January 1995 ==== |
| 83 | |
| 84 | two fixes, both caught by Roberto Manione and Paola: |
| 85 | - deeply nested structures (more than two levels) |
| 86 | could give syntax errors, and |
| 87 | - the transition label of an `else' statement wasn't |
| 88 | always printed correctly in the traces. |
| 89 | |
| 90 | ===== 2.0.7 - 2 February 1995 ==== |
| 91 | |
| 92 | - another fix of the implementation of data structures |
| 93 | to make references of deeply nested structure work |
| 94 | the way they should |
| 95 | - removed suboptimal working of safety marking of |
| 96 | atomic sequences. reductions are now slightly |
| 97 | larger in some cases. |
| 98 | - improved boundary checking of array indexing also |
| 99 | slightly (made it more efficient for some cases) |
| 100 | |
| 101 | ===== 2.0.8 - 7 February 1995 ==== |
| 102 | |
| 103 | - adjusted line number counting slightly in spinlex.c |
| 104 | to avoid annoying off-by-one errors. |
| 105 | |
| 106 | ===== 2.0.9 - 9 February 1995 ==== |
| 107 | |
| 108 | - removed a bug in the transition structures that are |
| 109 | generated for d_steps. (small fix in pangen2.h) |
| 110 | |
| 111 | ===== 2.1 - 15 February 1995 ==== |
| 112 | |
| 113 | - removed two errors in the implementation of d_steps: |
| 114 | one was related to the treatment of `else' during verification |
| 115 | another related to the execution of d_steps in guided simulations |
| 116 | - improved the treatment of rendez-vous in SPIN verbose printings |
| 117 | improves match with xspin; avoids misinterpretation of pids |
| 118 | - made mtype fields be interpreted uniformly in all SPIN modes |
| 119 | - added message sequence charts in xspin |
| 120 | - removed stutter-closedness checks from pangen2.h (no change |
| 121 | in functionality, just replaced a dubious check with a more |
| 122 | precise descriptive warning) |
| 123 | |
| 124 | ===== 2.1.1 - 17 February 1995 ==== |
| 125 | |
| 126 | - instantiated channels declared inside typedefs weren't |
| 127 | properly initialized |
| 128 | |
| 129 | ===== 2.2 - 19 February 1995 ==== |
| 130 | |
| 131 | - main extension of functionality: |
| 132 | added an interactive simulation mode (both in xspin and in spin itself) |
| 133 | that will be described at greater length in Newsletter #4. |
| 134 | also improved some of the printouts for verbose simulation runs. |
| 135 | |
| 136 | - added a precompiler directive -DREACH to force exploration of |
| 137 | all states reachable within N execution steps from the initial |
| 138 | system state, when the search is deliberately truncated with -mN. |
| 139 | normally such a truncated search does not give that guarantee. |
| 140 | (note that if a state at level N-1 is also reachable from the |
| 141 | initial state within 1 execution step, but it is reached via the |
| 142 | longer path first in the DFS - then all successors via the shorter |
| 143 | path would normally not be explored, because they succeed a |
| 144 | previously visited state. with -DREACH we remember the depth at |
| 145 | which a state was visited, and consider it unvisited when encountered |
| 146 | on a shorter path. not compatible with BITSTATE - for the obvious |
| 147 | reason (no room to store the depth counts). |
| 148 | |
| 149 | - fixed a bug in pangen[24].c that could cause an internal consistency check |
| 150 | in the runtime verifiers to fail, and cause the run to terminate with |
| 151 | the error `sv_save failed' |
| 152 | |
| 153 | ===== 2.2.1 - 23 February 1995 ==== |
| 154 | |
| 155 | - small refinements to interactive simulation mode (xspin and spin) |
| 156 | |
| 157 | ===== 2.2.2 - 24 February 1995 ==== |
| 158 | |
| 159 | - added missing prototype in 2.2.1, and fix parameter mistake in a |
| 160 | function that was added in 2.2.1 |
| 161 | |
| 162 | ===== 2.2.3 - 3 March 1995 ==== |
| 163 | |
| 164 | - bug fix in implementation of d_step (dstep.c) |
| 165 | and some mild improvements in error reporting |
| 166 | |
| 167 | ===== 2.2.4 - 9 March 1995 ==== |
| 168 | |
| 169 | - made sure process numbers assigned by simulator |
| 170 | are always the same as those assigned by the verifier |
| 171 | - by request: added a binary exclusive-or operator ('^') |
| 172 | |
| 173 | ===== 2.2.5 - 14 March 1995 ==== |
| 174 | |
| 175 | - removed error in treatment of `else' during random simulation. |
| 176 | `else' was incorrectly considered to be executable also |
| 177 | in the middle of a rendez-vous handshake. no more. |
| 178 | |
| 179 | ===== 2.2.6 - 21 March 1995 ==== |
| 180 | |
| 181 | - made sure that variable declarations are reproduced in |
| 182 | the pan.c sources in the same order as they are given |
| 183 | in the original promela specification. this matters |
| 184 | in cases where new variables are initialized with each |
| 185 | others values. |
| 186 | - better error handling when a reference is made erroneously |
| 187 | to an assumed element of an undeclared structure |
| 188 | |
| 189 | ===== 2.2.7 - 23 March 1995 ==== |
| 190 | |
| 191 | - catches more cases of blocking executions inside d_step |
| 192 | sequences |
| 193 | - better handling of timeout, when using both blocking |
| 194 | atomic sequences and never claims. the behavior of the |
| 195 | simulator and the verifier didn't always match in these |
| 196 | cases. it does now. |
| 197 | |
| 198 | ===== 2.2.8 - 30 March 1995 ==== |
| 199 | |
| 200 | - inside dstep sequences `else' wasn't translated correctly |
| 201 | |
| 202 | ===== 2.2.9 - 12 April 1995 ==== |
| 203 | |
| 204 | - removed a mismatch between spin and xspin in dataflow output |
| 205 | - clarified the scope of dataflow checks spin's -? response |
| 206 | - fixed a typo that could confuse pid assignments when -DNOCLAIM is used |
| 207 | - improved some of spin's outputs a little for xspin's benefit |
| 208 | |
| 209 | ===== 2.2.10 - 18 April 1995 ==== |
| 210 | |
| 211 | - removed a redundancy in the creation of channel templates |
| 212 | during the generation of a verifier with spin option -a |
| 213 | |
| 214 | ===== 2.3.0 - 19 April 1995 ==== |
| 215 | |
| 216 | - an extension of functionality. until now the simulator would execute |
| 217 | a receive test (for instance: q?[var1,var2] ) erroneously with |
| 218 | side-effects, possibly altering the values of the variables. |
| 219 | any boolean condition in Promela, however, must be side-effect free |
| 220 | and therefore the verifier had the correct implementation (no value |
| 221 | transfers in a test of executability of this type) |
| 222 | michael griffioen noted that the poll of a message in a channel was |
| 223 | nonetheless usefull. this leads to a new type of operation in Promela. |
| 224 | pending more thorough documentation, here's an example of |
| 225 | each of the existing ones: |
| 226 | |
| 227 | A. q?var1,const,var2 - fifo receive (constants must be matched) |
| 228 | if successful, the message is removed |
| 229 | from the channel |
| 230 | B. q??var1,const,var - random receive (as A., but from any slot |
| 231 | that has a matching message, checked in |
| 232 | fifo order) if successful, the message is |
| 233 | removed from the channel |
| 234 | C. q?[var1,const,var2] - boolean test of executability of type A receive. |
| 235 | D. q??[var1,const,var2] - boolean test of executability of type B receive. |
| 236 | E. q?<var1,const,var2> - fifo poll, exactly as A, but the message is |
| 237 | not removed from the channel |
| 238 | F. q??<var1,const,var2> - random receive poll, exactly as B, but message |
| 239 | not removed from the channel |
| 240 | |
| 241 | there are still only two different ways to test the executability of a |
| 242 | receive operation without side-effects (be it a normal receive or a poll |
| 243 | operation) |
| 244 | the two new operations of type E and F allow one to retrieve the contents |
| 245 | of a message from a channel, without altering the state of the channel. |
| 246 | all constant fields must of course still be matched, and if no variables |
| 247 | are present, an operation of type E has the same effect as one of type C. |
| 248 | (and similarly for types F and D) |
| 249 | |
| 250 | ===== 2.3.1 - 20 April 1995 ==== |
| 251 | |
| 252 | - slightly more conservative treatment for the change from 2.2.10 |
| 253 | some redundancy is caused by the spec, and now flagged as warnings. |
| 254 | using a \ 5typedef structure that contains an initialized channel in |
| 255 | a formal parameter list, for instance, is always reduncant and uses |
| 256 | up channel templates in the verifier - without otherwise doing harm, |
| 257 | but there is a limit (255) to the number of templates that can exist. |
| 258 | the limit is now also checked and a warning is given when it is exceeded. |
| 259 | |
| 260 | ===== 2.3.2 - 25 April 1995 ==== |
| 261 | |
| 262 | - adjustment of output format of guided simulation to match a recent |
| 263 | change in Xspin (better tracking of printfs in MSC's) |
| 264 | |
| 265 | ===== 2.3.3 - 29 April 1995 ==== |
| 266 | |
| 267 | - bit or bool variables cannot be hidden - this is now reported as a |
| 268 | syntax error if attempted |
| 269 | - the reporting of the options during interactive simulations is |
| 270 | improved - mysterious options, such as [ATOMIC] are now avoided better |
| 271 | |
| 272 | ===== 2.3.4 - 1 May 1995 ==== |
| 273 | |
| 274 | - added the keyword D_proctype as an alternative to proctype to |
| 275 | indicate that all the corresponding processes are expected to |
| 276 | be deterministic. the determinism is not enforced, but it is |
| 277 | checked by the verifier. no other difference exists. a simulation |
| 278 | will not pick up violations of this requirement. |
| 279 | |
| 280 | ===== 2.3.5 - 13 May 1995 ==== |
| 281 | |
| 282 | - the check for enforcing determinism (2.3.4) was not placed |
| 283 | correctly. it is now. |
| 284 | |
| 285 | ===== 2.3.6 - 18 May 1995 ==== |
| 286 | |
| 287 | - removed bug in code generation for arrays of bools |
| 288 | - moved a debug-printf statement |
| 289 | |
| 290 | ===== 2.3.7 - 18 May 1995 ==== |
| 291 | |
| 292 | - removed bug in testing enabledness of run statements |
| 293 | during interactive simulations |
| 294 | |
| 295 | ===== 2.3.8 - 19 May 1995 ==== |
| 296 | |
| 297 | - small change in bitstate mode. the verifier checks if a |
| 298 | new state is previously visited, or appears on the dfs stack. |
| 299 | (information about presence in the stack is only needed to |
| 300 | enforce the partial order reduction rules) |
| 301 | in both cases (in bitstate mode) the check is done via hashing |
| 302 | into a bitarray; with the array for the statespace much larger |
| 303 | than the one for the stack. |
| 304 | so far, if either match succeeded, the search was truncated. |
| 305 | any match in the stack-array that is combined with no-match in |
| 306 | the statespace array, however, is necessarily caused by a |
| 307 | hash-collision (i.e., is a false match) and can be discarded. |
| 308 | the coverage of bitstate runs should improve slightly by this |
| 309 | change. nothing else will be affected. |
| 310 | |
| 311 | ===== 2.4.0 - 22 May 1995 ==== |
| 312 | |
| 313 | - new functionality: there is a new option to SPIN that |
| 314 | can be used in guided simulations (that is: in combination |
| 315 | with the option -t, when following a error trail produced |
| 316 | by one of the verifiers generated by SPIN) |
| 317 | for very lengthy trails, it can take a while to reach an |
| 318 | interesting point in the sequence. by adding the option |
| 319 | -jN one can now skip over the first N steps in the trail |
| 320 | (more precisely: supress the printing during those steps) |
| 321 | and quickly get to the interesting parts. |
| 322 | for instance: |
| 323 | spin -t -p -g -l -v -j1000 spec |
| 324 | skips the first 1000 steps and prints the rest. |
| 325 | caveat: if there are fewer than 1000 steps in the trail, |
| 326 | only the last state of the trail gets printed. |
| 327 | - avoiding some more redundant printouts during guided simulations |
| 328 | will also help to speed up the browsing of error trails with XSPIN |
| 329 | - the extension is supported in the new version of XSPIN as well |
| 330 | - the new version of XSPIN also supports BREAKPOINTS during |
| 331 | all types of simulation |
| 332 | breakpoints are supported via the MSC printf statements |
| 333 | * including a printf that starts with the prefix "MSC: " |
| 334 | in a Promela Model will cause the remainder of the line |
| 335 | printed to be included as a box inside the MSC charts |
| 336 | maintined by XSPIN. |
| 337 | * if the remainder of such a line contains the capitalized word |
| 338 | BREAK, the simulator will pause at that line and wait for |
| 339 | the user to reactivate the run (single step or run) |
| 340 | |
| 341 | ===== 2.4.1 - 4 June 1995 ==== |
| 342 | |
| 343 | - added runtime option -e to verifiers produced by SPIN. |
| 344 | with this option all errors encountered during the verification |
| 345 | are saved in a trail file - up to the limit imposed by -cN |
| 346 | (the default is one trail). the first trail has the extension .trail, |
| 347 | as before (which is also the only extension expected right now under |
| 348 | the guided simulation option -t of SPIN). subsequent trails have |
| 349 | extensions .trail1, .trail2, ... etc. |
| 350 | use this option in combination with -cN |
| 351 | using -c5 -e will produce the first 5 trails, |
| 352 | using -c0 -e will produce all trails. |
| 353 | - modified Xspin to work also with the new Tcl7.4/Tk4.0, which is now |
| 354 | in beta release. the changes should not affect the working under |
| 355 | the current version Tcl7.3/Tk3.6 |
| 356 | - there is now a file called `version_nr' in the directory /netlib/spin |
| 357 | on the distribution server. the file contains just the version |
| 358 | number from the currently distributed SPIN sources (avoids having to |
| 359 | download larger files to find out if anything changed) |
| 360 | - added runtime option -hN to choose another than the default hash-function |
| 361 | (useful in bitstate mode. N must be an integer between 1 and 32) |
| 362 | - improved the implementation of the new runtime option -s (for selecting |
| 363 | single-bit hashing instead of the default double-bit hashing) |
| 364 | especially useful in combination with -hN for sequential multihashing |
| 365 | techniques (iterative approximation of exhaustive searches for very large |
| 366 | problem sizes) |
| 367 | - starting with this version of Xspin there will also be a separate upgrades |
| 368 | script to keep the Tcl/Tk files up to date. |
| 369 | |
| 370 | ===== 2.4.2 - 11 June 1995 ==== |
| 371 | |
| 372 | - so far, variables were created and initialized in the simulator |
| 373 | as late as possible: upon the first reference. a variable that |
| 374 | is never referenced was therefore never created - which is some |
| 375 | sense of economy. however, if the local is initialized with an |
| 376 | expression that includes references to other variables (local or |
| 377 | global) then those other variables might well change value before |
| 378 | the first reference to the initialized local is made - and thus |
| 379 | the local might obtain an unexpected initial value. |
| 380 | the error was caught by Thierry Cattel - and lazy variable creation |
| 381 | is now abandoned. the verifier is unaffected by this fix -- it |
| 382 | already id the right thing (instant creation of all locals on process |
| 383 | initialization). |
| 384 | - channels deeply hidden inside structures were not properly logged |
| 385 | in the partial order reduction tables. it could cause an abort of |
| 386 | a verification run with the mysterious error "unknown q_id, q_cond." |
| 387 | it works properly now. error caught by Greg Duval. |
| 388 | - made a small change in output format (comments only) for remote |
| 389 | references |
| 390 | - made the new runtim option -e (from version 2.4.1) also accessible |
| 391 | from within XSPIN |
| 392 | - changed the MSC canvas in the simulation mode of XSPIn to no longer |
| 393 | be self-scrolling (it defeated any attempt from the user to select |
| 394 | other portions of the MSC to ponder, other than the tail, during a |
| 395 | run). also made the message transfer arrows wider - and added an |
| 396 | option to replace the symbolic step numbers in the MSC's with source |
| 397 | text. |
| 398 | |
| 399 | ===== 2.5 - 7 July 1995 ==== |
| 400 | |
| 401 | Fixes |
| 402 | - values of rendez-vous receives were printed incorrectly in printouts |
| 403 | of spin simulation runs - this could confuse xspin; the symptom was that |
| 404 | some rendez-vous send-recv arrows were not drawn in the MSC displays. |
| 405 | - rendez-vous operations that guarded escapes did not always execute |
| 406 | properly in random simulations. |
| 407 | - in xspin, the boxes produced by an MSC printf could lose its text |
| 408 | after the cursor would pass over it - that's no longer the case |
| 409 | - the use of a remote references used to disable the partial order |
| 410 | reduction algorithm. instead, such references now automatically label |
| 411 | the transition that enters or exits from the corresponding process state |
| 412 | as unsafe. this suffices to preserve the use of the partial order |
| 413 | reduction. (proposed by Ratan Nalumasu.) |
| 414 | |
| 415 | Small Changes |
| 416 | - added a print line in verbose output for process creations - as well |
| 417 | as process terminations. it will be used in a future version of xspin. |
| 418 | - made all xspin verification run timed - the user+system time info |
| 419 | appears in the xspin logs |
| 420 | - on aborted verification runs, xspin will now also print the partial |
| 421 | information gathered up to the point of the abort |
| 422 | - slightly changed the way aborts are handled in xspin |
| 423 | - never claims containing assignments (i.e., side-effects) can be useful |
| 424 | in some cases. spin will still generate warnings, but allows the user |
| 425 | to ignore them (i.e., the exit status of spin is no longer affected) |
| 426 | - in simulation mode - xspin now pays attention to filenames and will not |
| 427 | try to hilight lines in files that are not visible in the main text window |
| 428 | - added compile-time directive -DNOFAIR to allow compilation of a verifier |
| 429 | if it is known that the weak-fairness option will not be used -- this |
| 430 | avoids some memory overhead, and runs slightly faster. |
| 431 | the fastest run can be obtained by compiling -DNOCOMP -DNOFAIR (turning |
| 432 | off the state compression and the weak fairness related code) |
| 433 | the most memory frugal run (apart from the effects of -DREDUCE) can be |
| 434 | obtained by compiling with just -DNOFAIR (and leaving compression turned |
| 435 | on by default) note that memory consumed also goes up with the value |
| 436 | provided for the -m option (the maximum depth of the stack) |
| 437 | - added a file Doc/Pan.Directives with an overview of all user definable |
| 438 | compile-time directives of the above type. |
| 439 | |
| 440 | Extension |
| 441 | - added a mechanism to define process priorities for use during random |
| 442 | simulations - to make high priority processes more likely to execute |
| 443 | than low priority processes. |
| 444 | as alternatives to the standard: |
| 445 | run pname(...) |
| 446 | active proctype pname() { ... } |
| 447 | you may now add a numeric execution priority: |
| 448 | run pname(...) priority N |
| 449 | and/or |
| 450 | active proctype pname() priority N |
| 451 | (with N a number >= 1) |
| 452 | the default execution priority is 1; a higher number indicates a |
| 453 | higher priority. for instance, a priority 10 process is 10x more |
| 454 | likely to execute than a priority 1 process, etc. |
| 455 | the priority specified at the proctype declaration only affects the |
| 456 | processes that are initiated through the `active' prefix |
| 457 | a process instantiated with a run statement always gets the priority |
| 458 | that is explicitly or implicitly specified there (the default is 1). |
| 459 | the execution priorities have no effect during verification, guided, |
| 460 | or interactive simulation. |
| 461 | - added an example specification file (Test/priorities) to verify the |
| 462 | correct operation of the execution priorities |
| 463 | |
| 464 | ===== 2.5.1 - 12 July 1995 ==== |
| 465 | |
| 466 | - some tweaks to correct the last update (a simulation run could |
| 467 | fail to terminate - and xspin could fail to detect the zero exit |
| 468 | status of spin after warning messages are printed) |
| 469 | |
| 470 | ===== 2.6 - 16 July 1995 ==== |
| 471 | |
| 472 | - added a new option for executable verifiers - to compute the effective |
| 473 | value range of all variables during executions. |
| 474 | the option is enabled by compiling pan.c with the directive -DVAR_RANGES |
| 475 | values are tracked in the range 0..255 only - to keep the memory |
| 476 | and runtime overhead introduced by this feature reasonable. |
| 477 | (the overhead is now restricted to roughly 40 bytes per variable - |
| 478 | it would increase to over 8k per variable if extended to the full |
| 479 | range of 16-bit integers) |
| 480 | - a new option in the validation panel to support the above extension |
| 481 | was added |
| 482 | - xspin now supports compile-time option -DNOFAIR to produce faster |
| 483 | verifiers when the weak fairness option is not selected |
| 484 | - added an example in directory Test to illustrate dynamic creation |
| 485 | of processes (Test/erathostenes) |
| 486 | - removed an error message that attempted to warn when a data structure |
| 487 | that contained an initialized channel was passed to a process as a |
| 488 | formal parameter. it leads to the creation of a redundant channel, |
| 489 | but is otherwise harmless. |
| 490 | - changed the data types of some option flags from int to short |
| 491 | |
| 492 | ===== 2.6.1 - 18 July 1995 ==== |
| 493 | |
| 494 | - option -jN (introduced in version 2.4.0) -- to skip the verbose |
| 495 | printouts for the first N execution steps -- now also works in |
| 496 | random simulation mode. |
| 497 | only process creations and terminations are still always printed |
| 498 | - channel names are no longer included in the -DVAR_RANGES output |
| 499 | at least not by default (see version 2.6 - above) |
| 500 | to still include them, generate the verifier in verbose mode |
| 501 | as ``spin -a -v spec'' instead of the default ``spin -a spec'' |
| 502 | - predefined variable _last was not quite implemented correctly |
| 503 | in the verifier (the error was harmless, but if you tried to write |
| 504 | specifications that included this construct, you may have had |
| 505 | more trouble than necessary getting it to work properly) |
| 506 | |
| 507 | ===== 2.7.Beta - 24 July 1995 ==== |
| 508 | |
| 509 | Fixes |
| 510 | - when an atomic sequence blocks, the process executing that sequence |
| 511 | loses control, and another process can run. when all processes block, |
| 512 | the predefined variable 'timeout' becomes true, and all processes again |
| 513 | get a chance to execute. if all processes still block - we have reached |
| 514 | an end-state (valid or invalid, depending on how states are labeled). |
| 515 | until now, timeout was allowed to become true before an atomically |
| 516 | executing process could lose control - this is not strictly conform the |
| 517 | semantics given above, and therefore no longer possible. |
| 518 | - it is now caught as a runtime error (in verification) if an attempt |
| 519 | is made to perform a rendez-vous operation within a d_step sequence. |
| 520 | - it is also caught as an error if a 'timeout' statement is used inside |
| 521 | a d_step sequence (it may be used as the first statement only) |
| 522 | - an else statement that appears jointly with i/o statements in |
| 523 | a selection structure violates the rules of a partial order |
| 524 | reduction. a warning is now included if this combination is seen, both |
| 525 | at compile-time and at run-time. the combination should probably be |
| 526 | prevented alltogether since its semantics are also not always clear. |
| 527 | - one more correction to the implementation of 'else' inside dsteps |
| 528 | to avoid a possibly unjustified error report during verification |
| 529 | - a previously missed case of the appearance of multiple 'else' statements |
| 530 | in selection structures is now caught and reported |
| 531 | - fixed a missing case were process numbers (_pid's) did not match |
| 532 | between a verification run and a guided simulation run. (if a never |
| 533 | claim was used, there could be an off-by-one difference.) |
| 534 | - rendez-vous operations are now offered as a choice in interactive |
| 535 | simulation mode only when they are executable - as they should be |
| 536 | - the introduction of active proctypes in 2.5 introduced an obscure |
| 537 | line-number problem (after the first active proctype in a model |
| 538 | that contains initialized local vars, the line numbers could be |
| 539 | off). it's fixed in this version. |
| 540 | |
| 541 | Extensions |
| 542 | - The main extension added in this release is the inclusion of an |
| 543 | algorithm, due to Gerth, Peled, Wolper and Vardi, for the translation |
| 544 | from LTL formulae into Promela never claims. The new options are |
| 545 | supported both in SPIN directly, and from XSPIN's interface. |
| 546 | |
| 547 | - added the option to specify an enabling condition for each |
| 548 | proctype. the syntax is as follows: |
| 549 | proctype name(...) provided ( expression ) |
| 550 | { |
| 551 | ... |
| 552 | } |
| 553 | where the expression is a general side-effect free expression |
| 554 | that may contain constants, global variables, and it may contain |
| 555 | the predefined variables timeout and _pid, but not other local |
| 556 | variables or parameters, and no remote references. |
| 557 | |
| 558 | the proctype may be declared active or passive. no enabling |
| 559 | conditions can be specified on run statements unfortunately. |
| 560 | the provided clauses take effect both during simulation runs |
| 561 | and during verification runs. |
| 562 | |
| 563 | - extended XSPIN with a barchart that can give a dynamic display |
| 564 | of the relative fraction of the system execution that is used by |
| 565 | each process. modified the layout of the Simulation option panel, |
| 566 | to make some of the runtime display panels optional. |
| 567 | |
| 568 | - added a <Clear> button to most text windows (to clear the contents |
| 569 | of the display) |
| 570 | |
| 571 | - added <Larger> and <Smaller> scaling buttons to canvas displays |
| 572 | (that is: the FSM view displays and the MSC display). the buttons |
| 573 | show up when the image is complete (e.g., when the message sequence |
| 574 | chart has been completed) - so that it can be scaled to size as a |
| 575 | whole. |
| 576 | |
| 577 | - added new <Help> buttons, with matching explanations, to most display |
| 578 | panels - and updated and extended the help menus. |
| 579 | |
| 580 | ===== 2.7 - 3 August 1995 ==== |
| 581 | |
| 582 | - fixed possible memory allignment problem on sun sytems |
| 583 | - several fine tunings of xspin |
| 584 | - made it possible to let the vectorsize get larger than 2^15 bytes |
| 585 | to support very large models |
| 586 | - a provided clause has no effect inside d_step sequences, but it |
| 587 | is looked at during atomic sequences. this rule is now enforced |
| 588 | equally in simulation and validation. |
| 589 | - the use of enabled() and pc_value() outside never claims now triggers |
| 590 | a warning instead of an error message (i.e., it is now accepted). |
| 591 | in models with synchronous channels, the use of enabled() still makes |
| 592 | verification impossible (both random and interactive simulations will |
| 593 | work though) |
| 594 | - added an option to `preserve' a message sequence chart across |
| 595 | simulation runs (by default, all remnants of an old run are removed) |
| 596 | |
| 597 | ===== 2.7.1 - 9 August 1995 ==== |
| 598 | |
| 599 | - removed bug in the code that implements the compile time directive |
| 600 | to verifier source -DNOFAIR, which was introduced in version 2.5, |
| 601 | (and picked up starting with version 2.6 also via xspin). |
| 602 | |
| 603 | ===== 2.7.2 - 14 August 1995 ==== |
| 604 | |
| 605 | - the LTL formula parser accidentily swapped the arguments of U and V |
| 606 | operators. it does it correctly now. the associativity of U and |
| 607 | V now defaults to left-associative. |
| 608 | - arithmetic on channel id's was so far silently condoned. |
| 609 | it is now flagged as an error. it is still valid to say: c = d, |
| 610 | if both c and d are declared as chan's, but d may no longer be |
| 611 | part of an expression. |
| 612 | - unless operators now distribute properly to (only) the guard of |
| 613 | d_step sequences (but not into the body of the d_step). |
| 614 | |
| 615 | ===== 2.7.3 - 15 August 1995 ==== |
| 616 | |
| 617 | - tweek in implementation of provided clauses - to make it possible |
| 618 | to use `enabled()' inside them. |
| 619 | |
| 620 | ===== 2.7.4 - 25 September 1995 ==== |
| 621 | |
| 622 | - fixed a small omission in the implementation of dsteps |
| 623 | - allowed `else' to be combined with boolean channel references |
| 624 | such as len and receive-poll |
| 625 | - added some compiler directives for agressively collapsing |
| 626 | the size of state vectors during exhaustive explorations. |
| 627 | this option is still experimental |
| 628 | - made some cosmetic changes in the look and feel of xspin |
| 629 | |
| 630 | ===== 2.7.5 - 7 October 1995 ==== |
| 631 | |
| 632 | - the value returned by a run statement triggered and |
| 633 | unwarranted error report from spin, if assigned to a variable |
| 634 | - xspin didn't offer all possible choices in the menus, when |
| 635 | used in interactive simulation mode |
| 636 | - somewhat more careful in closing file descriptors once they |
| 637 | are no longer needed (to avoid running out on some systems) |
| 638 | - some small cosmetic changes in xspin (smaller arrows in the |
| 639 | message sequence chart - to improve readability) |
| 640 | |
| 641 | ===== 2.7.6 - 8 December 1995 ==== |
| 642 | |
| 643 | - added a compiler directive PC to allow for compiling the |
| 644 | SPIN sources for a PC. (this is only needed in the makefile |
| 645 | for spin itself - not for the pan.? files.) |
| 646 | if you generate a y.tab.c file with yacc on a standard Unix |
| 647 | machine, you must replace every occurrence of y.tab.[ch] |
| 648 | with y_tab.[ch] in all the spin sources as well before compiling. |
| 649 | some of the source file names also may need to be shortened. |
| 650 | - some syntax errors reported by spin fell between the cracks |
| 651 | in xspin simulations. they are now correctly reported in the |
| 652 | simulation window and the log window. |
| 653 | - in interactive simulation mode - typing `q' is now a recognized |
| 654 | way to terminate the session |
| 655 | - option -jN (skip output for the first N steps) now also works |
| 656 | for interactive simulations. the first N steps are then as in |
| 657 | a random simulation. |
| 658 | - FSMview in xspin is updated to offer also the statemachine |
| 659 | view for never claims - and to suppress the one for an init |
| 660 | segment, if none is used |
| 661 | - fixed a bug in implementation of hidden structures - some of |
| 662 | the references came out incorrectly in the pan.c code |
| 663 | |
| 664 | ===== 2.7.7 - 1 February 1996 ==== |
| 665 | |
| 666 | - made it possible to combine the search for acceptance cycles |
| 667 | with one for non-progress cycles, to find cycles with at least |
| 668 | one accepting state and no progress states. |
| 669 | the combined search is compatible with -f (weak fairness). |
| 670 | [note added at 2.8.0 -- this wasn't completely robust, and |
| 671 | therefore undone in 2.8.0] |
| 672 | - added the explicit choice for the specification of a positive |
| 673 | or a negative property in LTL interface to xspin |
| 674 | - fixed a bug in the ltl translator (it failed to produce the correct |
| 675 | automaton for the right-hand side of an until-clause, if that clause |
| 676 | contained boolean and-operators) |
| 677 | - in non-xspin mode, process states are now identified as <endstates> |
| 678 | (where applicable) in the simulation trails |
| 679 | - it is now flagged as an error if a `run' statement is used |
| 680 | inside a d_step sequence |
| 681 | - added two new options ( -i and -I ) for the generated verifiers |
| 682 | (pan -i / pan -I). recommended compilation of pan.c is with -DREACH |
| 683 | for exhaustive mode (-DREACH has no effect on BITSTATE mode). |
| 684 | option -i will search for the shortest path to an error. |
| 685 | the search starts as before - but when an error is found, the |
| 686 | search depth (-m) is automatically truncated to the length of that |
| 687 | error sequence - so that only shorter sequences can now be |
| 688 | found. the last sequence generated will be the shortest one possible. |
| 689 | option -I is more aggressive: it halves the search depth |
| 690 | whenever an error is found, to try to generate one that is at most |
| 691 | half the length of the last generated one. |
| 692 | if no errors are found at all, the use of -i or -I has no effect on |
| 693 | the coverage of search performed (but the effect of using -DREACH |
| 694 | is an increase in memory and time used, see the notes at version 2.2). |
| 695 | |
| 696 | ===== 2.7.8 - 25 February 1996 ==== |
| 697 | |
| 698 | Extensions |
| 699 | - a new runtime option on the verifiers produced by Spin is -q |
| 700 | it enforces stricter conformance to what is promised in the book. |
| 701 | by default, the verifiers produced by Spin require each process to have |
| 702 | either terminated or be in a state labeled with an endstate-label, when |
| 703 | the system as a whole terminates. the book says that for such a state |
| 704 | to be valid also all channels must be empty. option -q enforces that |
| 705 | stricter check (which is not always necessary). the option was suggested |
| 706 | by Pim Kars of Twente Univ., The Netherlands. |
| 707 | - `mtype' is now a real data-type, that can be used everywhere a `bit' |
| 708 | `byte' `short' or `int' data-type is valid. |
| 709 | variables of type `mtype' can be assigned symbolic values from the range |
| 710 | declared in mtype range definitions (i.e.: mtype = { ... }; ). |
| 711 | the value range of an mtype variable (global or local) remains equal |
| 712 | to that of a `byte' variable (i.e., 0..255). |
| 713 | for instance: |
| 714 | mtype = { full, empty, half_full }; |
| 715 | mtype glass = empty; |
| 716 | the extension was suggested by Alessandro Cimatti, Italy. |
| 717 | - the formfeed character (^L or in C-terms: \f) is now an acceptable |
| 718 | white space character -- this makes it easier to produce printable |
| 719 | promela documents straight from the source (also suggested by Cimatti). |
| 720 | - a new predefined and write-only (scratch) variable is introduced: _ |
| 721 | the variable can be assigned to in any context, but it is an error to |
| 722 | try to read its value. for instance: |
| 723 | q?_,_,_; /* to remove a message from q */ |
| 724 | _ = 12; /* assign a value to _ (not very useful) */ |
| 725 | the value of _ is not stored in the state-vector |
| 726 | it may replace the need for the keyword `hidden' completely |
| 727 | the syntax was suggested by Norman Ramsey (inspired by Standard ML) |
| 728 | |
| 729 | Fixes |
| 730 | - the FSM-view mode in xspin wasn't very robust, especially when moving |
| 731 | nodes, or changing scale. it should be much better now. button-1 or |
| 732 | button-2 can move nodes around. click button-1 at any edge to see |
| 733 | its edge label (it no longer comes up when you hover over the edge - |
| 734 | the magic point was too hard to find in many cases). |
| 735 | - fixed bug in processing of structure names, introduced in 2.7.5, caught |
| 736 | by Thierry Cattel, France. |
| 737 | - trying to pass an array hidden inside a structure as a parameter |
| 738 | to a process (in a run statement) was not caught as a syntax error |
| 739 | - trying to pass too many parameters in same also wasn't caught |
| 740 | - in interactive mode, the menus provided by xspin were sometimes |
| 741 | incorrect for interactions in a rendez-vous system, caught by Pim Kars. |
| 742 | |
| 743 | ===== 2.8.0 - 19 March 1996 ==== |
| 744 | |
| 745 | - new version of the Spin sources that can be compiled, installed, and |
| 746 | used successfully on PC systems running Windows95. |
| 747 | (Because of remaining flaws in the latest Tcl/Tk 7.5/4.1 beta 3 |
| 748 | release, Xspin will not run on Windows 3.1 systems. Spin itself |
| 749 | however will work correctly on any platform.) |
| 750 | to compile, you'll need the public domain version of gcc and yacc for PCs, |
| 751 | (see README.spin under Related Software, for pointers on where to |
| 752 | get these if you don't already have them) |
| 753 | |
| 754 | to use Spin on a PC, compile the Spin sources with directive -DPC |
| 755 | (if you have no `make' utitility on the PC, simply execute the |
| 756 | following three commands to obtain a spin.exe |
| 757 | byacc -v -d spin.y |
| 758 | gcc -DPC *.c -o spin |
| 759 | coff2exe spin |
| 760 | alternatively, use the precompiled spin.exe from the distribution |
| 761 | (contained in the pc_spin280.zip file) |
| 762 | |
| 763 | - small extension of xspin - lines with printf("MSC: ...\n") show up |
| 764 | in xspin's graphical message sequence chart panel. the colors can now |
| 765 | also be changed from the default yellow to red green or blue, |
| 766 | respectively, as follows; |
| 767 | printf("MSC: ~R ...\n") |
| 768 | printf("MSC: ~G ...\n") |
| 769 | printf("MSC: ~B ...\n") |
| 770 | (suggested by Michael Griffioen, The Netherlands) |
| 771 | - small changes to improve portability and ANSI compliance of the C code |
| 772 | - compile-time option -DREDUCE (partial order reduction) is now the |
| 773 | default type of verification. both spin and xspin now use this default. |
| 774 | to compile a verifier without using reduction, compile -DNOREDUCE |
| 775 | - missed case of syntax check for use of _ as lvalue corrected |
| 776 | - missed case of printing mtype values in symbolic form also corrected |
| 777 | - printfs no longer generate output during verification runs |
| 778 | (this was rarely useful, since statements are executed in DFS search |
| 779 | order and maybe executed repeatedly in seemingly bewildering order) |
| 780 | a compile time directive -DPRINTF was added to suppress this change |
| 781 | (this may be useful in debugging, but in little else) |
| 782 | this relies on stdarg.h being available on your system - if not, compile |
| 783 | Spin itself with -DPRINTF, and the new code will not be added. |
| 784 | |
| 785 | ===== 2.8.1 - 12 April 1996 ==== |
| 786 | |
| 787 | - we found a case where the partial order reduction method |
| 788 | introduced in Spin version 2.0 was not compatible with |
| 789 | the nested depth-first search method that Spin uses for |
| 790 | cycle detection (i.e., runtime options -a and -l) |
| 791 | the essence of the problem is that reachability properties |
| 792 | are affected by the so-called `liveness proviso' from the |
| 793 | partial order reduction method. this `liveness proviso' |
| 794 | acted on different states in the 1st and in the 2nd dfs, |
| 795 | which could affect the basic reachability properties of states. |
| 796 | the problem is corrected in 2.8.1. as a side-effect of this |
| 797 | upgrade, a few other problems with the implementation of the |
| 798 | nested depth first searches were also corrected. in some cases |
| 799 | the changes do cause an increase of memory requirements. |
| 800 | a new compiler directive -DSAFETY is added to make sure that |
| 801 | more frugal verifiers can be produced if liveness is not required. |
| 802 | - other fixes - one small fix of interactive simulation mode - |
| 803 | some small fixes to avoid compiler warnings in tl_parse.c - |
| 804 | a fix in pangen3.h to avoid a compile-time error for a few |
| 805 | cases of index bound-checking. small fixes in tl_buchi and |
| 806 | tl_trans to correct treatment of "[]true" and "[]false" |
| 807 | - cosmetic changes to the xspin tcl/tk files |
| 808 | |
| 809 | ===== 2.8.2 - 19 April 1996 ==== |
| 810 | |
| 811 | - revised Doc/WhatsNew.ps to match the extensions in the |
| 812 | current version of the software |
| 813 | - one more change to the algorithm for acceptance cycle detection |
| 814 | - changed filenames for multiple error-trails (to ease use on PCs) |
| 815 | from spec.trail%d to spec%d.trail |
| 816 | - some small changes to improve portability |
| 817 | |
| 818 | ===== 2.8.3 - 23 April 1996 ==== |
| 819 | |
| 820 | - corrected a missed optimization in the new acceptance cycle detection |
| 821 | algorithm from 2.8.[12] |
| 822 | - corrected a problem with blocking atomic sequences in pangen1.h |
| 823 | - added a predefined function predicate np_ |
| 824 | the value of np_ is true if the system is in a non-progress state |
| 825 | and false otherwise. (claim stutter doesn't count as non-progress.) |
| 826 | np_ can only be used inside never claims, and if it is used all |
| 827 | transitions into and out of progress states become visible/global |
| 828 | under the partial order reduction |
| 829 | - background: |
| 830 | the intended purpose of np_ is to support a more efficient check |
| 831 | for the existence of non-progress cycles. (the efficient check we |
| 832 | had was lost with the changes from 2.8.[12]) instead of the default |
| 833 | check with runtime option -l, a more efficient method (under partial |
| 834 | order reduction) is to use the never claim: |
| 835 | never { |
| 836 | /* non-progress: <>[] np_ */ |
| 837 | do |
| 838 | :: skip |
| 839 | :: np_ -> break |
| 840 | od; |
| 841 | accept: do |
| 842 | :: np_ |
| 843 | od |
| 844 | } |
| 845 | and to perform a standard check for acceptance cycles (runtime |
| 846 | option -a) -- the partial order reduction algorithm can optimize |
| 847 | a search for the existence of acceptance cycles much better than |
| 848 | one for non-progress cycles. |
| 849 | a related advantage of searching for non-progress cycles with an |
| 850 | LTL property is that the LTL formula (<>[] np_) can easily be |
| 851 | combined with extra LTL properties, to built more sophisticated |
| 852 | types of searches. |
| 853 | |
| 854 | ===== 2.8.4 - 25 April 1996 ==== |
| 855 | |
| 856 | - cycles are closed at a different point in the dfs with the change from |
| 857 | 2.8.[12], as a result, the cycle-point was no longer accurate - which |
| 858 | could be confusing. fixed |
| 859 | - all moves through progress states and accepting states within the program |
| 860 | are visible under the partial order reduction rules. it is unlikely that |
| 861 | one would use extra accept labels in a program, if an LTL property or a |
| 862 | never claim with accept labels is used, but just in case, this is covered. |
| 863 | |
| 864 | ===== 2.8.5 - 7 May 1996 ==== |
| 865 | |
| 866 | - process creation and process deletion are global actions |
| 867 | they were incorrectly labeled as safe/local actions for the |
| 868 | purposes of partial order reduction. they are global, because |
| 869 | the execution of either one can change the executability of |
| 870 | similar actions in other processes |
| 871 | - didn't catch as an error when too many message parameters are |
| 872 | specified in a receive test q?[...] (in verifications). |
| 873 | it was reported in all other cases, just not for queue tests |
| 874 | (the simulator reported it correctly, when flag -r is used) |
| 875 | - peculiar nestings of array and non-array structure elements |
| 876 | could generate incorrect code |
| 877 | - with fairness enabled (-f), cycles were sometimes closed at the |
| 878 | wrong place in the runtime verifiers. |
| 879 | - a variable initialized with itself could cause spin to go into |
| 880 | an infinite loop. the error is now caught properly. |
| 881 | |
| 882 | ===== 2.8.6 - 17 May 1996 ==== |
| 883 | |
| 884 | - timeout's weren't always marked as global actions in partial |
| 885 | order reductions - they are now -- this can cause a small increase |
| 886 | in the number of reached states during reduced searches |
| 887 | - fixed error that could cause a coredump on a remote reference |
| 888 | during guided simulations (reported by Joe Lin, Bellcore) |
| 889 | - improved the efficiency of partial order search for acceptance |
| 890 | cycles in bitstate mode. (for non-progress cycles, though, we still |
| 891 | can't take much advantage of reduction during bitstate searches) |
| 892 | - fixed the error that caused the extent of a cycle not to be |
| 893 | marked correctly in bitstate mode (the trails were always correct, |
| 894 | but the cycle point was sometimes placed incorrectly) |
| 895 | - fixed error that could cause non-existent acceptance cycles to |
| 896 | be produced in bitstate mode (hopefully the last aftershock from |
| 897 | the correction of the cycle detection method in version 2.8.1) |
| 898 | |
| 899 | ===== 2.9.0 - 14 July 1996 ==== |
| 900 | |
| 901 | - Important Change: |
| 902 | Spin now contains a predefined never claim template that captures |
| 903 | non-progress as a standard LTL property (it is the template described |
| 904 | under the notes for 2.8.3 above) |
| 905 | this made it possible to unify the code for -a and -l; it brings |
| 906 | option -l (non-progress cycle detection) within the same automata |
| 907 | theoretic framework as -a; and it secures full compatibility of |
| 908 | both options -a and -l with partial order reduced searches. |
| 909 | |
| 910 | compiled versions of pan.c now support *either* -a *or* -l, not both |
| 911 | |
| 912 | by default, the verifiers check for safety properties and standard |
| 913 | buchi acceptance (option -a). |
| 914 | to search for non-progress cycles (i.e., to *replace* option -a with |
| 915 | option -l), compile the verifier with the new directive -DNP |
| 916 | - Xspin 2.9.0 supports this change, and makes it invisible to the user. |
| 917 | |
| 918 | - the state vector length is now added explicitly into the state vector. |
| 919 | in virtually all cases this is redundant, but it is safer. |
| 920 | it can optionally be omitted from the state vector again (saving |
| 921 | 4 bytes of overhead per state) with the new compiler directive -DNOVSZ |
| 922 | |
| 923 | - the verifiers didn't allow a d_step sequence to begin with a |
| 924 | rendez-vous receive operation. that's now fixed. |
| 925 | |
| 926 | - change in the as-yet non-documented mode for extra agressive |
| 927 | state compressions (added in version 2.7.4, not enabled yet for |
| 928 | normal use - more information on this mode will come later) |
| 929 | |
| 930 | - assignments to channel variables can violate xr/xs assertions. |
| 931 | there is now a check to catch such violations |
| 932 | |
| 933 | - updated the PC executable of xspin for the newer current version of |
| 934 | gcc - updated the readme files to match the above changes |
| 935 | |
| 936 | - added the code for handling the Next Operator from LTL. the code is |
| 937 | not yet enabled (to enable it, compile the sources with -DNXT added). |
| 938 | note that when partial order reduction is used this operator cannot |
| 939 | be used. we'll figure out the appropriate warnings and then enable |
| 940 | the code (i.e., when you use it, you must compile pan.c with -DNOREDUCE). |
| 941 | - in the process of this update, we also caught a bug in the translation |
| 942 | of LTL formulae into never claims (affecting how the initial state of |
| 943 | the claim was encoded). the implementation has meanwhile been subjected |
| 944 | to a more thorough check of the correctness of the translation -- using |
| 945 | another model checker (cospan) as a sanity check. (both model checkers |
| 946 | have passed the test) |
| 947 | |
| 948 | ===== 2.9.1 - 16 September 1996 ==== |
| 949 | |
| 950 | - no major changes - some purification and minor fixes |
| 951 | - updated email address for bug reports to bell-labs.com in |
| 952 | all source files |
| 953 | - disallowed remote references inside d_step sequences |
| 954 | (the verifier has no problem, but the simulator may |
| 955 | resolve these differently can cause strange guided |
| 956 | simulation results) |
| 957 | - provided some missing arguments to a routine in pangen1.c |
| 958 | that could trigger compile time errors before |
| 959 | - improved the COLLAPSE modes to be slightly more frugal |
| 960 | - added explicit casts from shorts to ints to avoid warnings |
| 961 | of some compilers... also fixed a possible bad reference |
| 962 | to the stack if an error is found in the first execution step |
| 963 | - fixed a case where the cycle-extent wasn't set correctly |
| 964 | (found by stavros tripakis) |
| 965 | - write and rewrite just a single trail-file for options -[iI] |
| 966 | (instead of numbered trails) |
| 967 | - fixed a bug in weak fairness cycle detection that had crept |
| 968 | in with the overhaul from version 2.8 |
| 969 | - fixed order of variable initialization in simulator (can |
| 970 | make a difference if a local variable is initialized with |
| 971 | the value of a parameter, which should now work correctly) |
| 972 | - expanded the number of options accessible through Xspin |
| 973 | |
| 974 | ===== 2.9.2 - 28 September 1996 ==== |
| 975 | |
| 976 | - with a -c0 flag, the 2.9.1 verifiers would still stop at the |
| 977 | first error encountered, instead of ignoring all errors. |
| 978 | has been corrected (-c0 means: don't stop at errors) |
| 979 | - corrected the instructions and the numbers in Test/README.tests |
| 980 | for the current version of spin (for leader and pftp there are |
| 981 | some small differences) |
| 982 | |
| 983 | ===== 2.9.3 - 5 October 1996 ==== |
| 984 | |
| 985 | - added a function eval() to allow casting a variable name into |
| 986 | a constant value inside receive arguments. this makes it possible |
| 987 | to match a message field with a variable value, as in |
| 988 | q?eval(_pid),par2,par3 |
| 989 | until now, only constant values could be matched in this way. |
| 990 | note that in the above example the value of _pid does not change, |
| 991 | but it guarantees that the receive is unexecutable unless the first |
| 992 | message parameter is equal to the value of variable _pid |
| 993 | eval() can be used for any message field - the argument must be a |
| 994 | (local or global) variable reference (not be a general expression). |
| 995 | - in the process, discovered that global references inside the parameter |
| 996 | list of send or receive statements would not be detected for the |
| 997 | marking of safe and unsafe statements for the partial order reduction. |
| 998 | this is now corrected - it may lead to a small increase in the number |
| 999 | of reachable states under partial order reduction |
| 1000 | |
| 1001 | ===== 2.9.4 - 4 November 1996 ==== |
| 1002 | |
| 1003 | - the order of initialization of parameters and local variables after |
| 1004 | a process instantiation was incorrect in the verifier - this could |
| 1005 | be noticed when a local var was instantiated with a formal parameter |
| 1006 | inside the variable declaration itself (the verifier failed to do this). |
| 1007 | - added a missing case for interpreting eval() in run.c (see 2.9.3) |
| 1008 | - removed possible erroneous behavior during interactive simulations |
| 1009 | when a choice is made between multiple rendez-vous handshakes |
| 1010 | - added SVDUMP compiler directive and some extra code to allow for the |
| 1011 | creation of a statespace dump into a file called sv_dump |
| 1012 | - added an option in Xspin to redraw the layout of an FSM-view using |
| 1013 | the program 'dot' -- the option automatically enables itself if xspin |
| 1014 | notices that 'dot' is available on the host system (an extra button |
| 1015 | is created, giving the redraw option) |
| 1016 | |
| 1017 | ===== 2.9.5 - 18 February 1997 ==== |
| 1018 | |
| 1019 | - thoroughly revised -DCOLLAPSE -- it can now be used without |
| 1020 | further thought to reduce memory requirements of an exhaustive run |
| 1021 | by up to 80-90% without loss of information. the price is an |
| 1022 | increase in runtime by 2x to 3x. |
| 1023 | - added new compiler directives -DHYBRID_HASH and -DCOVEST |
| 1024 | (both for experimental use, see the Pan.Directives file) |
| 1025 | - renamed file sv_dump (see 2.9.4) to 'spec'.svd, for compatibility |
| 1026 | with PCs |
| 1027 | - removed spin's -D option (dataflow). it was inaccurate, and |
| 1028 | took up more source code than warranted (300 lines in main.c and |
| 1029 | another 60 or so in Xspin) |
| 1030 | |
| 1031 | ===== 2.9.6 - 20 March 1997 ==== |
| 1032 | |
| 1033 | - bug fix -- for vectorsizes larger than 1024 the generated |
| 1034 | code from 2.9.5 contained an error in the backward execution |
| 1035 | of the transition for send operations. (this did not |
| 1036 | affect the verification unless a compiler directive -DVECTORSZ=N |
| 1037 | with N>1024 was used -- which triggered an error-report) |
| 1038 | - sometimes one may try typing 'pan -h' instead of 'pan -?' |
| 1039 | to get the options listing of the verifiers. this now gives |
| 1040 | the expected response. |
| 1041 | - previous versions of the spin Windows95 executable in pc_spin*.zip |
| 1042 | were compiled as 16-bit executable -- the current version is a |
| 1043 | 32-bit executable. the newer versions of tcl/tk actually care |
| 1044 | about the difference and will hang if you try to do a simulation |
| 1045 | run with one of the older spin executables installed... |
| 1046 | - discrepancy in the stats on memory use reported at the end of a |
| 1047 | bitstate run corrected. |
| 1048 | - new xspin295 file that corrects a problem when xspin is used on |
| 1049 | unix systems with a file name argument (it reported an undeclared |
| 1050 | function). |
| 1051 | |
| 1052 | ===== 2.9.7 - 18 April 1997 ==== |
| 1053 | |
| 1054 | - spin now recognizes a commandline option -P that can be used to |
| 1055 | define a different preprocessor. the default behavior on Unix |
| 1056 | systems corresponds to: |
| 1057 | spin -P/lib/cpp [..other options..] model |
| 1058 | and on solaris systems: |
| 1059 | spin -P/usr/ccs/lib/cpp [..other options..] model |
| 1060 | (note, these two are the defaults, so these are just examples) |
| 1061 | use this option to define your own preprocessor for Promela++ variants |
| 1062 | - bitstate mode can be made to hash over compressed state-vectors |
| 1063 | (using the byte-masking method). this can improve the coverage |
| 1064 | in some cases. to enable, use -DBCOMP |
| 1065 | - -DSVDUMP (see 2.9.4) now also works in -DBITSTATE mode |
| 1066 | - added compiletime option -DRANDSTORE=33 to reduce the probability of |
| 1067 | storing the bits in the hasharray in -DBITSTATE mode to 33% |
| 1068 | give an integer value between 0 and 99 -- low values increase |
| 1069 | the amount of work done (time complexity) roughly by the reverse |
| 1070 | of the probability (i.e., by 5x for -DRANDSTORE=20), but they also |
| 1071 | increase the effective coverage for oversized systems. this can be |
| 1072 | useful in sequential bitstate hashing to improve accumulative coverage. |
| 1073 | - combined the 3 readme-files into a single comprehensive README. |
| 1074 | |
| 1075 | ===== 3.0.0 - 29 April 1997 ==== |
| 1076 | |
| 1077 | - new additions to Spin's functionality that motivates upping the |
| 1078 | version number to 3.0: |
| 1079 | |
| 1080 | 1. a new BDD-like state compression option based on |
| 1081 | the storage of reachable states in an automaton, |
| 1082 | combined with a checkpoint/recovery option for long runs. |
| 1083 | for the automata based compression, compiled -DMA=N |
| 1084 | with N the maximum length of the statevector in bytes |
| 1085 | expected (spin will complain if you guess too low) |
| 1086 | for checkpointing, compile -DW_XPT |
| 1087 | to get a checkpoint file written out every multiple |
| 1088 | of one million states stored |
| 1089 | for restarting a run from a checkpoint file, compile -DR_XPT |
| 1090 | |
| 1091 | 2. addition of "event trace" definitions. for a description |
| 1092 | see Section 4 of the extended WhatsNew.ps |
| 1093 | |
| 1094 | 3. addition of a columnated simulation output mode |
| 1095 | for raw spin that mimicks the view one could so |
| 1096 | far only obtain with through the intermediacy of |
| 1097 | xspin. to use, say: |
| 1098 | spin -c spec (or spin -t -c spec) |
| 1099 | there is one column per running process. message send |
| 1100 | or receive events that cannot be associated with a process |
| 1101 | for any reason are printed in column zero. |
| 1102 | |
| 1103 | 4. addition of a Postscript output option to spin. |
| 1104 | this can be used to create a postscript file for a message |
| 1105 | flow of a simulation, without needing the intervention of |
| 1106 | xspin (which can be slow). |
| 1107 | spin -M spec |
| 1108 | generates the message flow in file spec.ps |
| 1109 | also supported is: |
| 1110 | spin -t -M spec |
| 1111 | to convert an error trail into postscript form. |
| 1112 | |
| 1113 | 5. addition of the ability in Xspin to automatically |
| 1114 | track variable values -- by prefixing their declaration |
| 1115 | in Promela with the keyword "show", e.g. "show byte cnt;" |
| 1116 | also added: automatic tracking of the state changes in |
| 1117 | the never claim, if present, during guided simulations |
| 1118 | (i.e., when inspecting an error.trail produced by the |
| 1119 | verifier) |
| 1120 | |
| 1121 | 6. addition of an option to convert LTL formula stored in files. |
| 1122 | |
| 1123 | 7. Xspin is now compatible with Windows95 and WindowsNT |
| 1124 | |
| 1125 | smaller, changes |
| 1126 | - spin generates hints when the data-type of a variable is |
| 1127 | over-declared (i.e., it will detect the use of integers for |
| 1128 | storing booleans etc.) |
| 1129 | - the spin -d output for structure variables now includes the |
| 1130 | name of the structure declaration (as the 3rd field, which |
| 1131 | was unused in this case) to make the listings unambiguous. |
| 1132 | [change from Frank Weil] |
| 1133 | - spin -t can now take an argument. without an argument |
| 1134 | spin -t spec opens spec.trail |
| 1135 | spin -t4 opens spec4.trail |
| 1136 | (multiple trails are generated with runtime option |
| 1137 | pan -c0 -e) |
| 1138 | - bugfix: local channels were not always restored correctly to |
| 1139 | their previous state on the reverse move of a process deletion |
| 1140 | in the verification (i.e., the deletion of the process to which |
| 1141 | those channels were local). |
| 1142 | - bugfix: stutter moves were only done in the 2nd dfs, to close |
| 1143 | cycles. this has to be done in both 1st and 2nd, to avoid missing |
| 1144 | the valid stutter extension of some finite behaviors |
| 1145 | - process death is now a conditionally safe action -- this partly |
| 1146 | reverses a decision made in version 2.8.5. |
| 1147 | the condition for safety is: this is the youngest process and |
| 1148 | there are fewer than the max nr of processes running. this means |
| 1149 | that the action cannot enable any blocked run statements, although |
| 1150 | it may enable more process deaths (i.e., of processes that now |
| 1151 | become youngest). |
| 1152 | it does imply that a process dies as quickly as possible. allowing |
| 1153 | them to also linger merely creates articifial execution scenarios |
| 1154 | where the number of active processes can grow without bound. |
| 1155 | compatibility with 2.8.5-2.9.7 on this issue can be forced by |
| 1156 | compiling pan.c with -DGLOB_ALPHA |
| 1157 | - atomics inside atomics or dsteps are now accepted by the parser, |
| 1158 | and ignored. |
| 1159 | - there is now a Syntax-Check option in Xspin |
| 1160 | [suggested by Klaus Havelund] |
| 1161 | - true and false are now predefined constants |
| 1162 | |
| 1163 | Subsequent updates will appear in a new file: V3.Updates |