...
 
Commits (318)
......@@ -119,7 +119,7 @@ arch-gcc-glibcxxdebug:
- 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:
......@@ -289,6 +289,8 @@ raspbian:
stage: build
only:
- branches
except:
- /wip/
tags:
- armv7
script:
......
......@@ -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
......@@ -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.
......@@ -284,12 +284,15 @@ 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 (old version).
gen/ Sources for libspotgen.
......@@ -325,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
------------------
......
......@@ -23,6 +23,7 @@ Henrich Lauko
Jan Strejček
Jean-Michel Couvreur
Jean-Michel Ilié
Jens Kreber
Jeroen Meijer
Jiraphapa Jiravaraphan
Joachim Klein
......@@ -42,6 +43,7 @@ Reuben Rowe
Rüdiger Ehlers
Silien Hong
Simon Jantsch
Shengping Shaw
Shufang Zhu
Sonali Dutta
Tereza Šťastná
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018, 2019 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.
......@@ -116,7 +116,7 @@ static const argp_option options[] =
{ "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", 0 },
"save automata for which problems were detected in FILENAME", 0 },
{ "verbose", OPT_VERBOSE, nullptr, 0,
"print what is being done, for debugging", 0 },
{ nullptr, 0, nullptr, 0,
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2019 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.
......@@ -133,6 +133,7 @@ enum {
OPT_MASK_ACC,
OPT_MERGE,
OPT_NONDET_STATES,
OPT_PARTIAL_DEGEN,
OPT_PRODUCT_AND,
OPT_PRODUCT_OR,
OPT_RANDOMIZE,
......@@ -266,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,
......@@ -363,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 },
......@@ -419,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;
......@@ -607,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;
......@@ -619,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;
......@@ -702,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;
......@@ -1005,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);
......@@ -1286,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();
......@@ -1326,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());
......@@ -1478,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)
......@@ -1559,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-2019 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.
......@@ -49,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",
......@@ -67,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
......@@ -89,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, "
......@@ -101,6 +109,7 @@ 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, "
......@@ -149,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 }
};
......@@ -585,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)
......
......@@ -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 }
};
......
......@@ -30,8 +30,8 @@ enum
static const argp_option options[] =
{
{ "trust-hoa", OPT_TRUST_HOA, "BOOL", 0,
"If False, properties listed in HOA files are ignored, "
"unless they can be easily verified. If True (the default) "
"If false, properties listed in HOA files are ignored, "
"unless they can be easily verified. If true (the default) "
"any supported property is trusted.", 1 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 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.
......@@ -35,7 +35,7 @@ display_version(FILE *stream, struct argp_state*)
fputs(program_name, stream);
fputs(" (" PACKAGE_NAME ") " PACKAGE_VERSION "\n\
\n\
Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita.\n\
Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita.\n\
License GPLv3+: \
GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>.\n\
This is free software: you are free to change and redistribute it.\n\
......
......@@ -70,7 +70,7 @@ static const argp_option options[] =
const struct argp_child children[] =
{
{ &finput_argp, 0, nullptr, 1 },
{ &finput_argp, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 },
{ &aoutput_o_format_argp, 0, nullptr, 0 },
{ &post_argp, 0, nullptr, 0 },
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 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.
......@@ -98,6 +98,7 @@ enum {
OPT_OMIT,
OPT_PRODUCTS,
OPT_REFERENCE,
OPT_SAVE_INCLUSION_PRODUCTS,
OPT_SEED,
OPT_STATES,
OPT_STOP_ERR,
......@@ -180,6 +181,9 @@ static const argp_option options[] =
"suppress all normal output in absence of error", 0 },
{ "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
"save formulas for which problems were detected in FILENAME", 0 },
{ "save-inclusion-products", OPT_SAVE_INCLUSION_PRODUCTS, "[>>]FILENAME",
0, "save automata representing products built to check inclusion "
"between automata", 0 },
{ "verbose", OPT_VERBOSE, nullptr, 0,
"print what is being done, for debugging", 0 },
{ nullptr, 0, nullptr, 0,
......@@ -220,7 +224,10 @@ static bool products_avg = true;
static bool opt_omit = false;
static const char* bogus_output_filename = nullptr;
static output_file* bogus_output = nullptr;
static const char* grind_output_filename = nullptr;
static output_file* grind_output = nullptr;
static const char* saved_inclusion_products_filename = nullptr;
static output_file* saved_inclusion_products = nullptr;
static bool verbose = false;
static bool quiet = false;
static bool ignore_exec_fail = false;
......@@ -507,6 +514,7 @@ parse_opt(int key, char* arg, struct argp_state*)
fail_on_timeout = true;
break;
case OPT_GRIND:
grind_output_filename = arg;
grind_output = new output_file(arg);
break;
case OPT_IGNORE_EXEC_FAIL:
......@@ -539,6 +547,12 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_REFERENCE:
tools_push_trans(arg, true);
break;
case OPT_SAVE_INCLUSION_PRODUCTS:
{
saved_inclusion_products = new output_file(arg);
saved_inclusion_products_filename = arg;
break;
}
case OPT_SEED:
seed = to_pos_int(arg, "--seed");
break;
......@@ -582,10 +596,14 @@ namespace
format(command, tools[translator_num].cmd);
std::string cmd = command.str();
auto disp_cmd = [&]() {
std::cerr << "Running [" << l << translator_num
<< "]: " << cmd << '\n';
};
auto disp_cmd =
[&]() {
std::cerr << "Running [" << l << translator_num;
const char* name = tools[translator_num].name;
if (name != tools[translator_num].spec)
std::cerr << ": " << name;
std::cerr << "]: " << cmd << '\n';
};
if (!quiet)
disp_cmd();
spot::process_timer timer;
......@@ -754,7 +772,8 @@ namespace
static bool
check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
const spot::const_twa_graph_ptr& aut_j,
size_t i, size_t j, bool icomp, bool jcomp)
size_t i, size_t j, bool icomp, bool jcomp,
const std::string& formula)
{
if (aut_i->num_sets() + aut_j->num_sets() >
spot::acc_cond::mark_t::max_accsets())
......@@ -781,6 +800,22 @@ namespace
auto prod = spot::product(aut_i, aut_j);
if (saved_inclusion_products)
{
std::ostringstream os;
if (icomp)
os << "Comp(N" << i << ')';
else
os << 'P' << i;
if (jcomp)
os << "*Comp(P" << j << ')';
else
os << "*N" << j;
os << ", " << formula;
prod->set_named_prop("automaton-name", new std::string(os.str()));
spot::print_hoa(saved_inclusion_products->ostream(), prod) << std::endl;
}
if (verbose)
{
std::cerr << "info: check_empty ";
......@@ -1243,6 +1278,33 @@ namespace
unalt(neg, i, 'N');
}
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char* prefix, const char* suffix)
{
if (!x[i])
return;
unsigned before = x[i]->num_sets();
cleanup_acceptance_here(x[i]);
unsigned after = x[i]->num_sets();
if (verbose && before != after)
{
if (print_first)
{
std::cerr << "info: removing unused sets...\n";
print_first = false;
}
std::cerr << "info: " << prefix << i
<< suffix << '\t' << before << " sets -> "
<< after << " sets\n";
}
};
for (size_t i = 0; i < m; ++i)
{
tmp(pos, i, " P", " ");
tmp(neg, i, " N", " ");
}
// Complement
if (!no_complement)
{
......@@ -1303,67 +1365,11 @@ namespace
}
}
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char* prefix, const char* suffix)
{
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:\t" << prefix << i
<< suffix << "\t(";
printsize(x[i]);
std::cerr << ") ->";
}
try
{
x[i] = remove_fin(x[i]);
}
catch (const std::runtime_error& err)
{
if (verbose)
std::cerr << " failed (" << err.what() << ")\n";
else
std::cerr << "info: preprocessing "
<< prefix << i << suffix
<< " failed (" << err.what() << ")\n";
x[i] = nullptr;
}
if (verbose && x[i])
{
std::cerr << " (";
printsize(x[i]);
std::cerr << ")\n";
}
}
else
{
// Remove useless sets nonetheless.
cleanup_acceptance_here(x[i]);
}
};
for (size_t i = 0; i < m; ++i)
{
tmp(pos, i, " P", " ");
tmp(neg, i, " N", " ");
tmp(comp_pos, i, "Comp(P", ")");
tmp(comp_neg, i, "Comp(N", ")");
}
if (smallest_pos_ref >= 0)
{
// Recompute the smallest references now, because removing
// alternation and Fin acceptance might have changed the
// sizes.
// Recompute the smallest references now, because
// removing alternation and useless acceptance sets
// might have changed the sizes.
smallest_pos_ref = smallest_ref(pos);
smallest_neg_ref = smallest_ref(neg);
......@@ -1392,7 +1398,8 @@ namespace
smallest_pos_ref >= 0 &&
(size_t)smallest_pos_ref != i)))
problems +=
check_empty_prod(pos[i], neg[j], i, j, false, false);
check_empty_prod(pos[i], neg[j], i, j, false, false,
fstr);
// Deal with the extra complemented automata if we
// have some.
......@@ -1413,17 +1420,17 @@ namespace
if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref)
problems +=
check_empty_prod(pos[i], comp_pos[j],
i, j, false, true);
i, j, false, true, fstr);
if (i != j && comp_neg[i] && !comp_pos[i])
if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref)
problems +=
check_empty_prod(comp_neg[i], neg[j],
i, j, true, false);
i, j, true, false, fstr);
if (comp_pos[i] && comp_neg[j] &&
(i == j || (!comp_neg[i] && !comp_pos[j])))
problems +=
check_empty_prod(comp_neg[j], comp_pos[i],
j, i, true, true);
j, i, true, true, fstr);
}
}
else
......@@ -1800,8 +1807,21 @@ main(int argc, char** argv)
}
}
delete bogus_output;
delete grind_output;
if (bogus_output)
{
bogus_output->close(bogus_output_filename);
delete bogus_output;
}
if (grind_output)
{
grind_output->close(grind_output_filename);
delete grind_output;
}
if (saved_inclusion_products)
{
saved_inclusion_products->close(saved_inclusion_products_filename);
delete saved_inclusion_products;
}
if (json_output)
print_stats_json(json_output);
......
......@@ -153,7 +153,7 @@ ARGMATCH_VERIFY(errors_args, errors_types);
const struct argp_child children[] =
{
{ &hoaread_argp, 0, "Parsing of automata:", 3 },
{ &finput_argp, 0, nullptr, 1 },
{ &finput_argp, 0, nullptr, 0 },
{ &trans_argp, 0, nullptr, 3 },
{ &aoutput_argp, 0, nullptr, 6 },
{ build_percent_list(), 0, nullptr, 7 },
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 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.
......@@ -223,6 +223,9 @@ static const argp_option options[] =
{ "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "ap", OPT_AP_N, "RANGE", 0,
"match formulas with a number of atomic propositions in RANGE", 0 },
{ "nth", 'N', "RANGE", 0,
"assuming input formulas are numbered from 1, keep only those in RANGE",
0 },
{ "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
{ "unique", 'u', nullptr, 0,
"drop formulas that have already been output (not affected by -v)", 0 },
......@@ -309,6 +312,7 @@ static spot::relabeling_style style = spot::Abc;
static bool remove_x = false;
static bool stutter_insensitive = false;
static range ap_n = { -1, -1 };
static range opt_nth = { 0, std::numeric_limits<int>::max() };
static int opt_max_count = -1;
static long int match_count = 0;
static const char* from_ltlf = nullptr;
......@@ -356,6 +360,9 @@ 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 'q':
output_format = quiet_output;
break;
......@@ -605,6 +612,8 @@ namespace
process_formula(spot::formula f,
const char* filename = nullptr, int linenum = 0) override
{
static unsigned order = 0;
++order;
spot::process_timer timer;
timer.start();
......@@ -618,7 +627,7 @@ namespace
if (negate)
f = spot::formula::Not(f);
bool matched = true;
bool matched = opt_nth.contains(order);
if (from_ltlf)
{
......
This diff is collapsed.
......@@ -230,6 +230,9 @@ sl(a) x sl(!a), performed on-the-fly
cl(a) x cl(!a)
.RE
.RE
This variable is used by the \fB--check=stutter-invariance\fR and
\fB--stutter-invariant\fR options, but it is ignored by
\fB--check=stutter-sensitive-example\fR.
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2019 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.
......@@ -117,6 +117,15 @@ the determinization algorithm.") },
the determinization algorithm.") },
{ DOC("det-stutter", "Set to 0 to disable optimizations based on \
the stutter-invariance in the determinization algorithm.") },
{ DOC("gen-reduce-parity", "When the postprocessor routines are \
configured to output automata with any kind of acceptance condition, \
but they happen to process an automaton with parity acceptance, they \
call a function to minimize the number of colors needed. This option \
controls what happen when this reduction does not reduce the number of \
colors: when set (the default) the output of the reduction is returned, \
this means the colors in the automaton may have changed slightly, and in \
particular, there is no transition with more than one color; when unset, \
the original automaton is returned.") },
{ DOC("gf-guarantee", "Set to 0 to disable alternate constructions \
for GF(guarantee)->[D]BA and FG(safety)->DCA. Those constructions \
are from an LICS'18 paper by J. Esparza, J. Křentínský, and S. Sickert. \
......
......@@ -42,6 +42,15 @@
#include "kernel.h"
#include "cache.h"
#ifdef __has_attribute
# if __has_attribute(fallthrough)
# define BUDDY_FALLTHROUGH __attribute__ ((fallthrough))
# endif
#endif
#ifndef BUDDY_FALLTHROUGH
# define BUDDY_FALLTHROUGH while (0);
#endif
/* Hash value modifiers to distinguish between entries in misccache */
#define CACHEID_CONSTRAIN 0x0
#define CACHEID_RESTRICT 0x1
......@@ -640,7 +649,7 @@ static BDD apply_rec(BDD l, BDD r)
r = tmp; \
op = bddop_imp; \
} \
/* fall through */ \
BUDDY_FALLTHROUGH; \
case bddop_imp: \
if (ISONE(r) || ISZERO(l)) \
return 1; \
......@@ -666,7 +675,7 @@ static BDD apply_rec(BDD l, BDD r)
r = tmp; \
op = bddop_diff; \
} \
/* fall through */ \
BUDDY_FALLTHROUGH; \
case bddop_diff: /* l - r = l &! r */ \
if (l == r || ISONE(r)) \
return 0; \
......
# -*- coding: utf-8 -*-
# Copyright (C) 2008-2019, Laboratoire de Recherche et Développement
# Copyright (C) 2008-2020, Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
......@@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.63])
AC_INIT([spot], [2.8.2.dev], [spot@lrde.epita.fr])
AC_INIT([spot], [2.9.0.dev], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
......@@ -142,6 +142,7 @@ fi
AX_CHECK_BUDDY
AC_CHECK_HEADERS([sys/times.h valgrind/memcheck.h spawn.h])
AX_CHECK_DIVINE
AC_CHECK_FUNCS([times kill alarm sigaction])
LT_CONFIG_LTDL_DIR([ltdl])
......@@ -234,6 +235,7 @@ AC_CONFIG_FILES([
spot/ltsmin/Makefile
spot/Makefile
spot/misc/Makefile
spot/mc/Makefile
spot/parseaut/Makefile
spot/parsetl/Makefile
spot/priv/Makefile
......@@ -242,8 +244,10 @@ AC_CONFIG_FILES([
spot/tl/Makefile
spot/twaalgos/gtec/Makefile
spot/twaalgos/Makefile
spot/twacube_algos/Makefile
spot/twa/Makefile
spot/gen/Makefile
spot/twacube/Makefile
python/Makefile
tests/core/defs
tests/ltsmin/defs:tests/core/defs.in
......
......@@ -4,7 +4,7 @@ Source: http://spot.lrde.epita.fr/dload/spot/
Files: *
Copyright: 2003-2007 Laboratoire d'Informatique de Paris 6 (LIP6)
2007-2019 Laboratoire de Recherche et Développement de l'Epita (LRDE)
2007-2020 Laboratoire de Recherche et Développement de l'Epita (LRDE)
License: GPL-3+
Spot is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by
......@@ -49,6 +49,33 @@ License: BSD-2-Clause
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
Files: spot/bricks/*
Copyright: 2010-2014 Petr Ročkai, Jiří Weiser, Vladimír Štill
License: BSD-2-Clause
Permission is hereby granted, without written agreement and without
license or royalty fees, to use, reproduce, prepare derivative
works, distribute, and display this software and its documentation
for any purpose, provided that (1) the above copyright notice and
the following two paragraphs appear in all copies of the source code
and (2) redistributions, including without limitation binaries,
reproduce these notices in the supporting documentation. Substantial
modifications to this software may be copyrighted by their authors
and need not follow the licensing terms described here, provided
that the new terms are clearly indicated in all files where they apply.
.
IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
.
JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
Files: utf8/*
Copyright: 2006 Nemanja Trifunovic
License: BSL-1.0
......@@ -183,3 +210,24 @@ License: MIT style
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.
Files: spot/priv/robin_hood.hh
Copyright: 2018-2019 Martin Ankerl
License: MIT
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
.
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
usr/include/spot
usr/include/spot/bricks
usr/lib/*-*/libspot.so
usr/lib/*-*/libspot.a
usr/lib/*-*/pkgconfig/libspot.pc
......
......@@ -27,12 +27,12 @@ LTOPLUG := $(shell gcc -v 2>&1 | \
# ARFLAGS is for Automake
# AR_FLAGS is for Libtool