4mtedd24m(n)                                                                4mtedd24m(n)

1mNAME0m
       tedd  - logic symbolic state space constructop and explorator (develop-
       ment in progress)

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


1mSYNOPSIS0m
       a 1mtedd 22m[-4mh24melp] [-p]
            [-order-auto |
             -order-(dfs|scan|bfs|rcm|wrcm|struct|lexical|sliced|
                     random|tpn)[,force][,rev][,flat][,4ti2]]
            [-sdd-variables n]
            [-order-force-limits p t] [-order-struct-limits p t]
            [-order-save file] [-order-load file]
            [-count-transitions] [-count-tokens] [-dead-states] [-dead-transi-
       tions]
            [-q | -v] [-exact] [-NET | -NDR | -TPN | -PNML | -TTS]
            [-inh] [-tc] [-dt] [-pr] [-nupn] [-stats] [-b n] [-t s]
            [infile] [outfile] [digestfile] [errorfile]



1mDESCRIPTION0m
       tedd computes the state space of a Petri net or of a discrete time Time
       Petri using logic-based symbolic techniques  (decision  diagrams).   It
       takes  as  input  Petri  net descriptions in textual form (.net, .pnml,
       .tpn formats) or graphical form  (.ndr format of files produced by  nd,
       .pnml with graphics).  Priorities, time constraints and Time Transition
       System  descriptions  in  .tts format are not supported yet.  tedd also
       allows to compute dead states and dead transitions in  the  spaces  ex-
       plored.

       Note:  this  preliminary  version  is a simplified variant of that used
       with success at the Model Checking Contest, with fewer options (no  net
       reductions nor transformations, in particular).



1mOPTIONS0m
       -4mh24melp  Recalls options.


       1mVariable order options:0m


       -order-auto
              Let tedd decide order of variables using its builtin metric.


       -order-<spec>[,force][,rev][,flat][,4ti2]]
              Use specified order, where

              spec is either:
                dfs: order variables as places are found in a dfs preorder traversal of net
                scan: same but in dfs postorder traversal
                bfs: same but in bfs traversal
                rcm: use Reverse Cuthill/McKee ordering
                wrcm: a variation of rcm taking arc weights into account
                struct: order making use of p-semiflows
                lexical: order variables according to place names, lexicographically
                sliced: a variant of lexical
                random: order variables randomly
                tpn: another variant of lexical order, recommended for tpn descriptions.
              force: apply force heuristic to order computed
              rev | reverse: reverse order computed
              flat: flatten order (put all variables in a single hierarchical level)
              4ti2: use 4ti2 instead of native algorithms to compute struct order.


       -sdd-variables n
              Sets to n the max number of varibles at each hierarchical level.


       -order-force-limit p t
              Skips force option when computing -order-auto and |P| > p or |T|
              > t


       -order-struct-limit p t
              Skips struct order when computing -order-auto and |P| > p or |T|
              > t



       -order-save file
              Saves order computed into a file.


       -order-load file
              Loads variable order from file.


       1mBuild options:0m


       -count-tokens
              Compute  and  print  the max number of tokens in a place and the
              max number of tokens in any marking.


       -count-transitions
              Compute and print the number of transitions of the state space.


       -dead-states
              Once the state space is built, compute the dead  states  (states
              without successors) and prints them if option -v passed.


       -dead-transitions
              Once  the  state  space  is  built, compute the dead transitions
              (those never fired) and prints them if option -v passed.



       1mInput options:0m


       -inh   Forget inhibitor and read arcs in the input net.


       -pr    Forget priority constraints in the input net.


       -tc    Forget time constraints in the input net.


       -dt    Forget data processing when reading a tts description.


       -nupn  Forget nupn information when reading a pnml description.



       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 and destination:0m


       -q | -v
              Specifies  the format of the output, quiet (-q) or verbose (-v).
              Relevant for -dead-stats and -dead-transitions.


       -exact Prints exact counts for the number of markings  or  states,  and
              the  number  of  transitions (if requested), instead of approxi-
              mated counts in scientific notation.


       outfile
              Where results are written.


       1mDigest destination:0m


       digestfile
              In addition to (possibly) its results in file outfile, tedd  may
              prints a summary of results in file digestfile (default stdout).



       1mErrors destination:0m


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



       1mOther flags:0m


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


       -po    Disables  state space generation, just parses input net and com-
              putes variable order.


       -stats Prints progress information on the fly, if available.


       -b n   Indicates that the marking of each place cannot exceed  n.  Tedd
              does not check it but may take advantage of this information for
              optimizing the state space representation.


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



       1mDefault options:0m

              tedd -q -pr -dt -order-auto




1mSHELL VARIABLES0m
       Several tables used by tedd are  statically  allocated,  including  the
       following, with the default sizes shown:

       table               default size (items)
       --------------------------------------------------------------
       HOMUTSIZE           10000
       HOMCACHESIZE        1000000
       HOMCACHETHRESHOLD   1000000
       REWCACHESIZE        100000
       REWCACHETHRESHOLD   1000000
       SDDUTSIZE           2000000
       SDDCACHESIZE        1000000
       SDDCACHETHRESHOLD   1000000

       These  initial  sizes  may be changed by defining shell variables named
       like the tables to be dimensioned, with the desired sizes assigned to.

       For better performances on nets with large state spaces,  it  might  be
       wise  to  augment the default sizes of the HOMCACHE, SDDUT and SDDCACHE
       tables. Three examples size sets follow; the code assigning these sizes
       tp the shell veriables should br added to your startup  file  or  to  a
       file  sourced before calling tedd (exact syntax depends on the shell im
       use).:

       table          medium size    large size     very large size
       --------------------------------------------------------------
       HOMCACHESIZE   10000000       20000000       30000000
       SDDUTSIZE      10000000       20000000       30000000
       SDDCACHESIZE   5000000        10000000       15000000





1mEXAMPLES0m
       tedd -tc ifip.ndr
       tedd tpn_examples/milner_scheduler/m100.tpn
       tedd tpn_examples/dining_philosophers/p1000.tpn -dead-states



1mSEE ALSO0m
       nd(n),  tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),   selt(n),
       sift(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 (smldd, ex-
       patSML libraries), Didier Le Botlan  (polycount),  Silvano  Dal  Zilio,
       LAAS/CNRS,  2000-2026, Bernard.Berthomieu@laas.fr.


Tina Tools                       Version 4.0.0                         4mtedd24m(n)
