diff --git a/NEWS b/NEWS index 4ba38c360..55f8695eb 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,9 @@ New in spot 2.0.0a (not yet released) * Add missing documentation for the option string passed to spot::make_emptiness_check_instantiator(). + * There is a now a spot(7) man page listing all installed + command-line tools. + Python: * The tgba_determinize() function is now accessible in Python. diff --git a/bin/Makefile.am b/bin/Makefile.am index e0e4254f8..85e5ca059 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -68,10 +68,10 @@ bin_PROGRAMS = \ randaut \ randltl -# Dummy program used just to generate man/spot-x.7 in a way that is -# consistent with the other man pages (e.g., with a version number that -# is automatically updated). -noinst_PROGRAMS = spot-x +# Dummy programs used just to generate man/spot-x.7 and man/spot.7 in +# a way that is consistent with the other man pages (e.g., with a +# version number that is automatically updated). +noinst_PROGRAMS = spot-x spot autfilt_SOURCES = autfilt.cc ltlfilt_SOURCES = ltlfilt.cc @@ -85,6 +85,7 @@ ltlgrind_SOURCES = ltlgrind.cc ltldo_SOURCES = ltldo.cc dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc +spot_SOURCES = spot.cc ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) EXTRA_DIST = options.py diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index 3aa77de5a..b7c9f51bb 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -37,6 +37,7 @@ dist_man1_MANS = \ randaut.1 \ randltl.1 dist_man7_MANS = \ + spot.7 \ spot-x.7 MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS) @@ -75,5 +76,8 @@ randaut.1: $(common_dep) $(srcdir)/randaut.x $(srcdir)/../randaut.cc spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc $(convman7) ../spot-x$(EXEEXT) $(srcdir)/spot-x.x $@ +spot.7: $(common_dep) $(srcdir)/spot.x $(srcdir)/../spot.cc + $(convman7) ../spot$(EXEEXT) $(srcdir)/spot.x $@ + ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc $(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@ diff --git a/bin/man/spot.x b/bin/man/spot.x new file mode 100644 index 000000000..f46305aa5 --- /dev/null +++ b/bin/man/spot.x @@ -0,0 +1,28 @@ +[NAME] +spot \- Command-line tools installed by Spot. + +[SYNOPSIS] + +Spot is a C++ library for ω-automata and LTL formulas manipulation. +It also comes with Python bindings and a set of command-line tools +that are listed below. + +[DESCRIPTION] +.\" Add any additional description here + +[SEE ALSO] +.BR randltl (1) +.BR genltl (1) +.BR ltlfilt (1) +.BR ltlrind (1) +.BR randaut (1) +.BR ltl2tgba (1) +.BR ltl2tgta (1) +.BR autfilt (1) +.BR ltlcross (1) +.BR ltldo (1) +.BR spot-x (7) + +.UR https://spot.lrde.epita.fr/ +The Spot web page. +.UE diff --git a/bin/spot.cc b/bin/spot.cc new file mode 100644 index 000000000..1478f1234 --- /dev/null +++ b/bin/spot.cc @@ -0,0 +1,78 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "common_sys.hh" +#include +#include +#include +#include +#include "common_setup.hh" + +const char argp_program_doc[] ="Command-line tools installed by Spot."; + +#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0 + +static const argp_option options[] = + { + { nullptr, 0, nullptr, 0, "Tools that output LTL/PSL formulas:", 0 }, + { DOC("randltl", "Generate random LTL or PSL formulas.") }, + { DOC("genltl", "Generate LTL formulas from scalable patterns.") }, + { DOC("ltlfilt", "Filter, convert, and transform LTL or PSL formulas.") }, + { 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 }, + { DOC("randaut", "Generate random ω-automata.") }, + { 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 " + "Generalized Testing Automata.") }, + { DOC("autfilt", "Filter, convert, and transform ω-automata.") }, + { DOC("dstar2tgba", "Convert ω-automata into variants of " + "Transition-based Büchi automata.") }, + { nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 }, + { DOC("ltlcross", "Cross-compare translators of LTL or PSL formulas " + "into ω-automata, watch for bugs, and generate statistics.") }, + { DOC("ltldo", "Wrap any tool that inputs LTL or PSL formulas and possibly " + "outputs ω-automata; provides Spot's I/O interface.") }, + { nullptr, 0, nullptr, 0, nullptr, 0 } + }; + +const struct argp_child children[] = + { + { &misc_argp_hidden, 0, nullptr, -1 }, + { nullptr, 0, nullptr, 0 } + }; + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, nullptr, nullptr, argp_program_doc, children, + nullptr, nullptr }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + std::cerr << "This binary serves no purpose other than generating" + << " the spot.7 manpage.\n"; + + return 1; +} diff --git a/doc/org/tools.org b/doc/org/tools.org index cb062df47..acdcaa0e9 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -71,7 +71,8 @@ convenience, you can browse their HTML versions: [[./man/ltlfilt.1.html][=ltlfilt=]](1), [[./man/randaut.1.html][=randaut=]](1), [[./man/randltl.1.html][=randltl=]](1), -[[./man/spot-x.7.html][=spot-x=]](7). +[[./man/spot-x.7.html][=spot-x=]](7), +[[./man/spot.7.html][=spot=]](7). * Advanced use-cases