Spinroot

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Spin Version 6.2.4 now available

==== Version 6.2.4 - 10 March 2013 ====

- never claims generated from inline ltl formula are now automatically
  added when replaying an error trial (so it will no longer say 'claim
  ignored' in those cases)
- improved treatment of the STDIN channel on linux systems
- changed the format of never claims to improve error-trails
  (by using an assertion in some cases instead of a goto to
   the end of the claim -- this also includes changing 'if' into 'do'
   in some cases, which may affect postprocessors that rely on the
   older format)
- changed parser to allow constant expressions in more places where
  earlier only numeric constants were accepted (e.g., for active [...]
  specifying the size of a channel, and the size of an array)
- small improvements in memory use for parallel bfs mode (BFS_PAR)
- added a BFS_NOTRAIL mode for parallel bfs, reducing memory use if
  no counter-example error trail is expected
- fixed bug in the evaluation of 'enabled(pid)' during verifications
- fixed bug in implementation of weak-fairness algorithm, which could
  in rare causes cause a fair cycle to go unreported.
- improved calculation of hash-factor for very large bitstate spaces
- fix bug introduced in 6.2.3 that gave a compiler error for -DBITSTATE
- other minor code cleanup