---

Manual Reference Pages  - reduce (n)

---

NAME

reduce - Tina reduction tool

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

CONTENTS

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.

-help	Recalls 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 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.
-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), scan(n), play(n), walk(n), formats(n)

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