From c769f74750ac9bff9fcab89d2a4b6a9e67fdb3d3 Mon Sep 17 00:00:00 2001 From: martinez Date: Thu, 17 Jun 2004 16:27:36 +0000 Subject: [PATCH] * src/tgbatest/spotlbtt.test: We don't check the post-reduction with scc and delayed simulation. * src/tgbatest/ltl2tgba.cc: Adjust parameters. * src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test. * src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs. * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: Remove some useless comments. * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC. * src/ltlvisit/reducform.cc: Correct some bug for multop. * src/ltltest/reduccmp.test: More Test. * src/ltltest/reduc.cc: Thinko * src/ltltest/equals.cc: Reduction compare --- ChangeLog | 17 +++ src/ltltest/equals.cc | 3 - src/ltltest/reduc.cc | 3 +- src/ltltest/reduccmp.test | 37 +++++- src/ltltest/syntimpl.test | 33 +++--- src/ltlvisit/reducform.cc | 96 +++++++-------- src/tgba/tgbareduc.cc | 183 +++++++++++++++++------------ src/tgba/tgbareduc.hh | 1 + src/tgbaalgos/reductgba_sim.cc | 24 +++- src/tgbaalgos/reductgba_sim.hh | 8 +- src/tgbaalgos/reductgba_sim_del.cc | 65 +++++++--- src/tgbatest/Makefile.am | 4 + src/tgbatest/ltl2tgba.cc | 28 ++--- src/tgbatest/reductgba.cc | 100 ++++++++++------ src/tgbatest/reductgba.test | 73 +++++++++--- src/tgbatest/spotlbtt.test | 4 +- 16 files changed, 429 insertions(+), 250 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6756e5a6a..6adbd71e7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2004-06-17 Thomas Martinez + + * src/tgbatest/spotlbtt.test: We don't check the post-reduction + with scc and delayed simulation. + + * src/tgbatest/ltl2tgba.cc: Adjust parameters. + * src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test. + * src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs. + * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: + Remove some useless comments. + * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC. + + * src/ltlvisit/reducform.cc: Correct some bug for multop. + * src/ltltest/reduccmp.test: More Test. + * src/ltltest/reduc.cc: Thinko + * src/ltltest/equals.cc: Reduction compare + 2004-06-17 Alexandre Duret-Lutz * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s. diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index f66d57647..a1650f3fc 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -84,11 +84,8 @@ main(int argc, char** argv) spot::ltl::formula* tmp; tmp = f1; f1 = spot::ltl::reduce(f1); - //std::string f2s = spot::ltl::to_string(f2); - //std::string f1s = spot::ltl::to_string(f1); spot::ltl::destroy(tmp); spot::ltl::dump(std::cout, f1); - //std::cout << f1s << " // " << f2s << std::endl; #endif int exit_code = f1 != f2; diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 5c6933f65..a3f2b2d18 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -179,6 +179,5 @@ main(int argc, char** argv) assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - //return exit_code; - return 0; + return exit_code; } diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 08ffe982e..0fd175b33 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -25,6 +25,38 @@ . ./defs || exit 1 +# No reduction +run 0 ./reduccmp 'a U b' 'a U b' +run 0 ./reduccmp 'a R b' 'a R b' +run 0 ./reduccmp 'a & b' 'a & b' +run 0 ./reduccmp 'a | b' 'a | b' +run 0 ./reduccmp 'a & (a U b)' 'a & (a U b)' +run 0 ./reduccmp 'a | (a U b)' 'a | (a U b)' + +# Syntactic reduction +run 0 ./reduccmp 'a & (!b R !a)' 'false' +run 0 ./reduccmp '(!b R !a) & a' 'false' +run 0 ./reduccmp '(!b R !a) | a' 'true' +run 0 ./reduccmp 'a | (!b R !a)' 'true' + +run 0 ./reduccmp 'a & (!b R !a) & c' 'false' +run 0 ./reduccmp 'c & (!b R !a) & a' 'false' +run 0 ./reduccmp 'a | (!b R !a) | c' 'true' +run 0 ./reduccmp 'c | (!b R !a) | a' 'true' + +run 0 ./reduccmp 'a & (b U a)' 'a' +run 0 ./reduccmp '(b U a) & a' 'a' +run 0 ./reduccmp 'a | (b U a)' '(b U a)' +run 0 ./reduccmp '(b U a) | a' '(b U a)' +run 0 ./reduccmp 'a U (b U a)' '(b U a)' + +run 0 ./reduccmp 'a & (b U a) & a' 'a' +run 0 ./reduccmp 'a & (b U a) & a' 'a' +run 0 ./reduccmp 'a | (b U a) | a' '(b U a)' +run 0 ./reduccmp 'a | (b U a) | a' '(b U a)' +run 0 ./reduccmp 'a U (b U a)' '(b U a)' + + # Basics reduction run 0 ./reduccmp 'X(true)' 'true' run 0 ./reduccmp 'X(false)' 'false' @@ -67,8 +99,3 @@ run 0 ./reduccmp 'Ga' 'Ga' run 0 ./reduccmp 'GFGa' 'FGa' run 0 ./reduccmp 'b R Ga' 'Ga' run 0 ./reduccmp 'b R FGa' 'FGa' - -# Syntactic reduction -run 0 ./reduccmp 'a & (b U a)' 'a' -run 0 ./reduccmp 'a | (b U a)' '(b U a)' -run 0 ./reduccmp 'a U (b U a)' '(b U a)' diff --git a/src/ltltest/syntimpl.test b/src/ltltest/syntimpl.test index 79ccd3dc5..aadbb125e 100755 --- a/src/ltltest/syntimpl.test +++ b/src/ltltest/syntimpl.test @@ -33,21 +33,6 @@ run 1 ./syntimpl 0 '(e R f)' '(g U f)' run 1 ./syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))' run 1 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)' -run 0 ./syntimpl 0 'Xa' 'XX(b U a)' -run 0 ./syntimpl 0 'XXa' 'X(b U a)' - -run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))' -run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)' - -run 0 ./syntimpl 0 'a' 'b' -run 0 ./syntimpl 0 'a' 'b + c' -run 0 ./syntimpl 0 'a + b' 'a' -run 0 ./syntimpl 0 'a' 'a * c' -run 0 ./syntimpl 0 'a * b' 'c' -run 0 ./syntimpl 0 'a' 'a U b' -run 0 ./syntimpl 0 'a' 'a R b' -run 0 ./syntimpl 0 'a R b' 'a' - run 1 ./syntimpl 0 '1' '1' run 1 ./syntimpl 0 '0' '0' @@ -81,3 +66,21 @@ run 1 ./syntimpl 0 'a R b' '1 R b' run 1 ./syntimpl 0 'b * (a U b)' 'a U b' run 1 ./syntimpl 0 'a U b' 'c + (a U b)' + +run 0 ./syntimpl 0 'Xa' 'XX(b U a)' +run 0 ./syntimpl 0 'XXa' 'X(b U a)' + +run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))' +run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)' + +run 0 ./syntimpl 0 'a' 'b' +run 0 ./syntimpl 0 'a' 'b + c' +run 0 ./syntimpl 0 'a + b' 'a' +run 0 ./syntimpl 0 'a' 'a * c' +run 0 ./syntimpl 0 'a * b' 'c' +run 0 ./syntimpl 0 'a' 'a U b' +run 0 ./syntimpl 0 'a' 'a R b' +run 0 ./syntimpl 0 'a R b' 'a' + +run 0 ./syntimpl 0 'p2' 'p3 || G(p2 && p5)' +run 0 ./syntimpl 0 '!(p3 || G(p2 && p5))' '!p2' \ No newline at end of file diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index 9a594f88c..47c15cab2 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -201,81 +201,71 @@ namespace spot if (opt_ & Reduce_Syntactic_Implications) { - formula* f1; - formula* f2; - multop::vec::iterator index = res->begin(); - multop::vec::iterator indextmp = index; - switch (mo->op()) - { - case multop::Or: - if (index != res->end()) - break; - f1 = *index++; - for (; index != res->end(); index++) - { - f2 = *index; - /* a < b => a + b = b */ - if (syntactic_implication(f1, f2)) // f1 < f2 - { - f1 = f2; - destroy(*indextmp); - res->erase(indextmp); - indextmp = index; - index--; - } - else if (syntactic_implication(f2, f1)) // f2 < f1 - { - destroy(*index); - res->erase(index); - index--; - } - } - break; - case multop::And: - if (index != res->end()) - break; - f1 = *index++; - for (; index != res->end(); index++) + bool removed = true;; + multop::vec::iterator f1; + multop::vec::iterator f2; + + while (removed) + { + removed = false; + f2 = f1 = res->begin(); + ++f1; + while (f1 != res->end()) { - f2 = *index; - /* a < b => a & b = a */ - if (syntactic_implication(f1, f2)) // f1 < f2 + assert(f1 != f2); + // a < b => a + b = b + // a < b => a & b = a + if ((syntactic_implication(*f1, *f2) && // f1 < f2 + (mo->op() == multop::Or)) || + ((syntactic_implication(*f2, *f1)) && // f2 < f1 + (mo->op() == multop::And))) { - destroy(*index); - res->erase(index); - index--; + // We keep f2 + destroy(*f1); + res->erase(f1); + removed = true; + break; } - else if (syntactic_implication(f2, f1)) // f2 < f1 + else if ((syntactic_implication(*f2, *f1) && // f2 < f1 + (mo->op() == multop::Or)) || + ((syntactic_implication(*f1,* f2)) && // f1 < f2 + (mo->op() == multop::And))) { - f1 = f2; - destroy(*indextmp); - res->erase(indextmp); - indextmp = index; - index--; + // We keep f1 + destroy(*f2); + res->erase(f2); + removed = true; + break; } + else + ++f1; } - break; } + // FIXME /* f1 < !f2 => f1 & f2 = false !f1 < f2 => f1 | f2 = true */ - for (index = res->begin(); index != res->end(); index++) - for (indextmp = res->begin(); indextmp != res->end(); indextmp++) - if (index != indextmp - && syntactic_implication_neg(*index, *indextmp, - mo->op() != multop::Or)) + for (f1 = res->begin(); f1 != res->end(); f1++) + for (f2 = res->begin(); f2 != res->end(); f2++) + if (f1 != f2 && + syntactic_implication_neg(*f1, *f2, + mo->op() != multop::Or)) { for (multop::vec::iterator j = res->begin(); j != res->end(); j++) destroy(*j); + res->clear(); + delete res; if (mo->op() == multop::Or) result_ = constant::true_instance(); else result_ = constant::false_instance(); return; } + } + if (res->size()) { result_ = multop::instance(mo->op(), res); diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index 168a28172..15a5c60f0 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -131,17 +131,15 @@ namespace spot const state_explicit* se = dynamic_cast(s); assert(se); sn_map::const_iterator i = state_name_map_.find(se->get_state()); - //seen_map::const_iterator j = si_.find(s); + seen_map::const_iterator j = si_.find(s); assert(i != state_name_map_.end()); - /* if (j != si_.end()) // SCC have been computed { os << ", SCC " << j->second; return i->second + std::string(os.str()); } else - */ - return i->second; + return i->second; } int @@ -244,8 +242,10 @@ namespace spot bdd cond_simul; bdd acc_simul; std::list ltmp; - const tgba_explicit::state* s1 = name_state_map_[this->format_state(s)]; - const tgba_explicit::state* s2 = name_state_map_[this->format_state(simul)]; + const tgba_explicit::state* s1 = + name_state_map_[tgba_explicit::format_state(s)]; + const tgba_explicit::state* s2 = + name_state_map_[tgba_explicit::format_state(simul)]; sp_map::iterator i = state_predecessor_map_.find(s1); if (i == state_predecessor_map_.end()) // 0 predecessor @@ -325,11 +325,13 @@ namespace spot // But it can be have some predecessor in state_predecessor_map_ !! // So, we remove from it. - ns_map::iterator k = name_state_map_.find(format_state(s)); + ns_map::iterator k = + name_state_map_.find(tgba_explicit::format_state(s)); if (k == name_state_map_.end()) // 0 predecessor return; - tgba_explicit::state* st = name_state_map_[format_state(s)]; + tgba_explicit::state* st = + name_state_map_[tgba_explicit::format_state(s)]; // for all successor q of s, we remove s of the predecessor of q. @@ -370,8 +372,10 @@ namespace spot void tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2) { - const tgba_explicit::state* s1 = name_state_map_[this->format_state(sim1)]; - const tgba_explicit::state* s2 = name_state_map_[this->format_state(sim2)]; + const tgba_explicit::state* s1 = + name_state_map_[tgba_explicit::format_state(sim1)]; + const tgba_explicit::state* s2 = + name_state_map_[tgba_explicit::format_state(sim2)]; const tgba_explicit::state* stmp = s1; const spot::state* simtmp = sim1; @@ -424,6 +428,7 @@ namespace spot ///////////////////////////////////////// + // From gtec.cc void tgba_reduc::remove_component(const spot::state* from) { @@ -459,6 +464,7 @@ namespace spot } } + // From gtec.cc void tgba_reduc::compute_scc() { @@ -558,6 +564,8 @@ namespace spot void tgba_reduc::delete_scc() { + std::cout << "delete_scc" << std::endl; + bool change = true; Sgi::hash_map::iterator i; Sgi::hash_map::iterator itmp; @@ -570,77 +578,23 @@ namespace spot change = false; for (i = state_scc_v_.begin(); i != state_scc_v_.end();) { - //std::cout << "Is terminal ? : " << std::endl; - if (is_terminal(i->second)) + std::cout << "delete_scc : [" + << this->format_state(i->second) + << "]" + << "is_terminal ??" << std::endl; + if (is_terminal(i->second)) { - //std::cout << " YES" << std::endl; - change = true; - this->remove_scc(const_cast(i->second)); + //change = true; + change = false; + //this->remove_scc(const_cast(i->second)); itmp = i; - ++i; - state_scc_v_.erase(itmp); - } - else - { - ++i; - //std::cout << " NO "<< std::endl; + //state_scc_v_.erase(itmp); } + ++i; } } } - bool - tgba_reduc::is_alpha_ball(const spot::state* s, int n) - { - /// FIXME - - bool b = false; - - seen_map::const_iterator i; - if (n == -1) - { - acc_ == bddfalse; - b = true; - assert(seen_ == NULL); - seen_ = new seen_map(); - i = si_.find(s); - assert(i->first != NULL); - n = i->second; - } - - seen_map::const_iterator sm = seen_->find(s); - if (sm == seen_->end()) - { - seen_->insert(std::pair(s, 1)); - i = si_.find(s); - assert(i->first != 0); - if (n != i->second) - return false; - } - else - { - return true; - } - - bool ret = true; - tgba_succ_iterator* j = this->succ_iter(s); - for (j->first(); !j->done(); j->next()) - { - acc_ |= j->current_acceptance_conditions(); - ret &= this->is_terminal(j->current_state(), n); - } - - if (b) - { - delete seen_; - seen_ = NULL; - if (acc_ == this->all_acceptance_conditions()) - ret = false; - } - - return ret; - } - bool tgba_reduc::is_terminal(const spot::state* s, int n) { @@ -650,12 +604,18 @@ namespace spot // So we can remove it safely without change the // automaton language. + std::cout << "is_terminal : [" + << this->format_state(s) + << "]" + << std::endl; + bool b = false; + // First call of is_terminal // seen_map::const_iterator i; if (n == -1) { - acc_ == bddfalse; + acc_ = bddfalse; b = true; assert(seen_ == NULL); seen_ = new seen_map(); @@ -663,11 +623,13 @@ namespace spot assert(i->first != NULL); n = i->second; } + /////////////////////////////// seen_map::const_iterator sm = seen_->find(s); if (sm == seen_->end()) { // this state is visited for the first time. + std::cout << "first time" << std::endl; seen_->insert(std::pair(s, 1)); i = si_.find(s); assert(i->first != 0); @@ -675,19 +637,27 @@ namespace spot return false; } else + // This state is already visited. { - // This state is already visited. + std::cout << "second time" << std::endl; return true; } bool ret = true; + spot::state* s2; tgba_succ_iterator* j = this->succ_iter(s); + int nb_succ = 0; for (j->first(); !j->done(); j->next()) { + std::cout << "successor " << nb_succ++ << std::endl; + s2 = j->current_state(); acc_ |= j->current_acceptance_conditions(); - ret &= this->is_terminal(j->current_state(), n); + ret &= this->is_terminal(s2, n); + delete s2; } + delete j; + // First call of is_terminal // if (b) { delete seen_; @@ -695,6 +665,7 @@ namespace spot if (acc_ == this->all_acceptance_conditions()) ret = false; } + /////////////////////////////// return ret; } @@ -704,6 +675,8 @@ namespace spot { // To remove a scc, we remove all his state. + std::cout << "remove_scc" << std::endl; + seen_map::iterator sm = si_.find(s); sm = si_.find(s); int n = sm->second; @@ -748,6 +721,62 @@ namespace spot } } + bool + tgba_reduc::is_alpha_ball(const spot::state* s, bdd label, int n) + { + /// FIXME + // a SCC is alpha ball if she's terminal but with some acceptance + // condition, and all transition have the same label. + // So we replace this SCC by a single state. + + bool b = false; + + seen_map::const_iterator i; + if ((n == -1) && + (label == bddfalse)) + { + acc_ == bddfalse; + b = true; + assert(seen_ == NULL); + seen_ = new seen_map(); + i = si_.find(s); + assert(i->first != NULL); + n = i->second; + } + + seen_map::const_iterator sm = seen_->find(s); + if (sm == seen_->end()) + { + seen_->insert(std::pair(s, 1)); + i = si_.find(s); + assert(i->first != 0); + if (n != i->second) + return false; + } + else + { + return true; + } + + bool ret = true; + tgba_succ_iterator* j = this->succ_iter(s); + for (j->first(); !j->done(); j->next()) + { + acc_ |= j->current_acceptance_conditions(); + ret &= this->is_terminal(j->current_state(), n); + } + + if (b) + { + delete seen_; + seen_ = NULL; + if (acc_ == this->all_acceptance_conditions()) + ret = false; + } + + return ret; + } + //////// JUST FOR DEBUG ////////// void diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index 656825d03..f94685800 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -139,6 +139,7 @@ namespace spot /// } /// \endverbatim bool is_alpha_ball(const spot::state* s, + bdd label = bddfalse, int n = -1); // Return true if we can't reach a state with diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 3e50669d1..59fa4d68c 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -33,7 +33,6 @@ namespace spot { num_ = num; sc_ = new state_couple(d_node, s_node); - //lnode_succ = new Sgi::vector; lnode_succ = new sn_v; lnode_pred = new sn_v; this->not_win = false; @@ -48,33 +47,48 @@ namespace spot delete sc_; } - void + bool spoiler_node::add_succ(spoiler_node* n) { + /* + bool exist = false; + for (sn_v::iterator i = lnode_succ->begin(); + i != lnode_succ->end();) + if (*i == n) + exist = true; + if (exist) + return false; + */ lnode_succ->push_back(n); + return true; } void spoiler_node::del_succ(spoiler_node* n) { - //std::cout << "del_succ : begin" << std::endl; for (sn_v::iterator i = lnode_succ->begin(); i != lnode_succ->end();) { if (*i == n) { - //std::cout << "erase" << std::endl; i = lnode_succ->erase(i); } else ++i; } - //std::cout << "del_succ : end" << std::endl; } void spoiler_node::add_pred(spoiler_node* n) { + /* + bool exist = false; + for (sn_v::iterator i = lnode_pred->begin(); + i != lnode_pred->end();) + if (*i == n) + exist = true; + if (!exist) + */ lnode_pred->push_back(n); } diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index dd1cd53ac..27056bf39 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -132,7 +132,10 @@ namespace spot int num); virtual ~spoiler_node(); - void add_succ(spoiler_node* n); + /// \brief Add a successor. + /// Return true if \a n wasn't yet in the list of successor, + /// false eitherwise. + bool add_succ(spoiler_node* n); void del_succ(spoiler_node* n); virtual void add_pred(spoiler_node* n); virtual void del_pred(); @@ -300,7 +303,8 @@ namespace spot virtual void build_couple(); virtual void build_link(); void build_recurse_successor_spoiler(spoiler_node* sn); - void build_recurse_successor_duplicator(duplicator_node* dn); + void build_recurse_successor_duplicator(duplicator_node* dn, + spoiler_node* sn); /// \brief The Jurdzinski's lifting algorithm. void lift(); diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 5f42eda5b..06ec835f6 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -311,7 +311,7 @@ namespace spot */ } - + /* void parity_game_graph_delayed::build_couple() { @@ -512,8 +512,8 @@ namespace spot } } } + */ - /* // We build only node which are reachable void parity_game_graph_delayed::build_couple() @@ -546,13 +546,15 @@ namespace spot // We create when it's possible a duplicator node // and recursively his successor. - spot::state* s1 = NULL; - bool exist_pred = false; + //spot::state* s1 = NULL; + //bool exist_pred = false; sn_v::iterator i1; for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1) { + /* exist_pred = false; + // We check if there is a predecessor only if the duplicator // is the initial state. s1 = automata_->get_init_state(); @@ -577,6 +579,7 @@ namespace spot if (!exist_pred) continue; + */ // We add a link between a spoiler and a (new) duplicator. // The acc of the duplicator must contains the @@ -590,10 +593,15 @@ namespace spot void parity_game_graph_delayed::build_recurse_successor_spoiler(spoiler_node* sn) { + std::cout << "build_recurse_successor_spoiler" << std::endl; + tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); + int i = 0; for (si->first(); !si->done(); si->next()) { + std::cout << "transition " << i++ << std::endl; + bdd btmp = si->current_acceptance_conditions() | dynamic_cast(sn)-> get_acceptance_condition_visited(); @@ -614,10 +622,18 @@ namespace spot nb_node_parity_game++); duplicator_vertice_.push_back(dn); - sn->add_succ(dn); + // dn is already a successor of sn. + if (!(sn->add_succ(dn))) + continue; (dn)->add_pred(sn); - build_recurse_successor_duplicator(dn); + /* TEST + bdd btmp2 = + dynamic_cast(sn)-> + get_acceptance_condition_visited(); + */ + + build_recurse_successor_duplicator(dn, sn); } delete s; } @@ -629,12 +645,18 @@ namespace spot void parity_game_graph_delayed:: - build_recurse_successor_duplicator(duplicator_node* dn) + build_recurse_successor_duplicator(duplicator_node* dn, + spoiler_node* sn) { - tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); + std::cout << "build_recurse_successor_duplicator" << std::endl; + tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); + + int i = 0; for (si->first(); !si->done(); si->next()) { + std::cout << "transition " << i++ << std::endl; + bdd btmp = dynamic_cast(sn)-> get_acceptance_condition_visited(); @@ -648,17 +670,19 @@ namespace spot s = si->current_state(); if (s->compare(*i1) == 0) { - spoiler_node_delayed* sn + spoiler_node_delayed* sn_n = new spoiler_node_delayed(sn->get_spoiler_node(), *i1, - bddtmp2, + btmp2, nb_node_parity_game++); - spoiler_vertice_.push_back(n1); + spoiler_vertice_.push_back(sn_n); - sn->add_succ(dn); - (dn)->add_pred(sn); + // dn is already a successor of sn. + if (!(dn->add_succ(sn_n))) + continue; + (sn_n)->add_pred(dn); - build_recurse_successor_spoiler(sn); + build_recurse_successor_spoiler(sn_n); } delete s; @@ -668,7 +692,7 @@ namespace spot delete si; } - */ + void parity_game_graph_delayed::add_dup_node(state*, @@ -686,6 +710,7 @@ namespace spot while (change) { + std::cout << "prune::change = true" << std::endl; change = false; for (Sgi::vector::iterator i = duplicator_vertice_.begin(); @@ -716,7 +741,7 @@ namespace spot ++i; } } - + std::cout << "prune::change = false" << std::endl; } void @@ -728,6 +753,7 @@ namespace spot while (change) { + std::cout << "lift::change = true" << std::endl; change = false; for (Sgi::vector::iterator i = duplicator_vertice_.begin(); @@ -742,7 +768,7 @@ namespace spot change |= (*i)->set_win(); } } - + std::cout << "lift::change = false" << std::endl; } simulation_relation* @@ -792,10 +818,15 @@ namespace spot return; this->build_sub_set_acc_cond(); */ + std::cout << "build couple" << std::endl; this->build_couple(); + std::cout << "build link" << std::endl; this->build_link(); + std::cout << "prune" << std::endl; this->prune(); + std::cout << "lift" << std::endl; this->lift(); + std::cout << "END" << std::endl; //this->print(std::cout); } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 6acc0f366..76f182c76 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -39,6 +39,7 @@ check_PROGRAMS = \ powerset \ readsave \ reductgba \ + reduccmp \ tgbaread \ tripprod @@ -55,12 +56,15 @@ mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc readsave_SOURCES = readsave.cc reductgba_SOURCES = reductgba.cc +reduccmp_SOURCES = reductgba.cc +reduccmp_CXXFLAGS = -DREDUCCMP tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. TESTS = \ + reduccmp.test \ reductgba.test \ explicit.test \ tgbaread.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index af33b66d2..9a700a972 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -88,6 +88,16 @@ syntax(char* prog) << " -r4 reduce formula using all rules" << std::endl << " -rd display the reduce formula" << std::endl << " -R same as -r, but as a set" << std::endl + << " -R1 use direct simulation to reduce the automata " + << "(implies -L)" + << std::endl + << " -R2 use delayed simulation to reduce the automata, incorrect" + << "(implies -L)" + << std::endl + << " -R3 use SCC to reduce the automata" + << std::endl + << " -Rd to display simulation relation" + << std::endl << " -s convert to explicit automata, and number states " << "in DFS order" << std::endl << " -S convert to explicit automata, and number states " @@ -102,17 +112,7 @@ syntax(char* prog) << " -X do not compute an automaton, read it from a file" << std::endl << " -y do not merge states with same symbolic representation " - << "(implies -f)" << std::endl - << " -R1 use direct simulation to reduce the automata " - << "(implies -L)" - << std::endl - << " -R2 use delayed simulation to reduce the automata, incorrect" - << "(implies -L)" - << std::endl - << " -R3 use SCC to reduce the automata" - << std::endl - << " -Rd to display simulation relation" - << std::endl; + << "(implies -f)" << std::endl; exit(2); } @@ -393,12 +393,6 @@ main(int argc, char** argv) to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); } - /* - spot::tgba* aut_red = 0; - if (reduc_aut != spot::Reduce_None) - a = aut_red = spot::reduc_tgba_sim(a, reduc_aut); - */ - spot::tgba_reduc* aut_red = 0; if (reduc_aut != spot::Reduce_None) { diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 1f9848b22..cb68bd5f4 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -45,81 +45,107 @@ void syntax(char* prog) { - std::cerr << prog << " option formula1" << std::endl; +#ifdef REDUCCMP + std::cerr << prog << " option file" << std::endl; +#else + std::cerr << prog << " option formula" << std::endl; +#endif exit(2); } int main(int argc, char** argv) { - if (argc < 2) + if (argc < 3) syntax(argv[0]); + int o = spot::ltl::Reduce_None; + switch (atoi(argv[1])) + { + case 0: + o = spot::Reduce_Scc; + break; + case 1: + o = spot::Reduce_Dir_Sim; + break; + case 2: + o = spot::Reduce_Del_Sim; + break; + case 3: + o = spot::Reduce_Dir_Sim | spot::Reduce_Scc; + break; + case 4: + o = spot::Reduce_Del_Sim | spot::Reduce_Scc; + break; + case 5: + // No Reduction + break; + default: + return 2; + } + int exit_code = 0; spot::simulation_relation* rel = NULL; spot::tgba* automata = NULL; - spot::tgba* aut_red = NULL; spot::tgba_reduc* automatareduc = NULL; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::bdd_dict* dict = new spot::bdd_dict(); - spot::ltl::parse_error_list p1; - spot::ltl::formula* f = spot::ltl::parse(argv[1], p1, env); - //std::cout << "Compute the automata" << std::endl; +#ifdef REDUCCMP + spot::tgba_parse_error_list pel; + automata = spot::tgba_parse(argv[2], pel, dict, env, false); + if (spot::format_tgba_parse_errors(std::cerr, pel)) + return 2; +#else + spot::ltl::parse_error_list p1; + spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env); + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) + return 2; automata = spot::ltl_to_tgba_fm(f, dict, false, true, false, true); +#endif - //std::cout << "Display the automata" << std::endl; spot::dotty_reachable(std::cout, automata); - - //std::cout << "Initialize the reduction automata" << std::endl; automatareduc = new spot::tgba_reduc(automata); - //aut_red = spot::reduc_tgba_sim(automata); - - //std::cout << "Compute the simulation relation" << std::endl; - //rel = spot::get_direct_relation_simulation(automatareduc); - rel = spot::get_delayed_relation_simulation(automatareduc); - //rel = NULL; - - //std::cout << "Display of the parity game" << std::endl; - - //std::cout << "Display of the simulation relation" << std::endl; - if (rel != NULL) - automatareduc->display_rel_sim(rel, std::cout); - - //std::cout << "Prune automata using simulation relation" << std::endl; - if (rel != NULL) - automatareduc->prune_automata(rel); - - //automatareduc->compute_scc(); - //std::cout << "Prune automata using scc" << std::endl; - //automatareduc->prune_scc(); - - //std::cout << "Display of scc" << std::endl; - //automatareduc->display_scc(std::cout); - + if (o & spot::Reduce_Dir_Sim) + { + rel = spot::get_direct_relation_simulation(automatareduc); + automatareduc->prune_automata(rel); + } + else if (o & spot::Reduce_Del_Sim) + { + rel = spot::get_delayed_relation_simulation(automatareduc); + automatareduc->quotient_state(rel); + } if (rel != NULL) + { + automatareduc->display_rel_sim(rel, std::cout); spot::free_relation_simulation(rel); + } + + if (o & spot::Reduce_Scc) + { + automatareduc->prune_scc(); + //automatareduc->display_scc(std::cout); + } if (automatareduc != NULL) { - std::cout << "Display of the minimize automata" << std::endl; - std::cout << std::endl; spot::dotty_reachable(std::cout, automatareduc); } - if (aut_red != NULL) - delete aut_red; if (automata != NULL) delete automata; if (automatareduc != NULL) delete automatareduc; +#ifndef REDUCCMP if (f != NULL) spot::ltl::destroy(f); +#endif assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); diff --git a/src/tgbatest/reductgba.test b/src/tgbatest/reductgba.test index 833b0260f..c0d33b317 100755 --- a/src/tgbatest/reductgba.test +++ b/src/tgbatest/reductgba.test @@ -25,24 +25,67 @@ set -e -check () +check() { - run 0 ./reductgba "$1" + run 0 ./reductgba "$1" "$2" } # We don't check the output, but just running these might be enough to # trigger assertions. -check 'a' -check 'a U b' -check 'a U Fb' -check 'X a' -check 'a & b & c' -check 'a | b | (c U (d & (g U (h ^ i))))' -check 'Xa & (b U !a) & (b U !a)' -check 'Fa & Xb & GFc & Gd' -check 'Fa & Xa & GFc & Gc' -check 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 'a R (b R c)' -check '(a U b) U (c U d)' -check '((Xp2)U(X(1)))*(p1 R(p2 R p0))' +# No reduction +check 0 'Fa & Xb & GFc & Gd' +check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' + +check 1 a +check 1 'a U b' +check 1 'X a' +check 1 'a & b & c' +check 1 'a | b | (c U (d & (g U (h ^ i))))' +check 1 'Xa & (b U !a) & (b U !a)' +check 1 'Fa & Xb & GFc & Gd' +check 1 'Fa & Xa & GFc & Gc' +check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +check 1 'a R (b R c)' +check 1 '(a U b) U (c U d)' +check 1 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' + +#reduction +check 1 'a U Fb' + + +#check 0 a +#check 0 'a U b' +#check 0 'a U Fb' + +#check 3 a +#check 3 'a U b' +#check 3 'a U Fb' + +#check 0 a +#check 0 'a U b' +#check 0 'a U Fb' +#check 0 'X a' +#check 0 'a & b & c' +#check 0 'a | b | (c U (d & (g U (h ^ i))))' +#check 0 'Xa & (b U !a) & (b U !a)' +#check 0 'Fa & Xb & GFc & Gd' +#check 0 'Fa & Xa & GFc & Gc' +#check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +#check 0 'a R (b R c)' +#check 0 '(a U b) U (c U d)' +#check 0 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' + +#check 3 a +#check 3 'a U b' +#check 3 'a U Fb' +#check 3 'X a' +#check 3 'a & b & c' +#check 3 'a | b | (c U (d & (g U (h ^ i))))' +#check 3 'Xa & (b U !a) & (b U !a)' +#check 3 'Fa & Xb & GFc & Gd' +#check 3 'Fa & Xa & GFc & Gc' +#check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +#check 3 'a R (b R c)' +#check 3 '(a U b) U (c U d)' +#check 3 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 5bdf468e9..89389b698 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -94,14 +94,14 @@ Algorithm Algorithm { Name = "Spot (Couvreur -- FM), post reduction" - Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R1 -R2 -F -f -t'" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R1 -F -f -t'" Enabled = yes } Algorithm { Name = "Spot (Couvreur -- FM), pre + post reduction" - Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -R1 -R2 -F -f -t'" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -R1 -F -f -t'" Enabled = yes }