* src/taalgos/tgba2ta.cc: Cosmetics.
This commit is contained in:
Alexandre Duret-Lutz
parent
92a3366488
commit
26f48b1df2
1 changed files with 470 additions and 494 deletions
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
|
||||
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -49,27 +49,25 @@ namespace spot
|
|||
namespace
|
||||
{
|
||||
typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
|
||||
}
|
||||
|
||||
void
|
||||
transform_to_single_pass_automaton(ta_explicit* testing_automata,
|
||||
state_ta_explicit* artificial_livelock_accepting_state = 0)
|
||||
static void
|
||||
transform_to_single_pass_automaton
|
||||
(ta_explicit* testing_automata,
|
||||
state_ta_explicit* artificial_livelock_acc_state = 0)
|
||||
{
|
||||
|
||||
if (artificial_livelock_accepting_state != 0)
|
||||
if (artificial_livelock_acc_state != 0)
|
||||
{
|
||||
state_ta_explicit* artificial_livelock_accepting_state_added =
|
||||
testing_automata->add_state(artificial_livelock_accepting_state);
|
||||
state_ta_explicit* artificial_livelock_acc_state_added =
|
||||
testing_automata->add_state(artificial_livelock_acc_state);
|
||||
|
||||
// unique artificial_livelock_accepting_state
|
||||
assert(artificial_livelock_accepting_state_added
|
||||
== artificial_livelock_accepting_state);
|
||||
artificial_livelock_accepting_state->set_livelock_accepting_state(true);
|
||||
artificial_livelock_accepting_state->free_transitions();
|
||||
// unique artificial_livelock_acc_state
|
||||
assert(artificial_livelock_acc_state_added
|
||||
== artificial_livelock_acc_state);
|
||||
artificial_livelock_acc_state->set_livelock_accepting_state(true);
|
||||
artificial_livelock_acc_state->free_transitions();
|
||||
}
|
||||
|
||||
|
||||
|
||||
ta::states_set_t states_set = testing_automata->get_states_set();
|
||||
ta::states_set_t::iterator it;
|
||||
|
||||
|
|
@ -78,7 +76,6 @@ namespace spot
|
|||
|
||||
for (it = states_set.begin(); it != states_set.end(); ++it)
|
||||
{
|
||||
|
||||
state_ta_explicit* source = static_cast<state_ta_explicit*> (*it);
|
||||
|
||||
transitions_to_livelock_states->clear();
|
||||
|
|
@ -95,27 +92,18 @@ namespace spot
|
|||
(dest)->get_transitions();
|
||||
bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();
|
||||
|
||||
|
||||
|
||||
//select transitions where a destination is a livelock state
|
||||
// which isn't a Buchi accepting state and has successors
|
||||
if (dest->is_livelock_accepting_state()
|
||||
&& (!dest->is_accepting_state()) && (!dest_trans_empty))
|
||||
{
|
||||
transitions_to_livelock_states->push_front(*it_trans);
|
||||
|
||||
}
|
||||
|
||||
//optimization to have, after
|
||||
// minimization, an unique livelock state which has no successors
|
||||
// optimization to have, after minimization, an unique
|
||||
// livelock state which has no successors
|
||||
if (dest->is_livelock_accepting_state() && (dest_trans_empty))
|
||||
{
|
||||
dest->set_accepting_state(false);
|
||||
|
||||
}
|
||||
|
||||
++it_trans;
|
||||
|
||||
}
|
||||
|
||||
if (transitions_to_livelock_states != 0)
|
||||
|
|
@ -123,33 +111,33 @@ namespace spot
|
|||
state_ta_explicit::transitions::iterator it_trans;
|
||||
|
||||
for (it_trans = transitions_to_livelock_states->begin();
|
||||
it_trans != transitions_to_livelock_states->end(); ++it_trans)
|
||||
it_trans != transitions_to_livelock_states->end();
|
||||
++it_trans)
|
||||
{
|
||||
if (artificial_livelock_accepting_state != 0)
|
||||
if (artificial_livelock_acc_state != 0)
|
||||
{
|
||||
testing_automata->create_transition(source,
|
||||
testing_automata->create_transition
|
||||
(source,
|
||||
(*it_trans)->condition,
|
||||
(*it_trans)->acceptance_conditions,
|
||||
artificial_livelock_accepting_state, true);
|
||||
artificial_livelock_acc_state, true);
|
||||
}
|
||||
else
|
||||
{
|
||||
testing_automata->create_transition(source,
|
||||
testing_automata->create_transition
|
||||
(source,
|
||||
(*it_trans)->condition,
|
||||
(*it_trans)->acceptance_conditions,
|
||||
((*it_trans)->dest)->stuttering_reachable_livelock,
|
||||
true);
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
delete transitions_to_livelock_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();
|
||||
|
|
@ -159,14 +147,14 @@ namespace spot
|
|||
&& (!state->is_accepting_state()) && (!state_trans_empty))
|
||||
state->set_livelock_accepting_state(false);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void
|
||||
compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
||||
static void
|
||||
compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
||||
bool single_pass_emptiness_check,
|
||||
state_ta_explicit* artificial_livelock_accepting_state)
|
||||
{
|
||||
state_ta_explicit*
|
||||
artificial_livelock_acc_state)
|
||||
{
|
||||
// We use five main data in this algorithm:
|
||||
// * sscc: a stack of strongly stuttering-connected components (SSCC)
|
||||
scc_stack_ta sscc;
|
||||
|
|
@ -200,7 +188,6 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
{
|
||||
state* init_state = (*it);
|
||||
init_set.push(init_state);
|
||||
|
||||
}
|
||||
|
||||
while (!init_set.empty())
|
||||
|
|
@ -225,12 +212,10 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
tgba_succ_iterator* iter = testing_automata->succ_iter(init);
|
||||
iter->first();
|
||||
todo.push(pair_state_iter(init, iter));
|
||||
|
||||
}
|
||||
|
||||
while (!todo.empty())
|
||||
{
|
||||
|
||||
state* curr = todo.top().first;
|
||||
|
||||
numbered_state_heap::state_index_p spi = h->find(curr);
|
||||
|
|
@ -267,14 +252,16 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
// removing states
|
||||
std::list<state*>::iterator i;
|
||||
bool is_livelock_accepting_sscc = (sscc.rem().size() > 1)
|
||||
&& ((sscc.top().is_accepting) || (sscc.top().condition
|
||||
== testing_automata->all_acceptance_conditions()));
|
||||
&& ((sscc.top().is_accepting)
|
||||
|| (sscc.top().condition ==
|
||||
testing_automata->all_acceptance_conditions()));
|
||||
|
||||
trace << "*** sscc.size() = ***"
|
||||
<< sscc.size() << std::endl;
|
||||
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
|
||||
{
|
||||
numbered_state_heap::state_index_p spi = h->index((*i));
|
||||
numbered_state_heap::state_index_p spi =
|
||||
h->index((*i));
|
||||
assert(spi.first->compare(*i) == 0);
|
||||
assert(*spi.second != -1);
|
||||
*spi.second = -1;
|
||||
|
|
@ -326,7 +313,6 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
succ->next();
|
||||
// We do not need SUCC from now on.
|
||||
|
||||
|
||||
// Are we going to a new state through a stuttering transition?
|
||||
bool is_stuttering_transition =
|
||||
testing_automata->get_state_condition(curr)
|
||||
|
|
@ -349,8 +335,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
h->insert(dest_clone, ++num);
|
||||
sscc.push(num);
|
||||
arc.push(acc_cond);
|
||||
sscc.top().is_accepting = testing_automata->is_accepting_state(
|
||||
dest);
|
||||
sscc.top().is_accepting =
|
||||
testing_automata->is_accepting_state(dest);
|
||||
|
||||
tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
|
||||
iter->first();
|
||||
|
|
@ -362,8 +348,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
if (*spi.second == -1)
|
||||
continue;
|
||||
|
||||
trace
|
||||
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
|
||||
trace << "***compute_livelock_acceptance_states: CYCLE***\n";
|
||||
|
||||
if (!curr->compare(dest))
|
||||
{
|
||||
|
|
@ -382,13 +367,11 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
self_loop_state->stuttering_reachable_livelock
|
||||
= self_loop_state;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
trace
|
||||
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
|
||||
<< std::endl;
|
||||
|
||||
<< "***compute_livelock_acceptance_states: CYCLE: "
|
||||
<< "self_loop_state***\n";
|
||||
}
|
||||
|
||||
// Now this is the most interesting case. We have reached a
|
||||
|
|
@ -434,16 +417,16 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
}
|
||||
delete h;
|
||||
|
||||
if ((artificial_livelock_accepting_state != 0)
|
||||
if ((artificial_livelock_acc_state != 0)
|
||||
|| single_pass_emptiness_check)
|
||||
transform_to_single_pass_automaton(testing_automata,
|
||||
artificial_livelock_accepting_state);
|
||||
|
||||
}
|
||||
artificial_livelock_acc_state);
|
||||
}
|
||||
|
||||
ta_explicit*
|
||||
build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool degeneralized,
|
||||
bool single_pass_emptiness_check, bool artificial_livelock_state_mode)
|
||||
bool single_pass_emptiness_check,
|
||||
bool artificial_livelock_state_mode)
|
||||
{
|
||||
|
||||
std::stack<state_ta_explicit*> todo;
|
||||
|
|
@ -458,21 +441,22 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
|
||||
bdd satone_tgba_condition;
|
||||
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
|
||||
atomic_propositions_set_, bddtrue)) != bddfalse)
|
||||
atomic_propositions_set_,
|
||||
bddtrue)) != bddfalse)
|
||||
{
|
||||
tgba_condition -= satone_tgba_condition;
|
||||
state_ta_explicit* init_state;
|
||||
if (degeneralized)
|
||||
{
|
||||
init_state =
|
||||
new state_ta_explicit(tgba_init_state->clone(),
|
||||
init_state = new
|
||||
state_ta_explicit(tgba_init_state->clone(),
|
||||
satone_tgba_condition, true,
|
||||
sba_->state_is_accepting(tgba_init_state));
|
||||
}
|
||||
else
|
||||
{
|
||||
init_state =
|
||||
new state_ta_explicit(tgba_init_state->clone(),
|
||||
init_state = new
|
||||
state_ta_explicit(tgba_init_state->clone(),
|
||||
satone_tgba_condition, true, false);
|
||||
}
|
||||
|
||||
|
|
@ -491,24 +475,28 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
|
||||
tgba_succ_iterator* tgba_succ_it =
|
||||
tgba_->succ_iter(source->get_tgba_state());
|
||||
for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next())
|
||||
for (tgba_succ_it->first(); !tgba_succ_it->done();
|
||||
tgba_succ_it->next())
|
||||
{
|
||||
const state* tgba_state = tgba_succ_it->current_state();
|
||||
bdd tgba_condition = tgba_succ_it->current_condition();
|
||||
bdd tgba_acceptance_conditions =
|
||||
tgba_succ_it->current_acceptance_conditions();
|
||||
bdd satone_tgba_condition;
|
||||
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
|
||||
atomic_propositions_set_, bddtrue)) != bddfalse)
|
||||
while ((satone_tgba_condition =
|
||||
bdd_satoneset(tgba_condition,
|
||||
atomic_propositions_set_, bddtrue))
|
||||
!= bddfalse)
|
||||
{
|
||||
|
||||
tgba_condition -= satone_tgba_condition;
|
||||
|
||||
bdd all_props = bddtrue;
|
||||
bdd dest_condition;
|
||||
if (satone_tgba_condition == source->get_tgba_condition())
|
||||
while ((dest_condition = bdd_satoneset(all_props,
|
||||
atomic_propositions_set_, bddtrue)) != bddfalse)
|
||||
while ((dest_condition =
|
||||
bdd_satoneset(all_props,
|
||||
atomic_propositions_set_, bddtrue))
|
||||
!= bddfalse)
|
||||
{
|
||||
all_props -= dest_condition;
|
||||
state_ta_explicit* new_dest;
|
||||
|
|
@ -519,12 +507,12 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
dest_condition,
|
||||
false,
|
||||
sba_->state_is_accepting(tgba_state));
|
||||
|
||||
}
|
||||
else
|
||||
{
|
||||
new_dest = new state_ta_explicit
|
||||
(tgba_state->clone(), dest_condition, false, false);
|
||||
(tgba_state->clone(),
|
||||
dest_condition, false, false);
|
||||
}
|
||||
state_ta_explicit* dest = ta->add_state(new_dest);
|
||||
|
||||
|
|
@ -539,41 +527,37 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
todo.push(dest);
|
||||
}
|
||||
|
||||
ta->create_transition(source, bdd_setxor(
|
||||
source->get_tgba_condition(),
|
||||
dest->get_tgba_condition()),
|
||||
bdd cs = bdd_setxor(source->get_tgba_condition(),
|
||||
dest->get_tgba_condition());
|
||||
ta->create_transition(source, cs,
|
||||
tgba_acceptance_conditions, dest);
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
tgba_state->destroy();
|
||||
}
|
||||
delete tgba_succ_it;
|
||||
|
||||
}
|
||||
|
||||
state_ta_explicit* artificial_livelock_accepting_state = 0;
|
||||
state_ta_explicit* artificial_livelock_acc_state = 0;
|
||||
|
||||
trace << "*** build_ta: artificial_livelock_accepting_state_mode = ***"
|
||||
trace << "*** build_ta: artificial_livelock_acc_state_mode = ***"
|
||||
<< artificial_livelock_state_mode << std::endl;
|
||||
|
||||
if (artificial_livelock_state_mode)
|
||||
{
|
||||
single_pass_emptiness_check = true;
|
||||
artificial_livelock_accepting_state = new state_ta_explicit(
|
||||
ta->get_tgba()->get_init_state(), bddtrue, false, false, true, 0);
|
||||
artificial_livelock_acc_state =
|
||||
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue,
|
||||
false, false, true, 0);
|
||||
trace
|
||||
<< "*** build_ta: artificial_livelock_accepting_state = ***"
|
||||
<< artificial_livelock_accepting_state << std::endl;
|
||||
|
||||
<< "*** build_ta: artificial_livelock_acc_state = ***"
|
||||
<< artificial_livelock_acc_state << std::endl;
|
||||
}
|
||||
|
||||
compute_livelock_acceptance_states(ta, single_pass_emptiness_check,
|
||||
artificial_livelock_accepting_state);
|
||||
|
||||
artificial_livelock_acc_state);
|
||||
return ta;
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
ta_explicit*
|
||||
|
|
@ -616,7 +600,6 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
|
||||
if (state->is_accepting_state())
|
||||
{
|
||||
|
||||
state_ta_explicit::transitions* trans = state->get_transitions();
|
||||
state_ta_explicit::transitions::iterator it_trans;
|
||||
|
||||
|
|
@ -625,23 +608,18 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
{
|
||||
(*it_trans)->acceptance_conditions
|
||||
= ta->all_acceptance_conditions();
|
||||
|
||||
}
|
||||
|
||||
state->set_accepting_state(false);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
return ta;
|
||||
}
|
||||
|
||||
tgta_explicit*
|
||||
tgba_to_tgta(const tgba* tgba_, bdd atomic_propositions_set_)
|
||||
{
|
||||
|
||||
state* tgba_init_state = tgba_->get_init_state();
|
||||
state_ta_explicit* artificial_init_state = new state_ta_explicit(
|
||||
tgba_init_state->clone(), bddfalse, true);
|
||||
|
|
@ -681,14 +659,12 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
|
|||
state_ta_explicit::transitions* trans = state->get_transitions();
|
||||
if (state->is_livelock_accepting_state())
|
||||
{
|
||||
|
||||
bool trans_empty = (trans == 0 || trans->empty());
|
||||
if (trans_empty || state->is_accepting_state())
|
||||
{
|
||||
ta->create_transition(state, bdd_stutering_transition,
|
||||
ta->all_acceptance_conditions(), state);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
if (state->compare(ta->get_artificial_initial_state()))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue