diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 479a246ea..a27a3dc7c 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -97,7 +97,7 @@ to_int(const char* s) // GF(p_1) & GF(p_2) & ... & GF(p_n) -formula* GF_n(spot::ltl::atomic_prop_set* ap, int n) +formula* GF_n(spot::ltl::atomic_prop_set* ap) { formula* result = 0; @@ -358,10 +358,6 @@ main(int argc, char** argv) while (max_tries_r--) { f = rf->generate(opt_f); - if (opt_wFair) - { - f = GF_n(atomic_prop_collect(f, 0), f->hash()); - } if (opt_r) { const spot::ltl::formula* g = simp.simplify(f); @@ -386,6 +382,14 @@ main(int argc, char** argv) continue; } } + + if (opt_wFair) + { + spot::ltl::formula* g = GF_n(atomic_prop_collect(f, 0)); + f = spot::ltl::unop::instance(unop::Not, + spot::ltl::binop::instance(binop::Implies, g, f)); + } + break; } if (max_tries_r < 0) diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 80cf9f92b..bce8fe137 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -71,7 +71,11 @@ namespace spot const ta* t, const kripke* k) : source_(s), ta_(t), kripke_(k) { - kripke_succ_it_ = k->succ_iter(s->get_kripke_state()); + kripke_source_condition = kripke_->state_condition(s->get_kripke_state()); + + kripke_succ_it_ = kripke_->succ_iter(s->get_kripke_state()); + kripke_current_dest_state = 0; + ta_succ_it_ = 0; current_state_ = 0; } @@ -82,6 +86,8 @@ namespace spot current_state_ = 0; delete ta_succ_it_; delete kripke_succ_it_; + if (kripke_current_dest_state != 0) + kripke_current_dest_state->destroy(); } void @@ -93,18 +99,27 @@ namespace spot { delete ta_succ_it_; ta_succ_it_ = 0; - kripke_succ_it_->next(); + next_kripke_dest(); } } void - ta_succ_iterator_product::first() + ta_succ_iterator_product::next_kripke_dest() { if (!kripke_succ_it_) return; - ta_succ_it_ = 0; - kripke_succ_it_->first(); + if (kripke_current_dest_state == 0) + { + kripke_succ_it_->first(); + } + else + { + kripke_current_dest_state->destroy(); + kripke_current_dest_state = 0; + kripke_succ_it_->next(); + } + // If one of the two successor sets is empty initially, we reset // kripke_succ_it_, so that done() can detect this situation easily. (We // choose to reset kripke_succ_it_ because this variable is already used by @@ -116,7 +131,34 @@ namespace spot return; } - next_non_stuttering_(); + kripke_current_dest_state = kripke_succ_it_->current_state(); + bdd kripke_current_dest_condition = kripke_->state_condition( + kripke_current_dest_state); + is_stuttering_transition_ = (kripke_source_condition + == kripke_current_dest_condition); + if (is_stuttering_transition_) + { + current_condition_ = bddtrue; + } + else + { + current_condition_ = bdd_setxor(kripke_source_condition, + kripke_current_dest_condition); + ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), + current_condition_); + ta_succ_it_->first(); + } + + } + + void + ta_succ_iterator_product::first() + { + + next_kripke_dest(); + + if (!done()) + next_non_stuttering_(); } void @@ -126,53 +168,38 @@ namespace spot current_state_ = 0; if (is_stuttering_transition()) { - ta_succ_it_ = 0; - kripke_succ_it_->next(); + next_kripke_dest(); } else step_(); if (!done()) - next_non_stuttering_(); + next_non_stuttering_(); + } void ta_succ_iterator_product::next_non_stuttering_() { - bdd sc = kripke_->state_condition(source_->get_kripke_state()); - while (!done()) { - state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); - bdd dc = kripke_->state_condition(kripke_succ_it_current_state); - is_stuttering_transition_ = (sc == dc); if (is_stuttering_transition_) { //if stuttering transition, the TA automata stays in the same state current_state_ = new state_ta_product(source_->get_ta_state(), - kripke_succ_it_current_state); - current_condition_ = bddtrue; + kripke_current_dest_state->clone()); return; } - if (ta_succ_it_ == 0) - { - current_condition_ = bdd_setxor(sc, dc); - ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), - current_condition_); - ta_succ_it_->first(); - } - if (!ta_succ_it_->done()) { current_state_ = new state_ta_product(ta_succ_it_->current_state(), - kripke_succ_it_current_state); + kripke_current_dest_state->clone()); return; } - kripke_succ_it_current_state->destroy(); step_(); } } @@ -201,9 +228,9 @@ namespace spot ta_succ_iterator_product::is_stuttering_transition() const { // assert(!done()); - // bdd sc = kripke_->state_condition(source_->get_kripke_state()); + // bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state()); // state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); - // bdd dc = kripke_->state_condition(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_; @@ -213,11 +240,11 @@ namespace spot ta_succ_iterator_product::current_condition() const { // assert(!done()); - // bdd sc = kripke_->state_condition(source_->get_kripke_state()); + // bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state()); // state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); - // bdd dc = kripke_->state_condition(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(sc, dc); + // return bdd_setxor(kripke_source_condition, kripke_current_dest_condition); return current_condition_; } diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index 9ab38995c..e79df4bc5 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -77,7 +77,8 @@ namespace spot class ta_succ_iterator_product : public ta_succ_iterator { public: - ta_succ_iterator_product(const state_ta_product* s, const ta* t, const kripke* k); + ta_succ_iterator_product(const state_ta_product* s, const ta* t, + const kripke* k); virtual ~ta_succ_iterator_product(); @@ -106,6 +107,10 @@ namespace spot step_(); void next_non_stuttering_(); + + void + next_kripke_dest(); + //@} protected: @@ -117,6 +122,8 @@ namespace spot state_ta_product* current_state_; bdd current_condition_; bool is_stuttering_transition_; + bdd kripke_source_condition; + state * kripke_current_dest_state; }; @@ -136,9 +143,11 @@ namespace spot succ_iter(const spot::state* s) const; virtual ta_succ_iterator_product* - succ_iter(const spot::state* s, bdd condition) const { + succ_iter(const spot::state* s, bdd condition) const + { - if(condition == bddtrue) return succ_iter(s); + if (condition == bddtrue) + return succ_iter(s); //TODO return 0; } diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index a4f65f652..e2a4d6e5d 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -254,7 +254,9 @@ namespace spot } } - if (!G->empty()) + delete I; + + if (!G->empty()) { unsigned s = G->size(); unsigned num = ++set_num;