0b55f123 |
1 | Distribution Update History of the SPIN sources |
2 | =============================================== |
3 | |
4 | ==== Version 4.0.0 - 1 January 2003 ==== |
5 | |
6 | See the end of the V3.Updates file for the main changes |
7 | between the last version 3.5.3 and version 4.0.0. |
8 | A glimpse of the Spin update history since 1989: |
9 | |
10 | Version 0: Jan. 1989 - Jan. 1990 5.6K lines: book version |
11 | Version 1: Jan. 1990 - Jan. 1995 7.9K lines: first version on netlib |
12 | Version 2: Jan. 1995 - Aug. 1997 6.1K lines: partial-order reduction |
13 | Version 3: Aug. 1997 - Jan. 2003 17.9K lines: bdd-like compression (MA) |
14 | Version 4: Jan. 2003 - 28.2K lines: embedded c-code, bfs |
15 | |
16 | ==== Version 4.0.1 - 7 January 2003 ==== |
17 | |
18 | - the rule that one cannot combine a run operator |
19 | in an expression with any other type of boolean |
20 | or arithmetic operator within the same expression |
21 | is now enforced. |
22 | - bfs now produces the usual stats upon finding |
23 | and error; and it now supports the -e option. |
24 | - extended bfs to deal also with safety properties |
25 | specified in never claims and trace assertions. |
26 | unlike the regular dfs search, the bfs search cannot |
27 | handle the use of atomic sequences inside never claims. |
28 | it will issue a warning, and will abort, if it sees this. |
29 | unless constructs, d_steps, etc. should all work also |
30 | within never claims |
31 | a warning is issued if accept labels are found inside |
32 | the never claim (to warn that the bfs search is restricted |
33 | to safety properties only). |
34 | the never claim does always work to restrict the search |
35 | space to the part that is covered by the claim. |
36 | - fixed bug in simulation mode, where atomicity was not |
37 | always correctly preserved across rv actions from one |
38 | atomic chain to another (if the sender action was the |
39 | last statement in an atomic sequence) reported by Judi Romijn. |
40 | - added the BFS option also in the advanced verification |
41 | options panel of xspin401.tcl |
42 | |
43 | ==== Version 4.0.2 - 6 March 2003 ==== |
44 | |
45 | - removed a long-standing bug in the marking of transitions |
46 | for partial order reduction: |
47 | the guard statement of an atomic or d_step sequence within |
48 | which a non-atomic,atomic,or d_step sequence is nested did |
49 | not always get the proper tag |
50 | if the tag assigned was local and it should have been global, |
51 | the p.o. reduction algorithm could make an invalid reduction. |
52 | such a case can indirectly be constructed if an atomic sequence |
53 | contains an call of an inline function as the first statement. |
54 | (this case was found by Bram de Wachter) |
55 | - removed reliance on tmpnam() in main.c -- gcc complains about |
56 | it allowing a race condition on the use of the name returned. |
57 | we now use fixed local names for the temporary files. |
58 | there could be a problem now if two users run spin within the |
59 | same directory simultaneously -- but that problem already |
60 | exists with xspin as well (pan.tmp and pan.pre) and is |
61 | easily avoided. (if needed, we could add a locking mechanism |
62 | at some point, but this seems overkill for the time being.) |
63 | - the -m option now works the same in breadth-first search as it |
64 | does in depth-first search. there's less of a strict reason |
65 | to cutoff the search at the -m depth with bfs, since the |
66 | stack is not pre-allocated in this case; it grows dynamically. |
67 | by setting -m to a very large number, one can therefore just |
68 | let the verifier proceed until it exhausts memory, or finishes |
69 | (that is to recreate the earlier behavior when needed). |
70 | - increased the size of some internal arrays a bit to better |
71 | accomodate the use of very long identifier or structure names. |
72 | - much improved rule for creating and locating error trail files: |
73 | if possible, the trail file is created by appending .trail |
74 | to the filename of the source model |
75 | some older operating systems don't like it if the filename |
76 | for the source model already contains a period, so if a |
77 | failure is detect, a second attempt is now made by stripping |
78 | the existing . extesion (e.g., .pml) and replacing it with |
79 | .trail (some os's also truncate this to .tra, which is also |
80 | accepted). |
81 | |
82 | ==== Version 4.0.3 - 3 April 2003 ==== |
83 | |
84 | - no verbose steps printed for never claim in guided simulations |
85 | unless -v is given as a commandline argument |
86 | state changes in the never claim are still printed, but with |
87 | the already existing separate output ("Never claim moves to...") |
88 | - new spin command-line option -I, to reproduce a version of the |
89 | specification after preprocessing and inlining operations are |
90 | done. the reproduced code is not complete: declarations and |
91 | process parameters are skipped, some internally generated labels |
92 | and jumps (e.g., replacing break statements) also become visible. |
93 | the version is intended only to show what the effect of inlining |
94 | and preprocessing is. |
95 | - change in sched.c to suppres printing of final value of variables |
96 | marked 'show' -- this looks like an assignment, which is confusing. |
97 | - small fixes in xspin, which is now xspin402.tcl |
98 | - in guided simulation mode, when a claim from an ltl property is |
99 | present, the simulator's pid nrs did not always agree with the |
100 | verifiers numbers -- this could lead to the wrong name for a |
101 | process being printed in the simulation trails. |
102 | |
103 | ==== Version 4.0.4 - 12 April 2003 ==== |
104 | |
105 | - there was a bug in 4.0.3 that prevented successful compilation |
106 | of pan.c (and unbalanced endif, caused by a missing newline |
107 | character in pangen1.h on line 3207) |
108 | - there was a maximum of 128 variables that could be changed per |
109 | atomic sequence, this is now 512. |
110 | |
111 | ==== Version 4.0.5 - 29 May 2003 ==== |
112 | |
113 | - correction in the reporting of process id's during guided simulation. |
114 | the numbers could be off by one when never claims are used. |
115 | (just a reporting problem, the run itself was always correct) |
116 | - increased bounds on the length of strings passed as preprocessor |
117 | commands |
118 | - explicit cast of return value ot strlen to int, to keep compilers |
119 | happier |
120 | - fixed subtle bug in the fairness option (reported by Dragan |
121 | Bosnacki). with fairness enabled, standard claim stutter could |
122 | in special cases cause a false acceptance cycle to be reported |
123 | (i.e., a cycle not containing an accepting state). |
124 | for compatibility, the old behavior can still be obtained by |
125 | compiling the pan.c verifiers with -DOLDFAIR. the default is |
126 | the fixed algorithm. |
127 | - restricted the maximum length of a string in the lookup table |
128 | for c_code segments to 1024 characters. this table is only used |
129 | to print out the code segment in error traces -- so the truncation |
130 | is cosmetic, not functional. it avoids compiler complaints about |
131 | excessively long strings though (which could prevent compilation). |
132 | - improved error reporting when a value outside the range of the |
133 | target data type is passed as an parameter in a run statement |
134 | |
135 | ==== Version 4.0.6 - 29 May 2003 ==== |
136 | |
137 | - the fix of the fairness option wasn't quite right. |
138 | directive -DOLDFAIR is gone again, and the real fix |
139 | is now in place. |
140 | |
141 | ==== Version 4.0.7 - 1 August 2003 ==== |
142 | |
143 | .------------------------------------------------------. |
144 | | Version 4.0.7 is the version of Spin that is | |
145 | | described in the Spin book (Addison-Wesley 2003) | |
146 | | and that is used for all examples there | |
147 | | http://spinroot.com/spin/Doc/Book_extras/index.html | |
148 | .------------------------------------------------------. |
149 | |
150 | - added (really restored) code for allowing separate |
151 | compilation of pan.c for model and claim |
152 | two new (previously undisclosed) commandline |
153 | options -S1 and -S2 -- usage documented in the new book |
154 | |
155 | - if it is detected that a c_expr statement definitely has |
156 | side effects, this now triggers a fatal error. |
157 | |
158 | - complains about more than 255 active processes |
159 | being declared in active prefix |
160 | |
161 | - fix in -A option: removed bug in handling of eval() |
162 | |
163 | - cosmetic changes: |
164 | endstate and end-state are now spelled 'end state' as |
165 | preferred by Websters dictionary (...) |
166 | hash-array, hash-table, and never-claim similarly |
167 | are now spelled without hyphens |
168 | |
169 | - improved error replay for models with embedded c code |
170 | |
171 | - the -m option is no longer automatically set in guided |
172 | simulation runs. |
173 | |
174 | - change spin.h to allow it to be included twice without |
175 | ill effects (happens in y.tab.c, generated from spin.y) |
176 | |
177 | - updated the make_gcc file for newer versions if cygwin |
178 | |
179 | ==== Version 4.1.0 - 4 December 2003 ==== |
180 | |
181 | - new spin option -h, when used it will print out the |
182 | seed number that was used for the random number |
183 | generator at the end of a simulation run -- useful |
184 | when you have to reproduce a run precisely, but forgot |
185 | to set an explicit seed value with option -n |
186 | |
187 | - c_track now has an optional extra argument, to be |
188 | documented - the extra qualifier cannot be used with BFS |
189 | (spin.h, spin.y, spinlex.c, pangen4.c, ...) |
190 | |
191 | - the documentation (book p. 41) says that unsigned data |
192 | can use a width specifier up to 32 bits -- it actually |
193 | only worked up to 31 bits. it now works as advertised. |
194 | fix courtesy of Doug McIlroy. (vars.c) |
195 | |
196 | - when trying to compile a model without initialized |
197 | channels, a confusing compiler error would result. |
198 | now avoided (spin.y, pangen1.c) |
199 | |
200 | - there is no longer a default maximum memory arena |
201 | on verifications, that would apply in the absence of |
202 | an explicit -DMEMCNT or -DMEMLIM setting (the default |
203 | was 256 Mb). |
204 | |
205 | - some more fixes to account for 64bit machines, courtesy |
206 | of C. Scott Ananian. |
207 | |
208 | - from Dominik Brettnacher, some instructions on compiling Spin |
209 | on a Mac under OS X, added to the installation README.html |
210 | file. |
211 | |
212 | - so far you could not use a -w parameter larger than |
213 | 31 during bitstate search -- this effectively limited |
214 | the max bitarray to about 512Mb. the max is now -w32 |
215 | which extends this to 1Gb (i.e., 4 10^9 bits). |
216 | (really should be allowed to go higher, but wordsize |
217 | gets in the way for now.) |
218 | |
219 | - suppressed a redundant 'transition failed' message |
220 | that could occur during guided simulations (guided.c) |
221 | |
222 | - fixed a long standing bug that could show up if the last |
223 | element of an atomic sequence was itself a sub-sequence |
224 | (e.g., defined as an inline or as an unless stmnt). |
225 | in those cases, atomicity could be lost before the |
226 | last statement (sequence) completed. (flow.c) |
227 | |
228 | - fixed two long standing bugs in parsing of |
229 | nested unless structures. the bug showed up in |
230 | a double nested unless that is itself embedded in a |
231 | non-atomic block. symptom was that some code became |
232 | unreachable (thanks to Judi Romijn for the example). |
233 | goto statements that survived state machine optimization |
234 | also did not properly get tagged with escape options. |
235 | |
236 | - also fixed a bug in handling excessively long assertion |
237 | strings (larger than 999 characters) during verification |
238 | |
239 | - revised the way that c_track is implemented (the points |
240 | where c_update and c_revert are called) to make it a |
241 | little easier to maintain |
242 | |
243 | - removed some no longer used code from pangen1.h |
244 | |
245 | - fixed bug in treatment of rendezvous statements in BFS mode |
246 | |
247 | - xspin408.tcl update: compiler errors are now printed in the |
248 | log window, as they should have been all along... |
249 | (courtesy Doug McIlroy) |
250 | |
251 | ==== Version 4.1.1 - 2 January 2004 ==== |
252 | |
253 | - extended bitstate hashing on 32-bit machines to work correctly |
254 | with -w arguments up to and including -w34 (courtesy Peter Dillinger) |
255 | - reduced amount of memory allocated to dfs stack in bitstate |
256 | mode to something more reasonable (it's accessed through a |
257 | hash function -- now related to the maxdepth, not the -w |
258 | parameter |
259 | - fixed bug that could cause problem with very long assertions |
260 | (more than 256 characters long) |
261 | |
262 | - in xspin411, verbose mode during verifications is now default |
263 | (it adds line numbers reached in the never claim to the output) |
264 | - small fixes to the search capability in most text windows |
265 | |
266 | ==== Version 4.1.2 - 21 February 2004 ==== |
267 | |
268 | - fixed bug in support for notrace assertions (the pan.c would |
269 | not compile if a notrace assertion was defined) |
270 | - fixed unintended feature interaction between bitstate search |
271 | and the -i or -I runtime flags for finding the shortest |
272 | counter-example |
273 | - some cosmetic changes to ease the life of static analyzers |
274 | - fixed implementation of Jenkins function to optionally |
275 | skip a semi-compression of the statevector -- to increase speed |
276 | (pointed out by Peter Dillinger) |
277 | - fixed bug in resetting memory stack arena that could show up |
278 | in iterative verification runs with pan -R argument |
279 | (also found by Peter Dillinger) |
280 | - new version of xspin 4.1.2, with a better layout of some |
281 | of the panels |
282 | |
283 | ==== Version 4.1.3 - 24 April 2004 ==== |
284 | |
285 | - changed from using "cpp" by default to using "gcc -E -x c" |
286 | given that most users/systems have gcc anyway to compile c programs |
287 | and not all systems have cpp in a fixed place. |
288 | there should be no visible effect of this change. |
289 | |
290 | - a rendezvous send operation inside an atomic sequence was |
291 | incorrectly accepted as a candidate for merging with subsequent |
292 | statements in the atomic sequence. it is the only type of statement |
293 | that can cause loss of atomicity (and a switch to another process) |
294 | when *executable* (rather than when blocking, as is the case for |
295 | all other types of statements, including asynchronous sends). |
296 | this is now fixed, such that if there is at least one rv channel |
297 | in the system, send operations inside atomic sequences cannot |
298 | be merged with any other statement |
299 | (in general, we cannot determine statically if a send operation |
300 | targets an rv channel or an asynchronous channel, so we can only |
301 | safely allow the merging if there are no rv channels at all). |
302 | this can cause a small increase in the number of stored states |
303 | for models with rendezvous cannels |
304 | |
305 | - counter-examples produced for liveness properties (non-progress or |
306 | acceptance cycles) often contained one step too many -- now fixed |
307 | |
308 | - added check for reuse of varnames in multiple message fields |
309 | i.e., q?x,x is not allowed (would cause trouble in the verifier) |
310 | |
311 | - added a warning against using a remote reference to a label |
312 | that is declared inside an atomic or d_step sequence -- such |
313 | labels are always invisible to the never claim (since the |
314 | executing of the sequence containing the label is meant to be |
315 | indivisible), which can cause confusion. |
316 | |
317 | - "StackOnly" can be used as an alternative to "UnMatched" when used |
318 | as the optional 3rd argument a c_track primitive (see Spin2004 paper) |
319 | |
320 | ==== Version 4.2.0 - 27 June 2004 ==== |
321 | |
322 | - main.c now recognizes __OpenBSD__ and treats it the same as __FreeBSD__ |
323 | |
324 | - general cleanup of code (removing some ifdefs etc) |
325 | |
326 | - allow reuse of varnames in multiple message fields (see 4.1.3) if |
327 | var is an array variable (e.g., using different elements) |
328 | |
329 | - deleted support for directive -DCOVEST -- replaced with -DNOCOVEST |
330 | |
331 | - deleted support for directive -DHYBRID_HASH |
332 | |
333 | - deleted support for directive -DOHASH, -DJHASH, -DEXTENDED |
334 | added -DMM for an experimental/debugging mode (non-documented) |
335 | |
336 | - replaced Jenkins' original hashfunction with an extended version |
337 | contributed by Peter Dillinger. |
338 | it uses more of the information to generate multiple pseudo hash values |
339 | (multi-hashing with anywhere from 1,2,... hash-functions) |
340 | |
341 | - added runtime verifier flag -k to support multi-hashing in Bitstate mode. |
342 | pan -k2 reproduces the default behavior, with 2 bits set per state. |
343 | pan -k1 is the same as the old pan -s (which also still works). |
344 | (as also first suggested by Dillinger and Manolios from Georgia Tech.) |
345 | |
346 | - some more useful hints are generated at the end of each bitstate |
347 | run about possible improvements in coverage, based on the results |
348 | obtained in the last run. |
349 | |
350 | - updated xspin420.tcl to match the above changes in verification options. |
351 | |
352 | ==== Version 4.2.1 - 8 October 2004 ==== |
353 | |
354 | - improvement of BFS mode for partial order reduction, thanks to |
355 | Dragan Bosnacki |
356 | - fewer redundant declarations and fewer complaints from static analyzers |
357 | - a d_step could under some circumstances interfere with a rendezvous |
358 | in progress (e.g., when the d_step started with an if statement, or |
359 | when it started with a send or receive rather then a straight guard |
360 | condition (i.e., an expression). this now works as it should. |
361 | - 4.2.0 attempted to make support for coverage estimates the default. |
362 | this, however, means that on some systems the pan.c source has to be |
363 | compiled with an additional -lm flag (for the math library) |
364 | coverage estimates had to be turned off explicitly by compiling with |
365 | -DNOCOVEST |
366 | in 4.2.1 the earlier default is restored, meaning that you have to |
367 | specify -DCOVEST to get the coverage estimates (and presumably you |
368 | will then know to compile also with -lm) |
369 | - fixed bug that caused an internal name conflict on the verification |
370 | of the mobile1 model from the Test distribution |
371 | - fixed a problem that prevented having more than 127 distinct proctypes |
372 | the max is now 255, the same as the max number of running processes. |
373 | - fix to restore bitstate hashing to work on 64-bit machines |
374 | we still only compute a 32-bit hash; the largest usable bitstate |
375 | hash-array remains 2^35 bits (i.e., 2^32 bytes or 4 Gigabytes). |
376 | (the maximum on 32-bit machines remains -w34 or 2 Gigabytes) |
377 | for 64-bit mode, we will extend this soon to take advantage of |
378 | larger memory sizes available on those machines. [see 4.2.5] |
379 | - the default number of hash-functions used in bitstate hashing |
380 | is now 3 (equivalent to a runtime option -k3), which gives slightly |
381 | better coverage in most cases |
382 | |
383 | ==== Version 4.2.2 - 12 December 2004 ==== |
384 | |
385 | - verifiers now can be compiled with -DRANDOMIZE (for dfs mode only) |
386 | to achieve that transitions within each process are explored in |
387 | random, rather than fixed, order. the other in which processes are |
388 | explored remains fixed, with most recently created process explored |
389 | first (if we can think of a good way of supporting random mode |
390 | for this, we may add this later). if there is an 'else' transition |
391 | among the option, no randomization is done (since 'else' currently |
392 | must be explored as the last option in a set, to work correctly). |
393 | this option can be useful to get more meaningful coverage of very |
394 | large states that cannot be explored exhaustively. |
395 | the idea for this option is Doron Peled's. |
396 | - fixed a limitation in the pan.c verifiers that prevented the use |
397 | of channels with more than 256 slots. this should rarely be an |
398 | issue, since very large asynchronous channels are seldomly useful |
399 | in verifications, but it might as well work. |
400 | - fix to avoid a compiler complaint about a missing prototype when |
401 | compiling pan.c with -DBFS |
402 | - renamed error message about us of hidden arrays in parameter list |
403 | to the more accurate description 'array of structures' |
404 | |
405 | ==== Version 4.2.3 - 5 February 2005 ==== |
406 | |
407 | - _pid and _ are no longer considered global for partial order reduction |
408 | - fixed bug that could lead to the error "confusing control structure" |
409 | during guided simulations (replay of error trails) |
410 | - fixed problem where an error trail could be 1 step too long for |
411 | invalid endstate errors |
412 | - added experimental 64-bit hash mode for 64-bit machines, |
413 | compile pan.c in bitstate mode with the additional directive -DHASH64 |
414 | the code is by Bob Jenkins: http://burtleburtle.net/bob/c/lookup8.c |
415 | [placeholder for a later extension for 64 bit machines] |
416 | |
417 | ==== Version 4.2.4 - 14 February 2005 ==== |
418 | |
419 | - added missing newline after #ifdef HASH64 -- introduced in 4.2.3 |
420 | this caused a compiler warning when compiling pan.c in -DBITSTATE mode |
421 | - a terminating run ending in an accept state was not stutter extended |
422 | unless a never claim was defined. this now works also without a |
423 | never claim, provided that a search for acceptance cycles is performed. |
424 | in the absence of a never claim the corresponding error type is |
425 | called a 'accept stutter' sequence (to distinguish it from 'claim stutter') |
426 | (bug report from Alice Miller) |
427 | the extension is disabled if the compiler directive -DNOSTUTTER is used, |
428 | just like for the normal claim stutter extension rule |
429 | - added support for using -DSC on file sizes larger than 2Gb (courtesy Hendrik Tews) |
430 | - in simulation mode, the guard statement of a d_step sequence was not |
431 | subject to escape clauses from a possible unless statement, contrary to the |
432 | language spec. in verification mode this did work correctly; simulation mode fixed. |
433 | (courtesy Theo Ruys and David Guaspari) |
434 | - added warning for use of an 'unless' construct inside a d_step sequence |
435 | |
436 | ==== Version 4.2.5 - 2 April 2005 ==== |
437 | |
438 | - the default bitstate space size is now 1 Mb (was 512K) |
439 | - the default hashtable size in exhaustive mode is now 512K slots (was 256K) |
440 | - fixed memory leak that can bite in very long simulation runs |
441 | (courtesy Hendrik Tews) |
442 | - now turns off dataflow optimization (setting dead variables to 0) |
443 | when remote variable references are used. (this is a little bit of |
444 | overkill, since we'd only need to turn it off for the variables |
445 | that are being monitored from the never claim, but it is simple and safe) |
446 | - you can now compile pan.c with -DHASH64 to invoke a 64bit Jenkins hash, |
447 | (enabled by default on 64bit machines) or disable it by compiling with -DHASH32 |
448 | (which is the default on 32bit machines) |
449 | the 64-bit version of Spin (and of the pan.c files it generates) has now been |
450 | fully tested; this means that we can now use more than 4 Gbyte of memory, both |
451 | in full state and in bitstate mode. |
452 | - added pan runtime options -M and -G (inspired by the work of Peter Dillinger |
453 | and Panagiotis Manolios on 3Spin), with a simple implementation. |
454 | (the code for pangen1.h actually got smaller in this update). |
455 | |
456 | these two new options are available in bitstate mode only and allow the user to |
457 | define a bitstate hash array that is not necessarily equal to a power of two. |
458 | if you use -M or -G, then this overrides any other setting you may have |
459 | used for -w. for example: |
460 | pan -M5 will use a hash array of 5 Megabytes |
461 | pan -G7 will use a hash array of 7 Gigabytes. |
462 | use this instead of -w when the hash array cannot be a power of 2 bytes large. |
463 | pan -M4 is technically the same as pan -w25 in that it will allocate |
464 | a hash array of 4 Megabytes (2^(25-3) bytes), but it can be slower |
465 | because indices into the hash-array are now computed with a modulo operator |
466 | instead of with faster bit masks and bit shifts. similarly, |
467 | pan -G1 is technicall the same as pan -M1024 or pan -w33 |
468 | whether the use of -M and -G is slower than -w depends on your compiler. |
469 | many modern compilers (e.g. gcc and microsoft visual studio) will automatically |
470 | optimize the hash array access anyway when it effectively is a power |
471 | of two large (i.e., independent of whether you use -w25 or -M4). |
472 | in a small set of tests on a 2.5 GHz machine, using both gcc and the MS |
473 | compilers, no meaningful difference in speed when using -M or -G could be |
474 | measured, compared with -w (not even for non powers of two hash array sizes). |
475 | (the difference in runtime was in the order of 3 to 4%). |
476 | |
477 | ==== Version 4.2.6 - 27 October 2005 ==== |
478 | |
479 | - mostly small fixes -- one bug fix for reading error trails on 64bit machines |
480 | (courtesy Ignacy Gawedzki) |
481 | - the full tar file now creates all files into a single common directory named |
482 | Spin, which will simplify keep track of versions and updates |
483 | - small update of xspin as well (now xspin4.2.6) |
484 | the main change in xspin is that on startup it will now look for a file with |
485 | the same name as the filename argument given (which is typically the name of |
486 | the file with the Promela model in it) with extension .xsp |
487 | so when executing "xspin model" the command will look for a file "model.xsp". |
488 | xspin will read this file (if present) for commands to execute upon startup. |
489 | (very useful for demos!) |
490 | commands must start with either "X:" or "L:" |
491 | an L: command must be followed by a number, which is used to set the number of |
492 | lines that should be visible in the command log window |
493 | an X: command can be followed by any shell command, that xspin will now execute |
494 | automatically, with the output appearing in the command log window |
495 | an example .xsp file: |
496 | |
497 | X: spin -a model |
498 | L: 25 |
499 | X: nice gcc -DMEMLIM=1000 -DCOLLAPSE -DSAFETY -DREACH -o pan pan.c |
500 | X: nice time -p ./pan -i -m150 |
501 | X: spin -t -c -q3 model |
502 | X: cp model.trail pan_in.trail |
503 | |
504 | ==== Version 4.2.7 - 23 June 2006 ==== |
505 | |
506 | - change in pc_zpp.c, courtesy of Sasha Ivanov, to fix an incorrect order of |
507 | preprocessing directives -- scanning "if" before "ifdef" and "ifndef" |
508 | |
509 | - all 3 very dubious types of statements in the following model were erroneously |
510 | accepted by Spin version 4.2.6 and predecessors. |
511 | they no longer are -- courtesy of the class of 2006 @ Caltech CS |
512 | active proctype X() { |
513 | chan q = [2] of { int, int }; |
514 | |
515 | _nr_pr++; /* change the number of processes... */ |
516 | _p = 3; /* change the state of process X.... */ |
517 | q!2(run X()); /* something really devious with run */ |
518 | } |
519 | |
520 | - added the compiler directive __NetBSD__ |
521 | |
522 | - the vectorsize is now always stored in an unsigned long, to avoid |
523 | some obscure bugs when the size is chosen too small |
524 | |
525 | - fix in the parsing of LTL formulae with spin -f to make sure that |
526 | unbalanced braces are always detected |
527 | |
528 | - added warning against use of rendezvous in BFS mode -- which cannot |
529 | guarantee that all invalid endstates will be preserved |
530 | |
531 | - minor things: make_pc now defaults to gcc instead of cl (the microsoft |
532 | visual studio compiler) |
533 | |
534 | - xspin4.2.7 disables some bindings that seem to be failing |
535 | consistently now on all platforms, although the reason is unclear |
536 | (this occurs in the automata view and the msc views, which are supposed |
537 | to track states or execution steps to source lines in the main text |
538 | window -- instead these bindings, if enabled, now seem to hang the gui) |
539 | |
540 | ==== Version 4.2.8 - 6 January 2007 ==== |
541 | |
542 | - added optimizations in cycle search described by Schwoon & Esparza 2005, |
543 | in 'a note on on-the-fly verification algorithms' and in |
544 | Gastin, Moro, and Zeitoun 2004, 'Minimization of counter-examples in Spin' |
545 | to allow for early detection of acceptance cycles, if a state is found |
546 | on the stack that is accepting, while still in the 1st dfs. the version |
547 | also mentioned in Schwoon & Esparza -- for the case where the source state |
548 | of such a transition is accepting -- is also included. |
549 | |
550 | - eleminated many of the #ifdef PC directives that distinguished between |
551 | use of y.tab.h and y_tab.h which is no longer needed with the newer |
552 | versions if yacc on cygwin (e.g., bison yacc) |
553 | |
554 | - the use of a non-local x[rs] assertion is now fatal |
555 | |
556 | - fixed small problem where scheduler could lose track of a process during |
557 | simulations |
558 | |
559 | - small rewrites for problems spotted by static analyzers |
560 | |
561 | - restored correct working of separate compilation option (-S[12]) |
562 | |
563 | - fixed initialization problem with local variables (making sure that |
564 | a local can be initialized with a parameter or with the value of a |
565 | previously declared and initialized local |
566 | |
567 | - emalloc now returns NULL when 0 bytes are requested (robert shelton 10/20/06) |
568 | |
569 | - using _stat instead of stat on WIN32 platforms for compatibility with cl.exe |
570 | |
571 | - avoided a problem with non-writable strings, in pan.c |
572 | |
573 | - renamed QPROVISO to Q_PROVISO in preparation for related updates in 4.3.0 |
574 | |
575 | - fixed problem with the final transition of an error trail sometimes |
576 | not appearing in the trail file (alex groce) |
577 | |
578 | ==== Version 4.2.9 - 8 February 2007 ==== |
579 | |
580 | - the optimization for cycle search from 4.2.8 wasn't complete -- it could cause |
581 | annoying messages to show up, and the start of a cycle not being identified |
582 | in all cases (Moti Ben-Ari) -- it now works they way it was intended |
583 | |
584 | - made it possible to compile pan.c with visual studio, provided that -DWIN32 or |
585 | -DWIN64 are included in the compiler directives; see make_pc for an example. |
586 | without this, file creat calls would crash the application -- because the windows |
587 | implementation of this call uses its own set of flags... |
588 | |
589 | - the spin parser now flags all cases where the wrong number of parameters |
590 | is specified in a run statement (as suggested by Klaus Havelund) |
591 | |
592 | - it is now possible to use a c_expr inside an expression, e.g. as in |
593 | x[ c_expr { 4 } ] = 3 or x[ c_expr { f() } ] (Rajeev Joshi) |
594 | |
595 | - a new option for ./pan when embedded C code is used: -S to replay the |
596 | error trace without printing anything other than the user-defined printfs |
597 | from the model itself or from inside c_code fragments - (Rajeev Joshi) |
598 | |
599 | ==== Version 4.3.0 - 22 June 2007 ==== |
600 | |
601 | - bug fix (thank you Claus Traulsen) for goto jumps from one atomic |
602 | sequence into another. if the first was globally safe, but the second |
603 | was not, then an erroneous partial-order reduction was possible |
604 | - small changes based on static analyzer output, to increase robustness |
605 | - smaller pan.c files generated if huge arrays are part of the model |
606 | - more accurate reporting of statecounts in bitstate liveness mode |
607 | - better portability for compilation with visual studio |
608 | - likely to be the last spin version 4 release -- the next should be 5.0 |
609 | which supports safety and liveness verification on multi-core systems |
610 | |
611 | ==== Version 5.0 - 26 October 2007 ==== |
612 | |
613 | - lots of small changes to make the sources friendlier to static analyzers, |
614 | like coverity, klocwork, codesonar, and uno, so that they find fewer things |
615 | to warn about |
616 | - improved check for a match of the number of operands specified to a run |
617 | operator with the number of formal parameters specified for the proctype |
618 | (courtesy an example by Klaus Havelund) |
619 | - memory counts are now printed properly as MB quantities (divided by |
620 | 1024*1024 instead of 1,000,000) |
621 | - more accurate treament of atomic sections that contain goto statements, |
622 | when they jump into a different atomic section (especially when the two |
623 | atomics have different properties under partial order reduction) |
624 | (courtesy and example by Claus Traulsen) |
625 | - improvement treatment of run statements for processes that initialize |
626 | local variables with global expressions. in these cases the run |
627 | statement itself is now recognized as global -- otherwise it can still |
628 | be treated as local under partial order reduction rules |
629 | - improved treatment of variable update printing when xspin is used. |
630 | before, large structures were always full printed on every step, which |
631 | could slow down xspin significantly -- this now happens only if there |
632 | was a change of at least one of the values printed. |
633 | |
634 | Additions: |
635 | - support for use of multi-core systems, for both safety and liveness |
636 | properties. see: http://www.spinroot.com/spin/multicore/ |
637 | - added the time of a run in seconds as part of all outputs, and in many |
638 | cases also the number of new states reached per second |
639 | |
640 | - new compile-time directives for pan.c supported in Version 5.0 include: |
641 | NCORE, SEP_STATE, USE_DISK, MAX_DSK_FILE, FULL_TRAIL, T_ALERT |
642 | and for more specialized use: |
643 | SET_SEG_SIZE, SET_WQ_SIZE, C_INIT, SHORT_T, ONESECOND |
644 | the following three can be left unspecified unless prompted by pan itself |
645 | on a first trial run: |
646 | VMAX, PMAX, QMAX, |
647 | the use of all the above directives is explained in |
648 | http://www.spinroot.com/spin/multicore/V5_Readme.html |
649 | for typical multi-core applications only the use of -DNCORE=N is |
650 | typically needed |
651 | - a small number of other new directives is not related to the use of |
652 | multicore verifications - their use is also explained (at the very |
653 | bottom of) the V5_Readme.html file mentioned above. they are: |
654 | FREQ, NUSCC, BUDGET, THROTTLE, LOOPSTATE, NO_V_PROVISO |