man: mention ltlsynt in spot(7)
Fixes #292. * bin/man/spot.x, bin/spot.cc: Add missing cross references. * tests/sanity/bin.test: Add safety checks so we do not forget again.
This commit is contained in:
parent
ba897bc3eb
commit
ddaaf2c1c8
3 changed files with 33 additions and 2 deletions
|
|
@ -22,6 +22,7 @@ that are listed below.
|
||||||
.BR ltldo (1)
|
.BR ltldo (1)
|
||||||
.BR ltlfilt (1)
|
.BR ltlfilt (1)
|
||||||
.BR ltlgrind (1)
|
.BR ltlgrind (1)
|
||||||
|
.BR ltlsynt (1)
|
||||||
.BR randaut (1)
|
.BR randaut (1)
|
||||||
.BR randltl (1)
|
.BR randltl (1)
|
||||||
.BR spot-x (7)
|
.BR spot-x (7)
|
||||||
|
|
|
||||||
|
|
@ -37,9 +37,9 @@ static const argp_option options[] =
|
||||||
{ DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but "
|
{ DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but "
|
||||||
"simpler ones. Use this when looking for shorter formula to "
|
"simpler ones. Use this when looking for shorter formula to "
|
||||||
"reproduce a bug.") },
|
"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("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 "
|
{ DOC("ltl2tgba", "Convert LTL or PSL into variants of Transition-based "
|
||||||
"Generalized Büchi Automata.") },
|
"Generalized Büchi Automata.") },
|
||||||
{ DOC("ltl2tgta", "Convert LTL or PSL into variants of Transition-based "
|
{ 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("autfilt", "Filter, convert, and transform ω-automata.") },
|
||||||
{ DOC("dstar2tgba", "Convert ω-automata into variants of "
|
{ DOC("dstar2tgba", "Convert ω-automata into variants of "
|
||||||
"Transition-based Büchi automata.") },
|
"Transition-based Büchi automata.") },
|
||||||
|
{ DOC("ltlsynt",
|
||||||
|
"Synthesize AIGER circuits from LTL/PSL specifications.") },
|
||||||
{ nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 },
|
{ nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 },
|
||||||
{ DOC("autcross", "Cross-compare tools processing ω-automata,"
|
{ DOC("autcross", "Cross-compare tools processing ω-automata,"
|
||||||
" watch for bugs, and generate statistics.") },
|
" watch for bugs, and generate statistics.") },
|
||||||
|
|
|
||||||
|
|
@ -55,6 +55,26 @@ do
|
||||||
fi
|
fi
|
||||||
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
|
# All man pages
|
||||||
case $manpage in
|
case $manpage in
|
||||||
*.1)
|
*.1)
|
||||||
|
|
@ -93,4 +113,12 @@ do
|
||||||
|
|
||||||
done
|
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
|
exit $exit_status
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue