diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index c7d51258a..e4ff5a61b 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -20,10 +20,14 @@ // 02111-1307, USA. #include +#include #include #include #include #include +#include +#include +#include #include "bdddict.hh" namespace spot @@ -140,6 +144,24 @@ namespace spot } + int + bdd_dict::register_clone_acc(int var, const void* for_me) + { + vf_map::iterator i = acc_formula_map.find(var); + assert(i != acc_formula_map.end()); + std::ostringstream s; + // FIXME: We could be smarter and reuse unused "$n" numbers. + s << ltl::to_string(i->second) << "$" + << ++clone_counts[var]; + ltl::formula* f = + ltl::atomic_prop::instance(s.str(), + ltl::default_environment::instance()); + int res = register_acceptance_variable(f, for_me); + ltl::destroy(f); + return res; + } + + int bdd_dict::register_anonymous_variables(int n, const void* for_me) { diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 43ac4670c..434d77703 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -54,6 +54,10 @@ namespace spot fv_map acc_map; ///< Maps acceptance conditions to BDD variables vf_map acc_formula_map; ///< Maps BDD variables to acceptance conditions + /// Clone counts. + typedef std::map cc_map; + cc_map clone_counts; + /// \brief Map Next variables to Now variables. /// /// Use with BuDDy's bdd_replace() function. @@ -109,6 +113,13 @@ namespace spot /// to convert this to a BDD. int register_acceptance_variable(const ltl::formula* f, const void* for_me); + /// \brief Clone an acceptance variable VAR for FOR_ME. + /// + /// This is used in products TGBAs when both operands share the + /// same acceptance variables but they need to be distinguished in + /// the result. + int register_clone_acc(int var, const void* for_me); + /// \brief Register BDD variables as acceptance variables. /// /// Register all variables occurring in \a f as acceptance variables diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 0c591a4ea..4439eea97 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -72,10 +72,11 @@ namespace spot tgba_succ_iterator_product::tgba_succ_iterator_product (tgba_succ_iterator* left, tgba_succ_iterator* right, - bdd left_neg, bdd right_neg) + bdd left_neg, bdd right_neg, bddPair* right_common_acc) : left_(left), right_(right), left_neg_(left_neg), - right_neg_(right_neg) + right_neg_(right_neg), + right_common_acc_(right_common_acc) { } @@ -165,7 +166,8 @@ namespace spot bdd tgba_succ_iterator_product::current_acceptance_conditions() const { return ((left_->current_acceptance_conditions() & right_neg_) - | (right_->current_acceptance_conditions() & left_neg_)); + | (bdd_replace(right_->current_acceptance_conditions(), + right_common_acc_) & left_neg_)); } //////////////////////////////////////////////////////////// @@ -178,13 +180,31 @@ namespace spot bdd lna = left_->neg_acceptance_conditions(); bdd rna = right_->neg_acceptance_conditions(); - left_acc_complement_ = bdd_exist(lna, bdd_support(rna)); - right_acc_complement_ = bdd_exist(rna, bdd_support(lna)); - all_acceptance_conditions_ = ((left_->all_acceptance_conditions() - & right_acc_complement_) - | (right_->all_acceptance_conditions() - & left_acc_complement_)); + right_common_acc_ = bdd_newpair(); + bdd common = bdd_exist(lna, bdd_exist(lna, rna)); + while (common != bddtrue) + { + assert(bdd_high(common) == bddfalse); + int var = bdd_var(common); + int varclone = dict_->register_clone_acc(var, this); + bdd_setpair(right_common_acc_, var, varclone); + common = bdd_low(common); + } + + bdd lac = left_->all_acceptance_conditions(); + bdd rac = right_->all_acceptance_conditions(); + + rna = bdd_replace(rna, right_common_acc_); + rac = bdd_replace(rac, right_common_acc_); + + left_acc_complement_ = lna; + assert(bdd_exist(lna, rna) == lna); + right_acc_complement_ = rna; + assert(bdd_exist(rna, lna) == rna); + + all_acceptance_conditions_ = ((lac & right_acc_complement_) + | (rac & left_acc_complement_)); neg_acceptance_conditions_ = lna & rna; dict_->register_all_variables_of(&left_, this); @@ -193,6 +213,7 @@ namespace spot tgba_product::~tgba_product() { + bdd_freepair(right_common_acc_); dict_->unregister_all_my_variables(this); } @@ -226,7 +247,8 @@ namespace spot global_state, global_automaton); return new tgba_succ_iterator_product(li, ri, left_acc_complement_, - right_acc_complement_); + right_acc_complement_, + right_common_acc_); } bdd diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index eacd4a653..8d8ad79cb 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -80,7 +80,8 @@ namespace spot public: tgba_succ_iterator_product(tgba_succ_iterator* left, tgba_succ_iterator* right, - bdd left_neg, bdd right_neg); + bdd left_neg, bdd right_neg, + bddPair* right_common_acc); virtual ~tgba_succ_iterator_product(); @@ -107,6 +108,7 @@ namespace spot bdd current_cond_; bdd left_neg_; bdd right_neg_; + bddPair* right_common_acc_; friend class tgba_product; }; @@ -153,6 +155,7 @@ namespace spot bdd right_acc_complement_; bdd all_acceptance_conditions_; bdd neg_acceptance_conditions_; + bddPair* right_common_acc_; // Disallow copy. tgba_product(const tgba_product&); tgba_product& operator=(const tgba_product&); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 6d81d3496..b3ec54301 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,6 +1,6 @@ -## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. +## Copyright (C) 2003, 2004, 2005, 2006 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. ## @@ -75,6 +75,7 @@ TESTS = \ explprod.test \ explpro2.test \ explpro3.test \ + explpro4.test \ tripprod.test \ mixprod.test \ dupexp.test \ diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index 8545c5653..931b22052 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -1,7 +1,7 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2003, 2004, 2005, 2006 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. # @@ -37,9 +37,9 @@ s1, s2, "b", p2; s1, s3, "a", p3; EOF -cat >expected <expected <<'EOF' +acc = "p2$1" "p3" "p2" "p1"; +"s1 * s1", "s2 * s2", "b & !a", "p2$1" "p1"; "s1 * s1", "s3 * s3", "a & !b", "p3" "p2"; EOF diff --git a/src/tgbatest/explpro4.test b/src/tgbatest/explpro4.test new file mode 100755 index 000000000..c10bcec67 --- /dev/null +++ b/src/tgbatest/explpro4.test @@ -0,0 +1,49 @@ +#!/bin/sh +# Copyright (C) 2006 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. + + +. ./defs + +set -e + +cat >input1 <input2 <expected <<'EOF' +acc = "p1$1" "p1"; +"s1 * s1", "s1 * s1", "a", "p1"; +"s1 * s1", "s1 * s1", "!a", "p1$1"; +EOF + +run 0 ./explprod input1 input2 > stdout +cat stdout +diff stdout expected +rm input1 input2 stdout expected