Spinroot

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Spin Version 6.3.0 now available

==== Version 6.3.0 - 4 May 2014 ====

- A new minor version number because the Promela syntax rules changed.
  A semi-colon at the end of the line is now optional.
  this is implemented by having the lexical analyzer insert the
  semi-colons automatically if they are missing.
  Almost all models will still parse correctly, but the change can in
  a few cases cause older models to trigger a syntax error if a
  statement seperator is assumed in an unsuspected place, e.g., in the
  middle of a multi-line expression. Avoid it by making sure a
  multi-line boolean expression is always enclosed in round braces,
  or by having the last token on a line be an operator.
  For instance, these expressions will parse correctly:
    if
    :: (a
       && b) -> ...
    :: a &&
        b -> ...
    fi
  but these do not:
    if
    :: (a)        // parser cannot see that the expression is incomplete
       && (b) -> ...
    :: a        // same here
       && b -> ...
    fi
  To revert to the old syntax rules, use spin option -o7

- added 5 new options:
    -run    compile and run, verify safety properties
    -runA   compile and run, find acceptance cycles
    -runAF  compile and run, find weakly-fair acceptance cycles
    -runNP  compile and run, find non-progress cycles
    -runNPF compile and run, find weakly-fair non-progress cycles
  for instance:
    spin -runA leader.pml

- spin option -M changed:
  replaced ps_msc.c with msc_tcl.c and with it changed the spin -M
  option from generating scenarios in Postscript to generating them
  as TclTk output. the new version of iSpin makes use of this as well.
  By default the maximum length of the scenario generated is 1024
  (equivalent to an option -u1024). To change it to a different
  value, use the -u option (e.g., spin -u2048 -M leader.pml).

- when using randomized searches (T_RAND, P_RAND, or RANDOMIZE, or pan_rand())
  the seed for the random number generator now also depends on the choice of -h
  (i.e., the seed will change if you change the hashfunction used with ./pan -h)

- added more support for verification of models extracted by Modex from
  C code with pthread library calls embedded.

- simplified the directory structure of the distribution somewhat by
  combining all examples Spin models in a single directory Examples,
  with subdirectories for specific subsets: LTL, Exercises, Book_1991
  (the old subdirectories Samples, Test, and iSpin/ltl_examples are now gone)

- bug fixes:
  - another bug fix in treatment of priorities in verification runs
    the priority tag in active proctype declarations was erroneously ignored
  - fixed the accuracy of reporting the cycle-point in liveness errors
    discovered in a breadth-first search with the piggyback algorithm
    (courtesy Ioannis Filippidis, 4/2014)
  - restored original settings for the piggyback algorithm, which restored
    much of the cycle finding capabilities that were lost after version 6.2.2
  - improved parser so that it can continue after the first syntax error
  - improved accuracy of line numbers in traces (courtesy Akira Tanaka, 3/2014)
  - prevented some compilation errors for unusual combinations of directives
  - removed some warnings for printf statements with the wrong qualifiers
    (e.g., %d for a long int, which should be %ld, etc.)

mlfv

Member

Registered: 2013-04-29

Posts: 28

Re: Spin Version 6.3.0 now available

Another case that now produces a syntax error is the unless e.g.
if  ...  fi
  unless ...

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Spin Version 6.3.0 now available

true -- the unless will have to be written following the "fi":
    if
    :: ...
    ...
    fi unless
        ....