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

80 columns.

Browse source 
* src/ltlvisit/apcollect.hh, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/tgbatest/ltl2tgba.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2012-08-21 14:18:13 +02:00
parent 173e100a41
commit aa230d1f8b
4 changed files with 33 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ltlvisit/apcollect.hh
View file

@ -53,7 +53,8 @@ namespace spot
atomic_prop_set* atomic_prop_set*
atomic_prop_collect(const formula* f, atomic_prop_set* s = 0); atomic_prop_collect(const formula* f, atomic_prop_set* s = 0);
/// \brief Return the set of atomic propositions occurring in a formula, as a BDD. /// \brief Return the set of atomic propositions occurring in a
/// formula, as a BDD.
/// ///
/// \param f the formula to inspect /// \param f the formula to inspect
/// \param a that automaton that should register the BDD variables used. /// \param a that automaton that should register the BDD variables used.

3
src/taalgos/minimize.cc
View file

@ -524,7 +524,8 @@ namespace spot
tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict()); tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict());
tgta_explicit* 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();

57
src/taalgos/tgba2ta.cc
View file

@ -272,9 +272,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
&& ((sscc.top().is_accepting) || (sscc.top().condition && ((sscc.top().is_accepting) || (sscc.top().condition
== testing_automata->all_acceptance_conditions())); == testing_automata->all_acceptance_conditions()));
trace trace << "*** sscc.size() = ***"
<< "*** sscc.size() = ***" << sscc.size() << std::endl;
<< sscc.size() << std::endl;
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((*i)); numbered_state_heap::state_index_p spi = h->index((*i));
@ -283,27 +282,27 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
*spi.second = -1; *spi.second = -1;
if (is_livelock_accepting_sscc) if (is_livelock_accepting_sscc)
{//if it is an accepting sscc add the state to {
//G (=the livelock-accepting states set) // if it is an accepting sscc add the state to
// G (=the livelock-accepting states set)
trace << "*** sscc.size() > 1: states: ***" trace << "*** sscc.size() > 1: states: ***"
<< testing_automata->format_state(*i) << testing_automata->format_state(*i)
<< std::endl; << std::endl;
state_ta_explicit * livelock_accepting_state = state_ta_explicit * livelock_accepting_state =
down_cast<state_ta_explicit*> (*i); down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state( livelock_accepting_state->
true); set_livelock_accepting_state(true);
if (single_pass_emptiness_check)
{
livelock_accepting_state->set_accepting_state(
true);
livelock_accepting_state->stuttering_reachable_livelock
= livelock_accepting_state;
}
if (single_pass_emptiness_check)
{
livelock_accepting_state
->set_accepting_state(true);
livelock_accepting_state
->stuttering_reachable_livelock
= livelock_accepting_state;
}
} }
} }
assert(!arc.empty()); assert(!arc.empty());
@ -474,8 +473,9 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
} }
else else
{ {
init_state = new state_ta_explicit(tgba_init_state->clone(), init_state =
satone_tgba_condition, true, false); new state_ta_explicit(tgba_init_state->clone(),
satone_tgba_condition, true, false);
} }
state_ta_explicit* s = ta->add_state(init_state); state_ta_explicit* s = ta->add_state(init_state);
@ -491,8 +491,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* source = todo.top(); state_ta_explicit* source = todo.top();
todo.pop(); todo.pop();
tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( tgba_succ_iterator* tgba_succ_it =
source->get_tgba_state()); 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(); const state* tgba_state = tgba_succ_it->current_state();
@ -557,8 +557,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state = 0; state_ta_explicit* artificial_livelock_accepting_state = 0;
trace trace << "*** build_ta: artificial_livelock_accepting_state_mode = ***"
<< "*** build_ta: artificial_livelock_accepting_state_mode = ***"
<< artificial_livelock_state_mode << std::endl; << artificial_livelock_state_mode << std::endl;
if (artificial_livelock_state_mode) if (artificial_livelock_state_mode)
@ -589,11 +588,11 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
state* tgba_init_state = tgba_->get_init_state(); state* tgba_init_state = tgba_->get_init_state();
if (artificial_initial_state_mode) if (artificial_initial_state_mode)
{ {
state_ta_explicit* artificial_init_state = new state_ta_explicit( state_ta_explicit* artificial_init_state =
tgba_init_state->clone(), bddfalse, true); new state_ta_explicit(tgba_init_state->clone(), bddfalse, true);
ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(), ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(),
artificial_init_state); artificial_init_state);
} }
else else
{ {
@ -623,7 +622,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit::transitions* trans = state->get_transitions(); state_ta_explicit::transitions* trans = state->get_transitions();
state_ta_explicit::transitions::iterator it_trans; state_ta_explicit::transitions::iterator it_trans;
for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) for (it_trans = trans->begin(); it_trans != trans->end();
it_trans++)
{ {
(*it_trans)->acceptance_conditions (*it_trans)->acceptance_conditions
= ta->all_acceptance_conditions(); = ta->all_acceptance_conditions();
@ -694,7 +694,8 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
} }
if (state->compare(ta->get_artificial_initial_state())) if (state->compare(ta->get_artificial_initial_state()))
ta->create_transition(state, bdd_stutering_transition, bddfalse, state); ta->create_transition(state, bdd_stutering_transition,
bddfalse, state);
state->set_livelock_accepting_state(false); state->set_livelock_accepting_state(false);
state->set_accepting_state(false); state->set_accepting_state(false);
@ -702,7 +703,5 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata,
} }
return tgta; return tgta;
} }
} }

2
src/tgbatest/ltl2tgba.cc
View file

@ -1174,7 +1174,7 @@ main(int argc, char** argv)
{ {
case 0: case 0:
spot::dotty_reachable(std::cout, spot::dotty_reachable(std::cout,
dynamic_cast<spot::tgta_explicit*>(a)->get_ta()); dynamic_cast<spot::tgta_explicit*>(a)->get_ta());
break; break;
case 12: case 12:
stats_reachable(a).dump(std::cout); stats_reachable(a).dump(std::cout);