README
1This directory contains the source of some command-line tools that
2expose some of Spot's algorithms to Unix users.
3
4Man pages are generated from the --help output of each tool,
5supplemented by any text in the man/*.x files. Usually the extra text
6contains either some bibliographical references, some formal
7definitions or some examples that are too long for --help. Having a
8few short examples at the end of --help is good.
9
10This directory also builds some non-installed binaries, like spot-x,
11whose purpose is just to generate a man-page with the same format as
12the other man pages (this includes keeping the version number
13up-to-date).
14
15There is also a script called 'options.py' that summerizes how the
16different short options are used among the tools.
17
18Routines that are shared by multiple command-line tools are stored in
19files called common_*.{cc,hh}.
20
21
22Recommendations when adding new tools or features:
23--------------------------------------------------
24
25 - Tools should be designed to work on multiple inputs (e.g., read
26 different outputs from multiple files, and accept many inputs from
27 the same file, including stdin). They should also all be designed
28 to produce several outputs, usually one per input. This way they
29 can be piped one onto the other easily.
30
31 - When naming an option, seek inspiration from the POSIX standard, or
32 from GNU extensions. For instance ltlfilt and autfilt both have a
33 -v option to invert the filter; this is inspired from grep's -v
34 option. The long version of this option (--invert-match) is also
35 the same as in grep.
36
37 - When adding a new option, implement only the --long-option by
38 default. Do not add a short version unless
39 (1) you are sure it will be frequently used interactively
40 (if it is only used in scripts, then a long option is enough)
41 (2) this option can be shared by multiple tools.
42
43 - As much as possible, use the same option names across tools. Use
44 the script options.py in this directory to check what short options
45 are used. It's OK if the same short option correspond to different
46 long names in the various tools, as long as the intent is similar.
47 For instance -n has different long options depending on the tool:
48 autfilt -n N means --max-count=N
49 randltl -n N means --formulas=N
50 randaut -n N means --automata=N
51 but in all cases, the intent is to specify the number of items
52 to output.
53
54 - In the --help output, all options should appear in a named
55 section (like "Input options:", "Output options:"), and those
56 sections are best ordered according to one's mental view
57 of how the tool works: first, it reads the input, then
58 it processes it, then it outputs the result. Keep --help
59 and --version at the very bottom.
60