...
 
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
This diff is collapsed.
// -*- 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 },
{ "complement", OPT_COMPLEMENT, nullptr, 0,
"complement each automaton (currently via determinization)", 0 },
"complement each automaton (different strategies are used)", 0 },
{ "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
"complement the acceptance condition (without touching the automaton)",
0 },
......@@ -361,6 +367,10 @@ static const argp_option options[] =
{ "sum-and", OPT_SUM_AND, "FILENAME", 0,
"build the sum with the automaton in FILENAME "
"to intersect languages", 0 },
{ "partial-degeneralize", OPT_PARTIAL_DEGEN, "NUM1,NUM2,...",
OPTION_ARG_OPTIONAL, "Degeneralize automata according to sets "
"NUM1,NUM2,... If no sets are given, partial degeneralization "
"is performed for all conjunctions of Inf and disjunctions of Fin.", 0 },
{ "separate-sets", OPT_SEP_SETS, nullptr, 0,
"if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
"Fin(x) by a new Fin(y) and adjust the automaton", 0 },
......@@ -373,6 +383,8 @@ static const argp_option options[] =
"(see spot-x)."
, 0 },
{ nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
{ "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM",
OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0},
{ "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
0 },
......@@ -415,8 +427,31 @@ static const struct argp_child children[] =
};
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
typedef std::set<std::vector<tr_t>> unique_aut_t;
struct canon_aut
{
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
unsigned num_states;
std::vector<tr_t> edges;
std::string acc;
canon_aut(const spot::const_twa_graph_ptr& aut)
: num_states(aut->num_states())
, edges(aut->edge_vector().begin() + 1,
aut->edge_vector().end())
{
std::ostringstream os;
aut->get_acceptance().to_text(os);
acc = os.str();
}
bool operator<(const canon_aut& o) const
{
return std::tie(num_states, edges, acc)
< std::tie(o.num_states, o.edges, o.acc);
};
};
typedef std::set<canon_aut> unique_aut_t;
static long int match_count = 0;
static spot::option_map extra_options;
static bool randomize_st = false;
......@@ -603,6 +638,7 @@ static bool opt_terminal_sccs_set = false;
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
static int opt_max_count = -1;
static range opt_nth = { 0, std::numeric_limits<int>::max() };
static bool opt_destut = false;
static char opt_instut = 0;
static bool opt_is_empty = false;
......@@ -615,6 +651,8 @@ static bool opt_complement = false;
static bool opt_complement_acc = false;
static char* opt_decompose_scc = nullptr;
static bool opt_dualize = false;
static bool opt_partial_degen_set = false;
static spot::acc_cond::mark_t opt_partial_degen = {};
static spot::acc_cond::mark_t opt_mask_acc = {};
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
......@@ -628,6 +666,7 @@ static bool opt_split_edges = false;
static const char* opt_sat_minimize = nullptr;
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
static int opt_highlight_accepting_run = -1;
static bool opt_highlight_languages = false;
static bool opt_dca = false;
static bool opt_streett_like = false;
......@@ -683,6 +722,8 @@ product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
static int
parse_opt(int key, char* arg, struct argp_state*)
{
// Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT;
// This switch is alphabetically-ordered.
switch (key)
{
......@@ -695,9 +736,11 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'n':
opt_max_count = to_pos_int(arg, "-n/--max-count");
break;
case 'N':
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case 'u':
opt->uniq =
std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
break;
case 'v':
opt_invert = true;
......@@ -764,7 +807,7 @@ parse_opt(int key, char* arg, struct argp_state*)
{
std::cerr << ", '" << acc_is_args[i] << '\'';
}
std::cerr << std::endl;
std::cerr << '\n';
exit(2);
}
}
......@@ -844,6 +887,10 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_HAS_UNIV_BRANCHING:
opt_has_univ_branching = true;
break;
case OPT_HIGHLIGHT_ACCEPTING_RUN:
opt_highlight_accepting_run =
arg ? to_pos_int(arg, "--highlight-accepting-run") : 1;
break;
case OPT_HIGHLIGHT_NONDET:
{
int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1;
......@@ -994,6 +1041,23 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
opt_nondet_states_set = true;
break;
case OPT_PARTIAL_DEGEN:
{
opt_partial_degen_set = true;
if (arg)
for (auto res : to_longs(arg))
{
if (res < 0)
error(2, 0, "acceptance sets should be non-negative:"
" --partial-degeneralize=%ld", res);
if (static_cast<unsigned long>(res) >=
spot::acc_cond::mark_t::max_accsets())
error(2, 0, "this implementation does not support that many"
" acceptance sets: --partial-degeneralize=%ld", res);
opt_partial_degen.set(res);
}
break;
}
case OPT_PRODUCT_AND:
{
auto a = read_automaton(arg, opt->dict);
......@@ -1145,6 +1209,7 @@ parse_opt(int key, char* arg, struct argp_state*)
default:
return ARGP_ERR_UNKNOWN;
}
END_EXCEPTION_PROTECT;
return 0;
}
......@@ -1274,6 +1339,9 @@ namespace
int
process_automaton(const spot::const_parsed_aut_ptr& haut) override
{
static unsigned order = 0;
++order;
spot::process_timer timer;
timer.start();
......@@ -1314,6 +1382,7 @@ namespace
bool matched = true;
matched &= opt_nth.contains(order);
matched &= opt_states.contains(aut->num_states());
matched &= opt_edges.contains(aut->num_edges());
matched &= opt_accsets.contains(aut->acc().num_sets());
......@@ -1466,6 +1535,19 @@ namespace
else if (opt_rem_unreach)
aut->purge_unreachable_states();
if (opt_partial_degen_set)
{
if (opt_partial_degen)
{
auto sets = opt_partial_degen & aut->acc().all_sets();
aut = spot::partial_degeneralize(aut, sets);
}
else
{
aut = spot::partial_degeneralize(aut);
}
}
if (opt->product_and)
aut = ::product(std::move(aut), opt->product_and);
if (opt->product_or)
......@@ -1492,7 +1574,7 @@ namespace
if (opt_complement)
{
aut = spot::dualize(ensure_deterministic(aut));
aut = spot::complement(aut);
aut->merge_edges();
}
......@@ -1528,6 +1610,9 @@ namespace
if (opt_highlight_languages)
spot::highlight_languages(aut);
if (opt_highlight_accepting_run >= 0)
aut->accepting_run()->highlight(opt_highlight_accepting_run);
if (!opt->hl_words.empty())
for (auto& word_aut: opt->hl_words)
{
......@@ -1544,8 +1629,7 @@ namespace
auto tmp =
spot::canonicalize(make_twa_graph(aut,
spot::twa::prop_set::all()));
if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
tmp->edge_vector().end()).second)
if (!opt->uniq->emplace(tmp).second)
return 0;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -24,6 +24,7 @@
#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_cout.hh"
#include "common_setup.hh"
#include <unistd.h>
#include <ctime>
......@@ -48,16 +49,22 @@ enum check_type
{
check_unambiguous = (1 << 0),
check_stutter = (1 << 1),
check_strength = (1 << 2),
check_semi_determinism = (1 << 3),
check_stutter_example = check_stutter | (1 << 2),
check_strength = (1 << 3),
check_semi_determinism = (1 << 4),
check_all = -1U,
};
static char const *const check_args[] =
{
"unambiguous",
/* Before we added --check=stutter-sensitive-example,
--check=stutter used to unambiguously refer to
stutter-invariant. */
"stutter",
"stutter-invariant", "stuttering-invariant",
"stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive",
"stutter-sensitive-example", "stuttering-sensitive-example",
"strength", "weak", "terminal",
"semi-determinism", "semi-deterministic",
"all",
......@@ -66,9 +73,11 @@ static char const *const check_args[] =
static check_type const check_types[] =
{
check_unambiguous,
check_stutter,
check_stutter, check_stutter,
check_stutter, check_stutter,
check_stutter, check_stutter,
check_stutter_example, check_stutter_example,
check_strength, check_strength, check_strength,
check_semi_determinism, check_semi_determinism,
check_all
......@@ -88,7 +97,7 @@ static const argp_option options[] =
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output format:", 3 },
{ "dot", 'd',
"1|a|A|b|B|c|C(COLOR)|e|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
"1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
OPTION_ARG_OPTIONAL,
"GraphViz's format. Add letters for "
"(1) force numbered states, "
......@@ -100,7 +109,9 @@ static const argp_option options[] =
"(C) color nodes with COLOR, "
"(d) show origins when known, "
"(e) force elliptic nodes, "
"(E) force rEctangular nodes, "
"(f(FONT)) use FONT, "
"(g) hide edge labels, "
"(h) horizontal layout, "
"(k) use state labels when possible, "
"(K) use transition labels (default), "
......@@ -147,8 +158,9 @@ static const argp_option options[] =
{ "format", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL,
"test for the additional property PROP and output the result "
"in the HOA format (implies -H). PROP may be any prefix of "
"'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
"in the HOA format (implies -H). PROP may be some prefix of "
"'all' (default), 'unambiguous', 'stutter-invariant', "
"'stutter-sensitive-example', 'semi-determinism', or 'strength'.",
0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
......@@ -303,6 +315,8 @@ const struct argp aoutput_o_format_argp = { o_options,
int parse_opt_aoutput(int key, char* arg, struct argp_state*)
{
// Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT;
// This switch is alphabetically-ordered.
switch (key)
{
......@@ -357,6 +371,7 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
default:
return ARGP_ERR_UNKNOWN;
}
END_EXCEPTION_PROTECT;
return 0;
}
......@@ -580,7 +595,9 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
if (opt_check)
{
if (opt_check & check_stutter)
spot::check_stutter_invariance(aut, f);
spot::check_stutter_invariance(aut, f, false,
(opt_check & check_stutter_example)
== check_stutter_example);
if (opt_check & check_unambiguous)
spot::check_unambiguous(aut);
if (opt_check & check_strength)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -19,6 +19,7 @@
#include "common_sys.hh"
#include "common_color.hh"
#include "common_setup.hh"
#include <argp.h>
#include <unistd.h>
......@@ -77,6 +78,8 @@ static const argp_option options_color[] =
static int
parse_opt_color(int key, char* arg, struct argp_state*)
{
// Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT;
// This switch is alphabetically-ordered.
switch (key)
{
......@@ -91,6 +94,7 @@ parse_opt_color(int key, char* arg, struct argp_state*)
default:
return ARGP_ERR_UNKNOWN;
}
END_EXCEPTION_PROTECT;
return 0;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2017 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2012-2017, 2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -37,16 +37,16 @@ static bool lenient = false;
static const argp_option options[] =
{
{ nullptr, 0, nullptr, 0, "Input options:", 1 },
{ "formula", 'f', "STRING", 0, "process the formula STRING", 1 },
{ "formula", 'f', "STRING", 0, "process the formula STRING", 0 },
{ "file", 'F', "FILENAME[/COL]", 0,
"process each line of FILENAME as a formula; if COL is a "
"positive integer, assume a CSV file and read column COL; use "
"a negative COL to drop the first line of the CSV file", 1 },
"a negative COL to drop the first line of the CSV file", 0 },
{ "lbt-input", OPT_LBT, nullptr, 0,
"read all formulas using LBT's prefix syntax", 1 },
"read all formulas using LBT's prefix syntax", 0 },
{ "lenient", OPT_LENIENT, nullptr, 0,
"parenthesized blocks that cannot be parsed as subformulas "
"are considered as atomic properties", 1 },
"are considered as atomic properties", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
......@@ -62,6 +62,8 @@ const struct argp finput_argp_headless = { options + 1, parse_opt_finput,
int
parse_opt_finput(int key, char* arg, struct argp_state*)
{
// Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT;
// This switch is alphabetically-ordered.
switch (key)
{
......@@ -80,6 +82,7 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
default:
return ARGP_ERR_UNKNOWN;
}
END_EXCEPTION_PROTECT;
return 0;
}
......@@ -154,6 +157,11 @@ job_processor::process_stream(std::istream& is,
}
else // We are reading column COL_TO_READ in a CSV file.
{
// Some people save CSV files with MSDOS encoding, and
// we don't want to include the \r in any %> output.
if (*line.rbegin() == '\r')
line.pop_back();
// If the line we have read contains an odd number
// of double-quotes, then it is an incomplete CSV line
// that should be completed by the next lines.
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2015, 2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -18,6 +18,7 @@