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