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

man: minor fixes

* bin/man/spot-x.x, bin/man/dstar2tgba.x, bin/ Cosmetics
* bin/man/README: New file.
parent f3657a67
To help with keeping man pages in sync with the binaries, the man page
for PROGRAM is automatically generated from two sources:
1. the --help output of bin/PROGRAM,
2. the bin/man/PROGRAM.x file
The tool help2man is responsible for doing this conversion.
The PROGRAM.x file has [sections] headers to indicate sections. The
rest of the file uses groff macros for man pages. For detail on this
syntax, run "man groff_man".
Note that some of the standard sections will be forced to the top or
bottom of the manpage by help2man, the rest will appear as ordered in
......@@ -60,9 +60,13 @@ would make more sense.
.BR ltl2dstar manual
.UE .
Documents the output format of ltl2dstar.
Documents the output format of
.BR ltl2dstar .
......@@ -55,17 +55,15 @@ convenient when chaining tools in a pipe. Set this variable to
passed to the printer by suffixing the output format with
\fB=\fR and the options. For instance running
.in +4n
.ft C
% SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
.in -4n
is the same as running
.in +4n
.ft C
% autfilt --dot=bar ...
.in -4n
but the use of the environment variable makes more sense if you set
it up once for many commands.
......@@ -105,6 +103,7 @@ Specifies the default algorithm that should be used
by the \f(CWis_obligation()\fR function. The value should
be one of the following:
.IP 1
Make sure that the formula and its negation are
realizable by non-deterministic co-Büchi automata.
......@@ -115,6 +114,7 @@ realizable by deterministic Büchi automata.
Make sure that the formula is realizable
by a weak and deterministic Büchi automata.
......@@ -134,9 +134,12 @@ ignoring them), and setting this variable will interfer with that.
Select the default algorithm that must be used to check the persistence
or recurrence property of a formula f. The values it can take are 1
or 2. Both methods work either on f or !f thanks to the duality of
persistence and recurrence classes.
See "" for more details. If
it is set to:
persistence and recurrence classes. See
this page
for more details. If it is set to:
.IP 1
It will try to check if f (or !f) is co-Büchi realizable in order to
......@@ -145,6 +148,7 @@ tell if f belongs to the persistence (or the recurrence) class.
It checks if f (or !f) is det-Büchi realizable to tell if f belongs
to the recurrence (or the persistence) class.
......@@ -202,6 +206,7 @@ variable should hold a value between 1 and 8, corresponding to the
following tests described in our Spin'15 paper (see the BIBLIOGRAPHY
section). The default is 8.
.IP 1
sl(a) x sl(!a)
.IP 2
......@@ -219,6 +224,7 @@ sl(a) x sl(!a), performed on-the-fly
.IP 8
cl(a) x cl(!a)
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// This file is part of Spot, a model checking library.
......@@ -43,7 +43,7 @@ static const argp_option options[] =
(0) disables it, (1) enables rules based on syntactic implications, \
(2) additionally allows automata-based implication checks, (3) enables \
more rules based on automata-based implication checks. The default value \
depends on the --low/--medium/--high settings.") },
depends on the --low, --medium, or --high settings.") },
{ nullptr, 0, nullptr, 0, "Translation options:", 0 },
{ DOC("ltl-split", "Set to 0 to disable the translation of automata \
as product or sum of subformulas.") },
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment