sift(n)                                                                sift(n)



NAME
       sift - high performance state space explorator and checker

       Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.


SYNOPSIS
       sift [-help] [-p]
            [-R | -P | -V | -Q |
             -D | -F | -F1 |
             -M | -E | -W | -S]
            [-incl | -equal]
            [-f form | -dead] [-c n] [-t s] [-b n]
            [-q | -k] [-NET | -NDR | -TPN | -PNML | -TTS]
            [-df | -bf ] [-inh] [-tc] [-pr] [-dt] [-stats]
            [infile] [outfile] [digestfile] [errorfile]



DESCRIPTION
       sift  builds  various state space abstractions for  extended Time Petri
       nets.  It  takes as input  descriptions in textual form  (.net,  .pnml,
       .tpn  formats) or graphical form  (.ndr format of files produced by nd,
       .pnml with graphics), or a  Time Transition System description in  .tts
       format.

       sift  serves  similar purposes as  the tina tool, with less options but
       handles large  states spaces much more efficiently.   sift also  allows
       to check reachability properties on the fly.



OPTIONS
       -help Recalls options.


       Operating mode options:


       -R     Builds  the  marking reachability graph of a Petri net (untimed,
              or with temporal information discarded).   This  option  forgets
              time constraints, it sets flag -tc.


       -V

              Builds   the  Covering  Step  Graph of  a  Petri net,  according
              to  the technique  of  Vernadat/Azema/Michel.  The  construction
              preserves  deadlocks.   This option forgets time constraints and
              priorities, it sets flags -tc -pr.


       -P     Builds  the partial marking  graph of  a Petri   net,  according
              to  the  persistent sets technique. The heuristic retained is to
              minimize local branching.  This option forgets time  constraints
              and priorities, it sets flags -tc and -pr.


       -Q     Builds   the   partial  marking  graph  of  a  Petri  net.  Com-
              bine  the persistent  sets  (-P)  and    covering   steps   (-V)
              methods.   This  option forgets time constraints and priorities,
              it sets flags -tc and -pr.


       -D     Builds the essential state graph of a Time Petri net,  according
              to  the  technique  of Popova. This graph preserves reachability
              and linear time temporal properties. Static intervals   must  be
              closed or unbounded and left-closed.   If no  temporal  informa-
              tion is  specified,  or if  all transitions bear interval [0,w[,
              then -D is silently replaced by -R.


       -F | -F1
              Builds   the  subgraph  of the  state graph  obtained by  firing
              integer delay transitions (unit  delays  if  -F1)  and  discrete
              transitions.   This  graph strictly includes that obtained by -D
              and  preserves  the  same properties. Static intervals  must  be
              closed   or  unbounded  and  left- closed. If no temporal infor-
              mation is specified, or if all transitions bear interval  [0,w[,
              then -F/-F1 is silently replaced by -R.


       -W     Builds  the  linear  state  class  graph   of  a Time Petri net,
              according to the technique  of  Berthomieu/Menasche  [IFIP1983].
              The  linear  state class graph  preserves  marking  reachability
              properties  and  linear  time temporal properties.   If no  tem-
              poral  information  is   specified,  or  if all transitions bear
              interval [0,w[, then -W  is   silently  replaced  by  -R.   This
              option removes priorities, it sets flag -pr.


       -M     As  -W  except  only markings are preserved.  Option -M is typi-
              cally faster than -W and yields  smaller  state  space  abstrac-
              tions, but it does not preserve firing sequences. ktz files cre-
              ated in mode -M only captured markings and the  firable  transi-
              tions,  represented as loop transitions on the markings they are
              firable from.


       -S     Builds the  strong state  class graph, according  to the   tech-
              nique  of  Berthomieu/Vernadat    [TACAS2003].     That    graph
              preserves   state  reachability   properties  and   linear  time
              temporal  properties;  it is also  compatible  with  priorities.
              If no  temporal  information  is specified,  or if  all  transi-
              tions   bear   interval [0,w[,  then -S  is silently replaced by
              -R.


       -E     As -S except only states are preserved.  Option -E is  typically
              faster  than -S and yields smaller state space abstractions, but
              it does not preserve firing sequences. ktz files created in mode
              -E  only  captured  markings and the firable transitions, repre-
              sented as loop transitions on  the  markings  they  are  firable
              from.


       -incl  Identify  two  state  classes when one is included in the other.
              This flag avoids to specify mode -M or -E when  analyzing  timed
              models.  It is silently ignored if the net is untimed or if some
              operating mode is  simultaneously  set,  otherwise  it  has  the
              effects  of  -M  if no priorities are specified, or of -E other-
              wise.


       -equal Identify two state classes when they are equal (default).   This
              flag undoes the effects of any preceding -incl flag.


       Exploration strategy flags:


       -df    Depth-first exploration (when meaningful)


       -bf    Breadth-first exploration (default)


       -inh   Removes inhibitor arcs from the input net.


       -pr    Removes priority constraints from the input net.


       -tc    Removes time constraints  from the input net.


       -dt    Forgets data processing when reading a tts description.


       Stopping conditions:

              If some of these conditions fail and the output is ktz, then the
              ktz file captures a partial state space including the  offending
              state  and  in which all non fully explored states bear property
              "sub".


       -c n   Stop if the number of state enumerated exceeds n; no effects  if
              n=0.


       -t n   Stop  if  exploration lasts longer than n seconds; no effects if
              n=0.


       -b n   Stops if the marking of some place exceeds n; no effects if n=0.
              Sift may take advantage of this value for choosing the represen-
              tation of states.


       -f form
              Stop if some state does not obey property form;  no  effects  if
              form=T.   Formula  form is any modality-free formula accepted by
              the selt model checker (check man selt for  details).  In  addi-
              tion,  an  atomic  proposition  is provided, "safe" or "L.safe",
              then asserts that the marking of each place does not exceed 1.


       -dead  Stop  if  some  deadlock  state  is  found;  shorthand  for   -f
              "-L.dead".



       Other flags:


       -p     Disables state space generation, just parses input net.


       -stats Prints progress information on the fly.


       Input format and source:


       -NET | -NDR | -PNML | -TPN | -TTS
              Specifies  the  format  of the input net. This flag is necessary
              when the input net is read on standard input,  or  read  from  a
              file  that does not bear the expected extension. By default, the
              net is assumed in .net or


       infile Where the  net is  read. The  input  format  is   determined  by
              the file type, according to the table below. If absent or speci-
              fied by "-", the net is  read on standard  input in the   format
              specified  by   the  input  flag.  If  both an  infile and  some
              input flag  are present,  then the format defined  by the  input
              flag supersedes  that determined  by the infile extension.

              file extension      input format
              --------------------------------------------------------------
              .net           net format
              .ndr           ndr format
              .tpn           tpn format
              .pnml               pnml format
              .tts           tts format


       Output format and destination:


       -q | -ktz
              Specifies  the format of the output. This flag is necessary when
              output is produced on standard output, or written in a file that
              does  not  bear  the  expected  extension. -q means no output is
              printed, while -k means some output is produced in .ktz  propri-
              etary compressed format.


       outfile
              Where  results  are  written. The output format is determined by
              the file type, according  to the  table  below.  If   absent  or
              specified   by  "-", then results are written on standard output
              in the format specified by the output format flag.  If  both  an
              outfile  and  some  output  flag  are  present,  then the format
              defined by  the output flag supersedes that  determined  by  the
              outfile extension.

              file extension      output format
              --------------------------------------------------------------
              .ktz           tina binary ktz format
              any other      textual output


       Digest destination:


       digestfile

              In  addition  to (possibly) its results in ktz form in file out-
              file, sift prints  a  summary  of  results  in  file  digestfile
              (default stdout).


       Errors destination:


       errorfile
              Where error messages are written. By default, errors are printed
              on standard error.



       Default options:

              Depend upon the features of the input net:
              If no time constraint:     sift -R -c 0 -t 0 -b 0 -f T -q
              Else, if no priorities:    sift -W -c 0 -t 0 -b 0 -f T -q
              Otherwise:                 sift -S -c 0 -t 0 -b 0 -f T -q



EXAMPLES
       sift -f "p1  t4" < ifip.ndr
       sift -PNML mynet.xml
       sift -f safe abp.ndr abp.ktz -stats



SEE ALSO
       nd(n),  tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),   tedd(n),
       selt(n), muse(n), pathto(n), play(n), formats(n)


AUTHORS
       Bernard Berthomieu LAAS/CNRS,  2000-2012, Bernard.Berthomieu@laas.fr.




Tina Tools                       Version 3.0.0                         sift(n)
