doc: add a spot(7) man page
Suggested by Akim Demaille. Fixes #171. * bin/man/spot.x, bin/spot.cc: New files. * bin/man/Makefile.am, bin/Makefile.am: Add them. * doc/org/tools.org, NEWS: Mention the new page.
This commit is contained in:
Alexandre Duret-Lutz
parent
d6e491a761
commit
9149724617
6 changed files with 123 additions and 8 deletions
3
NEWS
3
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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 $@
|
||||
|
|
|
|||
28
bin/man/spot.x
Normal file
28
bin/man/spot.x
Normal file
|
|
@ -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
|
||||
78
bin/spot.cc
Normal file
78
bin/spot.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include <string>
|
||||
#include <iostream>
|
||||
#include <cstdlib>
|
||||
#include <argp.h>
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue