From 020c981188611e3fb25e28a087f53ae1bab02b53 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Jan 2018 13:51:12 +0100 Subject: [PATCH] ltlcross: detect remove_fin failures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #314, reported by František Blahoudek. * bin/ltlcross.cc: Here. * tests/core/ltlcross3.test: Add new test case. * NEWS: Mention the bug. --- NEWS | 3 + bin/ltlcross.cc | 115 ++++++++++++++++++++++---------------- tests/core/ltlcross3.test | 65 ++++++++++++++++++++- 3 files changed, 132 insertions(+), 51 deletions(-) diff --git a/NEWS b/NEWS index ebeee2ac8..9b9cfd9f8 100644 --- a/NEWS +++ b/NEWS @@ -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 --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) Bugs fixed: diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 1563a28e6..06010a214 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -1240,9 +1240,21 @@ namespace printsize(x[i]); std::cerr << ") ->"; } - cleanup_acceptance_here(x[i]); - x[i] = remove_fin(x[i]); - if (verbose) + 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]); @@ -1371,52 +1383,19 @@ namespace std::vector pos_map(m); std::vector neg_map(m); for (size_t i = 0; i < m; ++i) - if (pos[i]) - { - if (verbose) - 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]) + { + spot::scc_info* sm = nullptr; + if (pos[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"; + " and P") << i + << " (" << pos[i]->num_states() << " st., " + << pos[i]->num_edges() << " ed.)\n"; - spot::scc_info* sm = nullptr; try { - auto p = spot::product(neg[i], statespace); + auto p = spot::product(pos[i], statespace); if (verbose) std::cerr << "info: product has " << p->num_states() << " st., " << p->num_edges() @@ -1427,16 +1406,54 @@ namespace catch (std::bad_alloc&) { 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) std::cerr << " #" << p << '/' << products << '\n'; std::cerr << '\n'; ++oom_count; } - - neg_map[i] = sm; - product_stats(nstats, i, sm); + pos_map[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) { diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 84d14dca9..818e27eea 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2012-2018 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -314,3 +314,64 @@ run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba' ltlcross --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv grep product out.csv && exit 1 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`