96ff2225e3
* bin/README, bin/common_conv.hh, bin/common_trans.cc,
bin/ltlsynt.cc, bin/spot-x.cc, spot/gen/automata.hh,
spot/graph/graph.hh, spot/ltsmin/ltsmin.hh,
spot/ltsmin/spins_interface.hh, spot/ltsmin/spins_kripke.hh,
spot/mc/bloemen.hh, spot/mc/bloemen_ec.hh, spot/mc/cndfs.hh,
spot/mc/deadlock.hh, spot/mc/intersect.hh, spot/mc/lpar13.hh,
spot/mc/mc_instanciator.hh, spot/misc/bareword.cc,
spot/misc/fixpool.hh, spot/misc/formater.hh, spot/misc/minato.hh,
spot/misc/satsolver.hh, spot/misc/timer.hh,
spot/parseaut/public.hh, spot/priv/partitioned_relabel.cc,
spot/priv/satcommon.hh, spot/ta/ta.hh, spot/ta/taexplicit.cc,
spot/ta/taproduct.hh, spot/ta/tgta.hh, spot/taalgos/reachiter.hh,
spot/taalgos/tgba2ta.hh, spot/tl/apcollect.cc,
spot/tl/apcollect.hh, spot/tl/formula.cc, spot/tl/parse.hh,
spot/tl/randomltl.hh, spot/tl/relabel.hh, spot/tl/simplify.cc,
spot/twa/acc.hh, spot/twa/bddprint.hh, spot/twa/formula2bdd.cc,
spot/twa/twa.hh, spot/twa/twagraph.cc, spot/twa/twagraph.hh,
spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh,
spot/twaalgos/alternation.hh, spot/twaalgos/cleanacc.cc,
spot/twaalgos/cobuchi.cc, spot/twaalgos/contains.cc,
spot/twaalgos/couvreurnew.cc, spot/twaalgos/cycles.hh,
spot/twaalgos/degen.cc, spot/twaalgos/degen.hh,
spot/twaalgos/dot.hh, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/dtwasat.hh,
spot/twaalgos/dualize.cc, spot/twaalgos/emptiness.hh,
spot/twaalgos/emptiness_stats.hh, spot/twaalgos/game.cc,
spot/twaalgos/genem.hh, spot/twaalgos/hoa.hh,
spot/twaalgos/langmap.hh, spot/twaalgos/ltl2tgba_fm.hh,
spot/twaalgos/magic.cc, spot/twaalgos/magic.hh,
spot/twaalgos/mask.hh, spot/twaalgos/mealy_machine.cc,
spot/twaalgos/mealy_machine.hh,
spot/twaalgos/minimize.hh, spot/twaalgos/parity.cc,
spot/twaalgos/parity.hh, spot/twaalgos/postproc.cc,
spot/twaalgos/product.hh, spot/twaalgos/reachiter.hh,
spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/remfin.hh, spot/twaalgos/sccfilter.cc,
spot/twaalgos/sccinfo.hh, spot/twaalgos/se05.cc,
spot/twaalgos/se05.hh, spot/twaalgos/simulation.hh,
spot/twaalgos/split.hh, spot/twaalgos/stats.hh,
spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh,
spot/twaalgos/tau03.hh, spot/twaalgos/tau03opt.hh,
spot/twaalgos/toparity.hh, spot/twaalgos/totgba.hh,
spot/twaalgos/translate.hh, spot/twaalgos/word.cc,
spot/twaalgos/word.hh, spot/twaalgos/zlktree.cc,
spot/twaalgos/zlktree.hh, spot/twacube/cube.hh,
spot/twacube/twacube.hh, tests/core/cube.cc,
tests/core/ltlsynt.test, tests/core/parity.cc,
tests/core/safra.cc, tests/core/twagraph.cc: here
59 lines
2.7 KiB
Text
59 lines
2.7 KiB
Text
This directory contains the source of some command-line tools that
|
|
expose some of Spot's algorithms to Unix users.
|
|
|
|
Man pages are generated from the --help output of each tool,
|
|
supplemented by any text in the man/*.x files. Usually the extra text
|
|
contains either some bibliographical references, some formal
|
|
definitions or some examples that are too long for --help. Having a
|
|
few short examples at the end of --help is good.
|
|
|
|
This directory also builds some non-installed binaries, like spot-x,
|
|
whose purpose is just to generate a man-page with the same format as
|
|
the other man pages (this includes keeping the version number
|
|
up-to-date).
|
|
|
|
There is also a script called 'options.py' that summarizes how the
|
|
different short options are used among the tools.
|
|
|
|
Routines that are shared by multiple command-line tools are stored in
|
|
files called common_*.{cc,hh}.
|
|
|
|
|
|
Recommendations when adding new tools or features:
|
|
--------------------------------------------------
|
|
|
|
- Tools should be designed to work on multiple inputs (e.g., read
|
|
different outputs from multiple files, and accept many inputs from
|
|
the same file, including stdin). They should also all be designed
|
|
to produce several outputs, usually one per input. This way they
|
|
can be piped one onto the other easily.
|
|
|
|
- When naming an option, seek inspiration from the POSIX standard, or
|
|
from GNU extensions. For instance ltlfilt and autfilt both have a
|
|
-v option to invert the filter; this is inspired from grep's -v
|
|
option. The long version of this option (--invert-match) is also
|
|
the same as in grep.
|
|
|
|
- When adding a new option, implement only the --long-option by
|
|
default. Do not add a short version unless
|
|
(1) you are sure it will be frequently used interactively
|
|
(if it is only used in scripts, then a long option is enough)
|
|
(2) this option can be shared by multiple tools.
|
|
|
|
- As much as possible, use the same option names across tools. Use
|
|
the script options.py in this directory to check what short options
|
|
are used. It's OK if the same short option correspond to different
|
|
long names in the various tools, as long as the intent is similar.
|
|
For instance -n has different long options depending on the tool:
|
|
autfilt -n N means --max-count=N
|
|
randltl -n N means --formulas=N
|
|
randaut -n N means --automata=N
|
|
but in all cases, the intent is to specify the number of items
|
|
to output.
|
|
|
|
- In the --help output, all options should appear in a named
|
|
section (like "Input options:", "Output options:"), and those
|
|
sections are best ordered according to one's mental view
|
|
of how the tool works: first, it reads the input, then
|
|
it processes it, then it outputs the result. Keep --help
|
|
and --version at the very bottom.
|