Commit 1fa048fe authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: diagnose complementations requiring too many colors

Fixes #411 reported by Frantiček Blahoudek.

* bin/ltlcross.cc: Catch the issue.
* tests/core/ltlcross6.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
parent f2403c91
Pipeline #20421 passed with stage
in 186 minutes and 55 seconds
......@@ -66,6 +66,11 @@ New in spot 2.9.0.dev (not yet released)
issues in intersecting_run(), exclusive_run(),
intersecting_word(), exclusive_word(), which all call reduce().
- ltlcross used to crash with "Too many acceptance sets used. The
limit is 32." when complementing an automaton would require more
acceptance sets than supported by Spot. This is now diagnosed
with --verbose, but does not prevent ltlcross from continuing.
New in spot 2.9 (2020-04-30)
Command-line tools:
......
......@@ -1336,25 +1336,37 @@ namespace
&& !spot::is_universal(from[i]))
missing_complement = true;
else
to[i] = spot::complement(from[i], aborter);
if (verbose)
{
if (to[i])
{
std::cerr << "\t(";
printsize(from[i]);
std::cerr << ") -> (";
printsize(to[i]);
std::cerr << ")\tComp(" << prefix << i << ")\n";
}
else
{
std::cerr << "\tnot complemented";
if (aborter)
aborter->print_reason(std::cerr << " (") << ')';
std::cerr << '\n';
}
}
try
{
to[i] = spot::complement(from[i], aborter);
if (verbose)
{
if (to[i])
{
std::cerr << "\t(";
printsize(from[i]);
std::cerr << ") -> (";
printsize(to[i]);
std::cerr << ")\tComp(" << prefix
<< i << ")\n";
}
else
{
std::cerr << "\tnot complemented";
if (aborter)
aborter->print_reason(std::cerr
<< " (") << ')';
std::cerr << '\n';
}
}
}
catch (const std::runtime_error& re)
{
missing_complement = true;
if (verbose)
std::cerr << "\tnot complemented ("
<< re.what() << ")\n";
}
}
};
missing_complement = false;
......
......@@ -310,6 +310,7 @@ TESTS_twa = \
core/ltlcross.test \
core/spotlbtt2.test \
core/ltlcross2.test \
core/ltlcross6.test \
core/autcross.test \
core/autcross2.test \
core/autcross3.test \
......
This diff is collapsed.
Supports Markdown
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