Commit c96513b6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

help2man: generate man pages for genltl and ltlfilt

* tools/help2man, tools/x-to-1.in: New files, copied from gnulib
1af55d85d9762a679b4302d5995f05ccd883e956.
* configure.ac: Create x-to-1 and export CROSS_COMPILING.
* Makefile.am: Distribute help2man.
* src/bin/Makefile.am (SUBDIRS): New.
* src/bin/man/Makefile.am: New file.
* src/bin/man/genltl.x, src/bin/man/ltlfilt.x: New files.
* src/bin/genltl.cc: Document the RANGE in the options,
and move the bibliography to genltl.x.
* README: Document src/bin/man
parent e0873cc7
......@@ -43,8 +43,8 @@ UTF8 = utf8/doc/ReleaseNotes utf8/doc/utf8cpp.html utf8/utf8.h \
utf8/utf8/checked.h utf8/utf8/core.h utf8/utf8/unchecked.h
ACLOCAL_AMFLAGS = -I m4
EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog $(UTF8) \
m4/gnulib-cache.m4
EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog tools/help2man \
$(UTF8) m4/gnulib-cache.m4
dist-hook: gen-ChangeLog
......
......@@ -144,6 +144,7 @@ src/ Sources for libspot.
sabatest/ Tests for saba/, sabaalgos/.
neverparse/ Parser for SPIN never claims.
bin/ User tools built using the Spot library.
man/ Man pages for the above tools.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
tl/ Documentation of the Temporal Logic operators.
......
......@@ -104,6 +104,8 @@ AC_CHECK_PROG([WRING2LBTT], [wring2lbtt], [wring2lbtt])
# an alias for swig-1.3. Let's use the former when available.
AC_CHECK_PROGS([SWIG], [swig2.0 swig], [swig])
AC_SUBST([CROSS_COMPILING], [$cross_compiling])
AC_CONFIG_FILES([
Makefile
bench/Makefile
......@@ -131,6 +133,7 @@ AC_CONFIG_FILES([
iface/Makefile
lib/Makefile
src/bin/Makefile
src/bin/man/Makefile
src/eltlparse/Makefile
src/eltltest/defs
src/eltltest/Makefile
......@@ -169,6 +172,7 @@ AC_CONFIG_FILES([
wrap/python/Makefile
wrap/python/ajax/Makefile
wrap/python/tests/Makefile
tools/x-to-1
])
AC_CONFIG_FILES([bench/ltl2tgba/ltl2baw.pl:bench/ltl2tgba/ltl2baw.in],
[chmod +x bench/ltl2tgba/ltl2baw.pl])
......
......@@ -19,13 +19,16 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) \
SUBDIRS = . man
AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \
-I$(top_builddir)/lib -I$(top_srcdir)/lib
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a
bin_PROGRAMS = ltlfilt genltl
ltlfilt_SOURCES = ltlfilt.cc common_output.cc
genltl_SOURCES = genltl.cc common_output.cc
noinst_HEADERS = common_output.hh
ltlfilt_SOURCES = ltlfilt.cc common_output.cc
genltl_SOURCES = genltl.cc common_output.cc
......@@ -107,19 +107,7 @@ to the extent permitted by law.";
const char* argp_program_bug_address = "<" SPOT_PACKAGE_BUGREPORT ">";
const char argp_program_doc[] ="\
Generate temporal logic formulas from predefined scalable patterns.\v\
RANGE may have one of the following forms: INT, INT..INT, or ..INT\n\
In the latter case, the missing number is assumed to be 1.\n\
\n\
Pattern names prefixed with 'ccj', 'gh', 'go', or 'rv' refer to:\n\
[gh] J. Geldenhuys and H. Hansen (Spin'06): Larger automata and less \
work for LTL model checking. LNCS 3925.\n\
[ccj] J. Cichoń, A. Czubak, and A. Jasiński (DepCoS'09): Minimal Büchi \
Automata for Certain Classes of LTL Formulas.\n\
[go] P. Gastin and D. Oddoux (CAV'01): Fast LTL to Büchi Automata \
Translation. LNCS 2102\n\
[rv] K. Rozier and M. Vardi (Spin'07): LTL Satisfiability Checking. \
LNCS 4595.\n";
Generate temporal logic formulas from predefined scalable patterns.";
#define OPT_AND_F 2
#define OPT_AND_FG 3
......@@ -190,7 +178,11 @@ static const argp_option options[] =
{ "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 },
OPT_ALIAS(gh-u2),
OPT_ALIAS(go-phi),
/**************************************************/
{ 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', "
"'INT..INT', or '..INT'.\nIn the latter case, the missing number "
"is assumed to be 1.", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
......
## -*- coding: utf-8 -*-
## Copyright (C) 2012 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 2 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 Spot; see the file COPYING. If not, write to the Free
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
common_dep = $(top_builddir)/configure.ac
x_to_1 = $(top_builddir)/tools/x-to-1
convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
"$(PERL)" "$(top_srcdir)/tools/help2man -N"
dist_man1_MANS = ltlfilt.1 genltl.1
MAINTAINERCLEANFILES = $(dist_man1_MANS)
man_aux = $(dist_man1_MANS:.1=.x)
ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
$(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@
genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc
$(convman) ../genltl$(EXEEXT) $(srcdir)/genltl.x $@
[NAME]
genltl \- generate LTL formulas from scalable patterns
[DESCRIPTION]
.\" Add any additional description here
[BIBLIOGRAPHY]
Prefixes used in pattern names refer to the following papers:
.TP
gh
J. Geldenhuys and H. Hansen: Larger automata and less
work for LTL model checking. Proceedings of Spin'06. LNCS 3925.
.TP
ccj
J. Cichoń, A. Czubak, and A. Jasiński (DepCoS'09): Minimal Büchi
Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09.
.TP
go
P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation.
Proceedings of CAV'01. LNCS 2102
.TP
rv
K. Rozier and M. Vardi: LTL Satisfiability Checking.
Proceedings of Spin'07. LNCS 4595.
[NAME]
ltlfilt \- filter files or lists of LTL/PSL formulas
[DESCRIPTION]
.\" Add any additional description here
#!/usr/bin/perl -w
# Generate a short man page from --help and --version output.
# Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2009,
# 2010, 2011, 2012 Free Software Foundation, Inc.
# This program 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, or (at your option)
# any later version.
# This program 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/>.
# Written by Brendan O'Dea <bod@debian.org>
# Available from ftp://ftp.gnu.org/gnu/help2man/
use 5.008;
use strict;
use Getopt::Long;
use Text::Tabs qw(expand);
use POSIX qw(strftime setlocale LC_ALL);
use Locale::gettext;
use Encode qw(decode encode);
use I18N::Langinfo qw(langinfo CODESET);
my $this_program = 'help2man';
my $this_version = '1.40.12';
my $encoding;
{
my $gettext = Locale::gettext->domain($this_program);
sub _ { $gettext->get($_[0]) }
my ($user_locale) = grep defined && length,
(map $ENV{$_}, qw(LANGUAGE LC_ALL LC_MESSAGES LANG)), 'C';
my $user_encoding = langinfo CODESET;
# Set localisation of date and executable's output.
sub configure_locale
{
delete @ENV{qw(LANGUAGE LC_MESSAGES LANG)};
setlocale LC_ALL, $ENV{LC_ALL} = shift || 'C';
$encoding = langinfo CODESET;
}
sub dec { $encoding ? decode $encoding, $_[0] : $_[0] }
sub enc { $encoding ? encode $encoding, $_[0] : $_[0] }
sub enc_user { encode $user_encoding, $_[0] }
sub kark # die with message formatted in the invoking user's locale
{
setlocale LC_ALL, $user_locale;
my $fmt = $gettext->get(shift);
my $errmsg = enc_user sprintf $fmt, @_;
die $errmsg, "\n";
}
}
sub N_ { $_[0] }
my $version_info = enc_user sprintf _(<<'EOT'), $this_program, $this_version;
GNU %s %s
Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2009, 2010,
2011, 2012 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Written by Brendan O'Dea <bod@debian.org>
EOT
my $help_info = enc_user sprintf _(<<'EOT'), $this_program, $this_program;
`%s' generates a man page out of `--help' and `--version' output.
Usage: %s [OPTION]... EXECUTABLE
-n, --name=STRING description for the NAME paragraph
-s, --section=SECTION section number for manual page (1, 6, 8)
-m, --manual=TEXT name of manual (User Commands, ...)
-S, --source=TEXT source of program (FSF, Debian, ...)
-L, --locale=STRING select locale (default "C")
-i, --include=FILE include material from `FILE'
-I, --opt-include=FILE include material from `FILE' if it exists
-o, --output=FILE send output to `FILE'
-p, --info-page=TEXT name of Texinfo manual
-N, --no-info suppress pointer to Texinfo manual
-l, --libtool exclude the `lt-' from the program name
--help print this help, then exit
--version print version number, then exit
EXECUTABLE should accept `--help' and `--version' options and produce output on
stdout although alternatives may be specified using:
-h, --help-option=STRING help option string
-v, --version-option=STRING version option string
--version-string=STRING version string
--no-discard-stderr include stderr when parsing option output
Report bugs to <bug-help2man@gnu.org>.
EOT
my $section = 1;
my $manual = '';
my $source = '';
my $help_option = '--help';
my $version_option = '--version';
my $discard_stderr = 1;
my ($opt_name, @opt_include, $opt_output, $opt_info, $opt_no_info, $opt_libtool,
$version_text);
my %opt_def = (
'n|name=s' => \$opt_name,
's|section=s' => \$section,
'm|manual=s' => \$manual,
'S|source=s' => \$source,
'L|locale=s' => sub { configure_locale pop },
'i|include=s' => sub { push @opt_include, [ pop, 1 ] },
'I|opt-include=s' => sub { push @opt_include, [ pop, 0 ] },
'o|output=s' => \$opt_output,
'p|info-page=s' => \$opt_info,
'N|no-info' => \$opt_no_info,
'l|libtool' => \$opt_libtool,
'help' => sub { print $help_info; exit },
'version' => sub { print $version_info; exit },
'h|help-option=s' => \$help_option,
'v|version-option=s' => \$version_option,
'version-string=s' => \$version_text,
'discard-stderr!' => \$discard_stderr,
);
# Parse options.
Getopt::Long::config('bundling');
die $help_info unless GetOptions %opt_def and @ARGV == 1;
configure_locale unless $encoding;
my %include = ();
my %append = ();
my @include = (); # retain order given in include file
# Process include file (if given). Format is:
#
# [section name]
# verbatim text
#
# or
#
# /pattern/
# verbatim text
#
while (@opt_include)
{
my ($inc, $required) = @{shift @opt_include};
next unless -f $inc or $required;
kark N_("%s: can't open `%s' (%s)"), $this_program, $inc, $!
unless open INC, $inc;
my $key;
my $hash = \%include;
while (<INC>)
{
# Convert input to internal Perl format, so that multibyte
# sequences are treated as single characters.
$_ = dec $_;
# [section]
if (/^\[([^]]+)\]\s*$/)
{
$key = uc $1;
$key =~ s/^\s+//;
$key =~ s/\s+$//;
$hash = \%include;
push @include, $key unless $include{$key};
next;
}
# /pattern/
if (m!^/(.*)/([ims]*)\s*$!)
{
my $pat = $2 ? "(?$2)$1" : $1;
# Check pattern.
eval { $key = qr($pat) };
if ($@)
{
$@ =~ s/ at .*? line \d.*//;
die "$inc:$.:$@";
}
$hash = \%append;
next;
}
# Check for options before the first section--anything else is
# silently ignored, allowing the first for comments and
# revision info.
unless ($key)
{
# handle options
if (/^-/)
{
local @ARGV = split;
GetOptions %opt_def;
}
next;
}
$hash->{$key} ||= '';
$hash->{$key} .= $_;
}
close INC;
kark N_("%s: no valid information found in `%s'"), $this_program, $inc
unless $key;
}
# Compress trailing blank lines.
for my $hash (\(%include, %append))
{
for (keys %$hash) { $hash->{$_} =~ s/\n+$/\n/ }
}
sub get_option_value;
# Grab help and version info from executable.
my $help_text = get_option_value $ARGV[0], $help_option;
$version_text ||= get_option_value $ARGV[0], $version_option;
# Translators: the following message is a strftime(3) format string, which in
# the English version expands to the month as a word and the full year. It
# is used on the footer of the generated manual pages. If in doubt, you may
# just use %x as the value (which should be the full locale-specific date).
my $date = enc strftime _("%B %Y"), localtime;
(my $program = $ARGV[0]) =~ s!.*/!!;
my $package = $program;
my $version;
if ($opt_output)
{
unlink $opt_output or kark N_("%s: can't unlink %s (%s)"),
$this_program, $opt_output, $! if -e $opt_output;
open STDOUT, ">$opt_output"
or kark N_("%s: can't create %s (%s)"), $this_program, $opt_output, $!;
}
# The first line of the --version information is assumed to be in one
# of the following formats:
#
# <version>
# <program> <version>
# {GNU,Free} <program> <version>
# <program> ({GNU,Free} <package>) <version>
# <program> - {GNU,Free} <package> <version>
#
# and separated from any copyright/author details by a blank line.
($_, $version_text) = ((split /\n+/, $version_text, 2), '');
if (/^(\S+) +\(((?:GNU|Free) +[^)]+)\) +(.*)/ or
/^(\S+) +- *((?:GNU|Free) +\S+) +(.*)/)
{
$program = $1;
$package = $2;
$version = $3;
}
elsif (/^((?:GNU|Free) +)?(\S+) +(.*)/)
{
$program = $2;
$package = $1 ? "$1$2" : $2;
$version = $3;
}
else
{
$version = $_;
}
$program =~ s!.*/!!;
# No info for `info' itself.
$opt_no_info = 1 if $program eq 'info';
# Translators: "NAME", "SYNOPSIS" and other one or two word strings in all
# upper case are manual page section headings. The man(1) manual page in your
# language, if available should provide the conventional translations.
for ($include{_('NAME')})
{
if ($opt_name) # --name overrides --include contents.
{
$_ = "$program \\- $opt_name\n";
}
elsif ($_) # Use first name given as $program
{
$program = $1 if /^([^\s,]+)(?:,?\s*[^\s,\\-]+)*\s+\\?-/;
}
else # Set a default (useless) NAME paragraph.
{
$_ = sprintf _("%s \\- manual page for %s %s") . "\n", $program,
$program, $version;
}
}
# Man pages traditionally have the page title in caps.
my $PROGRAM = uc $program;
# Set default page head/footers
$source ||= "$program $version";
unless ($manual)
{
for ($section)
{
if (/^(1[Mm]|8)/) { $manual = enc _('System Administration Utilities') }
elsif (/^6/) { $manual = enc _('Games') }
else { $manual = enc _('User Commands') }
}
}
# Extract usage clause(s) [if any] for SYNOPSIS.
# Translators: "Usage" and "or" here are patterns (regular expressions) which
# are used to match the usage synopsis in program output. An example from cp
# (GNU coreutils) which contains both strings:
# Usage: cp [OPTION]... [-T] SOURCE DEST
# or: cp [OPTION]... SOURCE... DIRECTORY
# or: cp [OPTION]... -t DIRECTORY SOURCE...
my $PAT_USAGE = _('Usage');
my $PAT_USAGE_CONT = _('or');
if ($help_text =~ s/^($PAT_USAGE):( +(\S+))(.*)((?:\n(?: {6}\1| *($PAT_USAGE_CONT): +\S).*)*)//om)
{
my @syn = $3 . $4;
if ($_ = $5)
{
s/^\n//;
for (split /\n/) { s/^ *(($PAT_USAGE_CONT): +)?//o; push @syn, $_ }
}
my $synopsis = '';
for (@syn)
{
$synopsis .= ".br\n" if $synopsis;
s!^\S*/!!;
s/^lt-// if $opt_libtool;
s/^(\S+) *//;
$synopsis .= ".B $1\n";
s/\s+$//;
s/(([][]|\.\.+)+)/\\fR$1\\fI/g;
s/^/\\fI/ unless s/^\\fR//;
$_ .= '\fR';
s/(\\fI)( *)/$2$1/g;
s/\\fI\\fR//g;
s/^\\fR//;
s/\\fI$//;
s/^\./\\&./;
$synopsis .= "$_\n";
}
$include{_('SYNOPSIS')} ||= $synopsis;
}
# Process text, initial section is DESCRIPTION.
my $sect = _('DESCRIPTION');
$_ = "$help_text\n\n$version_text";
# Normalise paragraph breaks.
s/^\n+//;
s/\n*$/\n/;
s/\n\n+/\n\n/g;
# Join hyphenated lines.
s/([A-Za-z])-\n *([A-Za-z])/$1$2/g;
# Temporarily exchange leading dots, apostrophes and backslashes for
# tokens.
s/^\./\x80/mg;
s/^'/\x81/mg;
s/\\/\x82/g;
# Translators: patterns are used to match common program output. In the source
# these strings are all of the form of "my $PAT_something = _('...');" and are
# regular expressions. If there is more than one commonly used string, you
# may separate alternatives with "|". Spaces in these expressions are written
# as " +" to indicate that more than one space may be matched. The string
# "(?:[\\w-]+ +)?" in the bug reporting pattern is used to indicate an
# optional word, so that either "Report bugs" or "Report _program_ bugs" will
# be matched.
my $PAT_BUGS = _('Report +(?:[\w-]+ +)?bugs|Email +bug +reports +to');
my $PAT_AUTHOR = _('Written +by');
my $PAT_OPTIONS = _('Options');
my $PAT_ENVIRONMENT = _('Environment');
my $PAT_FILES = _('Files');
my $PAT_EXAMPLES = _('Examples');
my $PAT_FREE_SOFTWARE = _('This +is +free +software');
# Start a new paragraph (if required) for these.
s/([^\n])\n($PAT_BUGS|$PAT_AUTHOR) /$1\n\n$2 /og;
# Convert iso-8859-1 copyright symbol or (c) to nroff
# character.
s/^Copyright +(?:\xa9|\([Cc]\))/Copyright \\(co/mg;
sub convert_option;
while (length)
{
# Convert some standard paragraph names.
if (s/^($PAT_OPTIONS): *\n//o)
{
$sect = _('OPTIONS');
next;
}
if (s/^($PAT_ENVIRONMENT): *\n//o)
{
$sect = _('ENVIRONMENT');
next;
}
if (s/^($PAT_FILES): *\n//o)
{
$sect = _('FILES');
next;
}
elsif (s/^($PAT_EXAMPLES): *\n//o)
{
$sect = _('EXAMPLES');
next;
}
# Copyright section
if (/^Copyright /)
{
$sect = _('COPYRIGHT');
}
# Bug reporting section.
elsif (/^($PAT_BUGS) /o)
{
$sect = _('REPORTING BUGS');
}
# Author section.
elsif (/^($PAT_AUTHOR)/o)
{
$sect = _('AUTHOR');
}
# Examples, indicated by an indented leading $, % or > are
# rendered in a constant width font.
if (/^( +)([\$\%>] )\S/)
{
my $indent = $1;
my $prefix = $2;
my $break = '.IP';
$include{$sect} ||= '';
while (s/^$indent\Q$prefix\E(\S.*)\n*//)
{
$include{$sect} .= "$break\n\\f(CW$prefix$1\\fR\n";
$break = '.br';
}