69daf9c261
This also fixes some empty lines and unsorted options that appeared in some tools. * tests/sanity/bin.test: Ensure this is done. * bin/README: Add a new paragraph about this. * bin/autcross.cc, bin/ltlcross.cc: Move the output options in their own section. * bin/common_color.cc: Assume color options are in group -15. * bin/common_finput.cc, bin/common_finput.hh: Add a headless variant. * bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Do not force the children groups, so that the options are correctly sorted. * bin/ltlsynt.cc: Add missing groups.
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 summerizes 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.
|