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

twaalgos/cobuchi: Optimize aug. subset construction when aut. is det

Browse source 
* spot/twaalgos/cobuchi.cc: Avoid the product of an automaton A and its
power construction Pow(A) when A is deterministic.
This commit is contained in:
Alexandre GBAGUIDI AISSE 2017-09-22 18:46:57 +02:00
parent ebe3a15dcc
commit 81af8359f5
1 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

18
spot/twaalgos/cobuchi.cc
View file

@ -32,7 +32,6 @@
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/strength.hh> #include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/sbacc.hh> // For issue #317 #include <spot/twaalgos/sbacc.hh> // For issue #317
#include <stack> #include <stack>
#include <unordered_map> #include <unordered_map>
@ -69,7 +68,22 @@ namespace spot
bool named_states, bool named_states,
struct power_map& pmap) struct power_map& pmap)
{ {
twa_graph_ptr res = product(aut_prod, tgba_powerset(aut_power, pmap)); twa_graph_ptr res = nullptr;
if (is_deterministic(aut_prod))
{
res = make_twa_graph(aut_prod, twa::prop_set::all());
auto v = new product_states;
res->set_named_prop("product-states", v);
for (unsigned s = 0; s < aut_power->num_states(); ++s)
v->emplace_back(s, s);
for (unsigned s = 0; s < aut_power->num_states(); ++s)
pmap.map_.push_back({s});
}
else
{
res = product(aut_prod, tgba_powerset(aut_power, pmap));
}
if (named_states) if (named_states)
{ {