4msift24m(n)                                                                4msift24m(n)

1mNAME0m
       sift - high performance state space explorator and checker

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


1mSYNOPSIS0m
       1msift 22m[-4mh24melp] [-p]
            [-R | -P | -V | -Q | -Z(v|i|vi) |
             -D | -F | -F1 |
             -W | -M | -H | -S | -E | -G]
            [-equal | -incl | -hull]
            [-f (form|file) | -dead] [-c n] [-t s] [-b n]
            [-q | -k] [-kts | -lts | -ks | -rsf | -rsd | -rs]
            [-NET | -NDR | -TPN | -PNML | -TTS]
            [-df | -bf | -rf] [-seed] [-tree] [-inh] [-tc] [-pr] [-nupn] [-dt]
       [-stats]
            [infile] [outfile] [digestfile] [errorfile]



1mDESCRIPTION0m
       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.



1mOPTIONS0m
       -4mh24melp  Recalls options.


       1mOperating mode options:0m


       -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.


       -Zv | -Zi | -Zvi
              Builds marking graphs for three "maximal steps" firing rules:
              -Zv, or -sleptsov: a step at marking m is an enabled  transition
              t  fired at its maximum enabledness multiplicity at m; that is a
              bag t*k, where k is the largest integer such that t is firable k
              times simultaneously at m;
              -Zi, or -salwicki: a step at m is a maximal set  of  transitions
              simultenaously firable at m;
              -Zvi, or -slepsalw: a combination of -Zv and -Zi. A step at m is
              a maximal bag of transitions simultenaously firable at m;
              These  options remove time constraints. In addition, options -Zi
              and -Zvi remove priorities.


       -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, ac-
              cording 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  in-
              terval [0,w[, then -W is  silently replaced by -R.  This  option
              removes priorities, it sets flag -pr.


       -M     Option  -M  computes the set of markings of a TPN.  Option -M is
              typically 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 capture markings and  the  firable  transi-
              tions  represented  as loop transitions on the markings they are
              firable from.


       -H     Option -H computes an overapproximation of the set  of  markings
              of a TPN. It is typically much faster than options -M and -W and
              produces a set of classes with exactly one firing domain associ-
              ated  with each marking.  Compared to -W, all classes associated
              with the same marking are merged into  a  single  class  obained
              from  the  dbm-hull of their domains (the smallest dbm including
              all of them). As for mode -M, ktz files created in mode -H  only
              capture markings and the firable transitions.


       -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     Option  -E  computes  the  set of states of a TPN.  Option -E is
              typically faster than -S and yields smaller state space abstrac-
              tions, but it does not preserve firing sequences. ktz files cre-
              ated in mode -E only captured markings and the  firable  transi-
              tions,  represented as loop transitions on the markings they are
              firable from.


       -G     Option -G computes an overapproximation of the set of states  of
              a  TPN.  It  is typically much faster than options -S and -E and
              produces a set of strong classes with exactly one  clock  domain
              associated with each marking.  Compared to -S, all classes asso-
              ciated  with  the  same  marking  are merged into a single class
              obained from the dbm-hull of their domains (the smallest dbm in-
              cluding all of them). As for mode -E, ktz files created in  mode
              -G only capture markings and the firable transitions.


       -equal Identify  two state classes when they are equal (default).  This
              flag has the effects of -W if no priorities are specified, or of
              -S otherwise; It is ignored if the net is untimed or if some op-
              erating mode is simultaneously set.


       -incl  Identify two state classes when one is included  in  the  other.
              This  flag has the effects of -M if no priorities are specified,
              or of -E otherwise; It is ignored if the net is  untimed  or  if
              some operating mode is simultaneously set.


       -hull  Merge  all  state classes with same marking into their dbm hull.
              This flag has the effects of -H if no priorities are  specified,
              or  of  -G  otherwise; It is ignored if the net is untimed or if
              some operating mode is simultaneously set.


       1mExploration strategy flags (when meaningful):0m


       -df    Depth-first exploration order


       -bf    Breadth-first exploration order (default)


       -rf    Random exploration order

              -seed Initializes the random number generator so that  different
              calls  of sift with order -rf on the same arguments may traverse
              the state space in different orders.


       1minput options:0m


       -inh   Removes inhibitor and read 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.


       -nupn  Forget nupn information when reading a pnml description.



       1mStorage strategy flags:0m


       -tree  Do not store states; assume any state computed is new.


       1mStopping conditions:0m


       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.


       -f file
              Equivalent to -f form, for the formula form read in file.


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



       1mOther flags:0m


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


       -stats Prints progress information on the fly.


       1mInput format and source:0m


       -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  in-
              put  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


       1mOutput format:0m


       -q | -4mk24mtz
              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 the .ktz pro-
              prietary compressed format.



       1mKtz output options:0m


       As  of Version  4.0.0, these  options specify  "profiles" for  the  ktz
       output.   A profile  makes precise the information to  be recorded into
       the ktz file.  Six profiles are  defined; the first three are  suitable
       for  model-checking tools  selt and muse, while the last  three are not
       and are only suitable for the scan reachability checking tool.


       -kts   Kripke Transition  System: the ktz records  state properties in-
              cluding divergence) and transition properties. This is  the  de-
              fault profile.


       -lts   Labelled  Transition  System:  Like -kts except state properties
              are omitted;


       -ks    Kripke Structure: Like -kts  except  transition  properties  are
              omitted;


       -rsf   Reachability  Set  +  Firable  transitions: Like -kts except all
              transition targets are replaced by  the  index  of  the  current
              state. This allows one to check reachability properties, absence
              of  deadlocks and quasi-liveness of transitions, but not LTL nor
              modal mu-calculus formulas.


       -rsd   Reachability Set +   Deadlocks:  Like  -rsf   except  transition
              properties  are  omitted. Allows  to check reachability  proper-
              ties and absence of deadlocks.


       -rs    Reachability Set: Like  -rsd  except  transitions  are  omitted.
              Only allows to check state reachability properties by tool scan.


       The  main benefit of profiles is to  decrease the size of the ktz files
       when the  intended properties of  the behavior do not  necessitate  all
       the  information recorded by the  default profile. For instance, if the
       properties of interest  are only about states, then it is   not  neces-
       sary to record in the ktz file information  about transitions, what can
       save a considerable space and speed up the processing on the file.


       Alternatively,   ktz   files  can  be stripped  of  undesired  informa-
       tion (i.e. have  their profile  changed) using the ktzio  tool (see the
       ktzio manual page).


       1mOutput destination:0m


       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  de-
              fined by  the output flag supersedes that determined by the out-
              file extension.

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


       1mDigest destination:0m


       digestfile

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


       1mErrors destination:0m


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



       1mDefault options:0m

              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



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



1mSEE ALSO0m
       nd(n),   tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),  tedd(n),
       selt(n), muse(n), pathto(n), scan(n), play(n), walk(n), reduce(n), for-
       mats(n), stan(n)


1mAUTHORS0m
       Bernard Berthomieu, with contributions by Alexandre Hamez (expatSML li-
       brary),  Didier   Le   Botlan   (polycount),   LAAS/CNRS,    2000-2026,
       Bernard.Berthomieu@laas.fr.


Tina Tools                       Version 4.0.0                         4msift24m(n)
