0b55f123 |
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 |