alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Never claim output used to print the degeneralized automaton

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2010-11-25 20:29:16 +01:00
parent 7627b9673b
commit 67f46b85b3
2 changed files with 23 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
* src/tgbatest/ltl2tgba.test: Test both -l and -f. This should

14
src/tgbatest/ltl2tgba.cc
View file

@ -1043,8 +1043,18 @@ main(int argc, char** argv)
{
assert(degeneralize_opt == DegenSBA);
const spot::tgba_sba_proxy* s =
static_cast<const spot::tgba_sba_proxy*>(degeneralized);
spot::never_claim_reachable(std::cout, s, f, spin_comments);
dynamic_cast<const spot::tgba_sba_proxy*>(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: