Commit 101c2533 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sanity: ensure that all environment variables are documented

* tests/sanity/getenv.test: New file.
* tests/Makefile.am: Add it.
* bin/man/spot-x.x: Document SPOT_STUTTER_CHECK and SPOT_DEBUG_PARSER.
parent 93969758
...@@ -65,6 +65,11 @@ is the same as running ...@@ -65,6 +65,11 @@ is the same as running
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
it up once for many commands. it up once for many commands.
.TP
\fBSPOT_DEBUG_PARSER\fR
If this variable is set to any value, the automaton parser of Spot is
executed in debug mode, showing how the input is processed.
.TP .TP
\fBSPOT_DOTDEFAULT\fR \fBSPOT_DOTDEFAULT\fR
Whenever the \f(CW--dot\fR option is used without argument (even Whenever the \f(CW--dot\fR option is used without argument (even
...@@ -129,6 +134,31 @@ all Streett automata, however we do not recommand setting it to less ...@@ -129,6 +134,31 @@ all Streett automata, however we do not recommand setting it to less
than 2, because the "Fin-removal" approach is better for single-pair than 2, because the "Fin-removal" approach is better for single-pair
Streett automata. Streett automata.
.TP
\fBSPOT_STUTTER_CHECK\fR
Select the default check used to decide stutter invariance. The
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.
.RS
.IP 1
sl(a) x sl(!a)
.IP 2
sl(cl(a)) x !a
.IP 3
cl(sl(a)) x !a
.IP 4
sl2(a) x sl2(!a)
.IP 5
sl2(cl(a)) x !a
.IP 6
cl(sl2(a)) x !a
.IP 7
sl(a) x sl(!a), performed on-the-fly
.IP 8
cl(a) x cl(!a)
.RE
.TP .TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
These variables control in which directory temporary files (e.g., These variables control in which directory temporary files (e.g.,
...@@ -182,6 +212,15 @@ SAT Solving. Proceedings of SAT'10. LNCS 6175. ...@@ -182,6 +212,15 @@ SAT Solving. Proceedings of SAT'10. LNCS 6175.
Our SAT-based minimization procedures are generalizations of this Our SAT-based minimization procedures are generalizations of this
paper to deal with TBA or TGBA. paper to deal with TBA or TGBA.
.TP
4.
Thibaud Michaud and Alexandre Duret-Lutz: Practical stutter-invariance
checks for ω-regular languages, Proceedings of SPIN'15. LNCS 9232.
Describes the stutter-invariance checks that can be selected through
\fBSPOT_STUTTER_CHECK\fR.
[SEE ALSO] [SEE ALSO]
.BR ltl2tgba (1) .BR ltl2tgba (1)
.BR ltl2tgta (1) .BR ltl2tgta (1)
......
...@@ -418,6 +418,7 @@ endif ...@@ -418,6 +418,7 @@ endif
TESTS_sanity = \ TESTS_sanity = \
sanity/80columns.test \ sanity/80columns.test \
sanity/bin.test \ sanity/bin.test \
sanity/getenv.test \
sanity/includes.test \ sanity/includes.test \
sanity/ipynb.pl \ sanity/ipynb.pl \
sanity/namedprop.test \ sanity/namedprop.test \
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 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/>.
# We used to loop over more directories before the source tree was
# rearranged. So there is only one left today, but we keep the loop
# in case we want to add more in the future.
set +x
DOC=bin/man/spot-x.x
rm -f getenv.log
TOP=${srcdir-.}/../..
for dir in "$TOP/spot" "$TOP/bin"; do
find "$dir" \( -name "${1-*}.hh" \
-o -name "${1-*}.hxx" \
-o -name "${1-*}.cc" \) \
-a -not -path '*.dir/*' \
-a -type f -a -print
done |
xargs sed -n 's/.*getenv("\([^"]*\)").*/\1/p' |
sort | uniq |
while read prop; do
if ! grep -q "$prop" "$TOP/$DOC"; then
echo "* $prop" >>getenv.log
fi
done
if test -f getenv.log; then
echo "These environment variables are not documented in $DOC:"
cat getenv.log
exit 1
fi
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