====== PComp command line options ======

<code>
Usage:
    pcomp [options] [@]file...

 The files in the command line are interpreted as STG files, except
 when prefixed with `@', in which case the file should contain a
 list of STG files, one per line (useful for avoiding the shell
 restriction on the length of the command line when composing many
 STGs). All the STGs, both in the command line and in the `@'-prefixed
 files, are used for composition.

 * The output signals of the STGs must be disjoint (this constraint
   can be waived with the -o option), and their union comprises
   the output signals of the composition. On the other hand, the input
   signals can be shared by several STGs, and also an output signal of
   some STG can be an input signal of zero or more other STGs.
 * The internal and dummy signals, as well as places, are renamed
   whenever necessary to avoid name clashes.
 * The composed STG is simplified by removing duplicate places.
 * 2-phase, 4-phase and mixed-phase STGs can be liberally composed.

Options:
  -d  Convert the common interface signals into dummy signals
      (useful for composing handshake components).
  -f[file]
      Stores the composed STG in file rather than standard output.
      The extension (.g, .pnml, or .pnml.gz) determines the format.
      If file is not specified, pcomp.g is used.
  -h  Print this help message and exit.
  -i  Convert the common interface signals into internal signals
      (useful for composing handshake components).
  -l[file]
      If the file name is not provided then `pcomp.xml.gz' is used.
      If the file name ends with `.xml' or `xml.gz' then the
      correspondence between the places and transitions of the
      component STGs and those of the composed STG is stored.
      Otherwise place names of the composed STG are stored, so that
      the i-th line corresponds to the places of i-th component STG
      Note that the same place can occur in several lines - this
      happens when some duplicate place is removed, and some
      equivalent place is listed instead.
  -o  Allow the STGs to share outputs.
  -p  Before doing the parallel composition, remove places whose
      presets do not contain dummy transitions and whose postsets
      contain only shared input signals on which the labelling is
      injective. This transformation results in a composed STG with
      fewer places, which has bisimilar behaviour provided the
      composition is free from computational interference. This
      option is incompatible with -o.
  -r  Rename all dummy transitions, so that their names do not
      contain '+', '-', or '/'. (Needed for compatibility with tools
      that do not allow dummy transitions to have signs, e.g. Petrify.)
  -u  Keep unused signal transition phases. This option considers
      e.g. x+ and x- as independent transition labels. By default,
      if two STGs are composed, and one of them has x+ but no x-,
      while the other has x- but no x+, the composed STG will have
      no transitions labelled by either x+ or x-. However, if this
      option is specified, both labels will occur in the composed STG.
</code>