Spinroot

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.