Spinroot

A forum for Spin users

You are not logged in.

#1 2014-09-21 21:48:30

spinroot
forum
Registered: 2010-11-18
Posts: 667
Website

Spin Version 6.4.0 now available

==== Version 6.4.0 - 19 September 2014 ====

A summary of the main new features in this version of Spin
(a full list of updates is always available in http://spinroot.com/spin/Doc/V6.Updates):

  - new ./pan runtime option flag -hash to randomly generate a hash polynomial,
    for instance to separate multiple runs with bitstate hashing better.
    the seed for the random number generator determines what polynomial
    is going to be generated (same seed means same polynomial). the seed
    can be changed with ./pan option -RSn where n is any positive integer
    e.g., obtained from a Unix/Linux system call 'rand.'
    for instance ./pan -RS`rand` -hash   # using backquotes around rand

  - extended the number of features that is supported in combination with
    the  new spin runtime options that were introduced in 6.3.0
    four main types of spin (not pan) options are now supported:

        spin [..options1..] -run      [..options2..] modelname.pml
        spin [..options1..] -replay   [..options2..] modelname.pml
        spin [..options1..] -biterate [..options2..] modelname.pml
        spin [..options1..] -swarmN,M [..options2..] modelname.pml

    other parse-time (options1) or runtime (options2) options can be
    passed along as shown above, and as explained below:

    o parse-time options are placed *before* the mode flag (-run, -replay, etc.)

    o compile-time and run-time options are placed *after* the mode flag.
        this can include compiler directives to be used to compile pan.c
        (which happens in the background), or to execute the resulting ./pan
        executable (which now also happens automatically).

    note 1: when you use this command:
           spin -DX=2 -m -run -DSAFETY -m100 modelname
        compiler directive -DX=2 is used in the preprocessing of the model, and
        compiler directive -DSAFETY is used to compile the resulting pan.c.
        and further, the first -m argument is interpreted by spin, and the
        second -m100 argument is interpreted by ./pan

    note 2: the new options make use of gcc, which is assumed to be
        installed on your system, so on Windows systems this is unlikely
        to work unless you also have cygwin with gcc installed.  you can
        change the compiler to be used by compiling the spin sources with
        a different choice for -DCPP (e.g., "-DCPP=clang -E -x c" might work)
        when using the new options on a Windows system with gcc may also
        doom you to 32-bit pan executables, which will limit the size of
        memory you can allocate for a search to 2GB. using linux is recommended.

    explanation of the use of the spin -replay option:
        this option can be used to replay an existing error trail-file
        (e.g., found with an earlier spin -run)
        if the model contains embedded c-code, the ./pan executable is used
        for the replay; otherwise spin itself is used for the replay.
        note that ./pan recognizes different runtime options than spin itself
        so it can matter which of these two cases applies for [..options2..]
        you can of course always still fall back on the old
           spin -t -p modelname.pml
        method for models withnout embedded C code, or the ./pan -r method for
        models with embedded C code.

    explanation of the use of the spin -run option:
        a synonym of this option is -search -- it behaves identical to -run.
        this option is used to generate a verifier (pan.c), compile it, and
        execute it run, all without further user intervention.
        new options that can be used in the [..options2..] part include:
          -bfs          to perform a breadth-first search
          -bfspar       to perform a parallel breadth-first search
          -bcs          to use the bounded-context-switching algorithm
          -bitstate     or -bit, to use bitstate storage
          -link file.c  to link the pan.c to file.c in the compilation
          -collapse     to use collapse state compression
          -hc           to use hashcompact storage
          -noclaim      to ignore all ltl and never claims
          -p_permute    to use process scheduling order permutation
          -p_rotateN    to use process scheduling order rotation by N (default 0)
          -p_reverse    to use process scheduling order reversal
          -ltl p        to verify the ltl property named p
          -safety       to compile for safety properties only (default is liveness+safety)
          -i            to use the dfs iterative shortening algorithm
          -a            to search for acceptance cycles (and compile correspondingly)
          -l            to search for non-progress cycles (and compile correspondingly)

    explanation of the use of the new spin -biterate option:
          uses bitstate compilation plus iterative search refinement for the
          execution of ./pan with hashtable size increasing step by step
          from -w18 upto -w35 -- until an error is found.
          this performs 18 runs sequentially, with the first runs executing
          very fast -- thus making it likely that errors are found very quickly
          each new run increases precision and runtime, until the max is reached

    explanation of the use of the new spin -swarmN,M option:
          the most advanced new search mode -- only for use on larger multi-core
          systems (e.g., 16 cores and up).
          this option performs N runs in parallel and increments -w every M runs
          for each run performed several other parameters are also randomized
          (e.g., the hash function used, process scheduling decisions, transition
           ordering, etc. similar to what the swarm preprocessor would do)

          the default value for N is 10, and the default for M is 1

          the swarm option makes use of a new compiler directive for pan.c files
          called -DPERMUTED that allows for more extensive options for process
          scheduling randomization (p_rotate, p_reverse, and p_permute, see below)

          spin -swarmN,M will use the following compilation directives and
          runtime parameters (most of this is meant to be internal to Spin,
          but listed here for completeness as background information).
          (the new options below are probably not too useful when used separately)
   
          swarm compilation adds:
             -DBITSTATE -DPUTPID and -DPERMUTED (a new directive, see below)
             -DSAFETY   unless there is also -a or -l parameter in [..options2..]
             -DNOFAIR   unless there is a -f parameter or there is no -a or -l

          runtime flags used (with randomized arguments):
             -w18       unless there already is a -w argument, then use that as starting point
             -i_reverse envoked on some of the runs, to change initialization orders of processes
             -t_reverse envoked on some of the runs, to reverse transition orders
                        unless -DT_RAND or -DT_REVERSE are defined
             -h0        unless there already is a -hN argument, then use that as starting point
                        or if the user specified -hash, then do not use -h
             -k1        unless there already is a -k argument, then use that as starting point
             -p_rotate0 unless there already is a different -p_rotateN argument,
                        unless there is a -p_permute argument, then do not use
             -RSn       using internal choice for n, overrides a user-defined argument
             -a         unless there is already a -a or -l argument
                        or there is a -DNOCLAIM directive
                        or there are no accept-state labels in the model or ltl formula
     
          the swarm option varies these parameters across all parallel runs:
             -w         every Nth iteration (from -swarmN,M):  18..35
             -h         every run 0..499  (unless the user defined -hash)
             -p_rotate  every run 0..255 (unless suppressed by p_normal or p_reverse)
             -k         every run 1..3
             -T         every run 0..1
             -P         every run 0..3
             -RSn       every run
             -p_reverse is enabled on every 5th run, but overriden by -P0/1
                        in half the cases (overrides p_rotate if selected)
             -p_normal  to revert to normal process scheduling at least once ever 6 runs

    the new -DPERMUTED directive enables a set of new runtime options to pan
    that support how the process scheduling selecting can be modified during the search:

        -p_permute  -- to randomly permute the processes (the default)
        -p_rotate   -- to rotate the process ready queue 1 slot
        -p_rotateN  -- to rotate the process ready queue N slots
                       (using -p_rotate0 will have no effect of course)
        -p_reverse  -- to reverse order for all processes
        -p_normal   -- perform process scheduling as if -DPERMUTED was not defined

    if more than one of these options is used, the last one wins.
    if -DPERMUTED is defined and none of these flags are used
    the default process scheduling order is -p_permute
    note that using -DPERMUTED adds overhead and slows down a search, which is only
    reasonable when used in combination with the swarm randomizations

- two additional pan runtime options were added that can affect process
  scheduling and transition selection orders:
        -i_reverse -- reverse the initialization order of all processes declared 'active'
        -t_reverse -- reverse the order of transition selections

- other smaller additions:
  - extended the number of builtin hash-polynomials (selected via -hN) from 32 to 100
  - can now place ltl formula anywhere in a Promela file -- it does not need
    to appear after all symbols that are referenced in the formula have been
    declared (the parser will now always defer processing until the entire
    specification has been parsed)
  - added a quick sanity check to parsing of ltl formula, to catch some common mistakes.

- some fixes:
  - removed some false warnings about duplicate label declarations
  - added -std=gnu99 to calls to the gcc compiler an preprocessor
    to make sure that // comments in Promela specifications are recognized
  - removed pc_zpp.c -- the builtin preprocessor used when compiled with -DPC
    the original reason for adding this was to avoid a command window
    from flashing on the screen when an external preprocessor was
    called from within xspin. that problem no longer seems to exist, and
    so this restricted version of the preprocessor is no longer needed
  - small improvements in typechecking in receive statements
  - improved the look of message sequence charts generated with spin -M
  - fewer compiler warnings when using models with priorities
  - deprecated flag ./pan -s now removed (sam as ./pan -k1)
  - fixed bug in implementation of bounded context switching code (-DBCS)
    that could cause states to be restored incorrectly
  - removed the mapping of type long to long long on windows pcs (-DPC)
  - improved parsing for very large models, saving about 20% of cpu-time,
    by switching from unsorted to sorted linked lists in a few places
  - a few more bug fixes in the implementation of support for dynamically
    changing priorities
  - fixed a bug in replay of error trails for ltl formula, for models where
    multiple formula are used, to make sure that the formula are parsed
    in the same way for verification and for replay.

- new or renamed compilation directives
  - -DREVERSE (gone) to reverse process selection order is renamed to
    -DP_REVERSE to make it more symmetric with the older
    -DT_REVERSE used to reverse the transition selection order
  - the new directive -DPERMUTED overrides -DP_REVERSE if both are used

Offline

#2 2014-10-06 03:56:25

spinroot
forum
Registered: 2010-11-18
Posts: 667
Website

Re: Spin Version 6.4.0 now available

Update for Version 6.4.1 - 5 October 2014

- two small fixes to 6.4.0
  - the new -run -biterate options wasn't working correctly

  - on windows32 and windows64 versions, suppressed logos from gcc
    and improved method for detecting whether gcc.exe is a symbolic
    link or not

Offline

#3 2014-10-08 16:49:47

spinroot
forum
Registered: 2010-11-18
Posts: 667
Website

Re: Spin Version 6.4.0 now available

==== Version 6.4.2 - 8 October 2014 ====

- restored the correct behavior for a standalone -run argument
  (i.e., without -swarm or -biterate), which should perform a single
  compilation and execution of the ./pan verifier
- less chatter on stdout for executed background commands
  (you can restore this by adding -v or -w -- if you use -w the
  commands generated for -biterate or -swarm are shown, but not
  executed)

Offline

Board footer

Powered by FluxBB