remfin: call remove_alternation if needed
* spot/twaalgos/remfin.cc: Here. * tests/core/alternating.test: Add a test case.
This commit is contained in:
parent
071d819c49
commit
f5b261d80e
2 changed files with 49 additions and 0 deletions
|
|
@ -24,6 +24,7 @@
|
||||||
#include <spot/twaalgos/totgba.hh>
|
#include <spot/twaalgos/totgba.hh>
|
||||||
#include <spot/twaalgos/isdet.hh>
|
#include <spot/twaalgos/isdet.hh>
|
||||||
#include <spot/twaalgos/mask.hh>
|
#include <spot/twaalgos/mask.hh>
|
||||||
|
#include <spot/twaalgos/alternation.hh>
|
||||||
|
|
||||||
//#define TRACE
|
//#define TRACE
|
||||||
#ifdef TRACE
|
#ifdef TRACE
|
||||||
|
|
@ -494,6 +495,9 @@ namespace spot
|
||||||
if (aut->prop_weak().is_true())
|
if (aut->prop_weak().is_true())
|
||||||
return remove_fin_weak(aut);
|
return remove_fin_weak(aut);
|
||||||
|
|
||||||
|
if (aut->is_alternating())
|
||||||
|
return remove_fin(remove_alternation(aut));
|
||||||
|
|
||||||
if (auto maybe = streett_to_generalized_buchi_maybe(aut))
|
if (auto maybe = streett_to_generalized_buchi_maybe(aut))
|
||||||
return maybe;
|
return maybe;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -157,3 +157,48 @@ State: 2 "t"
|
||||||
EOF
|
EOF
|
||||||
test 3 = `autfilt --stats=%s out.hoa`
|
test 3 = `autfilt --stats=%s out.hoa`
|
||||||
test 2 = `autfilt --tgba --stats=%s out.hoa`
|
test 2 = `autfilt --tgba --stats=%s out.hoa`
|
||||||
|
|
||||||
|
# If we have a weak input, remove-fin can just transform co-Büchi into
|
||||||
|
# Büchi.
|
||||||
|
autfilt --remove-fin out.hoa >res
|
||||||
|
cat >expected <<EOF
|
||||||
|
HOA: v1
|
||||||
|
States: 3
|
||||||
|
Start: 0
|
||||||
|
AP: 1 "a"
|
||||||
|
acc-name: Buchi
|
||||||
|
Acceptance: 1 Inf(0)
|
||||||
|
properties: univ-branch trans-labels explicit-labels state-acc complete
|
||||||
|
properties: very-weak
|
||||||
|
--BODY--
|
||||||
|
State: 0 {0}
|
||||||
|
[t] 1&0
|
||||||
|
State: 1
|
||||||
|
[0] 2
|
||||||
|
[t] 1
|
||||||
|
State: 2 {0}
|
||||||
|
[t] 2
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
diff expected res
|
||||||
|
|
||||||
|
# If we do not know that the input is weak, remove-fin will call
|
||||||
|
# remove_alternation().
|
||||||
|
autfilt --remove-fin --trust-hoa=no out.hoa >res
|
||||||
|
cat >expected <<EOF
|
||||||
|
HOA: v1
|
||||||
|
States: 2
|
||||||
|
Start: 0
|
||||||
|
AP: 1 "a"
|
||||||
|
acc-name: Buchi
|
||||||
|
Acceptance: 1 Inf(0)
|
||||||
|
properties: trans-labels explicit-labels trans-acc complete
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 1 {0}
|
||||||
|
State: 1
|
||||||
|
[t] 1
|
||||||
|
[0] 1 {0}
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
diff expected res
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue