.TH tedd n "Version 4.0.0" "Tina Tools"

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

.SH SYNOPSIS
a
.B tedd
[\-\f2h\f1elp] [-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-transitions]
     [-q | -v] [-exact] [-NET | -NDR | -TPN | -PNML | -TTS]
     [-inh] [-tc] [-dt] [-pr] [-nupn] [-stats] [-b n] [-t s]
     [infile] [outfile] [digestfile] [errorfile]


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


.SH OPTIONS

.TP
\-\f2h\f1elp
Recalls options.

.TP
.B Variable order options:

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

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

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

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

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

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


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

.TP
\-order-load file
Loads variable order from file.

.TP
.B Build options:

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

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

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

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


.TP
.B Input options:

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

.TP
\-pr
Forget priority constraints in the input net.

.TP
\-tc
Forget time constraints in the input net.

.TP
\-dt
Forget data processing when reading a tts description.

.TP
\-nupn
Forget nupn information when reading a pnml description.


.TP
.B Input format and source:

.TP
\-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
.ndr format.

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

.nf
file extension		input format
--------------------------------------------------------------
\&.net				net format
\&.ndr				ndr format
\&.tpn				tpn format
\&.pnml			pnml format
\&.tts			     tts format
.fi

.TP
.B Output format and destination:

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

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

.TP
outfile
Where results are written.

.TP
.B Digest destination:

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


.TP
.B Errors destination:

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


.TP
.B Other flags:

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

.TP
\-po
Disables state space generation, just parses input net and computes variable order.

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

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

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


.TP
.B Default options:

tedd -q -pr -dt -order-auto



.SH SHELL VARIABLES

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

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

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

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




.SH EXAMPLES

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


.SH 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), stan(n)

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

