#

Manual Reference Pages - tedd (n)

### NAME

> tedd - logic symbolic state space constructop and explorator (development in progress)

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

### CONTENTS

> Synopsis
> Description
> Options
> Shell Variables
> Examples
> See Also
> Authors

### SYNOPSIS

> tedd [-help] [-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] [-dead-states] [-dead-transitions]
> [-q | -v] [-NET | -NDR | -TPN | -PNML | -TTS]
> [-inh] [-tc] [-dt] [-pr] [-stats] [-b n] [-t s]
> [infile] [outfile] [digestfile] [errorfile]

### DESCRIPTION

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

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

### OPTIONS

> -help | Recalls options.
> Variable order options:
> -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.
> Build options:
> -count-transitions
> | Compute and print the number of transitions of the state space, if supported by tool. By defaut, neither tool computes the transition count as this can be expensive.
> -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.
> Input options:
> -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.
> 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 specified 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 format of the output, quiet (-q) or verbose (-v). Relevant for -dead-stats and -dead-transitions.
> outfile
> | Where results are written.
> Digest destination:
> digestfile
> | In addition to (possibly) its results in file outfile, tedd may 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.
> Other flags:
> -p | Disables state space generation, just parses input net.
> -po | Disables state space generation, just parses input net and computes 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.
> Default options:
> | tedd -q -pr -dt -order-auto

### SHELL VARIABLES

> 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

### EXAMPLES

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

### SEE ALSO

> 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), formats(n)

### AUTHORS

> Bernard Berthomieu, with contributions by Alexandre Hamez (smldd, expatSML libraries), Didier Le Botlan (polycount), Silvano Dal Zilio, LAAS/CNRS, 2000-2024, Bernard.Berthomieu@laas.fr.

Tina Tools | tedd (n) | Version 3.8.5

Generated by manServer 1.07 from src/tedd.n using man macros.