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

postproc: fix handling of --complete

Browse source 
* src/tgbaalgos/postproc.cc: Here.
* src/tgbatest/readsave.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-23 18:40:46 +01:00
parent 93271bed6f
commit 8dc6776c24
2 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tgbaalgos/postproc.cc
View file

@ -125,7 +125,11 @@ namespace spot
postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f)
{
if (type_ == TGBA && PREF_ == Any && level_ == Low)
{
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;

5
src/tgbatest/readsave.test
View file

@ -286,7 +286,7 @@ EOF
diff output expected
$autfilt -H <<EOF | $autfilt --dot=vcsn >output
cat >input <<EOF
HOA: v1
States: 4
Start: 2
@ -306,6 +306,7 @@ State: 3 "s3"
[0] 1
--END--
EOF
$autfilt -H input | $autfilt --dot=vcsn >output
cat >expected <<EOF
digraph G {
@ -334,3 +335,5 @@ digraph G {
EOF
diff output expected
test 1 = `$autfilt -H input --complete | $autfilt --is-complete --count`