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

Cleaning code of TA Product and Emptiness-check

Browse source 
* src/ta/taproduct.cc, src/taalgos/emptinessta.cc:
remove unused (commented) code.
This commit is contained in:
Ala-Eddine Ben-Salem 2011-12-06 16:01:37 +01:00 • committed by Alexandre Duret-Lutz
parent d64b40452c
commit db2fcfa97a
2 changed files with 1 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ta/taproduct.cc
View file

@ -216,52 +216,24 @@ namespace spot
state_ta_product* state_ta_product*
ta_succ_iterator_product::current_state() const ta_succ_iterator_product::current_state() const
{ {
//assert(!done());
//if stuttering transition, the TA automata stays in the same state
// if (is_stuttering_transition())
// return new state_ta_product(source_->get_ta_state(),
// kripke_succ_it_->current_state());
//
// return new state_ta_product(ta_succ_it_->current_state(),
// kripke_succ_it_->current_state());
return current_state_->clone(); return current_state_->clone();
} }
bool bool
ta_succ_iterator_product::is_stuttering_transition() const ta_succ_iterator_product::is_stuttering_transition() const
{ {
// assert(!done());
// bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state());
// state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
// bdd kripke_current_dest_condition = kripke_->state_condition(kripke_succ_it_current_state);
// delete kripke_succ_it_current_state;
return is_stuttering_transition_; return is_stuttering_transition_;
} }
bdd bdd
ta_succ_iterator_product::current_condition() const ta_succ_iterator_product::current_condition() const
{ {
// assert(!done());
// bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state());
// state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
// bdd kripke_current_dest_condition = kripke_->state_condition(kripke_succ_it_current_state);
// delete kripke_succ_it_current_state;
// return bdd_setxor(kripke_source_condition, kripke_current_dest_condition);
return current_condition_; return current_condition_;
} }
bdd bdd
ta_succ_iterator_product::current_acceptance_conditions() const ta_succ_iterator_product::current_acceptance_conditions() const
{ {
// assert(!done());
// bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state());
// state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
// bdd kripke_current_dest_condition = kripke_->state_condition(kripke_succ_it_current_state);
// delete kripke_succ_it_current_state;
// return bdd_setxor(kripke_source_condition, kripke_current_dest_condition);
return current_acceptance_conditions_; return current_acceptance_conditions_;
} }
@ -382,7 +354,6 @@ namespace spot
return 0; return 0;
} }
//TODO BUG FIX
bool bool
ta_product::is_initial_state(const spot::state* s) const ta_product::is_initial_state(const spot::state* s) const
{ {

2
src/taalgos/emptinessta.cc
View file

@ -216,7 +216,7 @@ namespace spot
(a_->is_hole_state_in_ta_component(curr)) (a_->is_hole_state_in_ta_component(curr))
&& a_->is_livelock_accepting_state(curr); && a_->is_livelock_accepting_state(curr);
//may be Buchi accepting scc or livelock accepting scc (contains a TA "hole and livelock accepting state") //may be Buchi accepting scc or livelock accepting scc (contains a livelock accepting state that have no successors in TA)
scc.top().is_accepting = (a_->is_accepting_state(curr) scc.top().is_accepting = (a_->is_accepting_state(curr)
&& (!succ->is_stuttering_transition() && (!succ->is_stuttering_transition()
|| a_->is_livelock_accepting_state(curr))) || a_->is_livelock_accepting_state(curr)))