From 2aad5b10d2d114b2ffeffcf0060aa71971295f34 Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Wed, 6 Apr 2011 22:15:05 +0200 Subject: [PATCH] TA Product optimization and WFair Formulas generation * src/ta/taproduct.cc: TA Product optimization * src/ltltest/randltl.cc: WFair Formulas generation --- src/ltltest/randltl.cc | 47 +++++++++++++++++++ src/ta/taproduct.cc | 101 +++++++++++++++++++++-------------------- 2 files changed, 98 insertions(+), 50 deletions(-) diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 2461532fc..479a246ea 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -28,6 +28,7 @@ #include #include #include +#include #include "ltlast/atomic_prop.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" @@ -36,6 +37,14 @@ #include "ltlenv/defaultenv.hh" #include "misc/random.hh" +#include "ltlast/allnodes.hh" + + +using namespace spot; +using namespace spot::ltl; + +environment& env(default_environment::instance()); + void syntax(char* prog) { @@ -86,6 +95,35 @@ to_int(const char* s) return res; } + +// GF(p_1) & GF(p_2) & ... & GF(p_n) +formula* GF_n(spot::ltl::atomic_prop_set* ap, int n) +{ + + formula* result = 0; + + multop::type op = multop::And; + + spot::ltl::atomic_prop_set::const_iterator i = ap->begin(); + while (i != ap->end()) + { + + std::ostringstream p; + p << (*i)->name(); + ++i; + formula* f = unop::instance(unop::G, + unop::instance(unop::F, + env.require(p.str()))); + + if (result) + result = multop::instance(op, f, result); + else + result = f; + } + return result; +} + + int main(int argc, char** argv) { @@ -102,6 +140,7 @@ main(int argc, char** argv) bool opt_u = false; spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true); spot::ltl::ltl_simplifier simp(simpopt); + bool opt_wFair = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; @@ -183,6 +222,10 @@ main(int argc, char** argv) { opt_u = true; } + else if (!strcmp(argv[argn], "-wf")) + { + opt_wFair = true; + } else { ap->insert(static_cast @@ -315,6 +358,10 @@ 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); diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 51710649b..80cf9f92b 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -31,7 +31,7 @@ namespace spot state_ta_product::state_ta_product(const state_ta_product& o) : state(), ta_state_(o.get_ta_state()), kripke_state_( - o.get_kripke_state()->clone()) + o.get_kripke_state()->clone()) { } @@ -91,9 +91,9 @@ namespace spot ta_succ_it_->next(); if (ta_succ_it_->done()) { - delete ta_succ_it_; - ta_succ_it_ = 0; - kripke_succ_it_->next(); + delete ta_succ_it_; + ta_succ_it_ = 0; + kripke_succ_it_->next(); } } @@ -111,9 +111,9 @@ namespace spot // done().) if (kripke_succ_it_->done()) { - delete kripke_succ_it_; - kripke_succ_it_ = 0; - return; + delete kripke_succ_it_; + kripke_succ_it_ = 0; + return; } next_non_stuttering_(); @@ -126,8 +126,8 @@ namespace spot current_state_ = 0; if (is_stuttering_transition()) { - ta_succ_it_ = 0; - kripke_succ_it_->next(); + ta_succ_it_ = 0; + kripke_succ_it_->next(); } else step_(); @@ -144,34 +144,36 @@ namespace spot while (!done()) { - state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); - bdd dc = kripke_->state_condition(kripke_succ_it_current_state); + 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; - return; - } + 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; + 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_ == 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); - return; - } + if (!ta_succ_it_->done()) + { + current_state_ = new state_ta_product(ta_succ_it_->current_state(), + kripke_succ_it_current_state); + return; + } - kripke_succ_it_current_state->destroy(); - step_(); + kripke_succ_it_current_state->destroy(); + step_(); } } @@ -227,7 +229,7 @@ namespace spot ta_product::ta_product(const ta* testing_automata, const kripke* kripke_structure) : dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_( - kripke_structure) + kripke_structure) { assert(dict_ == kripke_structure->get_dict()); dict_->register_all_variables_of(&ta_, this); @@ -249,25 +251,24 @@ namespace spot ta::states_set_t::const_iterator it; ta::states_set_t initial_states_set; + state* kripke_init_state = kripke_->get_init_state(); + bdd kripke_init_state_condition = kripke_->state_condition( + kripke_init_state); for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) { - state* kripke_init_state = kripke_->get_init_state(); - if ((kripke_->state_condition(kripke_init_state)) - == (ta_->get_state_condition(*it))) - { - state_ta_product* stp = new state_ta_product((*it), - kripke_init_state); - initial_states_set.insert(stp); - } - else - { - kripke_init_state->destroy(); - } + if (kripke_init_state_condition == (ta_->get_state_condition(*it))) + { + state_ta_product* stp = new state_ta_product((*it), + kripke_init_state->clone()); + + initial_states_set.insert(stp); + } } + kripke_init_state->destroy(); return initial_states_set; } @@ -292,7 +293,7 @@ namespace spot const state_ta_product* s = down_cast (state); assert(s); return kripke_->format_state(s->get_kripke_state()) + " * \n" - + ta_->format_state(s->get_ta_state()); + + ta_->format_state(s->get_ta_state()); } bool @@ -323,9 +324,9 @@ namespace spot state* kr_s = stp->get_kripke_state(); return (ta_->is_initial_state(ta_s)) - && ((kripke_->get_init_state())->compare(kr_s) == 0) - && ((kripke_->state_condition(kr_s)) - == (ta_->get_state_condition(ta_s))); + && ((kripke_->get_init_state())->compare(kr_s) == 0) + && ((kripke_->state_condition(kr_s)) + == (ta_->get_state_condition(ta_s))); } bdd