reduce - Tina reduction toolPart of Tina Toolbox for analysis of Petri nets and Time Petri nets.

Synopsis

Description

Options

Examples

See Also

Authors

reduce[-help] [-p]

[-rg[,start][,redundant][,compact[+]]

[,convert][,mg][,4ti2][,transitions]]

[-redundant-limit n] [-redundant-time n]

[-inv-limit n] [-inv-time n]

[-tr[,cluster][,4ti2]]

[-semiflow-limit n] [-semiflow-time n]

[-nupn-limit n] [-no-nupn]

[-v | -q] [-t n]

[-NET | -NDR | -TPN | -PNML | -TTS]

[-inh] [-tc] [-dt] [-pr] [-sw] [-stats]

[infile] [outfile] [errorfile]

Tool reduce includes an implementation of the reduction system presented in papers:

B Berthomieu, D Le Botlan, S Dal Zilio International Symposium on Model Checking Software (SPIN), LNCS 10869, pp 65-84, Springer, 2018.B Berthomieu, D Le Botlan, S Dal Zilio International Journal on Software Tools for Technology Transfer 22(2), pp 163-181, Springer, 2020.

To these reductions, reduce adds the capability of clustering safe place invariants into a single place, thanks to the tina tools supporting generalized read arcs and generalized inhibitor arcs.

The input is a net description in any format supported by the Tina tools (.net, .ndr, .tpn, .pnml or .tts); the output is a net in the tina .net format annotated by reduction equations (as comments). The input net should not have time constraints, priorities nor special arcs (read or inhibitors arcs); the output net may have special arcs.

- helpRecalls options.

Reduction specification and limits:

-rg[,start][,redundant][,compact[+]][,convert][,mg][,4ti2][,transitions] Reduction preserving the reachability set (through reduction equations). By default (-rg without options), only removes duplicated and constant places, and duplicated and identity transitions. The options are:

start: fire start transitions redundant: remove redundant places and redundant transitions (using ILP) compact[+]: agglomerate places (two options) convert: clusters each complementary pair of places into a single place mg: computes equational descriptions of their reachability set for some special cases of nets transitions: keep a copy of each transition (among duplicates) 4ti2: use tool 4ti2 for computing redundant places and transitions rather than native algorithms.The toolset 4ti2 must be installed by the user.

-redundant-limit n Limit on the size of nets (|P| or |T|) for application of the redundant option.

-redundant-time n Timeout on the computation of redundant places and transitions, if requested.

-inv-limit n Limit on the size of nets (|P|) for application of the mg option.

-inv-time n Timeout on the computation of equational description for option mg, if requested.

Transformation specification and limits:

-tr[,cluster][,4ti2] Reduction preserving the reachability set (through transformation relations). Currently, the sole transformation provided is cluster.

cluster: Clusters safe place invariants into a single place, using an encoding relying on special arcs. The safe invariants are deduced either from the nupn information in the pnml file, of any, or from the place semiflows of the net, otherwise. 4ti2: use tool 4ti2 for computing place semiflows rather than native algorithms.The toolset 4ti2 must be installed by the user.

-semiflow-limit n Limit on the size of nets (|P|) for computation of p-semiflows for the cluster option.

-semiflow-time n Timeout on the computation of semiflows for option cluster, if requested.

-nupn-limit n | -no-nupn Forget nupn information in input net, if any (-no-nupn), or forget it only if |P| > n (-nupn-limit n).

Input options:

-inh Forget inhibitor 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.

-sw Forget stopwatches in the input net.

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 Verbosity level, quiet (-q) or verbose (-v).

outfile Where results are written. If absent or specified by "-", results are written on standard output.

Errors destination:

errfile Where error messages are written. If absent or specified by "-", error messages are written on standard error.

Other flags:

-t s Limit on total duration of reduction.

-stats Print some statistics information, if available.

reduce -rg,redundant,compact HouseConstruction-PT-00100.pnml reduce -rg,redundant,compact+ models/Angiogenesis-PT-20.pnml reduce -rg,redundant,compact models/AirplaneLD-PT-0010.pnml reduce -rg,start,redundant,compact+ models/IBM319-PT-none.pnml reduce -rg,redundant,compact,mg,4ti2 models/CircularTrains-PT-024.pnml

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

Bernard Berthomieu LAAS/CNRS, 2000-2012, Bernard.Berthomieu@laas.fr

Tina Tools | reduce (n) | Version 3.7.0 |