alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

man: fix several issues

Browse source 
The \f(CW macro to switch to "constant-width" does not seem to
honored when converting to html, and I've found some patch to
groff removing its use from their own man page.
https://lists.gnu.org/archive/html/groff-commit/2020-07/msg00015.html
Lets use \fC instead, as it seems to produce some <tt> in HTML.

Two manpages had URLs pointing to spot.lrde.epita.fr instead of
spot.lre.epita.fr.

Finally, spot-x.x had an incorrectly closed .EX block, that completly
broke the HTML conversion.

* bin/man/autcross.x, bin/man/ltl2tgba.x, bin/man/ltlcross.x,
bin/man/spot-x.x, bin/man/spot.x: Fix the aforementioned issues.
This commit is contained in:
Alexandre Duret-Lutz 2024-04-03 23:05:12 +02:00
parent a17d8a0501
commit 848d1a3901
5 changed files with 44 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

12
bin/man/autcross.x
View file

@ -59,29 +59,29 @@ Information about how the execution of the tool went.
values: values:
.RS .RS
.TP .TP
\f(CW"ok"\fR \fC"ok"\fR
The tool ran succesfully (this does not imply that the produced The tool ran succesfully (this does not imply that the produced
automaton is correct) and autcross could parse the resulting automaton is correct) and autcross could parse the resulting
automaton. In this case \fBexit_code\fR is always 0. automaton. In this case \fBexit_code\fR is always 0.
.TP .TP
\f(CW"timeout"\fR \fC"timeout"\fR
The tool ran for more than the number of seconds The tool ran for more than the number of seconds
specified with the \fB\-\-timeout\fR option. In this specified with the \fB\-\-timeout\fR option. In this
case \fBexit_code\fR is always -1. case \fBexit_code\fR is always -1.
.TP .TP
\f(CW"exit code"\fR \fC"exit code"\fR
The tool terminated with a non-zero exit code. The tool terminated with a non-zero exit code.
\fBexit_code\fR contains that value. \fBexit_code\fR contains that value.
.TP .TP
\f(CW"signal"\fR \fC"signal"\fR
The tool terminated with a signal. The tool terminated with a signal.
\fBexit_code\fR contains that signal's number. \fBexit_code\fR contains that signal's number.
.TP .TP
\f(CW"parse error"\fR \fC"parse error"\fR
The tool terminated normally, but autcross could not The tool terminated normally, but autcross could not
parse its output. In this case \fBexit_code\fR is always -1. parse its output. In this case \fBexit_code\fR is always -1.
.TP .TP
\f(CW"no output"\fR \fC"no output"\fR
The tool terminated normally, but without creating the specified The tool terminated normally, but without creating the specified
output file. In this case \fBexit_code\fR is always -1. output file. In this case \fBexit_code\fR is always -1.
.RE .RE

10
bin/man/ltl2tgba.x
View file

@ -13,7 +13,7 @@ condition, meanings that a run of the automaton is accepted iff it
visits ininitely often multiple acceptance sets, and it also uses visits ininitely often multiple acceptance sets, and it also uses
transition-based acceptance, i.e., those acceptance sets are sets of transition-based acceptance, i.e., those acceptance sets are sets of
transitions. TGBA are often more consise than traditional Büchi transitions. TGBA are often more consise than traditional Büchi
automata. For instance the LTL formula \f(CWGFa & GFb\fR can be automata. For instance the LTL formula \fCGFa & GFb\fR can be
translated into a single-state TGBA while a traditional Büchi translated into a single-state TGBA while a traditional Büchi
automaton would need 3 states. Compare automaton would need 3 states. Compare
.PP .PP
@ -158,11 +158,11 @@ are not recognized, i.e., infinite words that start with a bad prefix.
.PP .PP
Because of this limited expressiveness, a monitor for some given LTL Because of this limited expressiveness, a monitor for some given LTL
or PSL formula may accept a larger language than the one specified by or PSL formula may accept a larger language than the one specified by
the formula. For instance a monitor for the LTL formula \f(CWa U b\fR the formula. For instance a monitor for the LTL formula \fCa U b\fR
will reject (for instance) any word starting with \f(CW!a&!b\fR as will reject (for instance) any word starting with \fC!a&!b\fR as
there is no way such a word can validate the formula, but it will not there is no way such a word can validate the formula, but it will not
reject a finite prefix repeating only \f(CWa&!b\fR as such a prefix reject a finite prefix repeating only \fCa&!b\fR as such a prefix
could be extented in a way that is comptible with \f(CWa U b\fR. could be extented in a way that is comptible with \fCa U b\fR.
.PP .PP
For more information about monitors, we refer the readers to the For more information about monitors, we refer the readers to the
following two papers (the first paper describes the construction of following two papers (the first paper describes the construction of

28
bin/man/ltlcross.x
View file

@ -12,7 +12,7 @@ for 100 random formulas, using a timeout of 2 minutes. Because
knows those tools, there is no need to specify their input and knows those tools, there is no need to specify their input and
output. A trace of the execution of the two tools, including any output. A trace of the execution of the two tools, including any
potential issue detected, is reported on standard error, while potential issue detected, is reported on standard error, while
statistics are written to \f(CWresults.json\fR. statistics are written to \fCresults.json\fR.
.PP .PP
.in +4n .in +4n
.nf .nf
@ -26,14 +26,14 @@ The next command compares
.BR ltl3ba , .BR ltl3ba ,
and and
.BR ltl2tgba (1) .BR ltl2tgba (1)
on a set of formulas saved in file \f(CWinput.ltl\fR. on a set of formulas saved in file \fCinput.ltl\fR.
Statistics are again writen Statistics are again writen
as CSV into \f(CWresults.csv\fR. This examples specify the as CSV into \fCresults.csv\fR. This examples specify the
input and output for each tool, to show how this can be done. input and output for each tool, to show how this can be done.
Note the use of \f(CW%L\fR to indicate that the formula passed t Note the use of \fC%L\fR to indicate that the formula passed t
for the formula in for the formula in
.BR spin (1)'s .BR spin (1)'s
format, and \f(CW%f\fR for the format, and \fC%f\fR for the
formula in Spot's format. Each of these tool produces an formula in Spot's format. Each of these tool produces an
automaton in a different format (respectively, LBTT's format, automaton in a different format (respectively, LBTT's format,
Spin's never claims, and HOA format), but Spot's parser can Spin's never claims, and HOA format), but Spot's parser can
@ -51,7 +51,7 @@ distinguish and understand these three formats.
Rabin or Streett automata output by Rabin or Streett automata output by
.B ltl2dstar .B ltl2dstar
in its historical format can be read from a in its historical format can be read from a
file specified with \f(CW%D\fR instead of \f(CW%O\fR. For instance: file specified with \fC%D\fR instead of \fC%O\fR. For instance:
.PP .PP
.in +4n .in +4n
.nf .nf
@ -99,7 +99,7 @@ The formula translated.
\fBtool\fR \fBtool\fR
The tool used to translate this formula. This is either the value of the The tool used to translate this formula. This is either the value of the
full \fICOMMANDFMT\fR string specified on the command-line, or, full \fICOMMANDFMT\fR string specified on the command-line, or,
if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\fICMD\fR, if \fICOMMANDFMT\fR has the form \fC{\fISHORTNAME\fR\fC}\fR\fICMD\fR,
the value of \fISHORTNAME\fR. the value of \fISHORTNAME\fR.
.TP .TP
\fBexit_status\fR, \fBexit_code\fR \fBexit_status\fR, \fBexit_code\fR
@ -110,29 +110,29 @@ Otherwise, \fBexit_status\fR is a string that can take the following
values: values:
.RS .RS
.TP .TP
\f(CW"ok"\fR \fC"ok"\fR
The translator ran succesfully (this does not imply that the produced The translator ran succesfully (this does not imply that the produced
automaton is correct) and ltlcross could parse the resulting automaton is correct) and ltlcross could parse the resulting
automaton. In this case \fBexit_code\fR is always 0. automaton. In this case \fBexit_code\fR is always 0.
.TP .TP
\f(CW"timeout"\fR \fC"timeout"\fR
The translator ran for more than the number of seconds The translator ran for more than the number of seconds
specified with the \fB\-\-timeout\fR option. In this specified with the \fB\-\-timeout\fR option. In this
case \fBexit_code\fR is always -1. case \fBexit_code\fR is always -1.
.TP .TP
\f(CW"exit code"\fR \fC"exit code"\fR
The translator terminated with a non-zero exit code. The translator terminated with a non-zero exit code.
\fBexit_code\fR contains that value. \fBexit_code\fR contains that value.
.TP .TP
\f(CW"signal"\fR \fC"signal"\fR
The translator terminated with a signal. The translator terminated with a signal.
\fBexit_code\fR contains that signal's number. \fBexit_code\fR contains that signal's number.
.TP .TP
\f(CW"parse error"\fR \fC"parse error"\fR
The translator terminated normally, but ltlcross could not The translator terminated normally, but ltlcross could not
parse its output. In this case \fBexit_code\fR is always -1. parse its output. In this case \fBexit_code\fR is always -1.
.TP .TP
\f(CW"no output"\fR \fC"no output"\fR
The translator terminated normally, but without creating the specified The translator terminated normally, but without creating the specified
output file. In this case \fBexit_code\fR is always -1. output file. In this case \fBexit_code\fR is always -1.
.RE .RE
@ -150,7 +150,7 @@ translated automaton. Column \fBedges\fR counts the number of edges
(labeled by Boolean formulas) in the automaton seen as a graph, while (labeled by Boolean formulas) in the automaton seen as a graph, while
\fBtransitions\fR counts the number of assignment-labeled transitions \fBtransitions\fR counts the number of assignment-labeled transitions
that might have been merged into a formula-labeled edge. For instance that might have been merged into a formula-labeled edge. For instance
an edge labeled by \f(CWtrue\fR will be counted as 2^3=8 transitions if an edge labeled by \fCtrue\fR will be counted as 2^3=8 transitions if
the automaton uses 3 atomic propositions. the automaton uses 3 atomic propositions.
.TP .TP
\fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR \fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR

36
bin/man/spot-x.x
View file

@ -10,7 +10,7 @@ spot-x \- Common fine-tuning options and environment variables.
.\" Add any additional description here .\" Add any additional description here
[SAT\-MINIMIZE VALUES] [SAT\-MINIMIZE VALUES]
When the sat-minimize=K option is used to enable SAT-based When the \fBsat-minimize=K\fR option is used to enable SAT-based
minimization of deterministic automata, a SAT solver is minimization of deterministic automata, a SAT solver is
used to minimize an input automaton with N states into an used to minimize an input automaton with N states into an
output automaton with 1≤M≤N states. The parameter K specifies output automaton with 1≤M≤N states. The parameter K specifies
@ -72,12 +72,12 @@ passed to the printer by suffixing the output format with
.in +4n .in +4n
.EX .EX
% SPOT_DEFAULT_FORMAT=dot=bar autfilt ... % SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
.EN .EE
.in -4n .in -4n
is the same as running is the same as running
.in +4n .in +4n
.EX .EX
% autfilt --dot=bar ... % autfilt \-\-dot=bar ...
.EE .EE
.in -4n .in -4n
but the use of the environment variable makes more sense if you set but the use of the environment variable makes more sense if you set
@ -92,9 +92,9 @@ executed in debug mode, showing how the input is processed.
\fBSPOT_DOTDEFAULT\fR \fBSPOT_DOTDEFAULT\fR
Whenever the \fB\-\-dot\fR option is used without argument (even Whenever the \fB\-\-dot\fR option is used without argument (even
implicitely via \fBSPOT_DEFAULT_FORMAT\fR), the contents of this implicitely via \fBSPOT_DEFAULT_FORMAT\fR), the contents of this
variable is used as default argument. If you have some default variable are used as default argument. If you have some default
settings in \fBSPOT_DOTDEFAULT\fR and want to append to options settings in \fBSPOT_DOTDEFAULT\fR and want to append to options
\f(CWxyz\fR temporarily for one call, use \fB\-\-dot=.xyz\fR: \fCxyz\fR temporarily for one call, use \fB\-\-dot=.xyz\fR:
the dot character will be replaced by the contents of the the dot character will be replaced by the contents of the
\fBSPOT_DOTDEFAULT\fR environment variable. \fBSPOT_DOTDEFAULT\fR environment variable.
@ -123,7 +123,7 @@ is actually used)
.TP .TP
\fBSPOT_O_CHECK\fR \fBSPOT_O_CHECK\fR
Specifies the default algorithm that should be used Specifies the default algorithm that should be used
by the \f(CWis_obligation()\fR function. The value should by the \fCis_obligation()\fR function. The value should
be one of the following: be one of the following:
.RS .RS
.RS .RS
@ -141,24 +141,24 @@ by a weak and deterministic Büchi automata.
.TP .TP
\fBSPOT_OOM_ABORT\fR \fBSPOT_OOM_ABORT\fR
If this variable is set, Out-Of-Memory errors will \f(CWabort()\fR the If this variable is set, Out-Of-Memory errors will \fCabort()\fR the
program (potentially generating a coredump) instead of raising an program (potentially generating a coredump) instead of raising an
exception. This is useful to debug a program and to obtain a stack exception. This is useful to debug a program and to obtain a stack
trace pointing to the function doing the allocation. When this trace pointing to the function doing the allocation. When this
variable is unset (the default), \f(CWstd::bad_alloc\fR are thrown on variable is unset (the default), \fCstd::bad_alloc\fR are thrown on
memory allocation failures, and the stack is usually unwinded up to memory allocation failures, and the stack is usually unwinded up to
top-level, losing the original context of the error. Note that at top-level, losing the original context of the error. Note that at
least \f(CWltlcross\fR has some custom handling of least \fCltlcross\fR has some custom handling of
\f(CWstd::bad_alloc\fR to recover from products that are too large (by \fCstd::bad_alloc\fR to recover from products that are too large (by
ignoring them), and setting this variable will interfer with that. ignoring them), and setting this variable will interfer with that.
.TP .TP
\fBSPOT_PR_CHECK\fR \fBSPOT_PR_CHECK\fR
Select the default algorithm that must be used to check the persistence 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 between or recurrence property of a formula f. The values it can take are between
1 and 3. All methods work either on f or !f thanks to the duality of 1 and 3. All methods work either on f or !f thanks to the duality of
persistence and recurrence classes. See persistence and recurrence classes. See
.UR https://spot.lrde.epita.fr/hierarchy.html .UR https://spot.lre.epita.fr/hierarchy.html
this page this page
.UE .UE
for more details. If it is set to: for more details. If it is set to:
@ -196,8 +196,8 @@ format.
If set, this variable should indicate how to call an external If set, this variable should indicate how to call an external
SAT\-solver \- by default, Spot uses PicoSAT, which is distributed SAT\-solver \- by default, Spot uses PicoSAT, which is distributed
with. This is used by the sat\-minimize option described above. with. This is used by the sat\-minimize option described above.
The format to follow is the following: \f(CW"<sat_solver> [options] %I >%O"\fR. The format to follow is the following: \fC"<sat_solver> [options] %I >%O"\fR.
The escape sequences \f(CW%I\fR and \f(CW%O\fR respectively The escape sequences \fC%I\fR and \fC%O\fR respectively
denote the names of the input and output files. These temporary files denote the names of the input and output files. These temporary files
are created in the directory specified by \fBSPOT_TMPDIR\fR or are created in the directory specified by \fBSPOT_TMPDIR\fR or
\fBTMPDIR\fR (see below). The SAT\-solver should follow the convention \fBTMPDIR\fR (see below). The SAT\-solver should follow the convention
@ -281,7 +281,7 @@ This is mostly useful for debugging.
.TP .TP
\fBSPOT_XCNF\fR \fBSPOT_XCNF\fR
Assign a folder path to this variable to generate XCNF files whenever Assign a folder path to this variable to generate XCNF files whenever
SAT\-based minimization is used \- the file is outputed as "incr.xcnf" SAT\-based minimization is used \- the file is output as "incr.xcnf"
in the specified directory. This feature works only with an external in the specified directory. This feature works only with an external
SAT\-solver. See \fBSPOT_SATSOLVER\fR to know how to provide one. Also note SAT\-solver. See \fBSPOT_SATSOLVER\fR to know how to provide one. Also note
that this needs an incremental approach without restarting the encoding i.e that this needs an incremental approach without restarting the encoding i.e
@ -290,8 +290,8 @@ autfilt (see sat\-minimize options described above or autfilt man page).
The XCNF format is the one used by the SAT incremental competition. The XCNF format is the one used by the SAT incremental competition.
[BIBLIOGRAPHY] [BIBLIOGRAPHY]
The following papers are related to some of the options and
The following papers are related to some of the options and environment variables. environment variables.
.TP .TP
1. 1.
@ -344,7 +344,7 @@ Kyveli Doveri and Pierre Ganty and Nicolas Mazzocchi:
FORQ-Based Language Inclusion Formal Testing. FORQ-Based Language Inclusion Formal Testing.
Proceedings of CAV'22. LNCS 13372. Proceedings of CAV'22. LNCS 13372.
The containment check implemented as spot::contains_forq(), and The containment check implemented as \fCspot::contains_forq()\fR, and
used for Büchi automata when \fBSPOT_CONTAINMENT_CHECK=forq\fR. used for Büchi automata when \fBSPOT_CONTAINMENT_CHECK=forq\fR.
[SEE ALSO] [SEE ALSO]

2
bin/man/spot.x
View file

@ -27,6 +27,6 @@ that are listed below.
.BR randltl (1) .BR randltl (1)
.BR spot-x (7) .BR spot-x (7)
.UR https://spot.lrde.epita.fr/ .UR https://spot.lre.epita.fr/
The Spot web page. The Spot web page.
.UE .UE