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