alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Before this change, all automata would construct their own

Browse source 
dictionaries (map of BDD variables to LTL formulae).  This was
cumbersome, because to multiply two automata we had to build a
common dictionary (the union of the two LTL formula spaces), and
install wrappers to translate each automaton's BDD answers into
the common dictionary.  This translation, that had to be repeated
when several products were nested, was time consuming and was a
hindrance for some optimizations.
In the new scheme, all automata involved in a product must
share the same dictionary.  An empty dictionary should be
constructed by the user and passed to the automaton' constructors
as necessary.
This huge change removes most code than it adds.

* src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
* src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files.  These
partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
* src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
* src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
src/tgba/dictunion.hh, src/tgba/dictunion.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
Delete.
* src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files.  These
replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
bddfactory.hh and bddfactory.cc.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
Get next_to_now from the dictionary.
* src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
not a const tgba_bdd_dict*.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
Adjust to use the new dictionary, stored in data_.
* src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh: Likewise.  Plus
now_to_next_ is now also stored in the dictionary.
* src/tgba/tgbabddconcreteproduct.cc: Likewise.  Now
that both operand share the same product, there is not
point in using tgba_bdd_translate_factory.
* src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
Store a bdd_dict (taken as constructor argument).
(tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
(tgba_bdd_core_data::translate): Remove.
(tgba_bdd_core_data::next_to_now): Remove (now in dict).
(tgba_bdd_core_data::dict): New pointer.
* src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Adjust to use the new dictionary.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise.  Do
not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
(ltl_to_tgba): Take a dict argument.
* src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
* src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
a dictionary, and pass it to the automata' constructors.
* src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
option.
* iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
(tgba_gspn::get_dict): Adjust return type.
* iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
use the new dictionary instead.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-14 21:42:59 +00:00
parent 3013ba8da6
commit cab3be9795
52 changed files with 930 additions and 1034 deletions
Download patch file Download diff file Expand all files Collapse all files

75
ChangeLog
View file

@ -1,4 +1,77 @@
2003-07-13 Alexandre Duret-Lutz <adl@gnu.org>
2003-07-14 Alexandre Duret-Lutz <aduret@src.lip6.fr>
Before this change, all automata would construct their own
dictionaries (map of BDD variables to LTL formulae). This was
cumbersome, because to multiply two automata we had to build a
common dictionary (the union of the two LTL formula spaces), and
install wrappers to translate each automaton's BDD answers into
the common dictionary. This translation, that had to be repeated
when several products were nested, was time consuming and was a
hindrance for some optimizations.
In the new scheme, all automata involved in a product must
share the same dictionary. An empty dictionary should be
constructed by the user and passed to the automaton' constructors
as necessary.
This huge change removes most code than it adds.
* src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
* src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files. These
partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
* src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
* src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
src/tgba/dictunion.hh, src/tgba/dictunion.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
Delete.
* src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files. These
replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
bddfactory.hh and bddfactory.cc.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
Get next_to_now from the dictionary.
* src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
not a const tgba_bdd_dict*.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
Adjust to use the new dictionary, stored in data_.
* src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh: Likewise. Plus
now_to_next_ is now also stored in the dictionary.
* src/tgba/tgbabddconcreteproduct.cc: Likewise. Now
that both operand share the same product, there is not
point in using tgba_bdd_translate_factory.
* src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
Store a bdd_dict (taken as constructor argument).
(tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
(tgba_bdd_core_data::translate): Remove.
(tgba_bdd_core_data::next_to_now): Remove (now in dict).
(tgba_bdd_core_data::dict): New pointer.
* src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Adjust to use the new dictionary.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise. Do
not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
(ltl_to_tgba): Take a dict argument.
* src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
* src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
a dictionary, and pass it to the automata' constructors.
* src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
option.
* iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
(tgba_gspn::get_dict): Adjust return type.
* iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
use the new dictionary instead.
2003-07-13 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* configure.ac: Bump version to 0.0e.

72
iface/gspn/gspn.cc
View file

@ -4,7 +4,6 @@
#include "gspnlib.h"
#include "gspn.hh"
#include "ltlvisit/destroy.hh"
#include "tgba/bddfactory.hh"
namespace spot
{
@ -12,52 +11,59 @@ namespace spot
// tgba_gspn_private_
//////////////////////////////////////////////////////////////////////
struct tgba_gspn_private_ : public bdd_factory
struct tgba_gspn_private_
{
int refs; // reference count
tgba_bdd_dict dict;
bdd_dict* dict;
typedef std::pair<AtomicPropKind, bdd> ab_pair;
typedef std::map<AtomicProp, ab_pair> prop_map;
prop_map prop_dict;
AtomicProp *all_indexes;
size_t index_count;
tgba_gspn_private_(const gspn_environment& env)
: refs(0)
tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env)
: refs(0), dict(dict)
{
const gspn_environment::prop_map& p = env.get_prop_map();
for (gspn_environment::prop_map::const_iterator i = p.begin();
i != p.end(); ++i)
try
{
int var = create_node();
i->second->ref();
dict.var_map[i->second] = var;
dict.var_formula_map[var] = i->second;
for (gspn_environment::prop_map::const_iterator i = p.begin();
i != p.end(); ++i)
{
int var = dict->register_proposition(i->second, this);
AtomicProp index;
int err = prop_index(i->first.c_str(), &index);
if (err)
throw gspn_exeption(err);
AtomicPropKind kind;
err = prop_kind(index, &kind);
if (err)
throw gspn_exeption(err);
AtomicProp index;
int err = prop_index(i->first.c_str(), &index);
if (err)
throw gspn_exeption(err);
AtomicPropKind kind;
err = prop_kind(index, &kind);
if (err)
throw gspn_exeption(err);
prop_dict[index] = ab_pair(kind, bdd_ithvar(var));
}
prop_dict[index] = ab_pair(kind, ithvar(var));
index_count = prop_dict.size();
all_indexes = new AtomicProp[index_count];
unsigned idx = 0;
for (prop_map::const_iterator i = prop_dict.begin();
i != prop_dict.end(); ++i)
all_indexes[idx++] = i->first;
}
// If an exception occurs during the loop, dict will
// be cleaned and that will dereferenciate the formula
// it contains. No need to handle anything explicitely.
catch (...)
{
// If an exception occurs during the loop, we need to clean
// all BDD variables which have been registered so far.
dict->unregister_all_my_variables(this);
}
}
index_count = prop_dict.size();
all_indexes = new AtomicProp[index_count];
unsigned idx = 0;
for (prop_map::const_iterator i = prop_dict.begin();
i != prop_dict.end(); ++i)
all_indexes[idx++] = i->first;
tgba_gspn_private_::~tgba_gspn_private_()
{
dict->unregister_all_my_variables(this);
}
bdd index_to_bdd(AtomicProp index) const
@ -239,9 +245,9 @@ namespace spot
//////////////////////////////////////////////////////////////////////
tgba_gspn::tgba_gspn(const gspn_environment& env)
tgba_gspn::tgba_gspn(bdd_dict* dict, const gspn_environment& env)
{
data_ = new tgba_gspn_private_(env);
data_ = new tgba_gspn_private_(dict, env);
}
tgba_gspn::tgba_gspn(const tgba_gspn& other)
@ -299,7 +305,7 @@ namespace spot
return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_);
}
const tgba_bdd_dict&
bdd_dict*
tgba_gspn::get_dict() const
{
return data_->dict;

16
iface/gspn/gspn.hh
View file

@ -2,7 +2,7 @@
# define SPOT_IFACE_GSPN_HH
// Try not to include gspnlib.h here, or it will polute the user's
// namespace with internal C symbols.
// namespace with internal C symbols.
# include <string>
# include "tgba/tgba.hh"
@ -20,7 +20,7 @@ namespace spot
: err(err)
{
}
int
get_err() const
{
@ -29,7 +29,7 @@ namespace spot
private:
int err;
};
class gspn_environment : public ltl::environment
{
@ -42,11 +42,11 @@ namespace spot
bool declare(const std::string& prop_str);
virtual ltl::formula* require(const std::string& prop_str);
/// Get the name of the environment.
virtual const std::string& name();
typedef std::map<const std::string, ltl::atomic_prop*> prop_map;
typedef std::map<const std::string, ltl::atomic_prop*> prop_map;
/// Get the map of atomic proposition known to this environment.
const prop_map& get_prop_map() const;
@ -62,20 +62,20 @@ namespace spot
class tgba_gspn: public tgba
{
public:
tgba_gspn(const gspn_environment& env);
tgba_gspn(bdd_dict* dict, const gspn_environment& env);
tgba_gspn(const tgba_gspn& other);
tgba_gspn& operator=(const tgba_gspn& other);
virtual ~tgba_gspn();
virtual state* get_init_state() const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
private:
tgba_gspn_private_* data_;
};
}
#endif // SPOT_IFACE_GSPN_HH

1
src/Makefile.am
View file

@ -9,6 +9,7 @@ lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
libspot_la_LDFLAGS = $(BUDDY_LDFLAGS)
libspot_la_LIBADD = \
misc/libmisc.la \
ltlenv/libltlenv.la \
ltlparse/libltlparse.la \
ltlvisit/libltlvisit.la \

3
src/misc/.cvsignore
View file

@ -1,3 +1,6 @@
Makefile
Makefile.in
.deps
.libs
*.lo
*.la

12
src/misc/Makefile.am
View file

@ -1,2 +1,12 @@
AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
miscdir = $(pkgincludedir)/misc
misc_HEADERS = const_sel.hh
misc_HEADERS = \
bddalloc.hh \
const_sel.hh
noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
bddalloc.cc

123
src/misc/bddalloc.cc Normal file
View file

@ -0,0 +1,123 @@
#include <bdd.h>
#include <cassert>
#include "bddalloc.hh"
namespace spot
{
bool bdd_allocator::initialized = false;
int bdd_allocator::varnum = 2;
bdd_allocator::bdd_allocator()
{
initialize();
free_list.push_front(pos_lenght_pair(0, varnum));
}
void
bdd_allocator::initialize()
{
if (initialized)
return;
initialized = true;
bdd_init(50000, 5000);
bdd_setvarnum(varnum);
}
int
bdd_allocator::allocate_variables(int n)
{
// Browse the free list until we find N consecutive variables. We
// try not to fragment the list my allocating the variables in the
// smallest free range we find.
free_list_type::iterator best = free_list.end();
free_list_type::iterator cur;
for (cur = free_list.begin(); cur != free_list.end(); ++cur)
{
if (cur->second < n)
continue;
if (n == cur->second)
{
best = cur;
break;
}
if (best == free_list.end()
|| cur->second < best->second)
best = cur;
}
// We have found enough free variables.
if (best != free_list.end())
{
int result = best->first;
best->second -= n;
assert(best->second >= 0);
// Erase the range if it's now empty.
if (best->second == 0)
free_list.erase(best);
else
best->first += n;
return result;
}
// We haven't found enough adjacent free variables;
// ask BuDDy for some more.
// If we already have some free variable at the end
// of the variable space, allocate just the difference.
if (free_list.size() > 0
&& free_list.back().first + free_list.back().second == varnum)
{
int res = free_list.back().first;
int endvar = free_list.back().second;
assert(n > endvar);
bdd_extvarnum(n - endvar);
varnum += n - endvar;
free_list.pop_back();
return res;
}
else
{
// Otherwise, allocate as much variables as we need.
int res = varnum;
bdd_extvarnum(n);
varnum += n;
return res;
}
}
void
bdd_allocator::release_variables(int base, int n)
{
free_list_type::iterator cur;
int end = base + n;
for (cur = free_list.begin(); cur != free_list.end(); ++cur)
{
// Append to a range ...
if (cur->first + cur->second == base)
{
cur->second += n;
// Maybe the next item on the list can be merged.
free_list_type::iterator next = cur;
++next;
if (next != free_list.end()
&& next->first == end)
{
cur->second += next->second;
free_list.erase(next);
}
return;
}
// ... or prepend to a range ...
if (cur->first == end)
{
cur->first -= n;
cur->second += n;
return;
}
// ... or insert a new range.
if (cur->first > end)
break;
}
free_list.insert(cur, pos_lenght_pair(base, n));
}
}

32
src/misc/bddalloc.hh Normal file
View file

@ -0,0 +1,32 @@
#ifndef SPOT_MISC_BDDALLOC_HH
# define SPOT_MISC_BDDALLOC_HH
#include <list>
#include <utility>
namespace spot
{
/// Manage ranges of variables.
class bdd_allocator
{
protected:
/// Default constructor.
bdd_allocator();
/// Initialize the BDD library.
static void initialize();
/// Allocate \a n BDD variables.
int allocate_variables(int n);
/// Release \a n BDD variables starting at \a base.
void release_variables(int base, int n);
static bool initialized; ///< Whether the BDD library has been initialized.
static int varnum; ///< number of variable in use in the BDD library.
typedef std::pair<int, int> pos_lenght_pair;
typedef std::list<pos_lenght_pair> free_list_type;
free_list_type free_list; ///< Tracks unused BDD variables.
};
}
#endif // SPOT_MISC_BDDALLOC_HH

16
src/tgba/Makefile.am
View file

@ -4,9 +4,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
tgbadir = $(pkgincludedir)/tgba
tgba_HEADERS = \
bddfactory.hh \
bdddict.hh \
bddprint.hh \
dictunion.hh \
public.hh \
state.hh \
statebdd.hh \
@ -17,26 +16,19 @@ tgba_HEADERS = \
tgbabddconcretefactory.hh \
tgbabddconcreteproduct.hh \
tgbabddcoredata.hh \
tgbabdddict.hh \
tgbabddfactory.hh \
tgbabddtranslatefactory.hh \
tgbaexplicit.hh \
tgbaproduct.hh \
tgbatranslateproxy.hh
tgbaproduct.hh
noinst_LTLIBRARIES = libtgba.la
libtgba_la_SOURCES = \
bddfactory.cc \
bdddict.cc \
bddprint.cc \
dictunion.cc \
statebdd.cc \
succiterconcrete.cc \
tgbabddconcrete.cc \
tgbabddconcretefactory.cc \
tgbabddconcreteproduct.cc \
tgbabddcoredata.cc \
tgbabdddict.cc \
tgbabddtranslatefactory.cc \
tgbaexplicit.cc \
tgbaproduct.cc \
tgbatranslateproxy.cc
tgbaproduct.cc

271
src/tgba/bdddict.cc Normal file
View file

@ -0,0 +1,271 @@
#include <ltlvisit/clone.hh>
#include <ltlvisit/destroy.hh>
#include <ltlvisit/tostring.hh>
#include <cassert>
#include "bdddict.hh"
namespace spot
{
bdd_dict::bdd_dict()
: bdd_allocator(),
next_to_now(bdd_newpair()),
now_to_next(bdd_newpair())
{
}
bdd_dict::~bdd_dict()
{
assert_emptiness();
bdd_freepair(next_to_now);
bdd_freepair(now_to_next);
}
int
bdd_dict::register_proposition(const ltl::formula* f, const void* for_me)
{
int num;
// Do not build a variable that already exists.
fv_map::iterator sii = var_map.find(f);
if (sii != var_map.end())
{
num = sii->second;
}
else
{
f = clone(f);
num = allocate_variables(1);
var_map[f] = num;
var_formula_map[num] = f;
}
var_refs[num].insert(for_me);
return num;
}
int
bdd_dict::register_state(const ltl::formula* f, const void* for_me)
{
int num;
// Do not build a state that already exists.
fv_map::iterator sii = now_map.find(f);
if (sii != now_map.end())
{
num = sii->second;
}
else
{
f = ltl::clone(f);
num = allocate_variables(2);
now_map[f] = num;
now_formula_map[num] = f;
// Record that num+1 should be renamed as num when
// the next state becomes current.
bdd_setpair(next_to_now, num + 1, num);
bdd_setpair(now_to_next, num, num + 1);
}
var_refs[num].insert(for_me);
return num;
}
int
bdd_dict::register_accepting_variable(const ltl::formula* f,
const void* for_me)
{
int num;
// Do not build an accepting variable that already exists.
fv_map::iterator sii = acc_map.find(f);
if (sii != acc_map.end())
{
num = sii->second;
}
else
{
f = clone(f);
num = allocate_variables(1);
acc_map[f] = num;
acc_formula_map[num] = f;
}
var_refs[num].insert(for_me);
return num;
}
void
bdd_dict::register_all_variables_of(const void* from_other,
const void* for_me)
{
vr_map::iterator i;
for (i = var_refs.begin(); i != var_refs.end(); ++i)
{
ref_set& s = i->second;
if (s.find(from_other) != s.end())
s.insert(for_me);
}
}
void
bdd_dict::unregister_all_my_variables(const void* me)
{
vr_map::iterator i;
for (i = var_refs.begin(); i != var_refs.end();)
{
// Increment i++ now, we will possibly erase
// the current node (which would invalidate the iterator).
vr_map::iterator cur = i++;
ref_set& s = cur->second;
ref_set::iterator si = s.find(me);
if (si == s.end())
continue;
s.erase(si);
if (! s.empty())
continue;
// ME was the last user of this variable.
// Let's free it. First, we need to find
// if this is a Now, a Var, or an Acc variable.
int var = cur->first;
int n = 1;
const ltl::formula* f;
vf_map::iterator vi = var_formula_map.find(var);
if (vi != var_formula_map.end())
{
f = vi->second;
var_map.erase(f);
var_formula_map.erase(vi);
}
else
{
vi = now_formula_map.find(var);
if (vi != now_formula_map.end())
{
f = vi->second;
now_map.erase(f);
now_formula_map.erase(vi);
n = 2;
bdd_setpair(next_to_now, var + 1, var + 1);
bdd_setpair(now_to_next, var, var);
}
else
{
vi = acc_formula_map.find(var);
f = vi->second;
assert(vi != now_formula_map.end());
acc_map.erase(f);
acc_formula_map.erase(vi);
}
}
// Actually release the associated BDD variables, and the
// formula itself.
release_variables(var, n);
ltl::destroy(f);
var_refs.erase(cur);
}
}
bool
bdd_dict::is_registered(const ltl::formula* f, const void* by_me)
{
int var;
fv_map::iterator fi = var_map.find(f);
if (fi != var_map.end())
{
var = fi->second;
}
else
{
fi = now_map.find(f);
if (fi != now_map.end())
{
var = fi->second;
}
else
{
fi = acc_map.find(f);
if (fi == acc_map.end())
return false;
var = fi->second;
}
}
ref_set& s = var_refs[var];
return s.find(by_me) != s.end();
}
std::ostream&
bdd_dict::dump(std::ostream& os) const
{
fv_map::const_iterator fi;
os << "Atomic Propositions:" << std::endl;
for (fi = var_map.begin(); fi != var_map.end(); ++fi)
{
os << " " << fi->second << " (x"
<< var_refs.find(fi->second)->second.size() << "): ";
to_string(fi->first, os) << std::endl;
}
os << "States:" << std::endl;
for (fi = now_map.begin(); fi != now_map.end(); ++fi)
{
int refs = var_refs.find(fi->second)->second.size();
os << " " << fi->second << " (x" << refs << "): Now[";
to_string(fi->first, os) << "]" << std::endl;
os << " " << fi->second + 1 << " (x" << refs << "): Next[";
to_string(fi->first, os) << "]" << std::endl;
}
os << "Accepting Conditions:" << std::endl;
for (fi = acc_map.begin(); fi != acc_map.end(); ++fi)
{
os << " " << fi->second << " (x"
<< var_refs.find(fi->second)->second.size() << "): Acc[";
to_string(fi->first, os) << "]" << std::endl;
}
os << "Free list:" << std::endl;
free_list_type::const_iterator i;
for (i = free_list.begin(); i != free_list.end(); ++i)
os << " (" << i->first << ", " << i->second << ")";
os << std::endl;
return os;
}
void
bdd_dict::assert_emptiness() const
{
bool fail = false;
if (var_map.empty()
&& now_map.empty()
&& acc_map.empty())
{
if (! var_formula_map.empty())
{
std::cerr << "var_map is empty but var_formula_map is not"
<< std::endl;
fail = true;
}
if (! now_formula_map.empty())
{
std::cerr << "now_map is empty but now_formula_map is not"
<< std::endl;
fail = true;
}
if (! acc_formula_map.empty())
{
std::cerr << "acc_map is empty but acc_formula_map is not"
<< std::endl;
fail = true;
}
if (! var_refs.empty())
{
std::cerr << "maps are empty but var_refs is not" << std::endl;
fail = true;
vr_map::const_iterator i;
for (i = var_refs.begin(); i != var_refs.end(); ++i)
std::cerr << " " << i->first << ":" << i->second.size();
std::cerr << std::endl;
}
if (! fail)
return;
}
else
{
std::cerr << "some maps are not empty" << std::endl;
}
dump(std::cerr);
assert(0);
}
}

122
src/tgba/bdddict.hh Normal file
View file

@ -0,0 +1,122 @@
#ifndef SPOT_TGBA_BDDDICT_HH
# define SPOT_TGBA_BDDDICT_HH
#include <map>
#include <list>
#include <set>
#include <iostream>
#include <bdd.h>
#include "ltlast/formula.hh"
#include "misc/bddalloc.hh"
namespace spot
{
/// Map BDD variables to formulae.
class bdd_dict: public bdd_allocator
{
public:
bdd_dict();
~bdd_dict();
/// Formula-to-BDD-variable maps.
typedef std::map<const ltl::formula*, int> fv_map;
/// BDD-variable-to-formula maps.
typedef std::map<int, const ltl::formula*> vf_map;
fv_map now_map; ///< Maps formulae to "Now" BDD variables
vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae
fv_map var_map; ///< Maps atomic propisitions to BDD variables
vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions
fv_map acc_map; ///< Maps accepting conditions to BDD variables
vf_map acc_formula_map; ///< Maps BDD variables to accepting conditions
/// \brief Map Next variables to Now variables.
///
/// Use with BuDDy's bdd_replace() function.
bddPair* next_to_now;
/// \brief Map Now variables to Next variables.
///
/// Use with BuDDy's bdd_replace() function.
bddPair* now_to_next;
/// \brief Register an atomic proposition.
///
/// Return (and maybe allocate) a BDD variable designating formula
/// \a f. The \a for_me argument should point to the object using
/// this BDD variable, this is used for reference counting. It is
/// perfectly safe to call this function several time with the same
/// arguments.
///
/// \return The variable number. Use bdd_ithvar() or bdd_nithvar()
/// to convert this to a BDD.
int register_proposition(const ltl::formula* f, const void* for_me);
/// \brief Register a couple of Now/Next variables
///
/// Return (and maybe allocate) two BDD variables for a state
/// associated to formula \a f. The \a for_me argument should point
/// to the object using this BDD variable, this is used for
/// reference counting. It is perfectly safe to call this
/// function several time with the same arguments.
///
/// \return The first variable number. Add one to get the second
/// variable. Use bdd_ithvar() or bdd_nithvar() to convert this
/// to a BDD.
int register_state(const ltl::formula* f, const void* for_me);
/// \brief Register an atomic proposition.
///
/// Return (and maybe allocate) a BDD variable designating an
/// accepting set associated to formula \a f. The \a for_me
/// argument should point to the object using this BDD variable,
/// this is used for reference counting. It is perfectly safe to
/// call this function several time with the same arguments.
///
/// \return The variable number. Use bdd_ithvar() or bdd_nithvar()
/// to convert this to a BDD.
int register_accepting_variable(const ltl::formula* f, const void* for_me);
/// \brief Duplicate the variable usage of another object.
///
/// This tells this dictionary that the \a for_me object
/// will be using the same BDD variables as the \a from_other objects.
/// This ensure that the variables won't be freed when \a from_other
/// is deleted if \a from_other is still alive.
void register_all_variables_of(const void* from_other, const void* for_me);
/// \brief Release the variables used by object.
///
/// Usually called in the destructor if \a me.
void unregister_all_my_variables(const void* me);
/// Check whether formula \a f has already been registered by \a by_me.
bool is_registered(const ltl::formula* f, const void* by_me);
/// \brief Dump all variables for debugging.
/// \param os The output stream.
std::ostream& dump(std::ostream& os) const;
/// \brief Make sure the dictionary is empty.
///
/// This will print diagnostics and abort if the dictionary
/// is not empty. Use for debugging.
void assert_emptiness() const;
protected:
/// BDD-variable reference counts.
typedef std::set<const void*> ref_set;
typedef std::map<int, ref_set> vr_map;
vr_map var_refs;
private:
// Disallow copy.
bdd_dict(const bdd_dict& other);
bdd_dict& operator=(const bdd_dict& other);
};
}
#endif // SPOT_TGBA_BDDDICT_HH

48
src/tgba/bddfactory.cc
View file

@ -1,48 +0,0 @@
#include "bddfactory.hh"
namespace spot
{
bdd_factory::bdd_factory()
: varused(0)
{
initialize();
}
int
bdd_factory::create_node()
{
return create_nodes(1);
}
int
bdd_factory::create_pair()
{
return create_nodes(2);
}
int
bdd_factory::create_nodes(int i)
{
int res = varused;
varused += i;
if (varnum < varused)
{
bdd_extvarnum(varused - varnum);
varnum = varused;
}
return res;
}
void
bdd_factory::initialize()
{
if (initialized)
return;
initialized = true;
bdd_init(50000, 5000);
bdd_setvarnum(varnum);
}
bool bdd_factory::initialized = false;
int bdd_factory::varnum = 2;
}

60
src/tgba/bddfactory.hh
View file

@ -1,60 +0,0 @@
#ifndef SPOT_TGBA_BDDFACTORY_HH
# define SPOT_TGBA_BDDFACTORY_HH
#include <bdd.h>
namespace spot
{
/// \brief Help construct BDDs by reusing existing variables.
///
/// Spot uses BuDDy as BDD library, and BuDDy needs to
/// know the number of BDD variables in use. As a rule
/// of thumb: the more BDD variables the slowere. So
/// creating new BDD variables each time we build a new
/// Automata won't do.
///
/// To avoid variable explosion, we reuse existing variables
/// when building new automata, and only allocate new variables
/// when we ran out of existing variables. This class helps
/// reusing variables this way.
///
/// Using the same variables in different automata is not a
/// problem until an operation is performed on both automata.
/// In this case some homogenization of BDD variable will be
/// required. Such operation is out of the scope of this class.
class bdd_factory
{
public:
bdd_factory();
/// \brief Allocate a BDD variable.
///
/// The returned integer can be converted to a BDD using ithvar().
int create_node();
/// \brief Allocate a pair BDD variable.
///
/// The returned integer is the first variable of the pair,
/// it's successor (i.e., n + 1) is the second variable.
/// They can be converted to BDDs using ithvar().
int create_pair();
/// Convert a variable number into a BDD.
static bdd
ithvar(int i)
{
return bdd_ithvar(i);
}
protected:
static void initialize(); ///< Initialize the BDD library.
int create_nodes(int i); ///< Create \a i variables.
static bool initialized; ///< Whether the BDD library has been initialized.
static int varnum; ///< number of variable in use in the BDD library.
int varused; ///< Number of variables used for this construction.
};
}
#endif // SPOT_TGBA_BDDFACTORY_HH

28
src/tgba/bddprint.cc
View file

@ -6,7 +6,7 @@
namespace spot
{
/// Global dictionary used by print_handler() to lookup variables.
static const tgba_bdd_dict* dict;
static const bdd_dict* dict;
/// Global flag to enable Acc[x] output (instead of `x').
static bool want_acc;
@ -15,7 +15,7 @@ namespace spot
static void
print_handler(std::ostream& o, int var)
{
tgba_bdd_dict::vf_map::const_iterator isi =
bdd_dict::vf_map::const_iterator isi =
dict->var_formula_map.find(var);
if (isi != dict->var_formula_map.end())
to_string(isi->second, o);
@ -80,9 +80,9 @@ namespace spot
}
std::ostream&
bdd_print_sat(std::ostream& os, const tgba_bdd_dict& d, bdd b)
bdd_print_sat(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = &d;
dict = d;
where = &os;
want_acc = false;
assert(bdd_satone(b) == b);
@ -106,9 +106,9 @@ namespace spot
}
std::ostream&
bdd_print_acc(std::ostream& os, const tgba_bdd_dict& d, bdd b)
bdd_print_acc(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = &d;
dict = d;
where = &os;
want_acc = false;
bdd_allsat(b, print_acc_handler);
@ -116,7 +116,7 @@ namespace spot
}
std::string
bdd_format_sat(const tgba_bdd_dict& d, bdd b)
bdd_format_sat(const bdd_dict* d, bdd b)
{
std::ostringstream os;
bdd_print_sat(os, d, b);
@ -124,9 +124,9 @@ namespace spot
}
std::ostream&
bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
bdd_print_set(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = &d;
dict = d;
want_acc = true;
bdd_strm_hook(print_handler);
os << bddset << b;
@ -135,7 +135,7 @@ namespace spot
}
std::string
bdd_format_set(const tgba_bdd_dict& d, bdd b)
bdd_format_set(const bdd_dict* d, bdd b)
{
std::ostringstream os;
bdd_print_set(os, d, b);
@ -143,9 +143,9 @@ namespace spot
}
std::ostream&
bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
bdd_print_dot(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = &d;
dict = d;
want_acc = true;
bdd_strm_hook(print_handler);
os << bdddot << b;
@ -154,9 +154,9 @@ namespace spot
}
std::ostream&
bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
bdd_print_table(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = &d;
dict = d;
want_acc = true;
bdd_strm_hook(print_handler);
os << bddtable << b;

16
src/tgba/bddprint.hh
View file

@ -3,7 +3,7 @@
#include <string>
#include <iostream>
#include "tgbabdddict.hh"
#include "bdddict.hh"
#include <bdd.h>
namespace spot
@ -16,7 +16,7 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream& bdd_print_sat(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a list of literals.
///
@ -24,7 +24,7 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::string bdd_format_sat(const tgba_bdd_dict& dict, bdd b);
std::string bdd_format_sat(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a list of accepting conditions.
///
@ -34,33 +34,33 @@ namespace spot
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::ostream& bdd_print_acc(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a set.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream& bdd_print_set(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a set.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b);
std::string bdd_format_set(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a diagram in dotty format.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream& bdd_print_dot(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a table.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream& bdd_print_table(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
const bdd_dict* dict, bdd b);
}

80
src/tgba/dictunion.cc
View file

@ -1,80 +0,0 @@
#include <set>
#include "dictunion.hh"
#include "ltlvisit/clone.hh"
#include <bdd.h>
#include <cassert>
namespace spot
{
tgba_bdd_dict
tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r)
{
std::set<const ltl::formula*> now;
std::set<const ltl::formula*> var;
std::set<const ltl::formula*> acc;
tgba_bdd_dict::fv_map::const_iterator i;
// Merge Now variables.
for (i = l.now_map.begin(); i != l.now_map.end(); ++i)
now.insert(i->first);
for (i = r.now_map.begin(); i != r.now_map.end(); ++i)
now.insert(i->first);
// Merge atomic propositions.
for (i = l.var_map.begin(); i != l.var_map.end(); ++i)
var.insert(i->first);
for (i = r.var_map.begin(); i != r.var_map.end(); ++i)
var.insert(i->first);
// Merge accepting conditions.
for (i = l.acc_map.begin(); i != l.acc_map.end(); ++i)
acc.insert(i->first);
for (i = r.acc_map.begin(); i != r.acc_map.end(); ++i)
acc.insert(i->first);
// Ensure we have enough BDD variables.
int have = bdd_extvarnum(0);
int want = now.size() * 2 + var.size() + acc.size();
if (have < want)
bdd_setvarnum(want);
// Fill in the "defragmented" union dictionary.
// FIXME: Make some experiments with ordering of acc/var/now variables.
// Maybe there is one order that usually produces smaller BDDs?
// Next BDD variable to use.
int v = 0;
tgba_bdd_dict res;
std::set<const ltl::formula*>::const_iterator f;
for (f = acc.begin(); f != acc.end(); ++f)
{
clone(*f);
res.acc_map[*f] = v;
res.acc_formula_map[v] = *f;
++v;
}
for (f = var.begin(); f != var.end(); ++f)
{
clone(*f);
res.var_map[*f] = v;
res.var_formula_map[v] = *f;
++v;
}
for (f = now.begin(); f != now.end(); ++f)
{
clone(*f);
res.now_map[*f] = v;
res.now_formula_map[v] = *f;
v += 2;
}
assert (v == want);
return res;
}
}

13
src/tgba/dictunion.hh
View file

@ -1,13 +0,0 @@
#ifndef SPOT_TGBA_DICTUNION_HH
# define SPOT_TGBA_DICTUNION_HH
#include "tgbabdddict.hh"
namespace spot
{
/// Build the union of two dictionaries.
tgba_bdd_dict
tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r);
}
#endif // SPOT_TGBA_DICTUNION_HH

2
src/tgba/succiterconcrete.cc
View file

@ -140,7 +140,7 @@ namespace spot
// successor (a dead node) and we can skip it. We need to
// compute current_state_ anyway, so this test costs us nothing.
assert(dest == bdd_exist(current_, data_.notnext_set));
current_state_ = bdd_replace(dest, data_.next_to_now);
current_state_ = bdd_replace(dest, data_.dict->next_to_now);
}
while ((current_state_ & data_.relation) == bddfalse);
}

4
src/tgba/tgba.hh
View file

@ -3,7 +3,7 @@
#include "state.hh"
#include "succiter.hh"
#include "tgbabdddict.hh"
#include "bdddict.hh"
namespace spot
{
@ -64,7 +64,7 @@ namespace spot
/// This is useful when dealing with several automata (which
/// may use the same BDD variable for different formula),
/// or simply when printing.
virtual const tgba_bdd_dict& get_dict() const = 0;
virtual bdd_dict* get_dict() const = 0;
/// \brief Format the state as a string for printing.
///

13
src/tgba/tgbabddconcrete.cc
View file

@ -5,18 +5,21 @@
namespace spot
{
tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact)
: data_(fact.get_core_data()), dict_(fact.get_dict())
: data_(fact.get_core_data())
{
get_dict()->register_all_variables_of(&fact, this);
}
tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
: data_(fact.get_core_data()), dict_(fact.get_dict())
: data_(fact.get_core_data())
{
get_dict()->register_all_variables_of(&fact, this);
set_init_state(init);
}
tgba_bdd_concrete::~tgba_bdd_concrete()
{
get_dict()->unregister_all_my_variables(this);
}
void
@ -81,13 +84,13 @@ namespace spot
{
const state_bdd* s = dynamic_cast<const state_bdd*>(state);
assert(s);
return bdd_format_set(dict_, s->as_bdd());
return bdd_format_set(get_dict(), s->as_bdd());
}
const tgba_bdd_dict&
bdd_dict*
tgba_bdd_concrete::get_dict() const
{
return dict_;
return data_.dict;
}
bdd

3
src/tgba/tgbabddconcrete.hh
View file

@ -43,7 +43,7 @@ namespace spot
std::string format_state(const state* state) const;
const tgba_bdd_dict& get_dict() const;
bdd_dict* get_dict() const;
/// \brief Get the core data associated to this automaton.
///
@ -57,7 +57,6 @@ namespace spot
protected:
tgba_bdd_core_data data_; ///< Core data associated to the automaton.
tgba_bdd_dict dict_; ///< Dictionary used by the automaton.
bdd init_; ///< Initial state.
};
}

54
src/tgba/tgbabddconcretefactory.cc
View file

@ -3,8 +3,8 @@
#include "tgbabddconcretefactory.hh"
namespace spot
{
tgba_bdd_concrete_factory::tgba_bdd_concrete_factory()
: now_to_next_(bdd_newpair())
tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict)
: data_(dict)
{
}
@ -13,50 +13,26 @@ namespace spot
acc_map_::iterator ai;
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
destroy(ai->first);
get_dict()->unregister_all_my_variables(this);
}
int
tgba_bdd_concrete_factory::create_state(const ltl::formula* f)
{
// Do not build a state that already exists.
tgba_bdd_dict::fv_map::iterator sii = dict_.now_map.find(f);
if (sii != dict_.now_map.end())
return sii->second;
f = clone(f);
int num = create_pair();
dict_.now_map[f] = num;
dict_.now_formula_map[num] = f;
// Record that num+1 should be renamed as num when
// the next state becomes current.
bdd_setpair(data_.next_to_now, num + 1, num);
bdd_setpair(now_to_next_, num, num + 1);
int num = get_dict()->register_state(f, this);
// Keep track of all "Now" variables for easy
// existential quantification.
data_.declare_now_next (ithvar(num), ithvar(num + 1));
data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1));
return num;
}
int
tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f)
{
// Do not build a variable that already exists.
tgba_bdd_dict::fv_map::iterator sii = dict_.var_map.find(f);
if (sii != dict_.var_map.end())
return sii->second;
f = clone(f);
int num = create_node();
dict_.var_map[f] = num;
dict_.var_formula_map[num] = f;
int num = get_dict()->register_proposition(f, this);
// Keep track of all atomic proposition for easy
// existential quantification.
data_.declare_atomic_prop(ithvar(num));
data_.declare_atomic_prop(bdd_ithvar(num));
return num;
}
@ -86,18 +62,14 @@ namespace spot
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
{
// Register a BDD variable for this accepting condition.
int a = create_node();
const ltl::formula* f = clone(ai->first); // The associated formula.
dict_.acc_map[f] = a;
dict_.acc_formula_map[a] = f;
bdd acc = ithvar(a);
int num = get_dict()->register_accepting_variable(ai->first, this);
// Keep track of all accepting conditions for easy
// existential quantification.
data_.declare_accepting_condition(acc);
data_.declare_accepting_condition(bdd_ithvar(num));
}
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
{
bdd acc = ithvar(dict_.acc_map[ai->first]);
bdd acc = bdd_ithvar(get_dict()->acc_map[ai->first]);
// Complete acc with all the other accepting conditions negated.
acc &= bdd_exist(data_.negacc_set, acc);
@ -119,7 +91,7 @@ namespace spot
// state: the combination exists but won't allow further exploration
// because it fails the constraints.)
data_.relation &= bdd_replace(bdd_exist(data_.relation, data_.notnow_set),
now_to_next_);
get_dict()->now_to_next);
}
const tgba_bdd_core_data&
@ -128,10 +100,10 @@ namespace spot
return data_;
}
const tgba_bdd_dict&
bdd_dict*
tgba_bdd_concrete_factory::get_dict() const
{
return dict_;
return data_.dict;
}
void

10
src/tgba/tgbabddconcretefactory.hh
View file

@ -2,17 +2,16 @@
# define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
#include "ltlast/formula.hh"
#include "bddfactory.hh"
#include "tgbabddfactory.hh"
#include <map>
namespace spot
{
/// Helper class to build a spot::tgba_bdd_concrete object.
class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory
class tgba_bdd_concrete_factory: public tgba_bdd_factory
{
public:
tgba_bdd_concrete_factory();
tgba_bdd_concrete_factory(bdd_dict* dict);
virtual ~tgba_bdd_concrete_factory();
@ -50,7 +49,7 @@ namespace spot
void declare_accepting_condition(bdd b, const ltl::formula* a);
const tgba_bdd_core_data& get_core_data() const;
const tgba_bdd_dict& get_dict() const;
bdd_dict* get_dict() const;
/// Add a new constraint to the relation.
void constrain_relation(bdd new_rel);
@ -64,12 +63,9 @@ namespace spot
private:
tgba_bdd_core_data data_; ///< Core data for the new automata.
tgba_bdd_dict dict_; ///< Dictionary for the new automata.
typedef std::map<const ltl::formula*, bdd> acc_map_;
acc_map_ acc_; ///< BDD associated to each accepting condition
bddPair *now_to_next_; ///< \brief Rewriting pairs to transform
/// Now variables into Next variables.
};
}

24
src/tgba/tgbabddconcreteproduct.cc
View file

@ -1,6 +1,5 @@
#include <cassert>
#include "tgbabddconcreteproduct.hh"
#include "tgbabddtranslatefactory.hh"
#include "dictunion.hh"
namespace spot
{
@ -14,13 +13,13 @@ namespace spot
public:
tgba_bdd_product_factory(const tgba_bdd_concrete& left,
const tgba_bdd_concrete& right)
: dict_(tgba_bdd_dict_union(left.get_dict(),
right.get_dict())),
fact_left_(left, dict_),
fact_right_(right, dict_),
data_(fact_left_.get_core_data(), fact_right_.get_core_data()),
init_(fact_left_.get_init_state() & fact_right_.get_init_state())
: dict_(left.get_dict()),
left_(left),
right_(right),
data_(left_.get_core_data(), right_.get_core_data()),
init_(left_.get_init_bdd() & right_.get_init_bdd())
{
assert(dict_ == right.get_dict());
}
virtual
@ -34,7 +33,7 @@ namespace spot
return data_;
}
const tgba_bdd_dict&
bdd_dict*
get_dict() const
{
return dict_;
@ -47,9 +46,9 @@ namespace spot
}
private:
tgba_bdd_dict dict_;
tgba_bdd_translate_factory fact_left_;
tgba_bdd_translate_factory fact_right_;
bdd_dict* dict_;
const tgba_bdd_concrete& left_;
const tgba_bdd_concrete& right_;
tgba_bdd_core_data data_;
bdd init_;
};
@ -57,7 +56,6 @@ namespace spot
tgba_bdd_concrete
product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right)
{
tgba_bdd_product_factory p(left, right);
return tgba_bdd_concrete(p, p.get_init_state());
}

34
src/tgba/tgbabddcoredata.cc
View file

@ -1,8 +1,9 @@
#include <cassert>
#include "tgbabddcoredata.hh"
namespace spot
{
tgba_bdd_core_data::tgba_bdd_core_data()
tgba_bdd_core_data::tgba_bdd_core_data(bdd_dict* dict)
: relation(bddtrue),
accepting_conditions(bddfalse),
all_accepting_conditions(bddfalse),
@ -17,7 +18,7 @@ namespace spot
acc_set(bddtrue),
notacc_set(bddtrue),
negacc_set(bddtrue),
next_to_now(bdd_newpair())
dict(dict)
{
}
@ -36,7 +37,7 @@ namespace spot
acc_set(copy.acc_set),
notacc_set(copy.notacc_set),
negacc_set(copy.negacc_set),
next_to_now(bdd_copypair(copy.next_to_now))
dict(copy.dict)
{
}
@ -59,8 +60,9 @@ namespace spot
acc_set(left.acc_set & right.acc_set),
notacc_set(left.notacc_set & right.notacc_set),
negacc_set(left.negacc_set & right.negacc_set),
next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now))
dict(left.dict)
{
assert(dict == right.dict);
}
const tgba_bdd_core_data&
@ -74,11 +76,6 @@ namespace spot
return *this;
}
tgba_bdd_core_data::~tgba_bdd_core_data()
{
bdd_freepair(next_to_now);
}
void
tgba_bdd_core_data::declare_now_next(bdd now, bdd next)
{
@ -112,23 +109,4 @@ namespace spot
acc_set &= acc;
negacc_set &= !acc;
}
void
tgba_bdd_core_data::translate(bddPair* rewrite)
{
relation = bdd_replace(relation, rewrite);
accepting_conditions = bdd_replace(accepting_conditions, rewrite);
all_accepting_conditions = bdd_replace(all_accepting_conditions, rewrite);
now_set = bdd_replace(now_set, rewrite);
next_set = bdd_replace(next_set, rewrite);
nownext_set = bdd_replace(nownext_set, rewrite);
notnow_set = bdd_replace(notnow_set, rewrite);
notnext_set = bdd_replace(notnext_set, rewrite);
notvar_set = bdd_replace(notvar_set, rewrite);
var_set = bdd_replace(var_set, rewrite);
varandnext_set = bdd_replace(varandnext_set, rewrite);
acc_set = bdd_replace(acc_set, rewrite);
notacc_set = bdd_replace(notacc_set, rewrite);
negacc_set = bdd_replace(negacc_set, rewrite);
}
}

15
src/tgba/tgbabddcoredata.hh
View file

@ -2,6 +2,7 @@
# define SPOT_TGBA_TGBABDDCOREDATA_HH
#include <bdd.h>
#include "bdddict.hh"
namespace spot
{
@ -92,13 +93,13 @@ namespace spot
/// conditions.
bdd negacc_set;
/// Record pairings between Next and Now variables.
bddPair* next_to_now;
/// The dictionary used by the automata.
bdd_dict* dict;
/// \brief Default constructor.
///
/// Initially all variable set are empty and the \c relation is true.
tgba_bdd_core_data();
tgba_bdd_core_data(bdd_dict* dict);
/// Copy constructor.
tgba_bdd_core_data(const tgba_bdd_core_data& copy);
@ -111,8 +112,6 @@ namespace spot
const tgba_bdd_core_data& operator= (const tgba_bdd_core_data& copy);
~tgba_bdd_core_data();
/// \brief Update the variable sets to take a new pair of variables into
/// account.
void declare_now_next(bdd now, bdd next);
@ -122,12 +121,6 @@ namespace spot
/// \brief Update the variable sets to take a new accepting condition
/// into account.
void declare_accepting_condition(bdd prom);
/// \brief Translate BDD variables.
///
/// Rewrite the variables according to \a rewrite.
/// This used by spot::tgba_bdd_translate_factory.
void translate(bddPair* rewrite);
};
}

103
src/tgba/tgbabdddict.cc
View file

@ -1,103 +0,0 @@
#include "tgbabdddict.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
std::ostream&
tgba_bdd_dict::dump(std::ostream& os) const
{
fv_map::const_iterator sii;
os << "Atomic Propositions:" << std::endl;
for (sii = var_map.begin(); sii != var_map.end(); ++sii)
{
os << " " << sii->second << ": ";
to_string(sii->first, os) << std::endl;
}
os << "States:" << std::endl;
for (sii = now_map.begin(); sii != now_map.end(); ++sii)
{
os << " " << sii->second << ": Now[";
to_string(sii->first, os) << "]" << std::endl;
os << " " << sii->second + 1 << ": Next[";
to_string(sii->first, os) << "]" << std::endl;
}
os << "Accepting Conditions:" << std::endl;
for (sii = acc_map.begin(); sii != acc_map.end(); ++sii)
{
os << " " << sii->second << ": ";
to_string(sii->first, os) << std::endl;
}
return os;
}
bool
tgba_bdd_dict::contains(const tgba_bdd_dict& other) const
{
fv_map::const_iterator i;
for (i = other.var_map.begin(); i != other.var_map.end(); ++i)
{
fv_map::const_iterator i2 = var_map.find(i->first);
if (i2 == var_map.end() || i->second != i2->second)
return false;
}
for (i = other.now_map.begin(); i != other.now_map.end(); ++i)
{
fv_map::const_iterator i2 = now_map.find(i->first);
if (i2 == now_map.end() || i->second != i2->second)
return false;
}
for (i = other.acc_map.begin(); i != other.acc_map.end(); ++i)
{
fv_map::const_iterator i2 = acc_map.find(i->first);
if (i2 == acc_map.end() || i->second != i2->second)
return false;
}
return true;
}
tgba_bdd_dict::tgba_bdd_dict()
{
}
tgba_bdd_dict::tgba_bdd_dict(const tgba_bdd_dict& other)
: now_map(other.now_map),
now_formula_map(other.now_formula_map),
var_map(other.var_map),
var_formula_map(other.var_formula_map),
acc_map(other.acc_map),
acc_formula_map(other.acc_formula_map)
{
fv_map::iterator i;
for (i = now_map.begin(); i != now_map.end(); ++i)
ltl::clone(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::clone(i->first);
for (i = acc_map.begin(); i != acc_map.end(); ++i)
ltl::clone(i->first);
}
tgba_bdd_dict&
tgba_bdd_dict::operator=(const tgba_bdd_dict& other)
{
if (this != &other)
{
this->~tgba_bdd_dict();
new (this) tgba_bdd_dict(other);
}
return *this;
}
tgba_bdd_dict::~tgba_bdd_dict()
{
fv_map::iterator i;
for (i = now_map.begin(); i != now_map.end(); ++i)
ltl::destroy(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::destroy(i->first);
for (i = acc_map.begin(); i != acc_map.end(); ++i)
ltl::destroy(i->first);
}
}

40
src/tgba/tgbabdddict.hh
View file

@ -1,40 +0,0 @@
#ifndef SPOT_TGBA_TGBABDDDICT_H
# define SPOT_TGBA_TGBABDDDICT_H
#include <map>
#include <iostream>
#include "ltlast/formula.hh"
namespace spot
{
/// Dictionary of BDD variables.
struct tgba_bdd_dict
{
/// Formula-to-BDD-variable maps.
typedef std::map<const ltl::formula*, int> fv_map;
/// BDD-variable-to-formula maps.
typedef std::map<int, const ltl::formula*> vf_map;
fv_map now_map; ///< Maps formulae to "Now" BDD variables
vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae
fv_map var_map; ///< Maps atomic propisitions to BDD variables
vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions
fv_map acc_map; ///< Maps accepting conditions to BDD variables
vf_map acc_formula_map; ///< Maps BDD variables to accepting conditions
/// \brief Dump all variables for debugging.
/// \param os The output stream.
std::ostream& dump(std::ostream& os) const;
/// Whether this dictionary contains \a other.
bool contains(const tgba_bdd_dict& other) const;
tgba_bdd_dict();
tgba_bdd_dict(const tgba_bdd_dict& other);
tgba_bdd_dict& operator=(const tgba_bdd_dict& other);
~tgba_bdd_dict();
};
}
#endif // SPOT_TGBA_TGBABDDDICT_H

3
src/tgba/tgbabddfactory.hh
View file

@ -2,7 +2,6 @@
# define SPOT_TGBA_TGBABDDFACTORY_H
#include "tgbabddcoredata.hh"
#include "tgbabdddict.hh"
namespace spot
{
@ -15,8 +14,6 @@ namespace spot
public:
/// Get the core data for the new automata.
virtual const tgba_bdd_core_data& get_core_data() const = 0;
/// Get the dictionary for the new automata.
virtual const tgba_bdd_dict& get_dict() const = 0;
};
}

81
src/tgba/tgbabddtranslatefactory.cc
View file

@ -1,81 +0,0 @@
#include "tgbabddtranslatefactory.hh"
#include "dictunion.hh"
#include <cassert>
namespace spot
{
tgba_bdd_translate_factory::tgba_bdd_translate_factory
(const tgba_bdd_concrete& from, const tgba_bdd_dict& to)
: data_(from.get_core_data()), dict_(to)
{
bddPair* rewrite = compute_pairs(from.get_dict());
data_.translate(rewrite);
init_ = bdd_replace(from.get_init_bdd(), rewrite);
bdd_freepair(rewrite);
}
tgba_bdd_translate_factory::~tgba_bdd_translate_factory()
{
}
bddPair*
tgba_bdd_translate_factory::compute_pairs(const tgba_bdd_dict& from)
{
bddPair* rewrite = bdd_newpair();
tgba_bdd_dict::fv_map::const_iterator i_from;
tgba_bdd_dict::fv_map::const_iterator i_to;
for (i_from = from.now_map.begin(); i_from != from.now_map.end(); ++i_from)
{
i_to = dict_.now_map.find(i_from->first);
assert(i_to != dict_.now_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
bdd_setpair(rewrite, i_from->second + 1, i_to->second + 1);
bdd_setpair(data_.next_to_now, i_to->second + 1, i_to->second);
}
for (i_from = from.var_map.begin(); i_from != from.var_map.end(); ++i_from)
{
i_to = dict_.var_map.find(i_from->first);
assert(i_to != dict_.var_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
}
for (i_from = from.acc_map.begin();
i_from != from.acc_map.end();
++i_from)
{
i_to = dict_.acc_map.find(i_from->first);
assert(i_to != dict_.acc_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
}
return rewrite;
}
const tgba_bdd_core_data&
tgba_bdd_translate_factory::get_core_data() const
{
return data_;
}
const tgba_bdd_dict&
tgba_bdd_translate_factory::get_dict() const
{
return dict_;
}
bdd
tgba_bdd_translate_factory::get_init_state() const
{
return init_;
}
tgba_bdd_concrete
defrag(const tgba_bdd_concrete& a)
{
const tgba_bdd_dict& ad = a.get_dict();
tgba_bdd_dict u = tgba_bdd_dict_union(ad, ad);
tgba_bdd_translate_factory f(a, u);
return tgba_bdd_concrete(f, f.get_init_state());
}
}

43
src/tgba/tgbabddtranslatefactory.hh
View file

@ -1,43 +0,0 @@
#ifndef SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH
# define SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH
#include "tgbabddfactory.hh"
#include "tgbabddconcrete.hh"
namespace spot
{
/// A spot::tgba_bdd_factory than renumber BDD variables.
class tgba_bdd_translate_factory: public tgba_bdd_factory
{
public:
///\brief Construct a spot::tgba_bdd_translate_factory
///
/// \param from The Automata to copy.
/// \param to The dictionary of variable number to use.
tgba_bdd_translate_factory(const tgba_bdd_concrete& from,
const tgba_bdd_dict& to);
virtual ~tgba_bdd_translate_factory();
const tgba_bdd_core_data& get_core_data() const;
const tgba_bdd_dict& get_dict() const;
/// Get the new initial state.
bdd get_init_state() const;
protected:
/// Compute renaming pairs.
bddPair* compute_pairs(const tgba_bdd_dict& from);
private:
tgba_bdd_core_data data_;
tgba_bdd_dict dict_;
bdd init_;
};
/// Reorder the variables of an automata.
tgba_bdd_concrete defrag(const tgba_bdd_concrete& a);
}
#endif // SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH

77
src/tgba/tgbaexplicit.cc
View file

@ -80,13 +80,38 @@ namespace spot
// tgba_explicit
tgba_explicit::tgba_explicit()
: init_(0), all_accepting_conditions_(bddfalse),
tgba_explicit::tgba_explicit(bdd_dict* dict)
: dict_(dict), init_(0), all_accepting_conditions_(bddfalse),
neg_accepting_conditions_(bddtrue),
all_accepting_conditions_computed_(false)
{
}
tgba_explicit::tgba_explicit(const tgba_explicit& other)
: tgba(),
name_state_map_(other.name_state_map_),
state_name_map_(other.state_name_map_),
dict_(other.dict_),
init_(other.init_),
all_accepting_conditions_(other.all_accepting_conditions_),
neg_accepting_conditions_(other.neg_accepting_conditions_),
all_accepting_conditions_computed_(other.
all_accepting_conditions_computed_)
{
dict_->register_all_variables_of(&other, this);
}
tgba_explicit&
tgba_explicit::operator=(const tgba_explicit& other)
{
if (&other != this)
{
this->~tgba_explicit();
new (this) tgba_explicit(other);
}
return *this;
}
tgba_explicit::~tgba_explicit()
{
ns_map::iterator i;
@ -97,6 +122,7 @@ namespace spot
delete *i2;
delete i->second;
}
dict_->unregister_all_my_variables(this);
}
tgba_explicit::state*
@ -136,20 +162,9 @@ namespace spot
tgba_explicit::get_condition(ltl::formula* f)
{
assert(dynamic_cast<ltl::atomic_prop*>(f));
tgba_bdd_dict::fv_map::iterator i = dict_.var_map.find(f);
int v;
if (i == dict_.var_map.end())
{
v = create_node();
dict_.var_map[f] = v;
dict_.var_formula_map[v] = f;
}
else
{
ltl::destroy(f);
v = i->second;
}
return ithvar(v);
int v = dict_->register_proposition(f, this);
ltl::destroy(f);
return bdd_ithvar(v);
}
void
@ -167,22 +182,15 @@ namespace spot
void
tgba_explicit::declare_accepting_condition(ltl::formula* f)
{
tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f);
if (i == dict_.acc_map.end())
{
int v;
v = create_node();
dict_.acc_map[f] = v;
dict_.acc_formula_map[v] = f;
neg_accepting_conditions_ &= !ithvar(v);
}
int v = dict_->register_accepting_variable(f, this);
ltl::destroy(f);
neg_accepting_conditions_ &= bdd_nithvar(v);
}
bool
tgba_explicit::has_accepting_condition(ltl::formula* f) const
{
tgba_bdd_dict::fv_map::const_iterator i = dict_.acc_map.find(f);
return i != dict_.acc_map.end();
return dict_->is_registered(f, this);
}
bdd
@ -201,11 +209,10 @@ namespace spot
/* Unreachable code. */
assert(0);
}
tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f);
assert (i != dict_.acc_map.end());
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(i != dict_->acc_map.end());
ltl::destroy(f);
bdd v = ithvar(i->second);
bdd v = bdd_ithvar(i->second);
v &= bdd_exist(neg_accepting_conditions_, v);
return v;
}
@ -232,7 +239,7 @@ namespace spot
all_accepting_conditions());
}
const tgba_bdd_dict&
bdd_dict*
tgba_explicit::get_dict() const
{
return dict_;
@ -254,10 +261,10 @@ namespace spot
if (!all_accepting_conditions_computed_)
{
bdd all = bddfalse;
tgba_bdd_dict::fv_map::const_iterator i;
for (i = dict_.acc_map.begin(); i != dict_.acc_map.end(); ++i)
bdd_dict::fv_map::const_iterator i;
for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i)
{
bdd v = ithvar(i->second);
bdd v = bdd_ithvar(i->second);
all |= v & bdd_exist(neg_accepting_conditions_, v);
}
all_accepting_conditions_ = all;

11
src/tgba/tgbaexplicit.hh
View file

@ -5,7 +5,6 @@
#include <map>
#include "tgba.hh"
#include "ltlast/formula.hh"
#include "bddfactory.hh"
namespace spot
{
@ -14,10 +13,12 @@ namespace spot
class tgba_explicit_succ_iterator;
/// Explicit representation of a spot::tgba.
class tgba_explicit : public tgba, public bdd_factory
class tgba_explicit: public tgba
{
public:
tgba_explicit();
tgba_explicit(bdd_dict* dict);
tgba_explicit(const tgba_explicit& other);
tgba_explicit& tgba_explicit::operator=(const tgba_explicit& other);
struct transition;
typedef std::list<transition*> state;
@ -44,7 +45,7 @@ namespace spot
virtual spot::state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const spot::state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const spot::state* state) const;
virtual bdd all_accepting_conditions() const;
@ -59,7 +60,7 @@ namespace spot
typedef std::map<const tgba_explicit::state*, std::string> sn_map;
ns_map name_state_map_;
sn_map state_name_map_;
tgba_bdd_dict dict_;
bdd_dict* dict_;
tgba_explicit::state* init_;
mutable bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;

37
src/tgba/tgbaproduct.cc
View file

@ -1,6 +1,4 @@
#include "tgbaproduct.hh"
#include "tgbatranslateproxy.hh"
#include "dictunion.hh"
#include <string>
#include <cassert>
@ -146,31 +144,9 @@ namespace spot
// tgba_product
tgba_product::tgba_product(const tgba& left, const tgba& right)
: dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict()))
: dict_(left.get_dict()), left_(&left), right_(&right)
{
// Translate the left automaton if needed.
if (dict_.contains(left.get_dict()))
{
left_ = &left;
left_should_be_freed_ = false;
}
else
{
left_ = new tgba_translate_proxy(left, dict_);
left_should_be_freed_ = true;
}
// Translate the right automaton if needed.
if (dict_.contains(right.get_dict()))
{
right_ = &right;
right_should_be_freed_ = false;
}
else
{
right_ = new tgba_translate_proxy(right, dict_);
right_should_be_freed_ = true;
}
assert(dict_ == right.get_dict());
all_accepting_conditions_ = ((left_->all_accepting_conditions()
& right_->neg_accepting_conditions())
@ -178,14 +154,13 @@ namespace spot
& left_->neg_accepting_conditions()));
neg_accepting_conditions_ = (left_->neg_accepting_conditions()
& right_->neg_accepting_conditions());
dict_->register_all_variables_of(&left_, this);
dict_->register_all_variables_of(&right_, this);
}
tgba_product::~tgba_product()
{
if (left_should_be_freed_)
delete left_;
if (right_should_be_freed_)
delete right_;
dict_->unregister_all_my_variables(this);
}
state*
@ -208,7 +183,7 @@ namespace spot
right_->neg_accepting_conditions());
}
const tgba_bdd_dict&
bdd_dict*
tgba_product::get_dict() const
{
return dict_;

6
src/tgba/tgbaproduct.hh
View file

@ -103,7 +103,7 @@ namespace spot
virtual tgba_product_succ_iterator*
succ_iter(const state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const state* state) const;
@ -111,11 +111,9 @@ namespace spot
virtual bdd neg_accepting_conditions() const;
private:
bdd_dict* dict_;
const tgba* left_;
bool left_should_be_freed_;
const tgba* right_;
bool right_should_be_freed_;
tgba_bdd_dict dict_;
bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;
};

159
src/tgba/tgbatranslateproxy.cc
View file

@ -1,159 +0,0 @@
#include "tgbatranslateproxy.hh"
#include "bddprint.hh"
#include <cassert>
namespace spot
{
// tgba_translate_proxy_succ_iterator
// --------------------------------------
tgba_translate_proxy_succ_iterator::
tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
bddPair* rewrite)
: iter_(it), rewrite_(rewrite)
{
}
tgba_translate_proxy_succ_iterator::~tgba_translate_proxy_succ_iterator()
{
delete iter_;
}
void
tgba_translate_proxy_succ_iterator::first()
{
iter_->first();
}
void
tgba_translate_proxy_succ_iterator::next()
{
iter_->next();
}
bool
tgba_translate_proxy_succ_iterator::done() const
{
return iter_->done();
}
state*
tgba_translate_proxy_succ_iterator::current_state() const
{
state* s = iter_->current_state();
s->translate(rewrite_);
return s;
}
bdd
tgba_translate_proxy_succ_iterator::current_condition() const
{
return bdd_replace(iter_->current_condition(), rewrite_);
}
bdd
tgba_translate_proxy_succ_iterator::current_accepting_conditions() const
{
return bdd_replace(iter_->current_accepting_conditions(), rewrite_);
}
// tgba_translate_proxy
// ------------------------
tgba_translate_proxy::tgba_translate_proxy(const tgba& from,
const tgba_bdd_dict& to)
: from_(from), to_(to)
{
const tgba_bdd_dict& f = from.get_dict();
rewrite_to_ = bdd_newpair();
rewrite_from_ = bdd_newpair();
tgba_bdd_dict::fv_map::const_iterator i_from;
tgba_bdd_dict::fv_map::const_iterator i_to;
for (i_from = f.now_map.begin(); i_from != f.now_map.end(); ++i_from)
{
i_to = to_.now_map.find(i_from->first);
assert(i_to != to_.now_map.end());
bdd_setpair(rewrite_to_, i_from->second, i_to->second);
bdd_setpair(rewrite_to_, i_from->second + 1, i_to->second + 1);
bdd_setpair(rewrite_from_, i_to->second, i_from->second);
bdd_setpair(rewrite_from_, i_to->second + 1, i_from->second + 1);
}
for (i_from = f.var_map.begin(); i_from != f.var_map.end(); ++i_from)
{
i_to = to_.var_map.find(i_from->first);
assert(i_to != to_.var_map.end());
bdd_setpair(rewrite_to_, i_from->second, i_to->second);
bdd_setpair(rewrite_from_, i_to->second, i_from->second);
}
for (i_from = f.acc_map.begin(); i_from != f.acc_map.end(); ++i_from)
{
i_to = to_.acc_map.find(i_from->first);
assert(i_to != to_.acc_map.end());
bdd_setpair(rewrite_to_, i_from->second, i_to->second);
bdd_setpair(rewrite_from_, i_to->second, i_from->second);
}
all_accepting_conditions_ = bdd_replace(from.all_accepting_conditions(),
rewrite_to_);
neg_accepting_conditions_ = bdd_replace(from.neg_accepting_conditions(),
rewrite_to_);
}
tgba_translate_proxy::~tgba_translate_proxy()
{
bdd_freepair(rewrite_from_);
bdd_freepair(rewrite_to_);
}
state*
tgba_translate_proxy::get_init_state() const
{
state* s = from_.get_init_state();
s->translate(rewrite_to_);
return s;
}
tgba_translate_proxy_succ_iterator*
tgba_translate_proxy::succ_iter(const state* s) const
{
state* s2 = s->clone();
s2->translate(rewrite_from_);
tgba_translate_proxy_succ_iterator *res =
new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2),
rewrite_to_);
delete s2;
return res;
}
const tgba_bdd_dict&
tgba_translate_proxy::get_dict() const
{
return to_;
}
std::string
tgba_translate_proxy::format_state(const state* s) const
{
state* s2 = s->clone();
s2->translate(rewrite_from_);
std::string res = from_.format_state(s2);
delete s2;
return res;
}
bdd
tgba_translate_proxy::all_accepting_conditions() const
{
return all_accepting_conditions_;
}
bdd tgba_translate_proxy::neg_accepting_conditions() const
{
return neg_accepting_conditions_;
}
}

69
src/tgba/tgbatranslateproxy.hh
View file

@ -1,69 +0,0 @@
#ifndef SPOT_TGBA_TGBATRANSLATEPROXY_HH
# define SPOT_TGBA_TGBATRANSLATEPROXY_HH
#include "tgba.hh"
namespace spot
{
/// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber
/// BDD variables on the fly.
class tgba_translate_proxy_succ_iterator: public tgba_succ_iterator
{
public:
tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
bddPair* rewrite);
virtual ~tgba_translate_proxy_succ_iterator();
// iteration
void first();
void next();
bool done() const;
// inspection
state* current_state() const;
bdd current_condition() const;
bdd current_accepting_conditions() const;
protected:
tgba_succ_iterator* iter_;
bddPair* rewrite_;
};
/// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables
/// on the fly.
class tgba_translate_proxy: public tgba
{
public:
/// \brief Constructor.
/// \param from The spot::tgba to masquerade.
/// \param to The new dictionary to use.
tgba_translate_proxy(const tgba& from,
const tgba_bdd_dict& to);
virtual ~tgba_translate_proxy();
virtual state* get_init_state() const;
virtual tgba_translate_proxy_succ_iterator*
succ_iter(const state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual std::string format_state(const state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
private:
const tgba& from_; ///< The spot::tgba to masquerade.
tgba_bdd_dict to_; ///< The new dictionar to use.
bddPair* rewrite_to_; ///< The rewriting pair for from->to.
bddPair* rewrite_from_; ///< The rewriting pair for to->from.
bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;
};
}
#endif // SPOT_TGBA_TGBATRANSLATEPROXY_HH

4
src/tgbaalgos/lbtt.cc
View file

@ -64,7 +64,7 @@ namespace spot
// Conjunctions are printed by bdd_format_sat, so we just have
// to handle the other cases.
static std::string
bdd_to_lbtt(bdd b, const tgba_bdd_dict& d)
bdd_to_lbtt(bdd b, const bdd_dict* d)
{
if (b == bddfalse)
return "f";
@ -178,7 +178,7 @@ namespace spot
std::ostream&
lbtt_reachable(std::ostream& os, const tgba& g)
{
const tgba_bdd_dict& d = g.get_dict();
const bdd_dict* d = g.get_dict();
std::ostringstream body;
seen_map seen;

32
src/tgbaalgos/ltl2tgba.cc
View file

@ -38,7 +38,7 @@ namespace spot
void
visit(const atomic_prop* node)
{
res_ = fact_.ithvar(fact_.create_atomic_prop(node));
res_ = bdd_ithvar(fact_.create_atomic_prop(node));
}
void
@ -70,8 +70,8 @@ namespace spot
now <=> x | next
*/
int v = fact_.create_state(node);
bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1);
bdd now = bdd_ithvar(v);
bdd next = bdd_ithvar(v + 1);
bdd x = recurse(node->child());
fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp));
/*
@ -101,8 +101,8 @@ namespace spot
}
// Gx <=> x && XGx
int v = fact_.create_state(node);
bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1);
bdd now = bdd_ithvar(v);
bdd next = bdd_ithvar(v + 1);
fact_.constrain_relation(bdd_apply(now, child & next,
bddop_biimp));
res_ = now;
@ -116,8 +116,8 @@ namespace spot
case unop::X:
{
int v = fact_.create_state(node->child());
bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1);
bdd now = bdd_ithvar(v);
bdd next = bdd_ithvar(v + 1);
fact_.constrain_relation(bdd_apply(now, recurse(node->child()),
bddop_biimp));
res_ = next;
@ -153,8 +153,8 @@ namespace spot
now <=> f2 | (f1 & next)
*/
int v = fact_.create_state(node);
bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1);
bdd now = bdd_ithvar(v);
bdd next = bdd_ithvar(v + 1);
fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
bddop_biimp));
/*
@ -175,8 +175,8 @@ namespace spot
now <=> f2 & (f1 | next)
*/
int v = fact_.create_state(node);
bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1);
bdd now = bdd_ithvar(v);
bdd next = bdd_ithvar(v + 1);
fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
bddop_biimp));
res_ = now;
@ -231,18 +231,18 @@ namespace spot
};
tgba_bdd_concrete
ltl_to_tgba(const ltl::formula* f)
ltl_to_tgba(const ltl::formula* f, bdd_dict* dict)
{
// Normalize the formula. We want all the negation on
// the atomic proposition. We also suppress logic
// abbreviation such as <=>, =>, or XOR, since they
// Normalize the formula. We want all the negations on
// the atomic propositions. We also suppress logic
// abbreviations such as <=>, =>, or XOR, since they
// would involve negations at the BDD level.
const ltl::formula* f1 = ltl::unabbreviate_logic(f);
const ltl::formula* f2 = ltl::negative_normal_form(f1);
ltl::destroy(f1);
// Traverse the formula and draft the automaton in a factory.
tgba_bdd_concrete_factory fact;
tgba_bdd_concrete_factory fact(dict);
ltl_trad_visitor v(fact, true);
f2->accept(v);
ltl::destroy(f2);

2
src/tgbaalgos/ltl2tgba.hh
View file

@ -7,7 +7,7 @@
namespace spot
{
/// Build a spot::tgba_bdd_concrete from an LTL formula.
tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f);
tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f, bdd_dict* dict);
}
#endif // SPOT_TGBA_LTL2TGBA_HH

6
src/tgbaalgos/save.cc
View file

@ -42,10 +42,10 @@ namespace spot
std::ostream&
tgba_save_reachable(std::ostream& os, const tgba& g)
{
const tgba_bdd_dict& d = g.get_dict();
const bdd_dict* d = g.get_dict();
os << "acc =";
for (tgba_bdd_dict::fv_map::const_iterator ai = d.acc_map.begin();
ai != d.acc_map.end(); ++ai)
for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin();
ai != d->acc_map.end(); ++ai)
{
os << " \"";
ltl::to_string(ai->first, os) << "\"";

2
src/tgbaparse/public.hh
View file

@ -20,6 +20,7 @@ namespace spot
/// \param filename The name of the file to parse.
/// \param error_list A list that will be filled with
/// parse errors that occured during parsing.
/// \param dict The BDD dictionary where to use.
/// \param env The environment into which parsing should take place.
/// \param debug When true, causes the parser to trace its execution.
/// \return A pointer to the tgba built from \a filename, or
@ -33,6 +34,7 @@ namespace spot
/// \warning This function is not reentrant.
tgba_explicit* tgba_parse(const std::string& filename,
tgba_parse_error_list& error_list,
bdd_dict* dict,
ltl::environment& env
= ltl::default_environment::instance(),
bool debug = false);

25
src/tgbaparse/tgbaparse.yy
View file

@ -155,22 +155,23 @@ namespace spot
tgba_explicit*
tgba_parse(const std::string& name,
tgba_parse_error_list& error_list,
bdd_dict* dict,
environment& env,
bool debug)
{
if (tgbayyopen(name))
{
error_list.push_back
(tgba_parse_error(yy::Location(),
std::string("Cannot open file ") + name));
return 0;
}
tgba_explicit* result = new tgba_explicit;
tgbayy::Parser parser(debug, yy::Location(), error_list, env, result);
parser.parse();
tgbayyclose();
return result;
}
{
error_list.push_back
(tgba_parse_error(yy::Location(),
std::string("Cannot open file ") + name));
return 0;
}
tgba_explicit* result = new tgba_explicit(dict);
tgbayy::Parser parser(debug, yy::Location(), error_list, env, result);
parser.parse();
tgbayyclose();
return result;
}
}
// Local Variables:

39
src/tgbatest/explicit.cc
View file

@ -1,29 +1,40 @@
#include <iostream>
#include <cassert>
#include "ltlenv/defaultenv.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "ltlast/allnodes.hh"
int
main()
{
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::default_environment& e =
spot::ltl::default_environment::instance();
spot::tgba_explicit a;
spot::tgba_explicit* a = new spot::tgba_explicit(dict);
typedef spot::tgba_explicit::transition trans;
trans* t1 = a.create_transition("state 0", "state 1");
trans* t2 = a.create_transition("state 1", "state 2");
trans* t3 = a.create_transition("state 2", "state 0");
a.add_condition(t2, e.require("a"));
a.add_condition(t3, e.require("b"));
a.add_condition(t3, e.require("c"));
a.declare_accepting_condition(e.require("p"));
a.declare_accepting_condition(e.require("q"));
a.declare_accepting_condition(e.require("r"));
a.add_accepting_condition(t1, e.require("p"));
a.add_accepting_condition(t1, e.require("q"));
a.add_accepting_condition(t2, e.require("r"));
trans* t1 = a->create_transition("state 0", "state 1");
trans* t2 = a->create_transition("state 1", "state 2");
trans* t3 = a->create_transition("state 2", "state 0");
a->add_condition(t2, e.require("a"));
a->add_condition(t3, e.require("b"));
a->add_condition(t3, e.require("c"));
a->declare_accepting_condition(e.require("p"));
a->declare_accepting_condition(e.require("q"));
a->declare_accepting_condition(e.require("r"));
a->add_accepting_condition(t1, e.require("p"));
a->add_accepting_condition(t1, e.require("q"));
a->add_accepting_condition(t2, e.require("r"));
spot::dotty_reachable(std::cout, a);
spot::dotty_reachable(std::cout, *a);
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);
}

7
src/tgbatest/explprod.cc
View file

@ -22,13 +22,15 @@ main(int argc, char** argv)
if (argc != 3)
syntax(argv[0]);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env);
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env);
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2))
return 2;
@ -44,5 +46,6 @@ main(int argc, char** argv)
delete a1;
delete a2;
assert(spot::ltl::atomic_prop::instance_count() == 0);
delete dict;
return exit_code;
}

16
src/tgbatest/ltl2tgba.cc
View file

@ -5,7 +5,6 @@
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba.hh"
#include "tgba/bddprint.hh"
#include "tgba/tgbabddtranslatefactory.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
@ -19,7 +18,6 @@ syntax(char* prog)
<< std::endl
<< " -A same as -a, but as a set" << std::endl
<< " -d turn on traces during parsing" << std::endl
<< " -o re-order BDD variables in the automata" << std::endl
<< " -r display the relation BDD, not the reachability graph"
<< std::endl
<< " -R same as -r, but as a set" << std::endl
@ -35,7 +33,6 @@ main(int argc, char** argv)
int exit_code = 0;
bool debug_opt = false;
bool defrag_opt = false;
int output = 0;
int formula_index = 0;
@ -58,10 +55,6 @@ main(int argc, char** argv)
{
debug_opt = true;
}
else if (!strcmp(argv[formula_index], "-o"))
{
defrag_opt = true;
}
else if (!strcmp(argv[formula_index], "-r"))
{
output = 1;
@ -84,7 +77,6 @@ main(int argc, char** argv)
}
}
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
@ -93,12 +85,11 @@ main(int argc, char** argv)
exit_code =
spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
spot::bdd_dict* dict = new spot::bdd_dict();
if (f)
{
spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f);
spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict);
spot::ltl::destroy(f);
if (defrag_opt)
a = spot::defrag(a);
switch (output)
{
case 0:
@ -121,7 +112,7 @@ main(int argc, char** argv)
a.get_core_data().accepting_conditions);
break;
case 5:
a.get_dict().dump(std::cout);
a.get_dict()->dump(std::cout);
break;
case 6:
spot::lbtt_reachable(std::cout, a);
@ -139,5 +130,6 @@ main(int argc, char** argv)
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
delete dict;
return exit_code;
}

6
src/tgbatest/ltlprod.cc
View file

@ -37,9 +37,10 @@ main(int argc, char** argv)
if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2))
return 2;
spot::bdd_dict* dict = new spot::bdd_dict();
{
spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1);
spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2);
spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict);
spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2, dict);
spot::ltl::destroy(f1);
spot::ltl::destroy(f2);
@ -56,5 +57,6 @@ main(int argc, char** argv)
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
delete dict;
return exit_code;
}

7
src/tgbatest/mixprod.cc
View file

@ -24,6 +24,8 @@ main(int argc, char** argv)
if (argc != 3)
syntax(argv[0]);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel1;
@ -32,12 +34,12 @@ main(int argc, char** argv)
return 2;
spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env);
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2))
return 2;
{
spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1);
spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict);
spot::ltl::destroy(f1);
spot::tgba_product p(a1, *a2);
@ -49,5 +51,6 @@ main(int argc, char** argv)
assert(spot::ltl::multop::instance_count() == 0);
delete a2;
assert(spot::ltl::atomic_prop::instance_count() == 0);
delete dict;
return exit_code;
}

13
src/tgbatest/readsave.cc
View file

@ -1,7 +1,9 @@
#include <iostream>
#include <cassert>
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/save.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)
@ -29,10 +31,12 @@ main(int argc, char** argv)
filename_index = 2;
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
pel, env, debug);
pel, dict, env, debug);
exit_code =
spot::format_tgba_parse_errors(std::cerr, pel);
@ -46,5 +50,12 @@ main(int argc, char** argv)
{
exit_code = 1;
}
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);
return exit_code;
}

7
src/tgbatest/spotlbtt.cc
View file

@ -35,9 +35,11 @@ main(int argc, char** argv)
if (! std::getline(fin, input, '\0'))
{
std::cerr << "Cannot read " << argv[1] << std::endl;
exit(2);
exit(2);
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(input, pel, env);
@ -46,7 +48,7 @@ main(int argc, char** argv)
if (f)
{
spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f);
spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict);
spot::ltl::destroy(f);
spot::lbtt_reachable(std::cout, a);
}
@ -59,5 +61,6 @@ main(int argc, char** argv)
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
delete dict;
return exit_code;
}

13
src/tgbatest/tgbaread.cc
View file

@ -1,7 +1,9 @@
#include <iostream>
#include <cassert>
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)
@ -29,10 +31,12 @@ main(int argc, char** argv)
filename_index = 2;
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
pel, env, debug);
pel, dict, env, debug);
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
@ -46,5 +50,12 @@ main(int argc, char** argv)
{
return 1;
}
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);
return 0;
}

9
src/tgbatest/tripprod.cc
View file

@ -22,17 +22,19 @@ main(int argc, char** argv)
if (argc != 4)
syntax(argv[0]);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env);
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env);
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2))
return 2;
spot::tgba_parse_error_list pel3;
spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, env);
spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel3))
return 2;
@ -50,5 +52,6 @@ main(int argc, char** argv)
delete a2;
delete a3;
assert(spot::ltl::atomic_prop::instance_count() == 0);
delete dict;
return exit_code;
}