diff --git a/bin/man/spot.x b/bin/man/spot.x index 8ac229dde..eaa1e933b 100644 --- a/bin/man/spot.x +++ b/bin/man/spot.x @@ -22,6 +22,7 @@ that are listed below. .BR ltldo (1) .BR ltlfilt (1) .BR ltlgrind (1) +.BR ltlsynt (1) .BR randaut (1) .BR randltl (1) .BR spot-x (7) diff --git a/bin/spot.cc b/bin/spot.cc index 0cbe27f16..a1bb0a4e9 100644 --- a/bin/spot.cc +++ b/bin/spot.cc @@ -37,9 +37,9 @@ static const argp_option options[] = { DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but " "simpler ones. Use this when looking for shorter formula to " "reproduce a bug.") }, - { nullptr, 0, nullptr, 0, "Tools that output automata:", 0 }, + { nullptr, 0, nullptr, 0, "Tools that output automata or circuits:", 0 }, { DOC("randaut", "Generate random ω-automata.") }, - { DOC("genaut", "Generate ω from scalable patterns.") }, + { DOC("genaut", "Generate ω-automata from scalable patterns.") }, { DOC("ltl2tgba", "Convert LTL or PSL into variants of Transition-based " "Generalized Büchi Automata.") }, { DOC("ltl2tgta", "Convert LTL or PSL into variants of Transition-based " @@ -47,6 +47,8 @@ static const argp_option options[] = { DOC("autfilt", "Filter, convert, and transform ω-automata.") }, { DOC("dstar2tgba", "Convert ω-automata into variants of " "Transition-based Büchi automata.") }, + { DOC("ltlsynt", + "Synthesize AIGER circuits from LTL/PSL specifications.") }, { nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 }, { DOC("autcross", "Cross-compare tools processing ω-automata," " watch for bugs, and generate statistics.") }, diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test index f51e06b9a..10aba7620 100644 --- a/tests/sanity/bin.test +++ b/tests/sanity/bin.test @@ -55,6 +55,26 @@ do fi fi + case $binary in + spot);; + *) + if ! grep -q "BR $binary " $top_srcdir/bin/man/spot.x; then + echo "bin/$binary is not listed in bin/man/spot.x" + exit_status=2 + fi + ;; + esac + case $binary in + spot);; + spot-x);; + *) + if ! grep -q "\"$binary\"" $top_srcdir/bin/spot.cc; then + echo "bin/$binary is not listed in bin/spot.cc" + exit_status=2 + fi + ;; + esac + # All man pages case $manpage in *.1) @@ -93,4 +113,12 @@ do done +grep '^.BR [a-z0-9-]* ([0-9])' "$top_srcdir"/bin/man/spot.x | + while read br tool num; do + if ! test -f $top_builddir/bin/$tool; then + echo "bin/man/spot.x mentions unexisting tool $tool" + exit_status=2 + fi + done + exit $exit_status