...
 
Commits (571)
......@@ -61,6 +61,7 @@ debian-gcc-snapshot:
- ./configure --with-included-ltdl CXX='g++'
- make
- make distcheck DISTCHECK_CONFIGURE_FLAGS='--with-included-ltdl'
allow_failure: true
artifacts:
when: always
paths:
......@@ -82,6 +83,7 @@ alpine-gcc:
- ./configure
- make
- make check
- make distcheck || { chmod -R u+w ./spot-*; false; }
artifacts:
when: always
paths:
......@@ -114,11 +116,10 @@ arch-gcc-glibcxxdebug:
- /wip/
image: registry.lrde.epita.fr/spot-arch
script:
- env
- autoreconf -vfi
- ./configure --enable-devel --enable-c++17 --enable-glibcxx-debug
- make
- make distcheck
- make distcheck DISTCHECK_CONFIGURE_FLAGS='--enable-devel --enable-c++17 --enable-glibcxx-debug'
artifacts:
when: on_failure
paths:
......@@ -283,3 +284,23 @@ publish-unstable:
- dput lrde *.changes
- curl -X POST -F ref=master -F token=$TRIGGER_SPOT_WEB -F "variables[spot_branch]=next" https://gitlab.lrde.epita.fr/api/v4/projects/131/trigger/pipeline
- curl -X POST -F ref=master -F token=$TRIGGER_SANDBOX https://gitlab.lrde.epita.fr/api/v4/projects/181/trigger/pipeline
raspbian:
stage: build
only:
- branches
except:
- /wip/
tags:
- armv7
script:
- autoreconf -vfi
- ./configure
- make
- make distcheck || { chmod -R u+w ./spot-*; false; }
artifacts:
when: always
paths:
- ./spot-*/_build/sub/tests/*/*.log
- ./*.log
- ./*.tar.gz
......@@ -13,6 +13,7 @@ Denis Poitrenaud
Elie Abi Saad
Étienne Renault
Félix Abecassis
Florian Renkin
Guillaume Sadegh
Heikki Tauriainen
Henrich Lauko
......
......@@ -86,35 +86,34 @@ Avoiding org-mode runs
The files in doc/org/ are org-mode files (a mode of Emacs that we use
to author documents that embed executable snippets), they are used to
generate the doc/userdoc/ HTML documentation. If for some reason you
don't have emacs, or you simply want not to rebuild these files, use
another "magic touch":
don't have emacs, or you simply want not to rebuild these files, use:
touch doc/org-stamp
% touch doc/org-stamp
Silent Building with automake
-----------------------------
The classical makefiles generated by automake are very verbose during
build beacause they prints the full command line of every stage. This
verbosity is very usefull to help (remotely) users to compile
Spot. Nonetheless, for developpers, these compilations lines may be
annoying. To reduce this verbosity, just run:
build beacause they print the full command line of every stage. This
verbosity is very usefull to help (remotely) users to compile Spot.
Nonetheless, these compilations lines may be annoying for some
developers. To reduce this verbosity, just run:
make V=0
% make V=0
Executing a single test
-----------------------
All tests in subdirectories of tests/ are executed through the
tests/run script. That run script defines PATH and other environment
variables necessary so that Shell and Python scripts will use the
tests/run script. That script defines PATH and other environment
variables necessary so that shell and Python scripts will use the
version of Spot under development. For instance to execute
tests/core/acc.test, do:
% cd tests
% ./run core/acc.test
% cd tests
% ./run core/acc.test
A test run this way automatically executes in verbose mode. Any
temporary file generated by the script can be found in
......@@ -216,20 +215,19 @@ Finally generate a coverage report in HTML:
This should create the directory html/.
Coverage tests are automatically performed by our continuous
integration builds. You can find a report for each branch in the
artifacts of the debian-unstable-gcc-coverage job.
Link-time optimizations
-----------------------
This is currently a bit tricky to setup, because the toolchain is not
mature enough. However this is getting better and better. The Debian
packages we build nightly are mostly built with link-time optimization
(the shared library uses link-time optimization, but the command-line
binary are built without because of some bug with exception
propagation).
This used to be bit tricky to setup, but is now quite well supported.
Our Debian packages are built with link-time optimization.
You need:
1. a version of GCC (>= 4.9) with gold and pluing linker enabled.
1. a version of GCC (>= 4.9) with gold and pluging linker enabled.
2. a version of Libtool that knows how to deal with
-flto flags (Libtool 2.4.2 will work)
......@@ -250,9 +248,9 @@ Log driver for testsuite
The PASS/FAIL status for each test of the testsuite is printed by
tools/test-driver. This script can be changed to format the output
differently. When we use Teamcity (for continuous integration) we
change the output format to something that Teamcity will understand
with:
differently. In the past, when we used teamcity (for continuous
integration) we changed the output format to something that teamcity
would understand with:
make check LOG_DRIVER=$PWD/tools/test-driver-teamcity
......@@ -354,7 +352,7 @@ Exporting symbols
header.
* The directory src/priv/ can be used to store files that are
globaly private the library, and that do not really belongs to
globaly private to the library, and that do not really belong to
other directories.
* Functions and classes that are public should be marked with
......@@ -402,8 +400,9 @@ Comments
Issue #123 / issue #123 / Fixes #123 / fixes #123
(When gitlab sees a commit message containing "Fixes #123" or
"fixes #123" pushed to branch "next", it will automatically close
the issue.)
"fixes #123" pushed to branch "next", it should automatically
close the issue. But these days, it does not seem to work and
often require manual closing.)
Formating
---------
......
This diff is collapsed.
......@@ -44,16 +44,6 @@ an idea about how to generate a manual for the Python bindings
automatically, please do contribute!
History
=======
This project started in 2003 at LIP6 (www.lip6.fr). The main author
moved to LRDE (www.lrde.epita.fr) in 2007, and all regular
contributors are now at LRDE. The web site was moved from
spot.lip6.fr to spot.lrde.epita.fr in 2015, so do not be surprised if
you find links to the old site.
Keeping in touch
================
......@@ -67,6 +57,16 @@ releases of Spot. You may subscribe to that list at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
History
=======
This project started in 2003 at LIP6 (www.lip6.fr). The main author
moved to LRDE (www.lrde.epita.fr) in 2007, and all regular
contributors are now at LRDE. The web site was moved from
spot.lip6.fr to spot.lrde.epita.fr in 2015, so do not be surprised if
you find links to the old site.
Installation
============
......@@ -81,9 +81,15 @@ Especially, Python's headers files should be installed. If you don't
have Python installed, and do NOT want to install it, you should run
configure with the --disable-python option (see below).
Optional third-party dependencies
----------------------------------
Several tools and functions output automata as "dot files", to be
rendered graphically by tools from the GraphViz package. Installing
GraphViz is therefore highly recommended if you plan to display
automata.
If the SAT-solver glucose is found on your system, it will be used by
our test suite to test our SAT-based minimization algorithm.
......@@ -104,6 +110,17 @@ Spot follows the traditional `./configure && make && make check &&
make install' process. People unfamiliar with the GNU Build System
should read the file INSTALL for generic instructions.
If you plan to use the Python binding, we recommend you use one
of the following --prefix options when calling configure:
--prefix /usr
--prefix /usr/local (the default)
--prefix ~/.local (if you do not have root permissions)
The reason is that all these locations are usually automatically
searched by Python. If you use a different prefix directory, you may
have to tune the PYTHONPATH environment variable.
In addition to its usual options, ./configure will accept some
flags specific to Spot:
......@@ -184,6 +201,76 @@ Here are the meaning of the fine-tuning options, in case
flags from a built-in list.
Troubleshooting installations
-----------------------------
Spot installs five types of files, in different locations. It the
following, $prefix refers to the directory that was selected using
the --prefix option of configure (the default is /usr/local/).
1) command-line tools go into $prefix/bin/
2) shared or static libraries (depending on configure options)
are installed into $prefix/lib/
3) Python bindings (if not disabled with --disable-python) typically
go into a directory like $prefix/lib/pythonX.Y/site-packages/
where X.Y is the version of Python found during configure.
4) man pages go into $prefix/man
5) header files go into $prefix/include
Depending on how you plan to use Spot, you may have to adjust some
variables such that all these files can be found by the other programs
that look for them.
To test if command-line tools are correctly installed, try running
% ltl2tgba --version
If your shell reports that ltl2tgba is not found, add $prefix/bin
to you $PATH environment variable.
If the dynamic linker reports that some library (usually libspot.so or
libbddx.so) is not found, you probably have to instruct it to look into
some new directory. If you installed Spot as root into a classical
system prefix such as /usr or /usr/local/ it may be the case that you
simply have to refresh the cache. In GNU/Linux this is done by
running "ldconfig -v". If you installed Spot into a non-standard
directory, you may have to add $prefix/lib some some environment
variable: that variable is called LD_LIBRARY_PATH in GNU/Linux, and
its DYLD_LIBRARY_PATH in Darwin.
To test the Python bindings, try running
% python3
>>> import spot
>>> print(spot.version())
If you installed Spot with a prefix that is not one of those suggested
in the "Building and installing" section, it is likely that the above
import statement will fail to locate the spot package. You can show
the list of directories that are searched by Python using:
% python3
>>> import sys
>>> print(sys.path)
And you can modify that list of searched directories using the
PYTHONPATH environment variable.
To test if man pages can be found, simply try:
% man spot
If man reports a message like "No manual entry for spot", add
$prefix/man to the MANPATH environment variable.
Finally header files are needed if you write some C++ that uses Spot.
In that case you may need to pass some -I option to the compiler to
add some "include" directory. At link time, you may also need to add
some -L option if the libraries are not in some location that is
already searched by the linker. The file doc/userdoc/compile.html (or
its on-line version at https://spot.lrde.epita.fr/compile.html)
discusses this topic a bit more.
Layout of the source tree
=========================
......@@ -197,14 +284,17 @@ spot/ Sources for libspot.
kripke/ Kripke Structure interface.
tl/ Temporal Logic formulas and algorithms.
misc/ Miscellaneous support files.
mc/ All algorithms useful for model checking
parseaut/ Parser for automata in multiple formats.
parsetl/ Parser for LTL/PSL formulas.
priv/ Private algorithms, used internally but not exported.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
twa/ TωA objects and cousins (Transition-based ω-Automata).
twacube/ TωA objects based on cube (not-bdd).
twacube_algos/ TωAcube algorithms
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check.
gtec/ Couvreur's Emptiness-Check (old version).
gen/ Sources for libspotgen.
bin/ Command-line tools built on top of libspot.
man/ Man pages for the above tools.
......@@ -238,6 +328,7 @@ lib/ Gnulib's portability modules.
utf8/ Nemanja Trifunovic's utf-8 routines.
elisp/ Related emacs modes, used for building the documentation.
picosat/ A distribution of PicoSAT 965 (a satsolver library).
spot/bricks/ A collection of useful C++ code provided by DiVinE 3.3.2
Build-system stuff
------------------
......
We are grateful to these people for their comments, help, or
suggestions.
We are grateful to these people for their comments, help, or suggestions.
Akim Demaille
Andreas Tollkötter
Andrew Wells
Anton Pirogov
Ayrat Khalimov
Cambridge Yang
Caroline Lemieux
Christian Dax
Christopher Ziegler
......@@ -16,13 +17,17 @@ Felix Klaedtke
Florian Perlié-Long
František Blahoudek
Gerard J. Holzmann
Hashim Ali
Heikki Tauriainen
Henrich Lauko
Jan Strejček
Jean-Michel Couvreur
Jean-Michel Ilié
Jens Kreber
Jeroen Meijer
Jiraphapa Jiravaraphan
Joachim Klein
Juan Tzintzun
Juraj Major
Kristin Y. Rozier
Martin Dieguez Lodeiro
......@@ -33,15 +38,21 @@ Michael Weber
Mikuláš Klokočka
Ming-Hsien Tsai
Nikos Gorogiannis
Paul Guénézan
Reuben Rowe
Rüdiger Ehlers
Silien Hong
Simon Jantsch
Shengping Shaw
Shufang Zhu
Sonali Dutta
Tereza Šťastná
Tobias Meggendorfer.
Tomáš Babiak
Valentin Iovene
Victor Khomenko
Vitus Lam
Yann Thierry-Mieg
Yannick Molinghen
Yong Li
Yuri Victorovich
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -45,12 +45,9 @@
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/product.hh>
#include <spot/misc/escape.hh>
#include <spot/misc/timer.hh>
......@@ -116,10 +113,12 @@ static const argp_option options[] =
"all available optimizations (slow, default)", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output options:", -15 },
{ "quiet", 'q', nullptr, 0,
"suppress all normal output in absence of errors", 0 },
{ "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
"save formulas for which problems were detected in FILENAME", -1 },
"save automata for which problems were detected in FILENAME", 0 },
{ "verbose", OPT_VERBOSE, nullptr, 0,
"print what is being done, for debugging", -1 },
"print what is being done, for debugging", 0 },
{ nullptr, 0, nullptr, 0,
"If an output FILENAME is prefixed with '>>', it is open "
"in append mode instead of being truncated.", -14 },
......@@ -138,6 +137,7 @@ const struct argp_child children[] =
};
static bool verbose = false;
static bool quiet = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;
static bool fail_on_timeout = false;
......@@ -153,11 +153,17 @@ static output_file* bogus_output = nullptr;
static int
parse_opt(int key, char* arg, struct argp_state*)
{
// Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT;
switch (key)
{
case 'F':
jobs.emplace_back(arg, true);
break;
case 'q':
quiet = true;
verbose = false;
break;
case OPT_BOGUS:
{
bogus_output = new output_file(arg);
......@@ -199,6 +205,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break;
case OPT_VERBOSE:
verbose = true;
quiet = false;
break;
case ARGP_KEY_ARG:
if (arg[0] == '-' && !arg[1])
......@@ -209,6 +216,7 @@ parse_opt(int key, char* arg, struct argp_state*)
default:
return ARGP_ERR_UNKNOWN;
}
END_EXCEPTION_PROTECT;
return 0;
}
......@@ -388,8 +396,12 @@ namespace
format(command, tools[tool_num].cmd);
std::string cmd = command.str();
std::cerr << "Running [" << l << tool_num << "]: "
<< cmd << std::endl;
auto disp_cmd = [&]() {
std::cerr << "Running [" << l << tool_num
<< "]: " << cmd << '\n';
};
if (!quiet)
disp_cmd();
spot::process_timer timer;
timer.start();
int es = exec_with_timeout(cmd.c_str());
......@@ -401,12 +413,15 @@ namespace
{
if (fail_on_timeout)
{
if (quiet)
disp_cmd();
global_error() << "error: timeout during execution of command\n";
end_error();
}
else
{
std::cerr << "warning: timeout during execution of command\n";
if (!quiet)
std::cerr << "warning: timeout during execution of command\n";
++timeout_count;
}
status_str = "timeout";
......@@ -415,6 +430,8 @@ namespace
}
else if (WIFSIGNALED(es))
{
if (quiet)
disp_cmd();
status_str = "signal";
problem = true;
es = WTERMSIG(es);
......@@ -428,6 +445,8 @@ namespace
status_str = "exit code";
if (!ignore_exec_fail)
{
if (quiet)
disp_cmd();
problem = true;
global_error() << "error: execution returned exit code "
<< es << ".\n";
......@@ -436,8 +455,9 @@ namespace
else
{
problem = false;
std::cerr << "warning: execution returned exit code "
<< es << ".\n";
if (!quiet)
std::cerr << "warning: execution returned exit code "
<< es << ".\n";
++ignored_exec_fail;
}
}
......@@ -452,6 +472,8 @@ namespace
opt_parse);
if (!aut->errors.empty())
{
if (quiet)
disp_cmd();
status_str = "parse error";
problem = true;
es = -1;
......@@ -463,6 +485,8 @@ namespace
}
else if (aut->aborted)
{
if (quiet)
disp_cmd();
status_str = "aborted";
problem = true;
es = -1;
......@@ -512,19 +536,18 @@ namespace
if (aut_i->num_sets() + aut_j->num_sets() >
spot::acc_cond::mark_t::max_accsets())
{
std::cerr << "info: building " << autname(i)
<< '*' << autname(j, true)
<< " requires more acceptance sets than supported\n";
if (!quiet)
std::cerr << "info: building " << autname(i)
<< '*' << autname(j, true)
<< " requires more acceptance sets than supported\n";
return false;
}
auto prod = spot::product(aut_i, aut_j);
if (verbose)
std::cerr << "info: check_empty "
<< autname(i) << '*' << autname(j, true) << '\n';
auto w = prod->accepting_word();
auto w = aut_i->intersecting_word(aut_j);
if (w)
{
std::ostream& err = global_error();
......@@ -579,14 +602,21 @@ namespace
input_statistics.push_back(in_statistics());
std::cerr << bold << source << reset_color;
input_statistics[round_num].input_source = std::move(source);
if (auto name = input->get_named_prop<std::string>("automaton-name"))
{
std::cerr << '\t' << *name;
input_statistics[round_num].input_name = *name;
}
std::cerr << '\n';
input_statistics[round_num].input_name = *name;
auto disp_src = [&]() {
std::cerr << bold
<< input_statistics[round_num].input_source
<< reset_color;
if (!input_statistics[round_num].input_name.empty())
std::cerr << '\t'
<< input_statistics[round_num].input_name;
std::cerr << '\n';
};
if (!quiet)
disp_src();
input_statistics[round_num].input.set(input);
int problems = 0;
......@@ -612,7 +642,6 @@ namespace
problems += prob;
}
spot::cleanup_tmpfiles();
++round_num;
output_statistics.push_back(std::move(stats));
if (verbose)
......@@ -628,15 +657,16 @@ namespace
if (!no_checks)
{
std::cerr << "Performing sanity checks and gathering statistics..."
<< std::endl;
if (!quiet)
std::cerr
<< "Performing sanity checks and gathering statistics...\n";
{
bool print_first = true;
for (unsigned i = 0; i < mi; ++i)
{
if (!pos[i])
continue;
cleanup_acceptance_here(pos[i]);
if (!pos[i]->is_existential())
{
if (verbose)
......@@ -659,8 +689,6 @@ namespace
std::cerr << '\n';
}
}
if (is_universal(pos[i]))
neg[i] = dualize(pos[i]);
}
}
......@@ -668,19 +696,14 @@ namespace
bool print_first = verbose;
for (unsigned i = 0; i < mi; ++i)
{
if (pos[i] && !neg[i])
if (pos[i])
{
if (print_first)
{
std::cerr << "info: complementing non-deterministic "
"automata via determinization...\n";
std::cerr << "info: complementing automata...\n";
print_first = false;
}
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(level);
neg[i] = dualize(p.run(pos[i]));
neg[i] = spot::complement(pos[i]);
if (verbose)
{
std::cerr << "info: "
......@@ -690,54 +713,11 @@ namespace
printsize(neg[i], false);
std::cerr << '\t' << autname(i, true) << '\n';
}
cleanup_acceptance_here(pos[i]);
}
};
}
{
bool print_first = true;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
bool neg)
{
if (!x[i])
return;
if (x[i]->acc().uses_fin_acceptance())
{
if (verbose)
{
if (print_first)
{
std::cerr <<
"info: getting rid of any Fin acceptance...\n";
print_first = false;
}
std::cerr << "info: "
<< std::setw(8) << autname(i, neg) << '\t';
printsize(x[i], false);
std::cerr << " ->";
}
cleanup_acceptance_here(x[i]);
x[i] = remove_fin(x[i]);
if (verbose)
{
std::cerr << ' ';
printsize(x[i], false);
std::cerr << '\n';
}
}
else
{
// Remove useless sets nonetheless.
cleanup_acceptance_here(x[i]);
}
};
for (unsigned i = 0; i < mi; ++i)
{
tmp(pos, i, false);
tmp(neg, i, true);
}
}
// Just make a circular implication check
// A0 <= A1, A1 <= A2, ..., AN <= A0
unsigned ok = 0;
......@@ -766,15 +746,23 @@ namespace
}
else
{
std::cerr << "Gathering statistics..." << std::endl;
if (!quiet)
std::cerr << "Gathering statistics...\n";
}
if (problems && bogus_output)
print_hoa(bogus_output->ostream(), input) << std::endl;
std::cerr << std::endl;
if (problems && quiet)
{
std::cerr << "input automaton was ";
disp_src();
}
if (!quiet || problems)
std::cerr << '\n';
++round_num;
// Shall we stop processing now?
abort_run = global_error_flag && stop_on_error;
return problems;
......@@ -851,7 +839,7 @@ main(int argc, char** argv)
{
error(2, 0, "no automaton to translate");
}
else
else if (!quiet)
{
if (global_error_flag)
{
......@@ -860,21 +848,20 @@ main(int argc, char** argv)
err << ("error: some error was detected during the above "
"runs.\n Check file ")
<< bogus_output_filename
<< " for problematic automata.";
<< " for problematic automata.\n";
else
err << ("error: some error was detected during the above "
"runs,\n please search for 'error:' messages"
" in the above trace.");
err << std::endl;
" in the above trace.\n");
end_error();
}
else if (timeout_count == 0 && ignored_exec_fail == 0)
{
std::cerr << "No problem detected." << std::endl;
std::cerr << "No problem detected.\n";
}
else
{
std::cerr << "No major problem detected." << std::endl;
std::cerr << "No major problem detected.\n";
}
unsigned additional_errors = 0U;
......@@ -905,7 +892,7 @@ main(int argc, char** argv)
}
if (additional_errors == 1)
std::cerr << '.';
std::cerr << std::endl;
std::cerr << '\n';
}
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -49,6 +49,7 @@
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/dtwasat.hh>
......@@ -110,6 +111,7 @@ enum {
OPT_HIGHLIGHT_NONDET_EDGES,
OPT_HIGHLIGHT_NONDET_STATES,
OPT_HIGHLIGHT_WORD,
OPT_HIGHLIGHT_ACCEPTING_RUN,
OPT_HIGHLIGHT_LANGUAGES,
OPT_INSTUT,
OPT_INCLUDED_IN,
......@@ -131,6 +133,7 @@ enum {
OPT_MASK_ACC,
OPT_MERGE,
OPT_NONDET_STATES,
OPT_PARTIAL_DEGEN,
OPT_PRODUCT_AND,
OPT_PRODUCT_OR,
OPT_RANDOMIZE,
......@@ -264,6 +267,9 @@ static const argp_option options[] =
"keep automata that accept WORD", 0 },
{ "reject-word", OPT_REJECT_WORD, "WORD", 0,
"keep automata that reject WORD", 0 },
{ "nth", 'N', "RANGE", 0,
"assuming input automata are numbered from 1, keep only those in RANGE",
0 },
/**************************************************/
RANGE_DOC_FULL,
WORD_DOC,
......@@ -317,7 +323,7 @@ static const argp_option options[] =
{ "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
"remove unused acceptance sets from the automaton", 0 },