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

STA and TGTA optimisations

Browse source 
* src/taalgos/tgba2ta.cc: the transformations of TGBA
This commit is contained in:
Ala-Eddine Ben-Salem 2011-12-14 15:19:32 +01:00 • committed by Alexandre Duret-Lutz
parent 4eaa7b24df
commit 4a1d6dd67c
1 changed files with 42 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

60
src/taalgos/tgba2ta.cc
View file

@ -156,17 +156,25 @@ namespace spot
} }
state_ta_explicit* artificial_livelock_accepting_state = 0;
trace << "*** build_ta: artificial_livelock_accepting_state_mode = ***"
<< artificial_livelock_accepting_state_mode << std::endl;
state_ta_explicit* artificial_livelock_accepting_state = 0;
if (artificial_livelock_accepting_state_mode) if (artificial_livelock_accepting_state_mode)
{ {
state_ta_explicit* artificial_livelock_accepting_state =
artificial_livelock_accepting_state =
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue, new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue,
false, false, true, 0); false, false, true, 0);
trace << "*** build_ta: artificial_livelock_accepting_state = ***"
<< artificial_livelock_accepting_state << std::endl;
} }
compute_livelock_acceptance_states(ta,artificial_livelock_accepting_state);
compute_livelock_acceptance_states(ta, artificial_livelock_accepting_state);
return ta; return ta;
@ -212,6 +220,11 @@ namespace spot
assert(artificial_livelock_accepting_state_added assert(artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state); == artificial_livelock_accepting_state);
trace
<< "*** add_artificial_livelock_accepting_state: assert(artificial_livelock_accepting_state_added == artificial_livelock_accepting_state) = ***"
<< (artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state) << std::endl;
ta::states_set_t states_set = testing_automata->get_states_set(); ta::states_set_t states_set = testing_automata->get_states_set();
ta::states_set_t::iterator it; ta::states_set_t::iterator it;
@ -299,7 +312,8 @@ namespace spot
} }
void void
compute_livelock_acceptance_states(ta_explicit* testing_automata, state_ta_explicit* artificial_livelock_accepting_state) compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state)
{ {
// We use five main data in this algorithm: // We use five main data in this algorithm:
// * sscc: a stack of strongly stuttering-connected components (SSCC) // * sscc: a stack of strongly stuttering-connected components (SSCC)
@ -418,7 +432,9 @@ namespace spot
livelock_accepting_state->set_livelock_accepting_state( livelock_accepting_state->set_livelock_accepting_state(
true); true);
if (artificial_livelock_accepting_state != 0) livelock_accepting_state->set_accepting_state(true); if (artificial_livelock_accepting_state != 0)
livelock_accepting_state->set_accepting_state(
true);
} }
} }
@ -482,8 +498,8 @@ namespace spot
if (*spi.second == -1) if (*spi.second == -1)
continue; continue;
trace trace << "***compute_livelock_acceptance_states: CYCLE***"
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl; << std::endl;
if (!curr->compare(dest)) if (!curr->compare(dest))
{ {
@ -501,8 +517,8 @@ namespace spot
} }
trace trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
<< std::endl; << std::endl;
} }
@ -549,7 +565,17 @@ namespace spot
} }
delete h; delete h;
if (artificial_livelock_accepting_state != 0) add_artificial_livelock_accepting_state(testing_automata, artificial_livelock_accepting_state); trace
<< "*** compute_livelock_acceptance_states: PRE call add_artificial_livelock_accepting_state() method ... (artificial_livelock_accepting_state != 0) :***"
<< (artificial_livelock_accepting_state != 0) << std::endl;
if (artificial_livelock_accepting_state != 0)
add_artificial_livelock_accepting_state(testing_automata,
artificial_livelock_accepting_state);
trace
<< "*** compute_livelock_acceptance_states: POST call add_artificial_livelock_accepting_state() method ***"
<< std::endl;
} }
tgbta_explicit* tgbta_explicit*
@ -567,8 +593,7 @@ namespace spot
// build ta automata: // build ta automata:
build_ta(tgbta, atomic_propositions_set_, true, true, false); build_ta(tgbta, atomic_propositions_set_, true, true, false);
trace trace << "***tgba_to_tgbta: POST build_ta***" << std::endl;
<< "***tgba_to_tgbta: POST build_ta***" << std::endl;
// adapt a ta automata to build tgbta automata : // adapt a ta automata to build tgbta automata :
ta::states_set_t states_set = tgbta->get_states_set(); ta::states_set_t states_set = tgbta->get_states_set();
@ -597,13 +622,13 @@ namespace spot
if (trans_empty || state->is_accepting_state()) if (trans_empty || state->is_accepting_state())
{ {
trace trace
<< "***tgba_to_tgbta: PRE if (state->is_livelock_accepting_state()) ... create_transition ***" << "***tgba_to_tgbta: PRE if (state->is_livelock_accepting_state()) ... create_transition ***"
<< std::endl; << std::endl;
tgbta->create_transition(state, bdd_stutering_transition, tgbta->create_transition(state, bdd_stutering_transition,
tgbta->all_acceptance_conditions(), state); tgbta->all_acceptance_conditions(), state);
trace trace
<< "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***" << "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***"
<< std::endl; << std::endl;
} }
@ -615,8 +640,7 @@ namespace spot
state->set_livelock_accepting_state(false); state->set_livelock_accepting_state(false);
state->set_accepting_state(false); state->set_accepting_state(false);
trace trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl;
<< "***tgba_to_tgbta: POST create_transition ***" << std::endl;
} }