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

* src/taalgos/minimize.cc: Replace tgba_explicit_number by tgba_digraph.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2014-08-10 18:17:02 +02:00
parent 57e7bbb3b1
commit cbca22d1f1
1 changed files with 11 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/taalgos/minimize.cc
View file

@ -35,7 +35,7 @@
#include "misc/bddlt.hh" #include "misc/bddlt.hh"
#include "ta/tgtaexplicit.hh" #include "ta/tgtaexplicit.hh"
#include "taalgos/statessetbuilder.hh" #include "taalgos/statessetbuilder.hh"
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbagraph.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
namespace spot namespace spot
@ -74,7 +74,7 @@ namespace spot
// automaton // automaton
static void static void
build_result(const ta* a, std::list<hash_set*>& sets, build_result(const ta* a, std::list<hash_set*>& sets,
tgba_explicit_number* result_tgba, ta_explicit* result) tgba_digraph* result_tgba, ta_explicit* result)
{ {
// For each set, create a state in the tgbaulting automaton. // For each set, create a state in the tgbaulting automaton.
// For a state s, state_num[s] is the number of the state in the minimal // For a state s, state_num[s] is the number of the state in the minimal
@ -88,6 +88,7 @@ namespace spot
hash_set* h = *sit; hash_set* h = *sit;
for (hit = h->begin(); hit != h->end(); ++hit) for (hit = h->begin(); hit != h->end(); ++hit)
state_num[*hit] = num; state_num[*hit] = num;
result_tgba->new_state();
++num; ++num;
} }
@ -102,7 +103,6 @@ namespace spot
const state* src = *hit; const state* src = *hit;
unsigned src_num = state_num[src]; unsigned src_num = state_num[src];
state* tgba_state = result_tgba->add_state(src_num);
bdd tgba_condition = bddtrue; bdd tgba_condition = bddtrue;
bool is_initial_state = a->is_initial_state(src); bool is_initial_state = a->is_initial_state(src);
if ((a->get_artificial_initial_state() == 0) && is_initial_state) if ((a->get_artificial_initial_state() == 0) && is_initial_state)
@ -112,7 +112,7 @@ namespace spot
a->is_livelock_accepting_state(src); a->is_livelock_accepting_state(src);
state_ta_explicit* new_src = state_ta_explicit* new_src =
new state_ta_explicit(tgba_state, new state_ta_explicit(result_tgba->state_from_number(src_num),
tgba_condition, is_initial_state, tgba_condition, is_initial_state,
is_accepting_state, is_accepting_state,
is_livelock_accepting_state); is_livelock_accepting_state);
@ -143,7 +143,6 @@ namespace spot
if (i == state_num.end()) // Ignore useless destinations. if (i == state_num.end()) // Ignore useless destinations.
continue; continue;
state* tgba_state = result_tgba->add_state(i->second);
bdd tgba_condition = bddtrue; bdd tgba_condition = bddtrue;
is_initial_state = a->is_initial_state(dst); is_initial_state = a->is_initial_state(dst);
if ((a->get_artificial_initial_state() == 0) && is_initial_state) if ((a->get_artificial_initial_state() == 0) && is_initial_state)
@ -153,7 +152,7 @@ namespace spot
a->is_livelock_accepting_state(dst); a->is_livelock_accepting_state(dst);
state_ta_explicit* new_dst = state_ta_explicit* new_dst =
new state_ta_explicit(tgba_state, new state_ta_explicit(result_tgba->state_from_number(i->second),
tgba_condition, is_initial_state, tgba_condition, is_initial_state,
is_accepting_state, is_accepting_state,
is_livelock_accepting_state); is_livelock_accepting_state);
@ -487,9 +486,8 @@ namespace spot
minimize_ta(const ta* ta_) minimize_ta(const ta* ta_)
{ {
tgba_explicit_number* tgba = new tgba_explicit_number(ta_->get_dict()); auto tgba = new tgba_digraph(ta_->get_dict());
auto res = new ta_explicit(tgba, ta_->all_acceptance_conditions(),
ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions(),
0, /* own_tgba = */ true); 0, /* own_tgba = */ true);
partition_t partition = build_partition(ta_); partition_t partition = build_partition(ta_);
@ -509,10 +507,8 @@ namespace spot
minimize_tgta(const tgta_explicit* tgta_) minimize_tgta(const tgta_explicit* tgta_)
{ {
tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict()); auto tgba = new tgba_digraph(tgta_->get_dict());
auto res = new tgta_explicit(tgba, tgta_->all_acceptance_conditions(),
tgta_explicit* res = new tgta_explicit(tgba,
tgta_->all_acceptance_conditions(),
0, /* own_tgba = */ true); 0, /* own_tgba = */ true);
const ta_explicit* ta = tgta_->get_ta(); const ta_explicit* ta = tgta_->get_ta();