From 8dc6776c245c4ee8d1978ef420ff6a1323c65154 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 23 Jan 2015 18:40:46 +0100 Subject: [PATCH] postproc: fix handling of --complete * src/tgbaalgos/postproc.cc: Here. * src/tgbatest/readsave.test: Test it. --- src/tgbaalgos/postproc.cc | 12 +++++++++--- src/tgbatest/readsave.test | 5 ++++- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index acffc2f4b..da4fccdaa 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -125,7 +125,11 @@ namespace spot postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f) { if (type_ == TGBA && PREF_ == Any && level_ == Low) - return a; + { + if (COMP_) + a = tgba_complete(a); + return a; + } if (simul_ < 0) simul_ = (level_ == Low) ? 1 : 3; @@ -171,7 +175,7 @@ namespace spot if (m->num_states() < a->num_states()) a = m; } - if (COMP_ == Complete) + if (COMP_) a = tgba_complete(a); return a; } @@ -180,6 +184,8 @@ namespace spot { if (type_ == BA) a = do_degen(a); + if (COMP_ == Complete) + a = tgba_complete(a); return a; } @@ -381,7 +387,7 @@ namespace spot sim = dba ? dba : sim; - if (COMP_ == Complete) + if (COMP_) sim = tgba_complete(sim); return sim; diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 4b6505ebb..236378577 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -286,7 +286,7 @@ EOF diff output expected -$autfilt -H <output +cat >input <output cat >expected <