From 84060b49e582be37c957efae2769ed0991c52128 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Fri, 16 Oct 2009 17:00:46 +0200 Subject: [PATCH] Minor fixes. * src/misc/bddop.hh, src/tgba/taa.hh, src/tgbaalgos/ltl2taa.hh: Fix sanity (incorrect include guard). * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: Copyright 2009. * src/tgbaalgos/eltl2tgba_lacim.cc: Use abbreviations. * src/tgbatest/taa.cc: Fix it. --- ChangeLog | 11 +++++++++++ src/misc/bddop.hh | 6 +++--- src/tgba/taa.hh | 6 +++--- src/tgba/tgbacomplement.cc | 21 +++++++++++++++++++++ src/tgba/tgbacomplement.hh | 21 +++++++++++++++++++++ src/tgbaalgos/eltl2tgba_lacim.cc | 4 ++-- src/tgbaalgos/ltl2taa.hh | 6 +++--- src/tgbatest/taa.cc | 31 ++++++------------------------- 8 files changed, 70 insertions(+), 36 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8a1741cab..8938b9990 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2009-10-16 Damien Lefortier + + Minor fixes. + + * src/misc/bddop.hh, src/tgba/taa.hh, src/tgbaalgos/ltl2taa.hh: + Fix sanity (incorrect include guard). + * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: + Copyright 2009. + * src/tgbaalgos/eltl2tgba_lacim.cc: Use abbreviations. + * src/tgbatest/taa.cc: Fix it. + 2009-10-16 Damien Lefortier Add a new algorithm (from Tauriainen) to translate LTL formulae to diff --git a/src/misc/bddop.hh b/src/misc/bddop.hh index c374ae294..571354e83 100644 --- a/src/misc/bddop.hh +++ b/src/misc/bddop.hh @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_MISC_BDDOP_HH_ -# define SPOT_MISC_BDDOP_HH_ +#ifndef SPOT_MISC_BDDOP_HH +# define SPOT_MISC_BDDOP_HH #include "bdd.h" @@ -31,4 +31,4 @@ namespace spot bdd compute_all_acceptance_conditions(bdd neg_acceptance_conditions); } -#endif /* !SPOT_MISC_BDDOP_HH_ */ +#endif // SPOT_MISC_BDDOP_HH diff --git a/src/tgba/taa.hh b/src/tgba/taa.hh index 7319476c8..70a66fdec 100644 --- a/src/tgba/taa.hh +++ b/src/tgba/taa.hh @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBA_TAA_HH_ -# define SPOT_TGBA_TAA_HH_ +#ifndef SPOT_TGBA_TAA_HH +# define SPOT_TGBA_TAA_HH #include #include @@ -172,4 +172,4 @@ namespace spot }; } -#endif /* !SPOT_TGBA_TAAEXPLICIT_HH_ */ +#endif // SPOT_TGBA_TAA_HH diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc index 223a62950..830aff79a 100644 --- a/src/tgba/tgbacomplement.cc +++ b/src/tgba/tgbacomplement.cc @@ -1,3 +1,24 @@ +// Copyright (C) 2009 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 #include #include diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbacomplement.hh index 36dea136c..1c7eb08bf 100644 --- a/src/tgba/tgbacomplement.hh +++ b/src/tgba/tgbacomplement.hh @@ -1,3 +1,24 @@ +// Copyright (C) 2009 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_TGBACOMPLEMENT_HH #define SPOT_TGBA_TGBACOMPLEMENT_HH diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 19a580af8..9f0590331 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -37,7 +37,7 @@ namespace spot using namespace ltl; /// \brief Recursively translate a formula into a BDD. - class eltl_trad_visitor: public const_visitor + class eltl_trad_visitor : public const_visitor { public: eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) @@ -290,7 +290,7 @@ namespace spot // Traverse the formula and draft the automaton in a factory. tgba_bdd_concrete_factory fact(dict); eltl_trad_visitor v(fact, true); - f->accept(v); + f2->accept(v); ltl::destroy(f2); fact.finish(); diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index e6d41b441..6f6928375 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TAAALGOS_LTL2TAA_HH_ -# define SPOT_TAAALGOS_LTL2TAA_HH_ +#ifndef SPOT_TGBAALGOS_LTL2TAA_HH +# define SPOT_TGBAALGOS_LTL2TAA_HH #include "ltlast/formula.hh" #include "tgba/taa.hh" @@ -51,4 +51,4 @@ namespace spot taa* ltl_to_taa(const ltl::formula* f, bdd_dict* dict); } -#endif /* !SPOT_TAAALGOS_LTL2TAA_HH_ */ +#endif // SPOT_TGBAALGOS_LTL2TAA_HH diff --git a/src/tgbatest/taa.cc b/src/tgbatest/taa.cc index f4d0699b6..1851311e6 100644 --- a/src/tgbatest/taa.cc +++ b/src/tgbatest/taa.cc @@ -24,29 +24,9 @@ #include "misc/hash.hh" #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" +#include "tgbaalgos/dotty.hh" #include "tgba/taa.hh" -typedef Sgi::hash_set< - const spot::state*, spot::state_ptr_hash, spot::state_ptr_equal - > mset; - -void -dfs(spot::taa* a, const spot::state* s, mset& m) -{ - if (m.find(s) != m.end()) - return; - m.insert(s); - - spot::tgba_succ_iterator* i = a->succ_iter(s); - assert(i); - for (i->first(); !i->done(); i->next()) - { - std::cout << a->format_state(i->current_state()) << std::endl; - dfs(a, i->current_state(), m); - } - delete i; -} - int main() { @@ -70,11 +50,12 @@ main() a->add_condition(t2, e.require("b")); a->add_condition(t3, e.require("c")); - mset m; - spot::state* init = a->get_init_state(); - dfs(a, init, m); + spot::dotty_reachable(std::cout, a); - delete init; delete a; delete dict; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); }