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

bdddict: remove now/next variables.

Browse source 
These were only used by the BDD-based implementation of TGBA, which has
been removed.

* src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc: Remove
support for now/next variables.
This commit is contained in:
Alexandre Duret-Lutz 2014-07-09 23:32:23 +02:00
parent 116fe8654f
commit 18f6fe772b
3 changed files with 7 additions and 119 deletions
Download patch file Download diff file Expand all files Collapse all files

84
src/tgba/bdddict.cc
View file

@ -85,17 +85,13 @@ namespace spot
bdd_dict::bdd_dict()
// Initialize priv_ first, because it also initializes BuDDy
: priv_(new bdd_dict_priv()),
bdd_map(bdd_varnum()),
next_to_now(bdd_newpair()),
now_to_next(bdd_newpair())
bdd_map(bdd_varnum())
{
}
bdd_dict::~bdd_dict()
{
assert_emptiness();
bdd_freepair(next_to_now);
bdd_freepair(now_to_next);
delete priv_;
}
@ -138,35 +134,6 @@ namespace spot
register_propositions(bdd_low(f), for_me);
}
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 = f->clone();
num = priv_->allocate_variables(2);
now_map[f] = num;
bdd_map.resize(bdd_varnum());
bdd_map[num].type = now;
bdd_map[num].f = f;
bdd_map[num + 1].type = next;
bdd_map[num + 1].f = 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);
}
bdd_map[num].refs.insert(for_me); // Keep only references for now.
return num;
}
int
bdd_dict::register_acceptance_variable(const ltl::formula* f,
const void* for_me)
@ -315,7 +282,7 @@ namespace spot
// 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.
// if this is a Var or an Acc variable.
int n = 1;
const ltl::formula* f = 0;
switch (bdd_map[v].type)
@ -324,15 +291,6 @@ namespace spot
f = bdd_map[v].f;
var_map.erase(f);
break;
case now:
f = bdd_map[v].f;
now_map.erase(f);
bdd_setpair(now_to_next, v, v);
bdd_setpair(next_to_now, v + 1, v + 1);
n = 2;
break;
case next:
break;
case acc:
f = bdd_map[v].f;
acc_map.erase(f);
@ -388,16 +346,6 @@ namespace spot
return s.find(by_me) != s.end();
}
bool
bdd_dict::is_registered_state(const ltl::formula* f, const void* by_me)
{
fv_map::iterator fi = now_map.find(f);
if (fi == now_map.end())
return false;
ref_set& s = bdd_map[fi->second].refs;
return s.find(by_me) != s.end();
}
bool
bdd_dict::is_registered_acceptance_variable(const ltl::formula* f,
const void* by_me)
@ -423,12 +371,6 @@ namespace spot
case anon:
os << (r.refs.empty() ? "Free" : "Anon");
break;
case now:
os << "Now[" << to_string(r.f) << ']';
break;
case next:
os << "Next[" << to_string(r.f) << ']';
break;
case acc:
os << "Acc[" << to_string(r.f) << ']';
break;
@ -467,8 +409,6 @@ namespace spot
bool var_seen = false;
bool acc_seen = false;
bool now_seen = false;
bool next_seen = false;
bool refs_seen = false;
unsigned s = bdd_map.size();
for (unsigned i = 0; i < s; ++i)
@ -481,36 +421,18 @@ namespace spot
case acc:
acc_seen = true;
break;
case now:
now_seen = true;
break;
case next:
next_seen = true;
break;
case anon:
break;
}
refs_seen |= !bdd_map[i].refs.empty();
}
if (var_map.empty()
&& now_map.empty()
&& acc_map.empty())
if (var_map.empty() && acc_map.empty())
{
if (var_seen)
{
std::cerr << "var_map is empty but Var in map" << std::endl;
fail = true;
}
if (now_seen)
{
std::cerr << "now_map is empty but Now in map" << std::endl;
fail = true;
}
else if (next_seen)
{
std::cerr << "Next variable seen (without Now) in map" << std::endl;
fail = true;
}
if (acc_seen)
{
std::cerr << "acc_map is empty but Acc in map" << std::endl;

34
src/tgba/bdddict.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// 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.
@ -42,9 +42,7 @@ namespace spot
/// The BDD library uses integers to designate Boolean variables in
/// its decision diagrams. This class is used to map such integers
/// to objects actually used in Spot. These objects are usually
/// atomic propositions, but they can also be acceptance conditions,
/// or "Now/Next" variables (although the latter should be
/// eventually removed).
/// atomic propositions, but they can also be acceptance conditions.
///
/// When a BDD variable is registered using a bdd_dict, it is always
/// associated to a "user" (or "owner") object. This is done by
@ -72,14 +70,13 @@ namespace spot
/// BDD-variable-to-formula maps.
typedef std::map<int, const ltl::formula*> vf_map;
fv_map now_map; ///< Maps formulae to "Now" BDD variables
fv_map var_map; ///< Maps atomic propositions to BDD variables
fv_map acc_map; ///< Maps acceptance conditions to BDD variables
/// BDD-variable reference counts.
typedef std::set<const void*> ref_set;
enum var_type { anon = 0, now, next, var, acc };
enum var_type { anon = 0, var, acc };
struct bdd_info {
bdd_info() : type(anon) {}
var_type type;
@ -91,15 +88,6 @@ namespace spot
// Map BDD variables to their meaning.
bdd_info_map bdd_map;
/// \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
@ -121,19 +109,6 @@ namespace spot
/// automaton).
void register_propositions(bdd 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
@ -215,7 +190,6 @@ namespace spot
/// @{
/// Check whether formula \a f has already been registered by \a by_me.
bool is_registered_proposition(const ltl::formula* f, const void* by_me);
bool is_registered_state(const ltl::formula* f, const void* by_me);
bool is_registered_acceptance_variable(const ltl::formula* f,
const void* by_me);
/// @}

8
src/tgba/bddprint.cc
View file

@ -72,14 +72,6 @@ namespace spot
print_ltl(ref.f, o) << '"';
}
break;
case bdd_dict::now:
o << "Now[";
print_ltl(ref.f, o) << ']';
break;
case bdd_dict::next:
o << "Next[";
print_ltl(ref.f, o) << ']';
break;
case bdd_dict::anon:
o << '?' << v;
}