Commit 020c9811 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: detect remove_fin failures

Fixes #314, reported by František Blahoudek.

* bin/ltlcross.cc: Here.
* tests/core/ltlcross3.test: Add new test case.
* NEWS: Mention the bug.
parent a924bc56
...@@ -266,6 +266,9 @@ New in spot 2.4.4.dev (net yet released) ...@@ -266,6 +266,9 @@ New in spot 2.4.4.dev (net yet released)
set. In spot 2.4.x this function was only used by autfilt set. In spot 2.4.x this function was only used by autfilt
--simplify-acceptance; in 2.5 it is now used in remove_fin(). --simplify-acceptance; in 2.5 it is now used in remove_fin().
- ltlcross could crash when calling remove_fin() on an automaton
with 32 acceptance sets would need an additional set.
New in spot 2.4.4 (2017-12-25) New in spot 2.4.4 (2017-12-25)
Bugs fixed: Bugs fixed:
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// Développement de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -1240,9 +1240,21 @@ namespace ...@@ -1240,9 +1240,21 @@ namespace
printsize(x[i]); printsize(x[i]);
std::cerr << ") ->"; std::cerr << ") ->";
} }
cleanup_acceptance_here(x[i]); try
x[i] = remove_fin(x[i]); {
if (verbose) 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 << " ("; std::cerr << " (";
printsize(x[i]); printsize(x[i]);
...@@ -1371,52 +1383,19 @@ namespace ...@@ -1371,52 +1383,19 @@ namespace
std::vector<spot::scc_info*> pos_map(m); std::vector<spot::scc_info*> pos_map(m);
std::vector<spot::scc_info*> neg_map(m); std::vector<spot::scc_info*> neg_map(m);
for (size_t i = 0; i < m; ++i) for (size_t i = 0; i < m; ++i)
if (pos[i]) {
{ spot::scc_info* sm = nullptr;
if (verbose) if (pos[i])
std::cerr << ("info: building product between state-space and"
" P") << i
<< " (" << pos[i]->num_states() << " st., "
<< pos[i]->num_edges() << " ed.)\n";
spot::scc_info* sm = nullptr;
try
{
auto p = spot::product(pos[i], statespace);
if (verbose)
std::cerr << "info: product has " << p->num_states()
<< " st., " << p->num_edges()
<< " ed.\n";
sm = new
spot::scc_info(p, spot::scc_info_options::TRACK_STATES);
}
catch (std::bad_alloc&)
{
std::cerr << ("warning: not enough memory to build "
"product of P") << i << " with state-space";
if (products > 1)
std::cerr << " #" << p << '/' << products << '\n';
std::cerr << '\n';
++oom_count;
}
pos_map[i] = sm;
product_stats(pstats, i, sm);
}
if (!no_checks)
for (size_t i = 0; i < m; ++i)
if (neg[i])
{ {
if (verbose) if (verbose)
std::cerr << ("info: building product between state-space" std::cerr << ("info: building product between state-space"
" and N") << i " and P") << i
<< " (" << neg[i]->num_states() << " st., " << " (" << pos[i]->num_states() << " st., "
<< neg[i]->num_edges() << " ed.)\n"; << pos[i]->num_edges() << " ed.)\n";
spot::scc_info* sm = nullptr;
try try
{ {
auto p = spot::product(neg[i], statespace); auto p = spot::product(pos[i], statespace);
if (verbose) if (verbose)
std::cerr << "info: product has " << p->num_states() std::cerr << "info: product has " << p->num_states()
<< " st., " << p->num_edges() << " st., " << p->num_edges()
...@@ -1427,16 +1406,54 @@ namespace ...@@ -1427,16 +1406,54 @@ namespace
catch (std::bad_alloc&) catch (std::bad_alloc&)
{ {
std::cerr << ("warning: not enough memory to build " std::cerr << ("warning: not enough memory to build "
"product of N") << i << " with state-space"; "product of P") << i << " with state-space";
if (products > 1) if (products > 1)
std::cerr << " #" << p << '/' << products << '\n'; std::cerr << " #" << p << '/' << products << '\n';
std::cerr << '\n'; std::cerr << '\n';
++oom_count; ++oom_count;
} }
pos_map[i] = sm;
neg_map[i] = sm;
product_stats(nstats, i, sm);
} }
product_stats(pstats, i, sm);
}
if (!no_checks)
for (size_t i = 0; i < m; ++i)
{
spot::scc_info* sm = nullptr;
if (neg[i])
{
if (verbose)
std::cerr << ("info: building product between state-space"
" and N") << i
<< " (" << neg[i]->num_states() << " st., "
<< neg[i]->num_edges() << " ed.)\n";
try
{
auto p = spot::product(neg[i], statespace);
if (verbose)
std::cerr << "info: product has " << p->num_states()
<< " st., " << p->num_edges()
<< " ed.\n";
sm = new
spot::scc_info(p,
spot::scc_info_options::TRACK_STATES);
}
catch (std::bad_alloc&)
{
std::cerr << ("warning: not enough memory to build "
"product of N")
<< i << " with state-space";
if (products > 1)
std::cerr << " #" << p << '/' << products << '\n';
std::cerr << '\n';
++oom_count;
}
neg_map[i] = sm;
}
product_stats(nstats, i, sm);
}
if (!no_checks) if (!no_checks)
{ {
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche # Copyright (C) 2012-2018 Laboratoire de Recherche et Développement de
# et Développement de l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
...@@ -314,3 +314,64 @@ run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba' ...@@ -314,3 +314,64 @@ run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'
ltlcross --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv ltlcross --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv
grep product out.csv && exit 1 grep product out.csv && exit 1
check_csv out.csv check_csv out.csv
#
cat >fake <<\EOF
case $1 in
"foo")
cat <<\END
HOA: v1
name: "foo"
States: 1
Start: 0
AP: 5 "p0" "p1" "p2" "p3" "p4"
acc-name: parity min odd 32
Acceptance: 32 Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) &
(Inf(5) | (Fin(6) & (Inf(7) | (Fin(8) & (Inf(9) | (Fin(10) & (Inf(11)
| (Fin(12) & (Inf(13) | (Fin(14) & (Inf(15) | (Fin(16) & (Inf(17) |
(Fin(18) & (Inf(19) | (Fin(20) & (Inf(21) | (Fin(22) & (Inf(23) |
(Fin(24) & (Inf(25) | (Fin(26) & (Inf(27) | (Fin(28) & (Inf(29) |
(Fin(30) & Inf(31)))))))))))))))))))))))))))))))
--BODY--
State: 0
0 { 0} 0 { 1} 0 { 2} 0 { 3} 0 { 4} 0 { 5} 0 { 6} 0 { 7} 0 { 8} 0 { 9}
0 {10} 0 {11} 0 {12} 0 {13} 0 {14} 0 {15} 0 {16} 0 {17} 0 {18} 0 {19}
0 {20} 0 {21} 0 {22} 0 {23} 0 {24} 0 {25} 0 {26} 0 {27} 0 {28} 0 {29}
0 {30} 0 {31}
--END--
END
;;
"!(foo)")
cat <<\END
HOA: v1
name: "foo"
States: 1
Start: 0
AP: 5 "p0" "p1" "p2" "p3" "p4"
acc-name: parity min even 32
Acceptance: 32 Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & (Inf(4) |
(Fin(5) & (Inf(6) | (Fin(7) & (Inf(8) | (Fin(9) & (Inf(10) | (Fin(11)
& (Inf(12) | (Fin(13) & (Inf(14) | (Fin(15) & (Inf(16) | (Fin(17) &
(Inf(18) | (Fin(19) & (Inf(20) | (Fin(21) & (Inf(22) | (Fin(23) &
(Inf(24) | (Fin(25) & (Inf(26) | (Fin(27) & (Inf(28) | (Fin(29) &
(Inf(30) | Fin(31)))))))))))))))))))))))))))))))
--BODY--
State: 0
0 { 0} 0 { 1} 0 { 2} 0 { 3} 0 { 4} 0 { 5} 0 { 6} 0 { 7} 0 { 8} 0 { 9}
0 {10} 0 {11} 0 {12} 0 {13} 0 {14} 0 {15} 0 {16} 0 {17} 0 {18} 0 {19}
0 {20} 0 {21} 0 {22} 0 {23} 0 {24} 0 {25} 0 {26} 0 {27} 0 {28} 0 {29}
0 {30} 0 {31}
--END--
END
;;
esac
EOF
chmod +x fake
ltlcross './fake %f >%O' -f foo --verbose --csv=out.csv 2>stderr
cat stderr
test 2 = `grep -c 'info:.*-> failed (Too many .* used.)' stderr`
check_csv out.csv
ltlcross './fake %f >%O' -f foo --csv=out.csv 2>stderr
cat stderr
test 2 = `grep -c 'info: preproc.* failed (Too many .* used.)' stderr`
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