Spinroot

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Spin Version 6.3.1 now available

==== Version 6.3.1 - 11 May 2014 ====

- big improvement in the handling of the new -run parameter to Spin
  that will make it much easier to work with Spin.
  all new functionality is now supported by the -run parameter alone,
  so these four experimental options from 6.3.0 are no longer needed:
    -runA,-runAF, -runNP, -runNPF
  in the new setup, a -run parameter can be followed by any additional
  settings and options that should be passed to either the compiler
  (for compiling pan.c) or the ./pan verifier itself as runtime options.
  the rule is that all parameters that preceed a -run argument are
  interpreted by Spin itself for parsing the model; all parameters that
  follow a -run parameter are passed down to compiler or verifier
  for instance, to get the equivalent of -runNPF from 6.3.0, you can
  now say:
    spin -run -DNP -l -f spec.pml
  to get an immediate run searching for weakly fair non-progress cycles
  similarly, to optimize the compilation and reduce the run to a depth
  of 3000 step, you would say:
    spin -run -O2 -DNP -l -f -m3000 spec.pml
  with this new setup you should in principle never have to compile
  the pan.c source files manually, or invoke the verification manually.
  if you want to redefine a macro used in the Spin model itself, you
  can still pass that new definition directly to spin, by placing it
  before the -run parameter, for instance:
    spin -DMAX=24 -run -O2 -DNP -l -f -m3000 spec.pml
  (assuming that macro MAX is used inside spec.pml)

- new exercises and tutorials to match these changes in
    http://spinroot.com/spin/Man/1_Exercises.html
    http://spinroot.com/spin/Man/3_SpinGUI.html
    http://spinroot.com/spin/Man/4_SpinVerification.html

- bug fixes:
  - in simulations, dynamically changing process priorities did not always
    work correctly. now fixed
  - additional corrections to the line number reporting in simulations