Spinroot

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Spin Version 6.4.4 is now available

==== Version 6.4.4 - 1 November 2015 ====

- when compiletime option -DNP is defined after a -run flag, the runtime
  option -l is now added, if missing.
- removed the dummy definition of yywrap()
- added make32 for 32-bit linux builds (make -f make32)
- improved printing of mtype values in trace replay with pan
- improved support for cond_wait, cond_signal, and mutex_init
  for models extracted by modex (not meant to be called directly)
- improved replay of error traces when -DPERMUTED is used
- improved verbose output for -DPERMUTED options
- added 64-bit murmurhash function as an alternative on 64-bit systems
  it is enabled by compiling pan.c with an additional -DMURMUR directive
- replaced call srandom() with srand() and replaced random() with rand()
- added p_randrot to the set of options supported by -DPERMUTED for
  rotating the process scheduling list by a random amount (see 6.4.0)
- added a runtime option (for pan.c) called -rhash to generated a
  random hash-polynomial for the run (as determined by the seed for the
  random number generator, which can be changed with runtime option -RSnnn)
  if no seed is selected with -RS, then time is used to seed the random
  number generator. Compile pan.c with -DRHASH to enable this option.
  If -DRHASH is defined it will also enable directive -DPERMUTED.
  see VMCAI2016 paper for examples of its use in cloud / swarm verification.
- removed the warning "this search is more efficient if compiled with -DSAFETY"
- improved spin replay of error-traces for models using process priorities
  together with ltl properties or never claims
- added support for using c_expr inside ltl formula
- made select ( name : constant .. constant-expression ) work again,
  e.g. so that you can again say:  select (i : 0 .. N-1)
- other minor fixes and improvements throughout