* src/tgba/bdddict.cc, src/tgba/bdddict.cc (register_clone_acc):
New function. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Use it to distinguish acceptance conditions that are identical in both operands. * src/tgbatest/explpro4.test: New file. * src/tgbatest/explpro2.test, src/tgbatest/Makefile.am: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
cb9549e4d4
commit
c412cd4cc3
7 changed files with 129 additions and 21 deletions
|
|
@ -20,10 +20,14 @@
|
|||
// 02111-1307, USA.
|
||||
|
||||
#include <ostream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <ltlvisit/clone.hh>
|
||||
#include <ltlvisit/destroy.hh>
|
||||
#include <ltlvisit/tostring.hh>
|
||||
#include <ltlvisit/tostring.hh>
|
||||
#include <ltlast/atomic_prop.hh>
|
||||
#include <ltlenv/defaultenv.hh>
|
||||
#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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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<int, int> 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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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&);
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
acc = "p3" "p2" "p1";
|
||||
"s1 * s1", "s2 * s2", "b & !a", "p2" "p1";
|
||||
cat >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
|
||||
|
||||
|
|
|
|||
49
src/tgbatest/explpro4.test
Executable file
49
src/tgbatest/explpro4.test
Executable file
|
|
@ -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 <<EOF
|
||||
acc = p1;
|
||||
s1, s1, "a", p1;
|
||||
s1, s1, "!a", ;
|
||||
EOF
|
||||
|
||||
cat >input2 <<EOF
|
||||
acc= p1;
|
||||
s1, s1, "a", ;
|
||||
s1, s1, "!a", p1;
|
||||
EOF
|
||||
|
||||
cat >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
|
||||
Loading…
Add table
Add a link
Reference in a new issue