tedd(n)                                                                tedd(n)



NAME
       tedd - symbolic state space explorator and checker

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


SYNOPSIS
       tedd [-help] [-p]
            [-R | -F1]
            [-f form | -dead] [-t s]
            [-q | -k] [-NET | -NDR | -TPN | -PNML | -TTS]
            [-inh] [-tc] [-pr] [-dt] [-stats]
            [infile] [outfile] [digestfile] [errorfile]



DESCRIPTION
       tedd  is a preliminary version of a tool for state space exploration of
       Petri nets and Time Petri nets relying on decision diagram  based  sym-
       bolic methods. Only a few options are currently supported; more will be
       added in the future. tedd also allows to check reachability  properties
       on the fly.



OPTIONS
       -help Recalls options.


       Operating mode options:


       -R     Builds the set of reachable markings of a Petri net (untimed, or
              with  temporal  information  discarded).  The  net  is   assumed
              bounded; time constraints, priorities and data are forgotten.


       -F1

              Builds the set of discrete time reachable states of a Time Petri
              net.  If no temporal information is specified, or if all transi-
              tions bear interval [0,w[, then -F1  is silently replaced by -R.
              The net is assumed bounded; priorities and data are forgotten.



       Exploration strategy flags:


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


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


       -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",
              that 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 (if available).


       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 | -v
              Specifies the verbosity of output.


       outfile
              Where results are written.


       Digest destination:


       digestfile

              In addition to (possibly) its  results  in  file  outfile,  tedd
              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:     tedd -R -q
              Otherwise:                 tedd -F1 -q



EXAMPLES
       tedd -dead < abp.ndr
       tedd -PNML mynet.xml
       tedd -R ifip.ndr



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


AUTHORS
       Bernard   Berthomieu   and   Alexandre  Hamez,  LAAS/CNRS,   2000-2015,
       Bernard.Berthomieu@laas.fr.




Tina Tools                       Version 3.4.0                         tedd(n)
