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

Improving the construction of TGTA

Browse source 
* src/taalgos/tgba2ta.hh, src/taalgos/tgba2ta.cc:
optimization of the TGTA automaton obtained from a TGBA.
This commit is contained in:
Ala-Eddine Ben-Salem 2011-12-08 20:11:06 +01:00 • committed by Alexandre Duret-Lutz
parent db2fcfa97a
commit 4eaa7b24df
2 changed files with 49 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/taalgos/tgba2ta.cc
View file

@ -156,19 +156,18 @@ namespace spot
} }
compute_livelock_acceptance_states(ta);
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 = state_ta_explicit* 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);
add_artificial_livelock_accepting_state(ta,
artificial_livelock_accepting_state);
} }
compute_livelock_acceptance_states(ta,artificial_livelock_accepting_state);
return ta; return ta;
} }
@ -271,7 +270,7 @@ namespace spot
{ {
testing_automata->create_transition(source, (*it_conditions), testing_automata->create_transition(source, (*it_conditions),
bddfalse, artificial_livelock_accepting_state,true); bddfalse, artificial_livelock_accepting_state, true);
} }
} }
@ -279,6 +278,19 @@ namespace spot
} }
delete conditions_to_livelock_accepting_states; delete conditions_to_livelock_accepting_states;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
state_ta_explicit::transitions* state_trans =
(state)->get_transitions();
bool state_trans_empty = state_trans == 0 || state_trans->empty();
if (state->is_livelock_accepting_state()
&& (!state->is_accepting_state()) && (!state_trans_empty))
state->set_livelock_accepting_state(false);
}
} }
namespace namespace
@ -287,7 +299,7 @@ namespace spot
} }
void void
compute_livelock_acceptance_states(ta_explicit* testing_automata) 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)
@ -327,6 +339,7 @@ namespace spot
while (!init_set.empty()) while (!init_set.empty())
{ {
// Setup depth-first search from initial states. // Setup depth-first search from initial states.
{ {
state_ta_explicit* init = state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top()); down_cast<state_ta_explicit*> (init_set.top());
@ -373,8 +386,7 @@ namespace spot
todo.pop(); todo.pop();
// fill rem with any component removed, // fill rem with any component removed,
numbered_state_heap::state_index_p spi = numbered_state_heap::state_index_p spi = h->index(curr);
h->index(curr);
assert(spi.first); assert(spi.first);
sscc.rem().push_front(curr); sscc.rem().push_front(curr);
@ -393,8 +405,7 @@ namespace spot
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{ {
numbered_state_heap::state_index_p spi = h->index( numbered_state_heap::state_index_p spi = h->index((*i));
(*i));
assert(spi.first->compare(*i) == 0); assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1); assert(*spi.second != -1);
*spi.second = -1; *spi.second = -1;
@ -407,6 +418,7 @@ 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);
} }
} }
@ -470,8 +482,8 @@ namespace spot
if (*spi.second == -1) if (*spi.second == -1)
continue; continue;
trace << "***compute_livelock_acceptance_states: CYCLE***" trace
<< std::endl; << "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
if (!curr->compare(dest)) if (!curr->compare(dest))
{ {
@ -482,10 +494,15 @@ namespace spot
if (testing_automata->is_accepting_state(self_loop_state) if (testing_automata->is_accepting_state(self_loop_state)
|| (acc_cond || (acc_cond
== testing_automata->all_acceptance_conditions())) == testing_automata->all_acceptance_conditions()))
self_loop_state->set_livelock_accepting_state(true); {
self_loop_state->set_livelock_accepting_state(true);
self_loop_state->set_accepting_state(true);
}
trace trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
<< std::endl; << std::endl;
} }
@ -532,6 +549,7 @@ namespace spot
} }
delete h; delete h;
if (artificial_livelock_accepting_state != 0) add_artificial_livelock_accepting_state(testing_automata, artificial_livelock_accepting_state);
} }
tgbta_explicit* tgbta_explicit*
@ -549,7 +567,8 @@ 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 << "***tgba_to_tgbta: POST build_ta***" << std::endl; trace
<< "***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();
@ -575,27 +594,29 @@ namespace spot
{ {
bool trans_empty = (trans == 0 || trans->empty()); bool trans_empty = (trans == 0 || trans->empty());
if (trans_empty) 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;
} else {
state->set_livelock_accepting_state(false);
} }
} }
if (state->compare(tgbta->get_artificial_initial_state())) if (state->compare(tgbta->get_artificial_initial_state()))
tgbta->create_transition(state, bdd_stutering_transition, bddfalse, tgbta->create_transition(state, bdd_stutering_transition, bddfalse,
state); state);
trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl; state->set_livelock_accepting_state(false);
state->set_accepting_state(false);
trace
<< "***tgba_to_tgbta: POST create_transition ***" << std::endl;
} }

3
src/taalgos/tgba2ta.hh
View file

@ -40,8 +40,9 @@ namespace spot
bool artificial_livelock_accepting_state_mode = false, bool artificial_livelock_accepting_state_mode = false,
bool degeneralized = true); bool degeneralized = true);
//artificial_livelock_accepting_state is used in the case of TA+ automata
void void
compute_livelock_acceptance_states(ta_explicit* testing_automata); compute_livelock_acceptance_states(ta_explicit* testing_automata, state_ta_explicit* artificial_livelock_accepting_state = 0);
void void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata, add_artificial_livelock_accepting_state(ta_explicit* testing_automata,