Commit 17f91132 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 54e25e38
Pipeline #8559 failed with stages
in 341 minutes and 42 seconds
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