4mreduce24m(n)                                                            4mreduce24m(n)

1mNAME0m
       reduce  - Tina reduction tool

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



1mSYNOPSIS0m
       1mreduce 22m[-4mh24melp] [-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]



1mDESCRIPTION0m
       Tool  reduce  includes  an  implementation of the reduction system pre-
       sented 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 support-
       ing 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.



1mOPTIONS0m
       -4mh24melp  Recalls options.



       1mReduction specification and limits:0m


       -rg[,start][,redundant][,compact[+]][,convert][,mg][,4ti2][,transi-
       tions]
              Reduction  preserving  the  reachability  set (through reduction
              equations).  By default (-rg without options), only removes  du-
              plicated  and constant places, and duplicated and identity tran-
              sitions. 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  op-
              tion.


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




       1mTransformation specification and limits:0m


       -tr[,cluster][,4ti2]
              Reduction preserving the reachability set  (through  transforma-
              tion 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 for-
              get it only if |P| > n (-nupn-limit n).




       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.


       -sw    Forget stopwatches in the input net.



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



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



       1mErrors destination:0m


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


       1mOther flags:0m


       -t s   Limit on total duration of reduction.


       -stats Print some statistics information, if available.




1mEXAMPLES0m
       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



1mSEE ALSO0m
       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), for-
       mats(n), stan(n)


1mAUTHORS0m
       Bernard Berthomieu LAAS/CNRS,  2000-2026, Bernard.Berthomieu@laas.fr


Tina Tools                       Version 4.0.0                       4mreduce24m(n)
