Table of Contents

Command line options of backend tools

This is a summary of command line options for some of Workcraft backend tools.

Petrify command line options

usage: ./petrify [flags] [infile]

General options:
----------------
  -v           print version only
  -d[n]        debug level (n=1,2)
  -o outfile   STG output file (default: stdout)
  -no          output file not generated
  -log logfile log filename (default: petrify.log)
  -err errfile error filename (default: stderr)
  -nolog       no log file generated
  -ip          show implicit (1-fanin 1-fanout) places
  -dead        do not check for the existence of deadlock states
  -sis         print SIS output style (~ for toggle transitions)

Options for Petri net synthesis:
--------------------------------
  -all         search for all minimal regions (even for irredundant nets)
  -sat         generate a minimal satured Petri net
  -min         generate a Petri net with minimal regions only (no place merging)
  -opt         find the best result (may override other options)
  -noec        generate a Petri net without label splitting (possibly without excitation closure)
  -hide list   hide the signals in the list
  -bisim       maintain bisimilarity after removing events
  -mints       minimize the transition system before synthesis

Options for Petri net properties:
---------------------------------
  -p           generate a pure Petri net
  -fc          generate a Free-Choice net
  -efc         generate an Extended Free-Choice net
  -uc          generate a Unique-Choice net (with no extended free choices)
  -euc         generate a Unique-Choice net (with extended free choices)
  -er          generate a different label for each excitation region
  -sm          generate an SM-decomposable net

Options for STG transformations:
--------------------------------
  -tog         all +/- transitions are converted to toggle
  -untog       all toggle and hatch transitions are converted to +/-
  -2ph         expand channel events to 2-phase protocol (default)
  -4ph         expand channel events to 4-phase protocol
  -redc        concurrency reduction for logic optimization
  -redz        concurrency reduction for RTZ events only
  -redn1       conservative concurrency reduction for noise isolation
  -redn2       concurrency reduction for noise isolation
  -noise       noise analysis

Options for synthesis of asynchronous circuits:
-----------------------------------------------
  -csc[n]      solve CSC (with blocks of at most n intersecting regions)
  -icsc[n]     same as -csc with iterative removal of internal signals
  -ncsc[n]     maximum number of inserted state signals
  -tcsc        solve CSC aiming at improving performance (default for timing optimization)
  -acsc        solve CSC aiming at improving area (default if no timing optimization)
  -io          preserve I/O interface (ignore slow input events)
  -cg          generate complex gates
  -gc          generate generalized C elements
  -gcm         generate generalized C elements with monotonic covers
  -nosi        generate complex gates even for a non-SI specification
  -mc          generate monotonic covers
  -tm[n]       technology mapping (n is the depth of search)
  -tm_ratio[x] area/delay ratio for technology mapping
  -stm         sequential technology mapping (only latches are mapped)
  -nmap[n]     maximum number of inserted signals for technology mapping
  -eqn file    generate logic description in EQN format
  -blif file   generate logic description in BLIF format
  -vl file     generate logic description in Verilog format
  -rst0        generate reset pin active at 0 (only for Verilog netlists)
  -rst1        generate reset pin active at 1 (only for Verilog netlists)
  -lib file    read gate library
  -selckt      interactive selection of gates for each non-input signal
  -latch str   define allowed latches for sequential decomposition
  -nolatch     no latches used for technology mapping
  -lit[n]      logic decomposition with gates with at most n literals
  -cgd[n]      max number of complex gates for each gate decomposition
  -algd[n]     max number of algebraic divisors for each gate decomposition
  -mcd[n]      max number of monotonic covers for each signal decomposition
  -boold[n]    max number of boolean decompositions for each gate
  -ed          exhaustive decomposition
  -topt        logic optimization using timing constraints
  -atopt       logic optimization using automatic timing constraints
  -avg         timing optimization for average case (default: worst-case)

Advanced options:
-----------------
  -s[n]        search depth for label splitting (def. -s3, infinite with -s)
  -rc[n]       max number of non-essential regions for optimal irredundancy
  -cl[n]       max size of compatibility graph for one-hot->log encoding
  -nice_csc    CSC: attempts to find nice signal insertions
  -seq         CSC: do not increase concurrency of new state signals
  -fr[n]       CSC: frontier width for exploration of insertion blocks
  -cw[x]       CSC: tune eagerness to solve conflicts
  -redfr[n]    frontier width for exploration of concurrency reduction
  -trflat[n]   BDD node limit to flatten partitioned transition relations
  -boolmin[n]  define type of boolean minimization
  -notog       No toggle changes in transition relations
  -noreord     No dynamic variable reordering
  -reord[n]    Reordering frequency

MPSat command line options

Usage:
        mpsat [-h]
or
        mpsat <mode> [<options>] [<in_file>] [<out_file>]

The <mode> is one of the following:
  Unfolding/unravelling modes:
    -U[m|p] - Build a complete merged process (-Um) or unfolding prefix (-Up).
  Reachability-based formal verification modes:
    -D - Deadlock checking.
    -F[a|e|s]=<property_file> - Check a reachability-like property.
  Temporal property formal verification mode:
    -B=<property_file> - Check a stutter-invariant temporal property.
  Encoding conflicts detection and resolution modes:
    -C[c|n|u] - Check the CSC/normalcy/USC property.
    -R - Resolve CSC conflicts.
  Synthesis modes:
    -I[e|g|s] - Derive a complex-gate/gC/standard-C implementation.
    -T[=<gate_library>] - Logic decomposition and technology mapping.

The <options> are as follows:
  -# - Allow non-local configurations as cut-off correspondents.
  -! - Disable branching on auxiliary variables.
  -$N - Switch to SAT solver N (0-1).
  -@N - Use adequate order N (0-4).
  -a[N] - Compute all solutions (might be slow).
  -b - Generate backward conflict constraints.
  -c - Do not store cut-off events.
  -d - Allow dummy cut-off events when unfolding an STG.
  -e - Print out configurations rather than traces.
  -f[s|l|<COEFF>=<EXPR>] - Minimise (and perhaps specify) the cost function.
  -g[!][N] - Filter gates/latches used for logic decomposition.
  -i[+|-] - Specify whether to generate inclusion constraints.
  -jN - The number of working threads.
  -l - Replicate places with multiple self-loops.
  -mN - Use method N (1-9).
  -nN - Switch to memory efficient unfolding algorithm after N events.
  -pN - Controls the use of parallel (concurrent) inserions.
  -q - Quit early, after checking the property syntax.
  -r - Allows to use concurrency reduction for encoding conflict resolution.
  -t - Perform logic decomposition down to the gate/latch level.
  -vN - The verbosity level (0<=N<=9, the default is 0).
  -w[N] - Wait for user before exiting (prevents the window from closing).

Detailed help

PComp command line options

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.

Punf command line options

Usage:
     punf [-h]
or
     punf [<options>] <net_file>

       The input net file must be in either FORMAT_N or FORMAT_N2
       format (produced by the PEP tool). Alternatively, it must
       have the suffix `.g' and be in the STG format; then an STG
       unfolding prefix (which may differ from the underlying
       Petri net's unfolding prefix) is produced.
       As an experimental feature, high-level nets are supported.
       For now, only strictly safe nets are allowed, and there are
       some further restrictions, described in the manual.

Options (may be given in any order):

-h     Help.

-#     Using non-local configuration as cut-off correspondents.
         The current implementation is VERY INEFFICIENT.
         This option is not currently supported in the LTL mode.
-$N    Switch to SAT solver N (0-1).
         If N=0 then zChaff is used.
         If N=1 then MiniSAT is used (default).
-@[N]  Using adequate order N (0-4).
         Specifies the adequate order on configurations of the unfolding.
         If N is not specified or -@ is not used then the default
         value N=3 (for prefixes) or N=4 (for merged processes) is used.
         If N=0 then the set inclusion is used.
         If N=1 then the McMillan's order is used.
         If N=2 then the size-lexicographical order is used.
         If N=3 then the total Esparza/Roemer/Vogler (ERV) order is used.
         If N=4 then the total order with an efficient SAT encoding is used.
       Only the ERV order is currently supported in the LTL mode.
-B=filename
       Switches on the LTL-X verification mode. The file must be in
       the HOA format (http://adl.github.io/hoaf/) and specify a Buechi
       automaton for an LTL-X property. The adequate order must be -@3.
-c     Do not store cut-off events (except the successful terminals in
       the LTL mode).
-d     When unfolding an STG, allow dummy cut-off events.
       If this option is not specified, a dummy event e can only be
       declared cut-off if its corresponding configuration C is a
       subset of [e], and [e]\C contains only dummies.
       This option has effect only when unfolding an STG.
       It is automatically specified if the STG contains only dummy signals.
       (Currently ignored if -M is specified.)
-jN    Specifies the number of working threads. By default, it is equal
       to the number of processors. (Currently ignored if -M is specified.)
-l     Replicate places with multiple self-loops, so that each transition
       reading a particular place gets its own copy of that place. This
       transformation can significantly reduce the prefix size for nets
       with many self-loops.
-M     Generate a complete merged process.
-m[=filename]
       Specifies the name of the resulting file, whose extension also
       specifies the format. It can be either the legacy *.mci format
       for prefixes, the legacy *.mp format for merged processes (if -M
       is specified), or the new PNML-based *.pnml or *.pnml.gz format.
       If this option is not specified then the filename for the result
       is obtained by removing from the input filename the suffix `.ll_net',
       `.g' or `.hl_net' (if present), and appending the suffix `.pnml.gz',
       and the resulting prefix or merged process is stored in the new
       PNML-based format. If the filename is not specified (i.e. just -m
       is given) then no output file is created.
-nN    Abandon the concurrency relation and switch to a slower algorithm
       after the specified number of non-cut-off events is generated. The
       default value of N is 50000. If N is 0, the
       concurrency relation is not created. (Ignored if -M is specified.)
-vN    Verbosity level (0-9). The default is 0.
-w[N]  Wait for user input before exiting (prevents the window from closing).
       The possible values of N:
         0 - do not wait for user input, exit immediately;
         1 - wait for user input only if there are errors;
         2 - wait for user input only if there are errors or warnings;
         3 - always wait for user input.
       The default is -w0, and -w is equivalent to -w3.