Commit 90a466d6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

degen: consider common outgoing acceptance only inside an SCC

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case that is improved
by this.
* src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.test: Adjust.
parent 073334df
...@@ -106,7 +106,8 @@ namespace spot ...@@ -106,7 +106,8 @@ namespace spot
} }
}; };
// Acceptance set common to all outgoing transitions of some state. // Acceptance set common to all outgoing transitions (of the same
// SCC -- we do not care about the other) of some state.
class outgoing_acc class outgoing_acc
{ {
const tgba* a_; const tgba* a_;
...@@ -114,19 +115,28 @@ namespace spot ...@@ -114,19 +115,28 @@ namespace spot
typedef Sgi::hash_map<const state*, cache_entry, typedef Sgi::hash_map<const state*, cache_entry,
state_ptr_hash, state_ptr_equal> cache_t; state_ptr_hash, state_ptr_equal> cache_t;
cache_t cache_; cache_t cache_;
const scc_map* sm_;
public: public:
outgoing_acc(const tgba* a): a_(a) outgoing_acc(const tgba* a, const scc_map* sm): a_(a), sm_(sm)
{ {
} }
cache_t::const_iterator fill_cache(const state* s) cache_t::const_iterator fill_cache(const state* s)
{ {
unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0;
bdd common = a_->all_acceptance_conditions(); bdd common = a_->all_acceptance_conditions();
bdd union_ = bddfalse; bdd union_ = bddfalse;
tgba_succ_iterator* it = a_->succ_iter(s); tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next()) for (it->first(); !it->done(); it->next())
{ {
// Ignore transitions that leave the SCC of s.
const state* d = it->current_state();
unsigned s2 = sm_ ? sm_->scc_of_state(d) : 0;
d->destroy();
if (s2 != s1)
continue;
bdd set = it->current_acceptance_conditions(); bdd set = it->current_acceptance_conditions();
common &= set; common &= set;
union_ |= set; union_ |= set;
...@@ -325,8 +335,6 @@ namespace spot ...@@ -325,8 +335,6 @@ namespace spot
// Initialize scc_orders // Initialize scc_orders
scc_orders orders(a->all_acceptance_conditions()); scc_orders orders(a->all_acceptance_conditions());
outgoing_acc outgoing(a);
// Make sure we always use the same pointer for identical states // Make sure we always use the same pointer for identical states
// from the input automaton. // from the input automaton.
unicity_table uniq; unicity_table uniq;
...@@ -355,6 +363,9 @@ namespace spot ...@@ -355,6 +363,9 @@ namespace spot
if (use_scc) if (use_scc)
m.build_map(); m.build_map();
// Cache for common outgoing acceptances.
outgoing_acc outgoing(a, use_scc ? &m : 0);
queue_t todo; queue_t todo;
const state* s0 = uniq(a->get_init_state()); const state* s0 = uniq(a->get_init_state());
......
...@@ -103,3 +103,91 @@ grep 'states: 8' out ...@@ -103,3 +103,91 @@ grep 'states: 8' out
# easy to obtain a 4-state BA when tweaking the degeneralization # easy to obtain a 4-state BA when tweaking the degeneralization
# to ignore arc entering an SCC. # to ignore arc entering an SCC.
test 3 = "`../../bin/ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`" test 3 = "`../../bin/ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`"
# This 7-state DRA (built with
# ltlfilt -f 'F(a & GFb) | (Fc & Fa & F(c & GF!b))' -l |
# ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - -
# should be converted in into a 6-state DBA.
cat >in.dra <<EOF
DRA v2 explicit
Comment: "Union{Safra[NBA=3],Safra[NBA=5]}"
States: 7
Acceptance-Pairs: 2
Start: 5
AP: 3 "a" "b" "c"
---
State: 0
Acc-Sig: +0 +1
1
1
2
2
1
1
2
2
State: 1
Acc-Sig: +1
1
1
2
2
1
1
2
2
State: 2
Acc-Sig: +0
1
1
2
2
1
1
2
2
State: 3
Acc-Sig: +0
6
6
3
3
1
1
0
0
State: 4
Acc-Sig:
4
0
4
0
4
0
4
0
State: 5
Acc-Sig:
5
3
5
3
4
0
4
0
State: 6
Acc-Sig:
6
6
3
3
1
1
0
0
EOF
run 0 ../../bin/dstar2tgba in.dra -BD --stats=%s > out.stat
test 6 = "`cat out.stat`"
...@@ -85,7 +85,7 @@ done ...@@ -85,7 +85,7 @@ done
for opt in -TA; do for opt in -TA; do
../ltl2tgba -ks $opt -RT -DS 'Ga U b' > stdout ../ltl2tgba -ks $opt -RT -DS 'Ga U b' > stdout
grep 'transitions: 13$' stdout grep 'transitions: 11$' stdout
grep 'states: 6$' stdout grep 'states: 6$' stdout
done done
...@@ -119,11 +119,11 @@ grep 'states: 290$' stdout ...@@ -119,11 +119,11 @@ grep 'states: 290$' stdout
#tests with artificial livelock state: #tests with artificial livelock state:
run 0 ../ltl2tgba -ks -TA -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout run 0 ../ltl2tgba -ks -TA -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 790$' stdout grep 'transitions: 784$' stdout
grep 'states: 66$' stdout grep 'states: 66$' stdout
run 0 ../ltl2tgba -TA -RT -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout run 0 ../ltl2tgba -TA -RT -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 390$' stdout grep 'transitions: 384$' stdout
grep 'states: 26$' stdout grep 'states: 26$' stdout
run 0 ../ltl2tgba -TGTA -RT -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout run 0 ../ltl2tgba -TGTA -RT -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout
...@@ -138,7 +138,7 @@ grep 'states: 38$' stdout ...@@ -138,7 +138,7 @@ grep 'states: 38$' stdout
run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x -DS "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x -DS "$f" >stdout
grep 'transitions: 555$' stdout grep 'transitions: 551$' stdout
grep 'states: 40$' stdout grep 'states: 40$' stdout
......
...@@ -150,11 +150,10 @@ for opt in '' -D -DS; do ...@@ -150,11 +150,10 @@ for opt in '' -D -DS; do
../ltl2tgba -ks -f -R3 $opt "$f" > stdout ../ltl2tgba -ks -f -R3 $opt "$f" > stdout
grep 'transitions: 15$' stdout grep 'transitions: 15$' stdout
grep 'states: 6$' stdout grep 'states: 6$' stdout
../ltl2tgba -ks -f -R3f $opt "$f" > stdout
grep 'transitions: 15$' stdout
grep 'states: 6$' stdout
done done
# Note: this is worse with -R3f.
../ltl2tgba -ks -f -R3f -DS "$f" > stdout
grep 'transitions: 17$' stdout
grep 'states: 7$' stdout
# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' # Make sure 'GFa & GFb & GFc & GFd & GFe & GFf'
# has 7 states and 34 transitions after degeneralization. # has 7 states and 34 transitions after degeneralization.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment