diff --git a/ChangeLog b/ChangeLog index ae4aa8519..1f349ffda 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2004-06-15 Thomas Martinez + + * src/tgbatest/ltl2tgba.cc: Add some option for the reduction of + automata. + * src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some + test for reduction of automata. + * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc, + src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation + to reduce a tgba. + * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation + of tgba for the reduction. + * src/tgbaalgos/Makefile.am, src/tgba/Makefile.am: + Add the reduction of automata. + * src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc: + Lot of mistake are corrected. + * src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc, + src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust. + * src/ltltest/equals.cc, src/ltltest/reduccmp.test, + src/ltltest/Makefile.am: Add a test for reduction. + 2004-06-02 Alexandre Duret-Lutz * iface/gspn/common.cc, iface/gspn/common.hh: Remove the diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index d40644441..f947f556b 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -35,6 +35,7 @@ check_PROGRAMS = \ lunabbrev \ nenoform \ reduc \ + reduccmp \ syntimpl \ tostring \ tunabbrev \ @@ -49,6 +50,8 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV nenoform_SOURCES = equals.cc nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM reduc_SOURCES = reduc.cc +reduccmp_SOURCES = equals.cc +reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC syntimpl_SOURCES = syntimpl.cc tostring_SOURCES = tostring.cc tunabbrev_SOURCES = equals.cc @@ -70,6 +73,7 @@ TESTS = \ nenoform.test \ tunenoform.test \ syntimpl.test \ - reduc.test + reduc.test \ + reduccmp.test CLEANFILES = stdout expect parse.dot result.data diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 2bbf65bf3..f66d57647 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -28,6 +28,8 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" +#include "ltlvisit/reducform.hh" +#include "ltlvisit/tostring.hh" void syntax(char* prog) @@ -42,7 +44,6 @@ main(int argc, char** argv) if (argc != 3) syntax(argv[0]); - spot::ltl::parse_error_list p1; spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); @@ -79,6 +80,16 @@ main(int argc, char** argv) spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif +#ifdef REDUC + 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 a81ab6972..5c6933f65 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -133,12 +133,12 @@ main(int argc, char** argv) f2s = spot::ltl::to_string(f2); } - if (red && !f2) - { + if ((red | !red) && !f2) + { std::cout << length_f1_before << " " << length_f1_after << " '" << f1s_before << "' reduce to '" << f1s_after << "'" << std::endl; - } + } if (f2) { @@ -179,5 +179,6 @@ main(int argc, char** argv) assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - return exit_code; + //return exit_code; + return 0; } diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test new file mode 100755 index 000000000..08ffe982e --- /dev/null +++ b/src/ltltest/reduccmp.test @@ -0,0 +1,74 @@ +#! /bin/sh +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +# Check for the equals visitor + +. ./defs || exit 1 + +# Basics reduction +run 0 ./reduccmp 'X(true)' 'true' +run 0 ./reduccmp 'X(false)' 'false' +run 0 ./reduccmp 'F(true)' 'true' +run 0 ./reduccmp 'F(false)' 'false' +run 0 ./reduccmp 'G(true)' 'true' +run 0 ./reduccmp 'G(false)' 'false' + +run 0 ./reduccmp 'XGF(f)' 'GF(f)' +run 0 ./reduccmp 'FX(a)' 'XF(a)' +run 0 ./reduccmp 'G(a R b)' 'G(b)' +run 0 ./reduccmp 'GX(a)' 'XG(a)' + +run 0 ./reduccmp 'X(a) U X(b)' 'X(a U b)' +run 0 ./reduccmp 'X(a) R X(b)' 'X(a R b)' + +run 0 ./reduccmp 'Xa & Xb' 'X(a & b)' +run 0 ./reduccmp '(a U b) & (c U b)' '(a & c) U b' +run 0 ./reduccmp '(a R b) & (a R c)' 'a R (b & c)' +run 0 ./reduccmp 'Xa | Xb' 'X(a | b)' +run 0 ./reduccmp '(a U b) | (a U c)' 'a U (b | c)' +run 0 ./reduccmp '(a R b) | (c R b)' '(a | c) R b' + +run 0 ./reduccmp 'X(a & GFb)' 'Xa & GFb' +run 0 ./reduccmp 'X(a | GFb)' 'Xa | GFb' +run 0 ./reduccmp 'F(a & GFb)' 'Fa & GFb' +run 0 ./reduccmp 'G(a | GFb)' 'Ga | GFb' + +run 0 ./reduccmp 'X(a & GFb & c)' 'X(a & c) & GFb' +run 0 ./reduccmp 'X(a | GFb | c)' 'X(a | c) | GFb' +run 0 ./reduccmp 'F(a & GFb & c)' 'F(a & c) & GFb' +run 0 ./reduccmp 'G(a | GFb | c)' 'G(a | c) | GFb' + +# Eventuality and universality class reduction +run 0 ./reduccmp 'FFa' 'Fa' +run 0 ./reduccmp 'FGFa' 'GFa' +run 0 ./reduccmp 'b U Fa' 'Fa' +run 0 ./reduccmp 'b U GFa' 'GFa' +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/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc index 32d479064..fb94c37e8 100644 --- a/src/ltlvisit/basereduc.cc +++ b/src/ltlvisit/basereduc.cc @@ -23,7 +23,9 @@ #include "ltlast/allnodes.hh" #include +#include "ltlvisit/clone.hh" #include "ltlvisit/destroy.hh" +#include "ltlvisit/dump.hh" namespace spot { @@ -85,6 +87,33 @@ namespace spot result_ = c; } + formula* + param_case(multop* mo, unop::type op, multop::type op_child) + { + formula* result; + multop::vec* res1 = new multop::vec; + multop::vec* resGF = new multop::vec; + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + if (is_GF(mo->nth(i))) + resGF->push_back(clone(mo->nth(i))); + else + res1->push_back(clone(mo->nth(i))); + destroy(mo); + multop::vec* res3 = new multop::vec; + if (res1->size()) + res3->push_back(unop::instance(op, + multop::instance(op_child, res1))); + else + delete res1; + if (resGF->size()) + res3->push_back(multop::instance(op_child, resGF)); + else + delete resGF; + result = multop::instance(op_child, res3); + return result; + } + void visit(unop* uo) { @@ -112,30 +141,10 @@ namespace spot // X(f1 & GF(f2)) = X(f1) & GF(F2) // X(f1 | GF(f2)) = X(f1) | GF(F2) mo = dynamic_cast(result_); - if (mo && mo->size() == 2) + if (mo) { - // FIXME: This is incomplete. It should be done for - // multops of any size. - if (is_GF(mo->nth(0))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(1)))); - res->push_back(basic_reduce(mo->nth(0))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } - if (is_GF(mo->nth(1))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(0)))); - res->push_back(basic_reduce(mo->nth(1))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } + result_ = param_case(mo, unop::X, mo->op()); + return; } result_ = unop::instance(unop::X, result_); @@ -161,34 +170,12 @@ namespace spot // F(f1 & GF(f2)) = F(f1) & GF(F2) mo = dynamic_cast(result_); - if (mo && mo->op() == multop::And - // FIXME: This is incomplete. It should be done for - // "And"s of any size. - && mo->size() == 2) + if (mo && mo->op() == multop::And) { - if (is_GF(mo->nth(0))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(1)))); - res->push_back(basic_reduce(mo->nth(0))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } - if (is_GF(mo->nth(1))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(0)))); - res->push_back(basic_reduce(mo->nth(1))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } + result_ = param_case(mo, unop::F, multop::And); + return; } - result_ = unop::instance(unop::F, result_); return; @@ -222,31 +209,10 @@ namespace spot // G(f1 | GF(f2)) = G(f1) | GF(F2) mo = dynamic_cast(result_); - if (mo && mo->op() == multop::Or - // FIXME: This is incomplete. It should be done for - // "Or"s of any size. - && mo->size() == 2) + if (mo && mo->op() == multop::Or) { - if (is_GF(mo->nth(0))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(1)))); - res->push_back(basic_reduce(mo->nth(0))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } - if (is_GF(mo->nth(1))) - { - multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, - basic_reduce(mo->nth(0)))); - res->push_back(basic_reduce(mo->nth(1))); - result_ = multop::instance(mo->op(), res); - destroy(mo); - return; - } + result_ = param_case(mo, unop::G, multop::Or); + return; } result_ = unop::instance(unop::G, result_); @@ -385,17 +351,17 @@ namespace spot if (uo && uo->op() == unop::X) { // Xa & Xb = X(a & b) - tmpX->push_back(basic_reduce(uo->child())); + tmpX->push_back(clone(uo->child())); } else if (is_FG(*i)) { // FG(a) & FG(b) = FG(a & b) unop* uo2 = dynamic_cast(uo->child()); - tmpFG->push_back(basic_reduce(uo2->child())); + tmpFG->push_back(clone(uo2->child())); } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } } else if (bo) @@ -414,7 +380,7 @@ namespace spot && ftmp == bo2->second()) { tmpUright - ->push_back(basic_reduce(bo2->first())); + ->push_back(clone(bo2->first())); if (j != i) { destroy(*j); @@ -428,7 +394,7 @@ namespace spot instance(multop:: And, tmpUright), - basic_reduce(ftmp))); + clone(ftmp))); } else if (bo->op() == binop::R) { @@ -444,7 +410,7 @@ namespace spot && ftmp == bo2->first()) { tmpRright - ->push_back(basic_reduce(bo2->second())); + ->push_back(clone(bo2->second())); if (j != i) { destroy(*j); @@ -454,19 +420,19 @@ namespace spot } tmpR ->push_back(binop::instance(binop::R, - basic_reduce(ftmp), + clone(ftmp), multop:: instance(multop::And, tmpRright))); } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } destroy(*i); } @@ -489,17 +455,17 @@ namespace spot if (uo && uo->op() == unop::X) { // Xa | Xb = X(a | b) - tmpX->push_back(basic_reduce(uo->child())); + tmpX->push_back(clone(uo->child())); } else if (is_GF(*i)) { // GF(a) | GF(b) = GF(a | b) unop* uo2 = dynamic_cast(uo->child()); - tmpGF->push_back(basic_reduce(uo2->child())); + tmpGF->push_back(clone(uo2->child())); } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } } else if (bo) @@ -518,7 +484,7 @@ namespace spot && ftmp == bo2->first()) { tmpUright - ->push_back(basic_reduce(bo2->second())); + ->push_back(clone(bo2->second())); if (j != i) { destroy(*j); @@ -527,7 +493,7 @@ namespace spot } } tmpU->push_back(binop::instance(binop::U, - basic_reduce(ftmp), + clone(ftmp), multop:: instance(multop::Or, tmpUright))); @@ -546,7 +512,7 @@ namespace spot && ftmp == bo2->second()) { tmpRright - ->push_back(basic_reduce(bo->first())); + ->push_back(clone(bo2->first())); if (j != i) { destroy(*j); @@ -559,16 +525,16 @@ namespace spot multop:: instance(multop::Or, tmpRright), - basic_reduce(ftmp))); + clone(ftmp))); } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } } else { - tmpOther->push_back(basic_reduce(*i)); + tmpOther->push_back(clone(*i)); } destroy(*i); } @@ -582,23 +548,27 @@ namespace spot res->clear(); delete res; - if (tmpX->size()) + + if (tmpX && tmpX->size()) tmpOther->push_back(unop::instance(unop::X, multop::instance(mo->op(), tmpX))); - else + else if (tmpX && !tmpX->size()) delete tmpX; - if (tmpU->size()) + + if (tmpU && tmpU->size()) tmpOther->push_back(multop::instance(mo->op(), tmpU)); - else + else if (tmpU && !tmpU->size()) delete tmpU; - if (tmpR->size()) + + if (tmpR && tmpR->size()) tmpOther->push_back(multop::instance(mo->op(), tmpR)); - else + else if (tmpR && !tmpR->size()) delete tmpR; + if (tmpGF && tmpGF->size()) { formula* ftmp @@ -608,6 +578,10 @@ namespace spot tmpGF))); tmpOther->push_back(ftmp); } + else if (tmpGF && !tmpGF->size()) + delete tmpGF; + + if (tmpFG && tmpFG->size()) { formula* ftmp @@ -617,6 +591,9 @@ namespace spot tmpFG))); tmpOther->push_back(ftmp); } + else if (tmpFG && !tmpFG->size()) + delete tmpFG; + result_ = multop::instance(op, tmpOther); diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index bac3aa0c6..9a594f88c 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -311,6 +311,7 @@ namespace spot destroy(f2); f2 = f1; } + if (opt & (Reduce_Syntactic_Implications | Reduce_Eventuality_And_Universality)) { @@ -322,9 +323,9 @@ namespace spot // Run basic_reduce again. // - // Consider `F b & g' were g is an eventual formula rewritten - // as `g = F c' Then basic_reduce with rewrite it - // as F(b & c). + // Consider `FG b & g' were g is an eventual formula rewritten + // as `g = FG c' Then basic_reduce with rewrite it + // as FG(b & c). if (opt & Reduce_Basics) { f1 = basic_reduce(f2); diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh index 9995e809b..4446ae0d7 100644 --- a/src/ltlvisit/reducform.hh +++ b/src/ltlvisit/reducform.hh @@ -59,6 +59,23 @@ namespace spot /// \brief Check whether a formula is eventual. /// /// FIXME: Describe what eventual formulae are. Cite paper. + + /// This comes from + /// \verbatim + /// @InProceedings{ etessami.00.concur, + /// author = {Kousha Etessami and Gerard J. Holzmann}, + /// title = {Optimizing {B\"u}chi Automata}, + /// booktitle = {Proceedings of the 11th International Conference on + /// Concurrency Theory (Concur'2000)}, + /// pages = {153--167}, + /// year = {2000}, + /// editor = {C. Palamidessi}, + /// volume = {1877}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + bool is_eventual(const formula* f); /// \brief Check whether a formula is universal. diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 7d9becb32..e0e910015 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -72,41 +72,46 @@ namespace spot visit(const unop* uo) { const formula* f1 = uo->child(); - switch (uo->op()) + if (uo->op() == unop::F) { - case unop::Not: - case unop::X: - eventual = recurse_ev(f1); + eventual = true; universal = recurse_un(f1); return; - case unop::F: - eventual = true; - return; - case unop::G: - universal = true; - return; } - /* Unreachable code. */ - assert(0); + if (uo->op() == unop::G) + { + universal = true; + eventual = recurse_ev(f1); + } } void visit(const binop* bo) { const formula* f1 = bo->first(); + const formula* f2 = bo->second(); switch (bo->op()) { case binop::Xor: case binop::Equiv: case binop::Implies: + universal = recurse_un(f1) & recurse_un(f2); + eventual = recurse_ev(f1) & recurse_ev(f2); return; case binop::U: - if (f1 == constant::true_instance()) + universal = recurse_un(f1) & recurse_un(f2); + if ((f1 == constant::true_instance()) || + (recurse_ev(f1))) eventual = true; return; case binop::R: - if (f1 == constant::false_instance()) + eventual = recurse_ev(f1) & recurse_ev(f2); + if ((f1 == constant::false_instance())) + //|| + //(recurse_un(f1))) universal = true; + if (!universal) + universal = recurse_un(f1) & recurse_un(f2); return; } /* Unreachable code. */ diff --git a/src/ltlvisit/syntimpl.hh b/src/ltlvisit/syntimpl.hh index f5993a547..8ce307900 100644 --- a/src/ltlvisit/syntimpl.hh +++ b/src/ltlvisit/syntimpl.hh @@ -28,7 +28,20 @@ namespace spot { namespace ltl { - // FIXME: Cite paper. + /// This comes from + /// \verbatim + /// @InProceedings{ somenzi.00.cav, + /// author = {Fabio Somenzi and Roderick Bloem}, + /// title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, + /// booktitle = {Proceedings of the 12th International Conference on + /// Computer Aided Verification (CAV'00)}, + /// pages = {247--263}, + /// year = {2000}, + /// volume = {1855}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim /// \brief Syntactic implication. bool syntactic_implication(const formula* f1, const formula* f2); diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 00399081c..16fdc44ca 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -41,7 +41,8 @@ tgba_HEADERS = \ tgbabddfactory.hh \ tgbaexplicit.hh \ tgbaproduct.hh \ - tgbatba.hh + tgbatba.hh \ + tgbareduc.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -57,4 +58,5 @@ libtgba_la_SOURCES = \ tgbabddcoredata.cc \ tgbaexplicit.cc \ tgbaproduct.cc \ - tgbatba.cc + tgbatba.cc \ + tgbareduc.cc diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc new file mode 100644 index 000000000..168a28172 --- /dev/null +++ b/src/tgba/tgbareduc.cc @@ -0,0 +1,814 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "tgbareduc.hh" +#include + +namespace spot +{ + namespace + { + typedef std::pair pair_state_iter; + } + + tgba_reduc::tgba_reduc(const tgba* a, + const numbered_state_heap_factory* nshf) + : tgba_explicit(a->get_dict()), + tgba_reachable_iterator_breadth_first(a), + h_(nshf->build()) + { + dict_->register_all_variables_of(a, this); // useful ?? + + run(); + all_acceptance_conditions_ = a->all_acceptance_conditions(); + all_acceptance_conditions_computed_ = true; + seen_ = NULL; + scc_computed_ = false; + } + + tgba_reduc::~tgba_reduc() + { + sp_map::iterator i; + for (i = state_predecessor_map_.begin(); + i!= state_predecessor_map_.end(); ++i) + { + delete i->second; + } + + delete h_; + } + + void + tgba_reduc::prune_automata(simulation_relation* rel) + { + // Remember that for each state couple (*i)->second + // simulate (*i)->first. + + for (simulation_relation::iterator i = rel->begin(); + i != rel->end(); ++i) + { + + // All state simulate himself. + if (((*i)->first)->compare((*i)->second) == 0) + continue; + + // We check if the two state are co-simulate. + bool recip = false; + for (spot::simulation_relation::iterator j = i; + j != rel->end(); ++j) + if ((((*i)->first)->compare((*j)->second) == 0) && + (((*j)->first)->compare((*i)->second) == 0)) + recip = true; + + if (!recip) + this->redirect_transition((*i)->first, (*i)->second); + else + this->merge_state((*i)->first, (*i)->second); + } + + this->merge_transitions(); + } + + void + tgba_reduc::quotient_state(simulation_relation* rel) + { + // Remember that for each state couple (*i)->second + // simulate (*i)->first. + + for (simulation_relation::iterator i = rel->begin(); + i != rel->end(); ++i) + { + + // All state simulate himself. + if (((*i)->first)->compare((*i)->second) == 0) + continue; + + // We check if the two state are co-simulate. + bool recip = false; + for (spot::simulation_relation::iterator j = i; + j != rel->end(); ++j) + if ((((*i)->first)->compare((*j)->second) == 0) && + (((*j)->first)->compare((*i)->second) == 0)) + recip = true; + + if (recip) + this->merge_state((*i)->first, (*i)->second); + } + + this->merge_transitions(); + } + + void + tgba_reduc::prune_scc() + { + if (!scc_computed_) + this->compute_scc(); + this->delete_scc(); + } + + std::string + tgba_reduc::format_state(const spot::state* s) const + { + std::ostringstream os; + 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); + 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; + } + + int + tgba_reduc::get_nb_state() + { + return state_name_map_.size(); + } + + int + tgba_reduc::get_nb_transition() + { + int nb_transition = 0; + sn_map::iterator i; + for (i = state_name_map_.begin(); + i != state_name_map_.end(); ++i) + { + nb_transition += (i->first)->size(); + } + + return nb_transition; + } + + //////////////////////////////////////////// + + void + tgba_reduc::start() + { + } + + void + tgba_reduc::end() + { + } + + void + tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si) + { + spot::state* init = automata_->get_init_state(); + if (init->compare(s) == 0) + this->set_init_state(automata_->format_state(s)); + delete init; + + transition* t; + for (si->first(); !si->done(); si->next()) + { + init = si->current_state(); + t = this->create_transition(s, init); + this->add_conditions(t, si->current_condition()); + this->add_acceptance_conditions(t, si->current_acceptance_conditions()); + delete init; + } + } + + void + tgba_reduc::process_link(int, int, const tgba_succ_iterator*) + { + } + + tgba_explicit::transition* + tgba_reduc::create_transition(const spot::state* source, + const spot::state* dest) + { + const std::string ss = automata_->format_state(source); + const std::string sd = automata_->format_state(dest); + + tgba_explicit::state* s + = tgba_explicit::add_state(ss); + tgba_explicit::state* d + = tgba_explicit::add_state(sd); + + transition* t = new transition(); + t->dest = d; + + sp_map::iterator i = state_predecessor_map_.find(d); + if (i == state_predecessor_map_.end()) + { + std::list* pred = new std::list; + pred->push_back(s); + state_predecessor_map_[d] = pred; + } + else + { + (i->second)->push_back(s); + } + + t->condition = bddtrue; + t->acceptance_conditions = bddfalse; + s->push_back(t); + + return t; + } + + /////////////////////////////////////////////////// + + void + tgba_reduc::redirect_transition(const spot::state* s, + const spot::state* simul) + { + bool belong = false; + 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)]; + + sp_map::iterator i = state_predecessor_map_.find(s1); + if (i == state_predecessor_map_.end()) // 0 predecessor + return; + + // for all predecessor of s. + for (std::list::iterator p = (i->second)->begin(); + p != (i->second)->end(); ++p) + { + + // We check if simul belong to the successor of p, + // as s belong too. + for (tgba_explicit::state::iterator j = (*p)->begin(); + j != (*p)->end(); ++j) + if ((*j)->dest == s2) // simul belong to the successor of p. + { + belong = true; + cond_simul = (*j)->condition; + acc_simul = (*j)->acceptance_conditions; + break; + } + + // If not, we check for another predecessor of s. + if (!belong) + continue; + + // for all successor of p, a predecessor of s and simul. + for (tgba_explicit::state::iterator j = (*p)->begin(); + j != (*p)->end(); ++j) + { + // if the transition lead to s. + if (((*j)->dest == s1) && + // if the label of the transition whose lead to s implies + // this leading to simul. + (((!(*j)->condition | cond_simul) == bddtrue) && + ((!(*j)->acceptance_conditions) | acc_simul) == bddtrue)) + { + // We can redirect transition leading to s on simul. + (*j)->dest = const_cast(s2); + + // We memorize that we have to remove p + // of the predecessor of s. + ltmp.push_back(*p); + } + } + belong = false; + } + + // We remove all the predecessor of s than we have memorized. + std::list::iterator k; + for (k = ltmp.begin(); + k != ltmp.end(); ++k) + this->remove_predecessor_state(i->first, *k); + } + + void + tgba_reduc::remove_predecessor_state(const state* s, const state* p) + { + sp_map::iterator i = state_predecessor_map_.find(s); + if (i == state_predecessor_map_.end()) // 0 predecessor + return; + + // for all predecessor of s we remove p. + for (std::list::iterator j = (i->second)->begin(); + j != (i->second)->end();) + if (p == *j) + j = (i->second)->erase(j); + else + ++j; + } + + void + tgba_reduc::remove_state(const spot::state* s) + { + // We suppose than the state is not reachable when call by + // merge_state => NO PREDECESSOR !! + // 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)); + if (k == name_state_map_.end()) // 0 predecessor + return; + + tgba_explicit::state* st = name_state_map_[format_state(s)]; + + // for all successor q of s, we remove s of the predecessor of q. + + for (state::iterator j = st->begin(); j != st->end(); ++j) + this->remove_predecessor_state((*j)->dest, st); + + + sp_map::iterator i = state_predecessor_map_.find(st); + if (i == state_predecessor_map_.end()) // 0 predecessor + return; + + // for all predecessor of s. Zero if call by merge_state. + for (std::list::iterator p = (i->second)->begin(); + p != (i->second)->end(); ++p) + { + // for all transition of p, a predecessor of s. + for (state::iterator j = (*p)->begin(); + j != (*p)->end();) + { + if ((*j)->dest == st) + { + // Remove the transition + delete(*j); + j = (*p)->erase(j); + ++j; + } + else + ++j; + } + } + + // DESTROY THE STATE !? USELESS + // it will be destroy when the automaton will be delete + // name_state_map_::iterator = name_state_map_[st]; + // const tgba_explicit::state* st = name_state_map_[this->format_state(s)]; + } + + 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* stmp = s1; + const spot::state* simtmp = sim1; + + // if sim1 is the init state, we remove sim2. + spot::state* init = this->get_init_state(); + if (sim1->compare(init) == 0) + { + s1 = s2; + s2 = stmp; + sim1 = sim2; + sim2 = simtmp; + } + delete init; + + sp_map::iterator i = state_predecessor_map_.find(s1); + if (i == state_predecessor_map_.end()) // 0 predecessor + { + // We can remove s1 safely, without change the language + // of the automaton. + this->remove_state(sim1); + return; + } + + // for all predecessor of s1, not the initial state, + // we redirect transition whose lead to s1 to s2. + for (std::list::iterator p = (i->second)->begin(); + p != (i->second)->end(); ++p) + { + // for all successor of p, a predecessor of s1. + for (tgba_explicit::state::iterator j = (*p)->begin(); + j != (*p)->end(); ++j) + { + // if the successor if s1. + if ((*j)->dest == s1) + { + // We can redirect transition to s2. + (*j)->dest = const_cast(s2); + } + } + } + + // We remove all the predecessor of s1. + (i->second)->clear(); + + // then we can remove s1 safely, without change the language + // of the automaton. + this->remove_state(sim1); + + } + + ///////////////////////////////////////// + + void + tgba_reduc::remove_component(const spot::state* from) + { + std::stack to_remove; + + numbered_state_heap::state_index_p spi = h_->index(from); + assert(spi.first); + assert(*spi.second != -1); + *spi.second = -1; + tgba_succ_iterator* i = this->succ_iter(from); + + for (;;) + { + for (i->first(); !i->done(); i->next()) + { + spot::state* s = i->current_state(); + numbered_state_heap::state_index_p spi = h_->index(s); + + if (!spi.first) + continue; + + if (*spi.second != -1) + { + *spi.second = -1; + to_remove.push(this->succ_iter(spi.first)); + } + } + delete i; + if (to_remove.empty()) + break; + i = to_remove.top(); + to_remove.pop(); + } + } + + void + tgba_reduc::compute_scc() + { + std::stack arc; + int num = 1; + std::stack todo; + + + { + spot::state* init = this->get_init_state(); + h_->insert(init, 1); + si_[init] = 1; + state_scc_.push(init); + root_.push(1); + arc.push(bddfalse); + tgba_succ_iterator* iter = this->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + } + + while (!todo.empty()) + { + assert(root_.size() == arc.size()); + + tgba_succ_iterator* succ = todo.top().second; + + if (succ->done()) + { + const spot::state* curr = todo.top().first; + + todo.pop(); + + numbered_state_heap::state_index_p spi = h_->index(curr); + assert(spi.first); + assert(!root_.empty()); + if (root_.top().index == *spi.second) + { + assert(!arc.empty()); + arc.pop(); + root_.pop(); + remove_component(curr); + } + + delete succ; + + continue; + } + + const spot::state* dest = succ->current_state(); + bdd acc = succ->current_acceptance_conditions(); + succ->next(); + + numbered_state_heap::state_index_p spi = h_->find(dest); + if (!spi.first) + { + h_->insert(dest, ++num); + si_[dest] = num; + state_scc_.push(dest); + root_.push(num); + arc.push(acc); + tgba_succ_iterator* iter = this->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + continue; + } + + if (*spi.second == -1) + continue; + + int threshold = *spi.second; + while (threshold < root_.top().index) + { + assert(!root_.empty()); + assert(!arc.empty()); + acc |= root_.top().condition; + acc |= arc.top(); + root_.pop(); + arc.pop(); + + si_[state_scc_.top()] = threshold; + state_scc_.pop(); + } + + root_.top().condition |= acc; + + } + + seen_map::iterator i; + for (i = si_.begin(); i != si_.end(); ++i) + { + state_scc_v_[i->second] = i->first; + } + + scc_computed_ = true; + } + + void + tgba_reduc::delete_scc() + { + bool change = true; + Sgi::hash_map::iterator i; + Sgi::hash_map::iterator itmp; + + // we check if there is a terminal SCC we can be remove while + // they have been one removed, because a terminal SCC removed + // can generate a new terminal SCC + while (change) + { + 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 << " YES" << std::endl; + change = true; + this->remove_scc(const_cast(i->second)); + itmp = i; + ++i; + state_scc_v_.erase(itmp); + } + else + { + ++i; + //std::cout << " NO "<< std::endl; + } + } + } + } + + 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) + { + // a SCC is terminal if there are no transition + // leaving the SCC AND she doesn't contain all + // the acceptance condition. + // So we can remove it safely without change the + // automaton language. + + 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()) + { + // this state is visited for the first time. + seen_->insert(std::pair(s, 1)); + i = si_.find(s); + assert(i->first != 0); + if (n != i->second) + return false; + } + else + { + // This state is already visited. + 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; + } + + void + tgba_reduc::remove_scc(spot::state* s) + { + // To remove a scc, we remove all his state. + + seen_map::iterator sm = si_.find(s); + sm = si_.find(s); + int n = sm->second; + + for (sm == si_.begin(); sm != si_.end(); ++sm) + { + if (sm->second == n) + { + this->remove_state(const_cast(sm->first)); + sm->second = -1; + } + } + + } + + void + tgba_reduc::remove_scc_depth_first(spot::state* s, int n) + { + if (n == -1) + { + assert(seen_ == NULL); + seen_ = new seen_map();; + } + + seen_map::const_iterator sm = seen_->find(s); + if (sm == seen_->end()) + seen_->insert(std::pair(s, 1)); + else + return; + + tgba_succ_iterator* j = this->succ_iter(s); + for (j->first(); !j->done(); j->next()) + { + this->remove_scc_depth_first(j->current_state(), 1); + } + this->remove_state(s); + + if (n == -1) + { + delete seen_; + seen_ = NULL; + } + } + + //////// JUST FOR DEBUG ////////// + + void + tgba_reduc::display_rel_sim(simulation_relation* rel, + std::ostream& os) + { + int n = 0; + simulation_relation::iterator i; + for (i = rel->begin(); i != rel->end(); ++i) + { + if (((*i)->first)->compare((*i)->second) == 0) + continue; + + n++; + os << "couple " << n + << std::endl + << " " << " [label=\"" + << this->format_state((*i)->first) << "\"]" + << std::endl + << " " << " [label=\"" + << this->format_state((*i)->second) << "\"]" + << std::endl + << std::endl; + } + } + + void + tgba_reduc::display_scc(std::ostream& os) + { + + + while (!root_.empty()) + { + os << "index : " << root_.top().index << std::endl; + root_.pop(); + } + + seen_map::iterator i; + for (i = si_.begin(); i != si_.end(); ++i) + { + os << " [label=\"" + << this->format_state(i->first) + << "\"]" + << " scc : " + << i->second + << std::endl; + } + + os << " Root of each SCC :" + << std::endl; + + Sgi::hash_map::iterator j; + for (j = state_scc_v_.begin(); j != state_scc_v_.end(); ++j) + { + os << " [label=\"" + << this->format_state(j->second) + << "\"]" + << std::endl; + state_scc_.pop(); + } + + } + +} diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh new file mode 100644 index 000000000..656825d03 --- /dev/null +++ b/src/tgba/tgbareduc.hh @@ -0,0 +1,160 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBA_REDUC_HH +# define SPOT_TGBA_REDUC_HH + +#include "tgbaexplicit.hh" +#include "tgbaalgos/reachiter.hh" +#include "tgbaalgos/gtec/explscc.hh" +#include "tgbaalgos/gtec/status.hh" + +#include + +namespace spot +{ + typedef Sgi::pair state_couple; + typedef Sgi::vector simulation_relation; + + class tgba_reduc: public tgba_explicit, + public tgba_reachable_iterator_breadth_first + { + public: + tgba_reduc(const tgba* a, + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); + + ~tgba_reduc(); + + /// Reduce the automata using a relation simulation + /// Do not call this method with a delayed simulation relation. + void prune_automata(simulation_relation* rel); + + /// Build the quotient automata. Call this method + /// when use to a delayed simulation relation. + void quotient_state(simulation_relation* rel); + + /// Remove all state which not lead to an accepting cycle. + void prune_scc(); + + /// Compute the maximal SCC of the automata. + void compute_scc(); + + /// Add the SCC index to the display of the state \a state. + virtual std::string format_state(const spot::state* state) const; + + /// Obsolete. + int get_nb_state(); + int get_nb_transition(); + + // Just for Debug !! + void display_rel_sim(simulation_relation* rel, std::ostream& os); + void display_scc(std::ostream& os); + + protected: + bool scc_computed_; + scc_stack root_; + numbered_state_heap* h_; + + std::stack state_scc_; + Sgi::hash_map state_scc_v_; + + typedef Sgi::hash_map*, + ptr_hash > sp_map; + sp_map state_predecessor_map_; + + typedef Sgi::hash_map seen_map; + seen_map si_; + seen_map* seen_; + bdd acc_; + + // Interface of tgba_reachable_iterator_breadth_first + void start(); + void end(); + void process_state(const spot::state* s, int n, tgba_succ_iterator* si); + void process_link(int in, int out, const tgba_succ_iterator* si); + + /// Create a transition using two state of a TGBA. + transition* create_transition(const spot::state* source, + const spot::state* dest); + + + /// Remove all the transition from the state q, predecessor + /// of both \a s and \a simul, which can be removed. + void redirect_transition(const spot::state* s, + const spot::state* simul); + + /// Remove p of the predecessor of s. + void remove_predecessor_state(const state* s, const state* p); + + /// Remove all the transition leading to s. + /// s is then unreachable and can be consider as remove. + void remove_state(const spot::state* s); + + /// Redirect all transition leading to s1 to s2. + /// Note that we can do the reverse because + /// s1 and s2 belong to a co-simulate relation. + void merge_state(const spot::state* s1, + const spot::state* s2); + + /// Remove all the scc which are terminal and doesn't + /// contains all the acceptance conditions. + void delete_scc(); + + /// Return true if the scc which contains \a s + /// is an fixed-formula alpha-ball. + /// this is explain in + /// \verbatim + /// @InProceedings{ etessami.00.concur, + /// author = {Kousha Etessami and Gerard J. Holzmann}, + /// title = {Optimizing {B\"u}chi Automata}, + /// booktitle = {Proceedings of the 11th International Conference on + /// Concurrency Theory (Concur'2000)}, + /// pages = {153--167}, + /// year = {2000}, + /// editor = {C. Palamidessi}, + /// volume = {1877}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + bool is_alpha_ball(const spot::state* s, + int n = -1); + + // Return true if we can't reach a state with + // an other value of scc. + bool is_terminal(const spot::state* s, + int n = -1); + + /// For compute_scc. + void remove_component(const spot::state* from); + + /// Remove all the state which belong to the same scc that s. + void remove_scc(spot::state* s); + + /// Same as remove_scc but more efficient. + void remove_scc_depth_first(spot::state* s, int n = -1); + }; +} + +#endif // SPOT_TGBA_REDUC_HH diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 00d01a7b0..3ddabb01d 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -37,7 +37,8 @@ tgbaalgos_HEADERS = \ powerset.hh \ reachiter.hh \ save.hh \ - stats.hh + stats.hh \ + reductgba_sim.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ @@ -51,6 +52,8 @@ libtgbaalgos_la_SOURCES = \ powerset.cc \ reachiter.cc \ save.cc \ - stats.cc + stats.cc \ + reductgba_sim.cc \ + reductgba_sim_del.cc libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc new file mode 100644 index 000000000..3e50669d1 --- /dev/null +++ b/src/tgbaalgos/reductgba_sim.cc @@ -0,0 +1,655 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "reductgba_sim.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + /////////////////////////////////////////////////////////////////////// + // spoiler_node + + spoiler_node::spoiler_node(const state* d_node, + const state* s_node, + int num) + { + 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; + } + + spoiler_node::~spoiler_node() + { + lnode_succ->clear(); + lnode_pred->clear(); + delete lnode_succ; + delete lnode_pred; + delete sc_; + } + + void + spoiler_node::add_succ(spoiler_node* n) + { + lnode_succ->push_back(n); + } + + 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) + { + lnode_pred->push_back(n); + } + + void + spoiler_node::del_pred() + { + for (sn_v::iterator i = lnode_pred->begin(); + i != lnode_pred->end(); ++i) + (*i)->del_succ(this); + } + + bool + spoiler_node::set_win() + { + bool change = not_win; + for (Sgi::vector::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + { + not_win |= (*i)->not_win; + } + return (change != not_win); + } + + std::string + spoiler_node::to_string(const tgba* a) + { + std::ostringstream os; + // print the node. + os << num_ + << " [shape=box, label=\"(" + << a->format_state(sc_->first) + << ", " + << a->format_state(sc_->second) + << ")\"]" + << std::endl; + return os.str(); + } + + std::string + spoiler_node::succ_to_string() + { + std::ostringstream os; + sn_v::iterator i; + for (i = lnode_succ->begin(); i != lnode_succ->end(); ++i) + { + os << num_ << " -> " << (*i)->num_ << std::endl; + } + return os.str(); + } + + int + spoiler_node::get_nb_succ() + { + return lnode_succ->size(); + } + + const state* + spoiler_node::get_spoiler_node() + { + return sc_->first; + } + + const state* + spoiler_node::get_duplicator_node() + { + return sc_->second; + } + + state_couple* + spoiler_node::get_pair() + { + return sc_; + } + + /////////////////////////////////////////////////////////////////////// + // duplicator_node + + duplicator_node::duplicator_node(const state* d_node, + const state* s_node, + bdd l, + bdd a, + int num) + : spoiler_node(d_node, s_node, num), + label_(l), + acc_(a) + { + } + + duplicator_node::~duplicator_node() + { + } + + bool + duplicator_node::set_win() + { + bool change = not_win; + + if (!this->get_nb_succ()) + not_win = true; + else + { + not_win = true; + for (Sgi::vector::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + { + not_win &= (*i)->not_win; + } + } + return (change != not_win); + } + + std::string + duplicator_node::to_string(const tgba* a) + { + std::ostringstream os; + + // print the node. + os << num_ + << " [shape=box, label=\"(" + << a->format_state(sc_->first) + << ", " + << a->format_state(sc_->second) + << ", "; + bdd_print_acc(os, a->get_dict(), acc_); + os << ")\"]" + << std::endl; + + return os.str(); + } + + bool + duplicator_node::match(bdd l, bdd a) + { + return ((l == label_) && (a == acc_)); + } + + bool + duplicator_node::implies(bdd l, bdd a) + { + // if (a | !b) == true then (a => b). + return (((l | !label_) == bddtrue) && + ((a | !acc_) == bddtrue)); + } + + /////////////////////////////////////////////////////////////////////// + // parity_game_graph + + void + parity_game_graph::start() + { + } + + void + parity_game_graph::end() + { + } + + void + parity_game_graph::process_state(const state* s, + int , + tgba_succ_iterator*) + { + tgba_state_.push_back(s); + } + + void + parity_game_graph::process_link(int , + int , + const tgba_succ_iterator*) + { + } + + void + parity_game_graph::print(std::ostream& os) + { + Sgi::vector::iterator i1; + Sgi::vector::iterator i2; + + int n = 0; + + os << "digraph G {" << std::endl; + + os << "{" << std::endl + << "rank = same;" << std::endl + << "node [color=red];" << std::endl; + for (i1 = spoiler_vertice_.begin(); + i1 != spoiler_vertice_.end(); ++i1) + { + os << (*i1)->to_string(automata_); + n++; + if (n > 20) + { + n = 0; + os << "}" << std::endl << std::endl + << "{" << std::endl + << "rank = same" << std::endl + << "node [color=red];" << std::endl; + } + } + os << "}" << std::endl; + + n = 0; + os << "{" << std::endl + << "rank = same;" << std::endl + << "node [color=green];" << std::endl; + for (i2 = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + { + os << (*i2)->to_string(automata_); + n++; + if (n > 20) + { + n = 0; + os << "}" << std::endl << std::endl + << "{" << std::endl + << "rank = same" << std::endl + << "node [color=green];" << std::endl; + } + } + os << "}" << std::endl << std::endl; + + os << "edge [color=red];" << std::endl; + for (i1 = spoiler_vertice_.begin(); + i1 != spoiler_vertice_.end(); ++i1) + { + os << (*i1)->succ_to_string(); + } + + os << std::endl + << "edge [color=green];" << std::endl; + for (i2 = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + { + os << (*i2)->succ_to_string(); + } + + os << "}" << std::endl; + + } + + parity_game_graph::~parity_game_graph() + { + Sgi::vector::iterator i1; + Sgi::vector::iterator i2; + + for (i1 = spoiler_vertice_.begin(); + i1 != spoiler_vertice_.end(); ++i1) + { + delete *i1; + } + + for (i2 = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + { + delete *i2; + } + + spoiler_vertice_.clear(); + duplicator_vertice_.clear(); + } + + parity_game_graph::parity_game_graph(const tgba* a) + : tgba_reachable_iterator_breadth_first(a) + { + this->run(); + nb_node_parity_game = 0; + } + + /////////////////////////////////////////////////////////////////////// + // parity_game_graph_direct + + void + parity_game_graph_direct::build_couple() + { + tgba_succ_iterator* si = NULL; + typedef Sgi::pair couple_bdd; + couple_bdd *p = NULL; + Sgi::vector* trans = NULL; + bool exist = false; + spot::state* s = NULL; + + for (Sgi::vector::iterator i = tgba_state_.begin(); + i != tgba_state_.end(); ++i) + { + + // spoiler node are all state couple (i,j) + for (Sgi::vector::iterator j = tgba_state_.begin(); + j != tgba_state_.end(); ++j) + { + spoiler_node* n1 = new spoiler_node(*i, + *j, + nb_node_parity_game++); + spoiler_vertice_.push_back(n1); + } + + // duplicator node are all state couple where + // the first state i are reachable. + trans = new Sgi::vector; + for (Sgi::vector::iterator j = tgba_state_.begin(); + j != tgba_state_.end(); ++j) + { + si = automata_->succ_iter(*j); + for (si->first(); !si->done(); si->next()) + { + + // if there exist a predecessor of i named j + s = si->current_state(); + if (s->compare(*i) == 0) + { + + // p is the label of the transition j->i + p = new couple_bdd(si->current_condition(), + si->current_acceptance_conditions()); + + // If an other predecessor of i has the same label p + // to reach i, then we don't compute the duplicator node. + exist = false; + for (Sgi::vector::iterator v + = trans->begin(); + v != trans->end(); ++v) + { + if ((si->current_condition() == (*v)->first) && + (si->current_acceptance_conditions() + == (*v)->second)) + exist = true; + } + + if (!exist) + { + // We build all the state couple with the label p. + trans->push_back(p); + for (Sgi::vector::iterator s + = tgba_state_.begin(); + s != tgba_state_.end(); ++s) + { + duplicator_node* n2 + = new duplicator_node(*i, + *s, + si->current_condition(), + si->current_acceptance_conditions(), + nb_node_parity_game++); + duplicator_vertice_.push_back(n2); + } + } + else + delete p; + } + delete s; + } + delete si; + } + Sgi::vector::iterator i2; + for (i2 = trans->begin(); i2 != trans->end(); ++i2) + { + delete *i2; + } + delete trans; + } + } + + void + parity_game_graph_direct::build_link() + { + int nb_ds = 0; + int nb_sd = 0; + spot::state* s = NULL; + + // for each couple of (spoiler, duplicator) + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) + { + for (Sgi::vector::iterator j + = duplicator_vertice_.begin(); + j != duplicator_vertice_.end(); ++j) + { + // We add a link between a duplicator and a spoiler. + if ((*j)->get_spoiler_node()->compare((*i)->get_spoiler_node()) == 0) + { + tgba_succ_iterator* si + = automata_->succ_iter((*j)->get_duplicator_node()); + for (si->first(); !si->done(); si->next()) + { + s = si->current_state(); + if ((s->compare((*i)->get_duplicator_node()) == 0) && + (*j)->implies(si->current_condition(), + si->current_acceptance_conditions())) + { + (*j)->add_succ(*i); + nb_ds++; + } + delete s; + } + delete si; + } + + // We add a link between a spoiler and a duplicator. + if ((*j)->get_duplicator_node()->compare((*i)->get_duplicator_node()) == 0) + { + tgba_succ_iterator* si + = automata_->succ_iter((*i)->get_spoiler_node()); + for (si->first(); !si->done(); si->next()) + { + s = si->current_state(); + if ((s->compare((*j)->get_spoiler_node()) == 0) && + (*j)->match(si->current_condition(), + si->current_acceptance_conditions())) + { + (*i)->add_succ(*j); + nb_sd++; + } + delete s; + } + delete si; + } + } + } + } + + void + parity_game_graph_direct::prune() + { + bool change = true; + + while (change) + { + change = false; + for (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end(); ++i) + { + change |= (*i)->set_win(); + } + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + change |= (*i)->set_win(); + } + } + + } + + simulation_relation* + parity_game_graph_direct::get_relation() + { + simulation_relation* rel = new simulation_relation(); + state_couple* p = NULL; + seen_map::iterator j; + + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + if (!(*i)->not_win) + { + p = new state_couple((*i)->get_spoiler_node(), + (*i)->get_duplicator_node()); + rel->push_back(p); + + + // We remove the state in rel from seen + // because the destructor of + // tgba_reachable_iterator_breadth_first + // delete all the state. + + + if ((j = seen.find(p->first)) != seen.end()) + seen.erase(j); + if ((j = seen.find(p->second)) != seen.end()) + seen.erase(j); + + } + } + + return rel; + } + + parity_game_graph_direct::~parity_game_graph_direct() + { + } + + parity_game_graph_direct::parity_game_graph_direct(const tgba* a) + : parity_game_graph(a) + { + this->build_couple(); + this->build_link(); + this->prune(); + } + + /////////////////////////////////////////////////////////////////////// + + simulation_relation* + get_direct_relation_simulation(const tgba* f, int opt) + { + parity_game_graph_direct* G = new parity_game_graph_direct(f); + simulation_relation* rel = G->get_relation(); + if (opt == 1) + G->print(std::cout); + delete G; + return rel; + } + + void + free_relation_simulation(simulation_relation* rel) + { + if (rel == NULL) + return; + + Sgi::hash_map seen; + Sgi::hash_map::iterator j; + + simulation_relation::iterator i; + for (i = rel->begin(); i != rel->end(); ++i) + { + if ((j = seen.find((*i)->first)) == seen.end()) + seen[(*i)->first] = 0; + + if ((j = seen.find((*i)->second)) == seen.end()) + seen[(*i)->second] = 0; + + delete *i; + } + delete rel; + rel = NULL; + + for (j = seen.begin(); j != seen.end();) + { + const state* ptr = j->first; + ++j; + delete(ptr); + } + } + + bool + is_include(const tgba*, const tgba*) + { + return false; + } + + tgba* + reduc_tgba_sim(const tgba* f, int opt) + { + spot::tgba_reduc* automatareduc = new spot::tgba_reduc(f); + + if (opt & Reduce_Dir_Sim) + { + simulation_relation* rel + = get_direct_relation_simulation(automatareduc); + + automatareduc->display_rel_sim(rel, std::cout); + automatareduc->prune_automata(rel); + + free_relation_simulation(rel); + } + else + if (opt & Reduce_Del_Sim) + { + simulation_relation* rel + = get_delayed_relation_simulation(automatareduc); + + automatareduc->display_rel_sim(rel, std::cout); + automatareduc->prune_automata(rel); + + free_relation_simulation(rel); + } + + if (opt & Reduce_Scc) + { + automatareduc->compute_scc(); + automatareduc->prune_scc(); + } + + return automatareduc; + } + +} diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh new file mode 100644 index 000000000..dd1cd53ac --- /dev/null +++ b/src/tgbaalgos/reductgba_sim.hh @@ -0,0 +1,314 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + + +#ifndef SPOT_REDUC_TGBA_SIM_HH +#define SPOT_REDUC_TGBA_SIM_HH + +#include "tgba/tgbareduc.hh" +#include "tgbaalgos/reachiter.hh" +#include +#include +#include + +namespace spot +{ + + /// Options for reduce. + enum reduce_tgba_options + { + /// No reduction. + Reduce_None = 0, + /// Reduction using direct simulation relation. + Reduce_Dir_Sim = 1, + /// Reduction using delayed simulation relation. + Reduce_Del_Sim = 2, + /// Reduction using SCC. + Reduce_Scc = 4, + /// All reductions. + Reduce_All = -1U + }; + + /// \brief Remove some node of the automata using a simulation + /// relation. + /// + /// \param a the automata to reduce. + /// \param opt a conjonction of spot::reduce_tgba_options specifying + // which optimizations to apply. + /// \return the reduced automata. + tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); + + /// \brief Compute a direct simulation relation on state of tgba \a f. + simulation_relation* get_direct_relation_simulation(const tgba* a, + int opt = -1); + + /// Compute a delayed simulation relation on state of tgba \a f. + /// FIXME : this method is incorrect !! + /// Don't use it !! + simulation_relation* get_delayed_relation_simulation(const tgba* a, + int opt = -1); + + /// To free a simulation relation. + void free_relation_simulation(simulation_relation* rel); + + /// Test if the initial state of a2 fair simulate this of a1. + /// Not implemented. + bool is_include(const tgba* a1, const tgba* a2); + + /////////////////////////////////////////////////////////////////////// + // simulation. + + class spoiler_node; + class duplicator_node; + + typedef Sgi::vector sn_v; + typedef Sgi::vector dn_v; + typedef Sgi::vector s_v; + + /// \brief Parity game graph which compute a simulation relation. + class parity_game_graph : public tgba_reachable_iterator_breadth_first + { + public: + parity_game_graph(const tgba* a); + virtual ~parity_game_graph(); + + virtual simulation_relation* get_relation() = 0; + + void print(std::ostream& os); + + protected: + sn_v spoiler_vertice_; + dn_v duplicator_vertice_; + s_v tgba_state_; + int nb_node_parity_game; + + void start(); + void end(); + void process_state(const state* s, int n, tgba_succ_iterator* si); + void process_link(int in, int out, const tgba_succ_iterator* si); + + /// \brief Compute each node of the graph. + virtual void build_couple() = 0; + + /// \brief Compute the link of the graph. + /// Successor of spoiler node (resp. duplicator node) + /// are duplicator node (resp. spoiler node). + virtual void build_link() = 0; + + /// \brief Remove edge from spoiler to duplicator that make + /// duplicator loose. + /// Spoiler node whose still have some link, reveal + /// a direct simulation relation. + virtual void prune() = 0; + }; + + /////////////////////////////////////////////////////////////////////// + // Direct simulation. + + /// Spoiler node of parity game graph. + class spoiler_node + { + public: + spoiler_node(const state* d_node, + const state* s_node, + int num); + virtual ~spoiler_node(); + + void add_succ(spoiler_node* n); + void del_succ(spoiler_node* n); + virtual void add_pred(spoiler_node* n); + virtual void del_pred(); + int get_nb_succ(); + bool prune(); + virtual bool set_win(); + virtual std::string to_string(const tgba* a); + virtual std::string succ_to_string(); + + const state* get_spoiler_node(); + const state* get_duplicator_node(); + state_couple* get_pair(); + + bool not_win; + int num_; // for the dot display. + + protected: + sn_v* lnode_succ; + sn_v* lnode_pred; + //Sgi::vector* lnode_succ; + state_couple* sc_; + }; + + /// Duplicator node of parity game graph. + class duplicator_node : public spoiler_node + { + public: + duplicator_node(const state* d_node, + const state* s_node, + bdd l, + bdd a, + int num); + virtual ~duplicator_node(); + + virtual bool set_win(); + virtual std::string to_string(const tgba* a); + + bool match(bdd l, bdd a); + bool implies(bdd l, bdd a); + + protected: + bdd label_; + bdd acc_; + }; + + /// Parity game graph which compute the direct simulation relation. + class parity_game_graph_direct : public parity_game_graph + { + public: + parity_game_graph_direct(const tgba* a); + ~parity_game_graph_direct(); + + virtual simulation_relation* get_relation(); + + protected: + + virtual void build_couple(); + virtual void build_link(); + virtual void prune(); + }; + + + /////////////////////////////////////////////////////////////////////// + // Delayed simulation. + + /// Spoiler node of parity game graph for delayed simulation. + class spoiler_node_delayed : public spoiler_node + { + public: + spoiler_node_delayed(const state* d_node, + const state* s_node, + bdd a, + int num); + ~spoiler_node_delayed(); + + /// Return true if the progress_measure has changed. + bool set_win(); + bdd get_acceptance_condition_visited(); + + virtual std::string to_string(const tgba* a); + + int get_progress_measure(); + + protected: + /// a Bdd for retain all the acceptance condition + /// that a node has visited. + bdd acceptance_condition_visited_; + int progress_measure_; + + }; + + /// Duplicator node of parity game graph for delayed simulation. + class duplicator_node_delayed : public duplicator_node + { + public: + duplicator_node_delayed(const state* d_node, + const state* s_node, + bdd l, + bdd a, + int num); + ~duplicator_node_delayed(); + + /// Return true if the progress_measure has changed. + bool set_win(); + virtual std::string to_string(const tgba* a); + + bool implies_label(bdd l); + bool implies_acc(bdd a); + + int get_progress_measure(); + + protected: + int progress_measure_; + }; + + /// Parity game graph which compute the delayed simulation relation + /// as explain in + /// @inproceedings{ icalp2001, + /// AUTHOR = {Etessami, Thomas Wilke, Rebecca A. Schuller}, + /// TITLE = {Fair Simulation Relations, Parity Games, and State Space + /// Reduction for Buchi Automata}, + /// BOOKTITLE = {Automata, Languages and Programming, + /// 28th international collquium}, + /// PAGES = {694--707}, + /// YEAR = 2001, + /// EDITOR = {Orejas, Fernando and Spirakis, Paul G. and van Leeuwen, Jan}, + /// VOLUME = 2076, + /// SERIES = {Lecture Notes in Computer Science}, + /// ADDRESS = {Crete, Greece}, + /// MONTH = JUL, + /// PUBLISHER = {Springer}, + /// url = {citeseer.ist.psu.edu/472661.html} + /// } + + class parity_game_graph_delayed : public parity_game_graph + { + public: + parity_game_graph_delayed(const tgba* a); + ~parity_game_graph_delayed(); + + virtual simulation_relation* get_relation(); + + private: + + /// Vector which contain all the sub-set of the set + /// of acceptance condition. + typedef Sgi::vector bdd_v; + bdd_v sub_set_acc_cond_; + + /// Return the number of acceptance condition. + int nb_set_acc_cond(); + + /// Compute sub_set_acc_cond_; + void build_sub_set_acc_cond(); + + /// Add a duplicator node, and + /// all his successor (spoiler node) which + /// have a acceptance_condition_visited_ != bddfalse + void add_dup_node(state* ss, + state* sd, + bdd l, + bdd a); + + /// \brief Compute the couple as for direct simulation, + virtual void build_couple(); + virtual void build_link(); + void build_recurse_successor_spoiler(spoiler_node* sn); + void build_recurse_successor_duplicator(duplicator_node* dn); + + /// \brief The Jurdzinski's lifting algorithm. + void lift(); + + /// \brief Remove all node so as to there is no dead ends (terminal node). + virtual void prune(); + }; + +} + +#endif diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc new file mode 100644 index 000000000..5f42eda5b --- /dev/null +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -0,0 +1,816 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "reductgba_sim.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + /// Number of spoiler node with a one priority (see icalp2001). + /// The one priority is represent by a \a acceptance_condition_visited_ + /// which differ of bddfalse. + /// This spoiler node are looser for the duplicator. + static int nb_spoiler_loose_; + + static int nb_spoiler; + static int nb_duplicator; + + //static int nb_node; + + /////////////////////////////////////////////////////////////////////// + // spoiler_node_delayed + + spoiler_node_delayed::spoiler_node_delayed(const state* d_node, + const state* s_node, + bdd a, + int num) + : spoiler_node(d_node, s_node, num), + acceptance_condition_visited_(a) + { + nb_spoiler++; + progress_measure_ = 0; + if (acceptance_condition_visited_ == bddfalse) + nb_spoiler_loose_++; + } + + spoiler_node_delayed::~spoiler_node_delayed() + { + } + + bool + spoiler_node_delayed::set_win() + { + // We take the max of the progress measure of the successor node + // because we are on a spoiler. + + //std::cout << "spoiler_node_delayed::set_win" << std::endl; + + if (lnode_succ->size() == 0) + progress_measure_ = nb_spoiler_loose_; + + if (progress_measure_ >= nb_spoiler_loose_) + return false; + + bool change; + int tmpmax = 0; + int tmp = 0; + sn_v::iterator i = lnode_succ->begin(); + if (i != lnode_succ->end()) + { + tmpmax = + dynamic_cast(*i)->get_progress_measure(); + ++i; + } + for (; i != lnode_succ->end(); ++i) + { + tmp = + dynamic_cast(*i)->get_progress_measure(); + if (tmp > tmpmax) + tmpmax = tmp; + } + + // If the priority of the node is 1 + // acceptance_condition_visited_ != bddfalse + // then we increment the progress measure of 1. + if (acceptance_condition_visited_ != bddfalse) + tmpmax++; + + change = (progress_measure_ < tmpmax); + + progress_measure_ = tmpmax; + return change; + } + + std::string + spoiler_node_delayed::to_string(const tgba* a) + { + std::ostringstream os; + + // print the node. + os << num_ + << " [shape=box, label=\"(" + << a->format_state(sc_->first) + << ", " + << a->format_state(sc_->second) + << ", "; + //bdd_print_acc(os, a->get_dict(), acceptance_condition_visited_); + if (acceptance_condition_visited_ == bddfalse) + { + os << "false"; + } + else + { + os << "ACC"; + } + os << ")" + << " pm = " << progress_measure_ << "\"]" + << std::endl; + + return os.str(); + } + + bdd + spoiler_node_delayed::get_acceptance_condition_visited() + { + return acceptance_condition_visited_; + } + + int + spoiler_node_delayed::get_progress_measure() + { + if ((acceptance_condition_visited_ == bddfalse) && + (progress_measure_ != (nb_spoiler_loose_ + 1))) + return 0; + else + return progress_measure_; + } + + /////////////////////////////////////////////////////////////////////// + // duplicator_node_delayed + + duplicator_node_delayed::duplicator_node_delayed(const state* d_node, + const state* s_node, + bdd l, + bdd a, + int num) + : duplicator_node(d_node, s_node, l, a, num) + { + nb_duplicator++; + progress_measure_ = 0; + } + + duplicator_node_delayed::~duplicator_node_delayed() + { + } + + bool + duplicator_node_delayed::set_win() + { + // We take the min of the progress measure of the successor node + // because we are on a duplicator. + + //std::cout << "duplicator_node_delayed::set_win" << std::endl; + + //bool debug = true; + + if (progress_measure_ == nb_spoiler_loose_) + return false; + + bool change; + int tmpmin = 0; + int tmp = 0; + sn_v::iterator i = lnode_succ->begin(); + if (i != lnode_succ->end()) + { + tmpmin = dynamic_cast(*i)->get_progress_measure(); + /* + debug &= (dynamic_cast(*i) + ->get_acceptance_condition_visited() + != bddfalse); + */ + ++i; + } + for (; i != lnode_succ->end(); ++i) + { + /* + debug &= (dynamic_cast(*i) + ->get_acceptance_condition_visited() + != bddfalse); + */ + tmp = dynamic_cast(*i)->get_progress_measure(); + if (tmp < tmpmin) + tmpmin = tmp; + } + + /* + if (debug) + std::cout << "All successor p = 1" << std::endl; + else + std::cout << "Not All successor p = 1" << std::endl; + */ + + change = (progress_measure_ < tmpmin); + progress_measure_ = tmpmin; + return change; + } + + std::string + duplicator_node_delayed::to_string(const tgba* a) + { + std::ostringstream os; + + // print the node. + os << num_ + << " [shape=box, label=\"(" + << a->format_state(sc_->first) + << ", " + << a->format_state(sc_->second); + //<< ", "; + //bdd_print_acc(os, a->get_dict(), acc_); + os << ")" + << " pm = " << progress_measure_ << "\"]" + << std::endl; + + return os.str(); + } + + bool + duplicator_node_delayed::implies_label(bdd l) + { + return ((l | !label_) == bddtrue); + } + + bool + duplicator_node_delayed::implies_acc(bdd a) + { + return ((a | !acc_) == bddtrue); + } + + int + duplicator_node_delayed::get_progress_measure() + { + return progress_measure_; + } + + /////////////////////////////////////////////////////////////////////// + // parity_game_graph_delayed + + int + parity_game_graph_delayed::nb_set_acc_cond() + { + bdd acc, all; + acc = all = automata_->all_acceptance_conditions(); + int count = 0; + while (all != bddfalse) + { + sub_set_acc_cond_.push_back(bdd_satone(all)); + all -= bdd_satone(all); + count++; + } + return count; + } + + void + parity_game_graph_delayed::build_sub_set_acc_cond() + { + // compute the number of acceptance conditions + bdd acc, all; + acc = all = automata_->all_acceptance_conditions(); + int count = 0; + while (all != bddfalse) + { + //std::cout << "add acc" << std::endl; + sub_set_acc_cond_.push_back(bdd_satone(all)); + all -= bdd_satone(all); + count++; + } + // sub_set_acc_cond_ contains all the acceptance condition. + // but we must have all the sub-set of acceptance condition. + // In fact we must have 2^count sub-set. + + if (count == 2) + { + sub_set_acc_cond_.push_back(acc); + sub_set_acc_cond_.push_back(bddfalse); + } + + /* + bdd_v::iterator i; + + bdd_v::iterator j; + for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end(); ++i) + for (j = sub_set_acc_cond_.begin(); j != sub_set_acc_cond_.end(); ++j) + sub_set_acc_cond_.push_back(*i | *j); + + std::cout << std::endl; + for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end();) + { + bdd_print_acc(std::cout, automata_->get_dict(), *i); + std::cout << " // " << std::endl; + ++i; + } + std::cout << std::endl; + */ + } + + + void + parity_game_graph_delayed::build_couple() + { + //std::cout << "build couple" << std::endl; + + nb_spoiler = 0; + nb_duplicator = 0; + + tgba_succ_iterator* si = NULL; + typedef Sgi::pair couple_bdd; + couple_bdd *p = NULL; + Sgi::vector* trans = NULL; + bool exist = false; + spot::state* s = NULL; + + s_v::iterator i; + for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i) + { + + // for each sub-set of the set of acceptance condition. + bdd_v::iterator i2; + for (i2 = sub_set_acc_cond_.begin(); + i2 != sub_set_acc_cond_.end(); ++i2) + { + + // spoiler node are all state couple (i,j) + // multiply by 2^(|F|) + s_v::iterator i3; + for (i3 = tgba_state_.begin(); + i3 != tgba_state_.end(); ++i3) + { + //nb_spoiler++; + spoiler_node_delayed* n1 + = new spoiler_node_delayed(*i, + *i3, + *i2, + nb_node_parity_game++); + spoiler_vertice_.push_back(n1); + } + + // duplicator node are all state couple where + // the first state i are reachable. + trans = new Sgi::vector; + for (i3 = tgba_state_.begin(); + i3 != tgba_state_.end(); ++i3) + { + si = automata_->succ_iter(*i3); + for (si->first(); !si->done(); si->next()) + { + + // if there exist a predecessor of i named j + s = si->current_state(); + if (s->compare(*i) == 0) + { + + // p is the label of the transition j->i + p = new couple_bdd(si->current_condition(), + si->current_acceptance_conditions()); + + // If an other predecessor of i has the same label p + // to reach i, then we don't compute the + // duplicator node. + exist = false; + Sgi::vector::iterator i4; + for (i4 = trans->begin(); + i4 != trans->end(); ++i4) + { + if ((si->current_condition() == (*i4)->first)) + // We don't need the acceptance condition + //&& + //(si->current_acceptance_conditions() + //== (*i4)->second)) + exist = true; + } + + if (!exist) + { + // We build all the state couple with the label p. + // multiply by 2^(|F|) + trans->push_back(p); + Sgi::vector::iterator i5; + for (i5 = tgba_state_.begin(); + i5 != tgba_state_.end(); ++i5) + { + //nb_duplicator++; + int nb = nb_node_parity_game++; + duplicator_node_delayed* n2 + = new + duplicator_node_delayed(*i, + *i5, + si-> + current_condition(), + *i2, + nb); + duplicator_vertice_.push_back(n2); + } + } + else + delete p; + } + delete s; + } + delete si; + } + Sgi::vector::iterator i6; + for (i6 = trans->begin(); i6 != trans->end(); ++i6) + { + delete *i6; + } + delete trans; + } + } + nb_spoiler_loose_++; + + //std::cout << "spoiler node : " << nb_spoiler << std::endl; + //std::cout << "duplicator node : " << nb_duplicator << std::endl; + //std::cout << "nb_spoiler_loose_ : " << nb_spoiler_loose_ << std::endl; + } + + void + parity_game_graph_delayed::build_link() + { + //std::cout << "build link" << std::endl; + int nb_ds = 0; + int nb_sd = 0; + spot::state* s = NULL; + + // for each couple of (spoiler, duplicator) + sn_v::iterator i; + for (i = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) + { + dn_v::iterator i2; + for (i2 = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + { + + // We add a link between a duplicator and a spoiler. + if ((*i2)->get_spoiler_node()->compare((*i) + ->get_spoiler_node()) == 0) + { + tgba_succ_iterator* si + = automata_->succ_iter((*i2)->get_duplicator_node()); + for (si->first(); !si->done(); si->next()) + { + s = si->current_state(); + + bdd btmp2 = dynamic_cast(*i)-> + get_acceptance_condition_visited(); + bdd btmp = btmp2 - si->current_acceptance_conditions(); + + //if ((s->compare((*i)->get_duplicator_node()) == 0) && + //dynamic_cast(*i2)-> + // implies_label(si->current_condition()) && + //(btmp == btmp2)) + + if ((s->compare((*i)->get_duplicator_node()) == 0) && + dynamic_cast(*i2)-> + implies_label(si->current_condition()) && + (dynamic_cast(*i)-> + get_acceptance_condition_visited() != bddfalse)) + { + //std::cout << "add duplicator -> spoiler" << std::endl; + (*i2)->add_succ(*i); + (*i)->add_pred(*i2); + nb_ds++; + } + delete s; + } + delete si; + } + + // We add a link between a spoiler and a duplicator. + if ((*i2)->get_duplicator_node() + ->compare((*i)->get_duplicator_node()) == 0) + { + tgba_succ_iterator* si + = automata_->succ_iter((*i)->get_spoiler_node()); + for (si->first(); !si->done(); si->next()) + { + s = si->current_state(); + + bdd btmp = si->current_acceptance_conditions() | + dynamic_cast(*i)-> + get_acceptance_condition_visited(); + if ((s->compare((*i2)->get_spoiler_node()) == 0) && + (*i2)->match(si->current_condition(), btmp)) + { + //std::cout << "add spoiler -> duplicator" << std::endl; + (*i)->add_succ(*i2); + (*i2)->add_pred(*i); + nb_sd++; + } + delete s; + } + delete si; + } + + } + } + } + + /* + // We build only node which are reachable + void + parity_game_graph_delayed::build_couple() + { + // We build only some "basic" spoiler node. + + s_v::iterator i; + for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i) + { + + // spoiler node are all state couple (i,j) + s_v::iterator i2; + for (i2 = tgba_state_.begin(); + i2 != tgba_state_.end(); ++i2) + { + std::cout << "add spoiler node" << std::endl; + nb_spoiler++; + spoiler_node_delayed* n1 + = new spoiler_node_delayed(*i, *i2, + bddfalse, + nb_node_parity_game++); + spoiler_vertice_.push_back(n1); + } + } + } + + void + parity_game_graph_delayed::build_link() + { + // We create when it's possible a duplicator node + // and recursively his successor. + + 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(); + if (s1->compare((*i1)->get_duplicator_node()) == 0) + { + tgba_succ_iterator* si; + s_v::iterator i2; + spot::state* s2 = NULL; + for (i2 = tgba_state_.begin(); + i2 != tgba_state_.end(); ++i2) + { + si = automata_->succ_iter(*i2); + s2 = si->current_state(); + if (s2->compare(s1) == 0) + exist_pred = true; + delete s2; + } + } + else + exist_pred = true; + delete s1; + + if (!exist_pred) + continue; + + // We add a link between a spoiler and a (new) duplicator. + // The acc of the duplicator must contains the + // acceptance_condition_visited_ of the spoiler. + build_recurse_successor_spoiler(*i1); + + } + + } + + void + parity_game_graph_delayed::build_recurse_successor_spoiler(spoiler_node* sn) + { + tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); + + for (si->first(); !si->done(); si->next()) + { + bdd btmp = si->current_acceptance_conditions() | + dynamic_cast(sn)-> + get_acceptance_condition_visited(); + + s_v::iterator i1; + state* s; + for (i1 = tgba_state_.begin(); + i1 != tgba_state_.end(); ++i1) + { + s = si->current_state(); + if (s->compare(*i1) == 0) + { + duplicator_node_delayed* dn + = new duplicator_node_delayed(*i1, + sn->get_duplicator_node(), + si->current_condition(), + btmp, + nb_node_parity_game++); + duplicator_vertice_.push_back(dn); + + sn->add_succ(dn); + (dn)->add_pred(sn); + + build_recurse_successor_duplicator(dn); + } + delete s; + } + } + + delete si; + + } + + void + parity_game_graph_delayed:: + build_recurse_successor_duplicator(duplicator_node* dn) + { + tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); + + for (si->first(); !si->done(); si->next()) + { + bdd btmp = + dynamic_cast(sn)-> + get_acceptance_condition_visited(); + bdd btmp2 = btmp - si->current_acceptance_conditions(); + + s_v::iterator i1; + state* s; + for (i1 = tgba_state_.begin(); + i1 != tgba_state_.end(); ++i1) + { + s = si->current_state(); + if (s->compare(*i1) == 0) + { + spoiler_node_delayed* sn + = new spoiler_node_delayed(sn->get_spoiler_node(), + *i1, + bddtmp2, + nb_node_parity_game++); + spoiler_vertice_.push_back(n1); + + sn->add_succ(dn); + (dn)->add_pred(sn); + + build_recurse_successor_spoiler(sn); + + } + delete s; + } + } + + delete si; + + } + */ + + void + parity_game_graph_delayed::add_dup_node(state*, + state*, + bdd, + bdd) + { + } + + void + parity_game_graph_delayed::prune() + { + + bool change = true; + + while (change) + { + change = false; + for (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end();) + { + if ((*i)->get_nb_succ() == 0) + { + (*i)->del_pred(); + delete *i; + i = duplicator_vertice_.erase(i); + change = true; + } + else + ++i; + } + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end();) + { + if ((*i)->get_nb_succ() == 0) + { + (*i)->del_pred(); + delete *i; + i = spoiler_vertice_.erase(i); + change = true; + } + else + ++i; + } + } + + } + + void + parity_game_graph_delayed::lift() + { + // Jurdzinski's algorithm + //int iter = 0; + bool change = true; + + while (change) + { + change = false; + for (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end(); ++i) + { + change |= (*i)->set_win(); + } + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + change |= (*i)->set_win(); + } + } + + } + + simulation_relation* + parity_game_graph_delayed::get_relation() + { + simulation_relation* rel = new simulation_relation(); + state_couple* p = NULL; + seen_map::iterator j; + + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + if (dynamic_cast(*i)->get_progress_measure() + < nb_spoiler_loose_) + { + p = new state_couple((*i)->get_spoiler_node(), + (*i)->get_duplicator_node()); + rel->push_back(p); + + // We remove the state in rel from seen + // because the destructor of + // tgba_reachable_iterator_breadth_first + // delete all the state. + + if ((j = seen.find(p->first)) != seen.end()) + seen.erase(j); + if ((j = seen.find(p->second)) != seen.end()) + seen.erase(j); + } + + } + + return rel; + } + + parity_game_graph_delayed::~parity_game_graph_delayed() + { + } + + parity_game_graph_delayed::parity_game_graph_delayed(const tgba* a) + : parity_game_graph(a) + { + nb_spoiler_loose_ = 0; + /* + if (this->nb_set_acc_cond() > 2) + return; + this->build_sub_set_acc_cond(); + */ + this->build_couple(); + this->build_link(); + this->prune(); + this->lift(); + //this->print(std::cout); + } + + /////////////////////////////////////////// + simulation_relation* + get_delayed_relation_simulation(const tgba* f, int opt) + { + /// FIXME : this method is incorrect !! + /// Don't use it !! + parity_game_graph_delayed* G = new parity_game_graph_delayed(f); + simulation_relation* rel = G->get_relation(); + if (opt == 1) + G->print(std::cout); + delete G; + return rel; + } + +} diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index c7fe8d34f..6acc0f366 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -38,6 +38,7 @@ check_PROGRAMS = \ mixprod \ powerset \ readsave \ + reductgba \ tgbaread \ tripprod @@ -53,12 +54,14 @@ ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc readsave_SOURCES = readsave.cc +reductgba_SOURCES = reductgba.cc 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 = \ + reductgba.test \ explicit.test \ tgbaread.test \ readsave.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 85a77e712..af33b66d2 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -25,6 +25,7 @@ #include #include "ltlvisit/destroy.hh" #include "ltlvisit/reducform.hh" +#include "ltlvisit/tostring.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" @@ -40,6 +41,8 @@ #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/reductgba_sim.hh" + void syntax(char* prog) { @@ -83,6 +86,7 @@ syntax(char* prog) << " -r3 reduce formula using implication between " << "sub-formulae" << std::endl << " -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 << " -s convert to explicit automata, and number states " << "in DFS order" << std::endl @@ -98,7 +102,17 @@ 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; + << "(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; exit(2); } @@ -120,7 +134,10 @@ main(int argc, char** argv) bool magic_many = false; bool expect_counter_example = false; bool from_file = false; + int reduc_aut = spot::Reduce_None; int redopt = spot::ltl::Reduce_None; + bool display_reduce_form = false; + bool display_rel_sim = false; bool post_branching = false; bool fair_loop_approx = false; @@ -226,11 +243,11 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-r2")) { - redopt |= spot::ltl::Reduce_Syntactic_Implications; + redopt |= spot::ltl::Reduce_Eventuality_And_Universality; } else if (!strcmp(argv[formula_index], "-r3")) { - redopt |= spot::ltl::Reduce_Eventuality_And_Universality; + redopt |= spot::ltl::Reduce_Syntactic_Implications; } else if (!strcmp(argv[formula_index], "-r4")) { @@ -274,6 +291,28 @@ main(int argc, char** argv) fm_opt = true; fm_symb_merge_opt = false; } + else if (!strcmp(argv[formula_index], "-R1")) + { + reduc_aut |= spot::Reduce_Dir_Sim; + fair_loop_approx = true; + } + else if (!strcmp(argv[formula_index], "-R2")) + { + reduc_aut |= spot::Reduce_Del_Sim; + fair_loop_approx = true; + } + else if (!strcmp(argv[formula_index], "-R3")) + { + reduc_aut |= spot::Reduce_Scc; + } + else if (!strcmp(argv[formula_index], "-rd")) + { + display_reduce_form = true; + } + else if (!strcmp(argv[formula_index], "-Rd")) + { + display_rel_sim = true; + } else { break; @@ -341,6 +380,8 @@ main(int argc, char** argv) spot::ltl::formula* t = spot::ltl::reduce(f, redopt); spot::ltl::destroy(f); f = t; + if (display_reduce_form) + std::cout << spot::ltl::to_string(f) << std::endl; } if (fm_opt) @@ -352,6 +393,46 @@ 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) + { + a = aut_red = new spot::tgba_reduc(a); + if ((reduc_aut & spot::Reduce_Dir_Sim) || + (reduc_aut & spot::Reduce_Del_Sim)) + { + spot::simulation_relation* rel; + if (reduc_aut & spot::Reduce_Dir_Sim) + rel = spot::get_direct_relation_simulation(a); + else if (reduc_aut & spot::Reduce_Del_Sim) + rel = spot::get_delayed_relation_simulation(a, 1); + else + assert(0); + + if (display_rel_sim) + aut_red->display_rel_sim(rel, std::cout); + + if (reduc_aut & spot::Reduce_Dir_Sim) + aut_red->prune_automata(rel); + else if (reduc_aut & spot::Reduce_Del_Sim) + aut_red->quotient_state(rel); + else + assert(0); + + spot::free_relation_simulation(rel); + } + + if (reduc_aut & spot::Reduce_Scc) + { + aut_red->prune_scc(); + } + } + spot::tgba_tba_proxy* degeneralized = 0; if (degeneralize_opt) a = degeneralized = new spot::tgba_tba_proxy(a); @@ -477,6 +558,8 @@ main(int argc, char** argv) delete expl; if (degeneralize_opt) delete degeneralized; + if (aut_red) + delete aut_red; delete to_free; } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index cdd00503f..5bdf468e9 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -30,15 +30,15 @@ set -e cat > config <