Spinroot

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Spin Version 6.4.3 now available

A fresh new version of Spin is now on the website -- with changes that support
also the latest version of the C model extractor Modex version 2.6.

==== Version 6.4.3 - 16 December 2014 ====

- added definition of tas() function for powerpc64, courtesy of srirajpaul
- corrected parsing unsigned int variables in c_state declarations
- allow use of a variable name in an array bound, provided that variable
  is an initialized scalar - generats a warning when this is used
- made sure ltl formula are parsed the same way on replay of an error
  trail as when generating a verifier
- improved matching of labels if the same labelname is used in multiple scopes
  (e.g., different inlines)
- fewer issues with WindowsPC compiled versions
- the label "accept_all" in neverclaims is no longer treated as an indication
  of a check that requires cycle detection
- presence of -bfs will now preclude addition of -a flag in auto-generated runs
- fixed limit that was set too short when reproducing an MSC from an error-trail
  with spin option -M
- small improvement in replays of error-trails with ./pan -r
- improved support for Modex generated models
- now handles select statements in preprocessor (spinlex.c) rather than in the
  grammar -- replaces it with a true non-deterministic choice for relatively
  small ranges (1..32 entries), rather than a non-deterministically terminated
  do-loop, for simpler error trails
- fixed some minor type inaccuracies

mlfv

Member

Registered: 2013-04-29

Posts: 28

Re: Spin Version 6.4.3 now available

select statements with non-constant expressions now produce a syntax error

Error: expecting select ( name : constant .. constant ) near 'select'

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Spin Version 6.4.3 now available

True -- this was necessary to allow the select statement to
be converted into a non-deterministic choice.
You can disable this extension by recompiling spin
after removing the preprocessor directive EXPAND_SELECT
in spinlex.c

mlfv

Member

Registered: 2013-04-29

Posts: 28

Re: Spin Version 6.4.3 now available

It would very helpful to use both versions (perhaps the constant version with another name)