Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2010-11-18 06:15:15
Spin Version 6.0.0
Within a few weeks the new version 6 will be ready for distribution.
A few users have tested a beta-version of the new release with good results.
There are quite a few changes, and hopefully improvements.
A short summary is as follows.
- Inline LTL properties:
Instead of specifying a never claim, you can now
specify LTL properties directly inside a Promela model.
Any number of named properties can be included.
All properties will be converted into never claims in the background,
and you can choose which property should be checked for any run
using a new pan runtime parameter pan -N name.
Example:
ltl p1 { []<>p }
ltl p2 { <> (a > b) implies len(q) == 0 }
There are a few important points to note on this:
- Inline LTL properties state *positive* properties to prove, i.e.,
you do not need to negate them to find counter-examples.
(When spin generates the corresponding never claims, it will perform
the negation automatically.)
- You can use any valid Promela syntax to specify the predicates that serve as
state properties (e.g., the expression (a>b) or (len(q) == 0) above.
So you do not need to introduce any macros with propositional symbols anymore.
- White space is irrelevant -- you can insert newlines anywhere in the ltl block.
- You can use textual alternatives to the temporal and some propositional operators.
At the moment this includes the words: always, eventually, until, weakuntil,
stronguntil, implies, equivalent, release (the V operator). So the first property
above could also be written:
ltl p1 {
always
eventually p /* maybe some comment here */
}
- Improved scope rules:
So far, there were only two levels of scope for variable
declarations: global or proctype local.
Version 6 adopts more traditional block scoping rules:
for instance, a variable declared inside an inline definition or inside
an atomic or non-atomic block now has scope that is limited to that inline or block.
You can revert to the old scope rules by using spin -O (the capital letter Oh)
- Multiple never claims:
Other than multiple and named inline LTL properties, you can also include
multiple explicit (and named) never claims in a model. The name goes after
the keyword 'never' and before the curly brace.
As with inline LTL properties, the model checker will still only use one never
claim to perform a verification run, but you can choose on the
command line of pan which claim you want to use: pan -N name
- Synchronous xxx of claims:
If multiple never claims are defined, you can use spin to
generate a single claim which encodes the synchronous xxx
of all never claims defined, using the new option: spin -e spec.pml
- Dot support:
A new option for the executable pan supports the generation of
the state tables in the format accepted by the dot tool from
graphviz: pan -D (the older ascii format remains available as pan -d).
- Standardized output:
All filename / linenumber references are now in a new single standard
format, given as filename:linenumber, which allows postprocessing
tools to easily hotlink such references to the source.
This feature is exploited by the new replacement for xspin, called ispin
that will also be distributed soon.
Offline
#2 2010-11-18 09:21:50
- agroce
- Member
- Registered: 2010-11-18
- Posts: 1
Re: Spin Version 6.0.0
Great! Is this going to include the much desired renaming of the internal assert in generated code to something that lets you use assert in embedded C code?
Offline
#3 2010-11-18 16:33:36
Re: Spin Version 6.0.0
[quote=agroce]Great! Is this going to include the much desired renaming of the internal assert in generated code to something that lets you use assert in embedded C code?[/quote]
yes the new version also uses a more sensible naming for the internal evaluation of Promela asserts. In the C code it's now called 'spin_assert' to avoid clashes with assert functions in embedded C code.
Offline
Pages: 1