From 67f46b85b30f1ad011c5bd21ebbb6d897521f2b6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Nov 2010 20:29:16 +0100 Subject: [PATCH] Never claim output used to print the degeneralized automaton before some optional operations (like more optimizations, or a product). * src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last automaton computed, not just the automaton when we degeneralized it. We may have applied other algorithms since the original degeneralization. --- ChangeLog | 11 +++++++++++ src/tgbatest/ltl2tgba.cc | 14 ++++++++++++-- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index bd656264e..da9a9cac6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-11-25 Alexandre Duret-Lutz + + Never claim output used to print the degeneralized automaton + before some optional operations (like more optimizations, or a + product). + + * src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last + automaton computed, not just the automaton when we degeneralized + it. We may have applied other algorithms since the original + degeneralization. + 2010-11-25 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.test: Test both -l and -f. This should diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 9a788c2f0..cf86f6f43 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1043,8 +1043,18 @@ main(int argc, char** argv) { assert(degeneralize_opt == DegenSBA); const spot::tgba_sba_proxy* s = - static_cast(degeneralized); - spot::never_claim_reachable(std::cout, s, f, spin_comments); + dynamic_cast(a); + if (s) + spot::never_claim_reachable(std::cout, s, f, spin_comments); + else + { + // It is possible that we have applied other + // operations to the automaton since its initial + // degeneralization. Let's degeneralize again! + s = new spot::tgba_sba_proxy(a); + spot::never_claim_reachable(std::cout, s, f, spin_comments); + delete s; + } break; } case 9: