Commit ddf05b5d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,

src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
Doxygen comments.
parent 236a26ad
2003-05-27 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
Doxygen comments.
* src/tgba/bddprint.hh (bdd_format_set): New function.
* src/tgba/bddprint.cc (bdd_format_set): Likewise.
* src/tgba/state.hh: Add Doxygen comments.
......
......@@ -6,27 +6,54 @@
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();
int create_nodes(int i);
static bool initialized;
static int varnum;
int varused;
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.
};
}
......
......@@ -6,6 +6,7 @@
namespace spot
{
/// A state whose representation is a BDD.
class state_bdd: public state
{
public:
......@@ -14,6 +15,7 @@ namespace spot
{
}
/// Return the BDD part of the state.
bdd
as_bdd() const
{
......@@ -23,7 +25,7 @@ namespace spot
virtual int compare(const state* other) const;
protected:
bdd state_;
bdd state_; ///< BDD representation of the state.
};
}
......
......@@ -7,9 +7,18 @@
namespace spot
{
/// A concrete iterator over successors of a TGBA state.
class tgba_succ_iterator_concrete: public tgba_succ_iterator
{
public:
/// \brief Build a spot::tgba_succ_iterator_concrete.
///
/// \param successors The set of successors with ingoing conditions
/// and promises, represented as a BDD. The job of this iterator
/// will be to enumerate the satisfactions of that BDD and split
/// them into destination state, conditions, and promises.
/// \param d The core data of the automata. These contains
/// sets of variables useful to split a BDD.
tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors);
virtual ~tgba_succ_iterator_concrete();
......@@ -24,10 +33,10 @@ namespace spot
bdd current_promise();
private:
const tgba_bdd_core_data& data_;
bdd succ_set_; // The set of successors.
bdd next_succ_set_; // Unexplored successors (including current_).
bdd current_; // Current successor.
const tgba_bdd_core_data& data_; ///< Core data of the automata.
bdd succ_set_; ///< The set of successors.
bdd next_succ_set_; ///< Unexplored successors (including current_).
bdd current_; ///< Current successor.
};
}
......
......@@ -8,15 +8,35 @@
namespace spot
{
/// \brief A concrete spot::tgba implemented using BDDs.
///
class tgba_bdd_concrete: public tgba
{
public:
/// \brief Construct a tgba_bdd_concrete with unknown initial state.
///
/// set_init_state() should be called later.
tgba_bdd_concrete(const tgba_bdd_factory& fact);
/// \brief Construct a tgba_bdd_concrete with known initial state.
tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init);
~tgba_bdd_concrete();
/// \brief Set the initial state.
void set_init_state(bdd s);
state_bdd* get_init_state() const;
/// \brief Get the initial state directly as a BDD.
///
/// The sole point of this method is to prevent writing
/// horrors such as
/// \code
/// state_bdd* s = automata.get_init_state();
/// some_class some_instance(s->as_bdd());
/// delete s;
/// \endcode
bdd get_init_bdd() const;
tgba_succ_iterator_concrete* succ_iter(const state* state) const;
......@@ -24,13 +44,18 @@ namespace spot
std::string format_state(const state* state) const;
const tgba_bdd_dict& get_dict() const;
/// \brief Get the core data associated to this automaton.
///
/// These data includes the various BDD used to represent
/// the relation, encode variable sets, Next-to-Now rewrite
/// rules, etc.
const tgba_bdd_core_data& get_core_data() const;
protected:
tgba_bdd_core_data data_;
tgba_bdd_dict dict_;
bdd init_;
friend class tgba_tgba_succ_iterator;
tgba_bdd_core_data data_; ///< Core data associated to the automaton.
tgba_bdd_dict dict_; ///< Dictionary used by the automaton.
bdd init_; ///< Initial state.
};
}
......
......@@ -5,48 +5,62 @@
namespace spot
{
/// Core data for a TGBA encoded using BDDs.
struct tgba_bdd_core_data
{
// RELATION encodes the transition relation of the TGBA.
// It uses four kinds of variables:
// - "Now" variables, that encode the current state
// - "Next" variables, that encode the destination state
// - atomic propositions, which are things to verify before going on
// to the next state
// - promises: a U b, or F b, both implie that b should be verified
// eventually. We encode this with Prom[b], and check
// that promises are fullfilled in the emptyness check.
/// \brief encodes the transition relation of the TGBA.
///
/// \c relation uses four kinds of variables:
/// \li "Now" variables, that encode the current state
/// \li "Next" variables, that encode the destination state
/// \li atomic propositions, which are things to verify before going on
/// to the next state
/// \li promises: \c a \c U \c b, or \c F \cb, both imply that \c b
/// should be verified eventually. We encode this with \c Prom[b],
/// and check that promises are fullfilled in the emptyness check.
bdd relation;
// The conjunction of all Now variables, in their positive form.
/// The conjunction of all Now variables, in their positive form.
bdd now_set;
// The conjunction of all Now variables, in their negated form.
/// The conjunction of all Now variables, in their negated form.
bdd negnow_set;
// The (positive) conjunction of all variables which are not Now variables.
/// \brief The (positive) conjunction of all variables which are
/// not Now variables.
bdd notnow_set;
// The (positive) conjunction of all variables which are not atomic
// propositions.
/// \brief The (positive) conjunction of all variables which are
/// not atomic propositions.
bdd notvar_set;
// The (positive) conjunction of all variables which are not promises.
/// The (positive) conjunction of all variables which are not promises.
bdd notprom_set;
// Record pairings between Next and Now variables.
/// Record pairings between Next and Now variables.
bddPair* next_to_now;
/// \brief Default constructor.
///
/// Initially all variable set are empty and the \c relation is true.
tgba_bdd_core_data();
/// Copy constructor.
tgba_bdd_core_data(const tgba_bdd_core_data& copy);
// Merge two core_data.
/// \brief Merge two tgba_bdd_core_data.
///
/// This is used when building a product of two automata.
tgba_bdd_core_data(const tgba_bdd_core_data& left,
const tgba_bdd_core_data& right);
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);
/// \brief Update the variable sets to take a new automic proposition into
/// account.
void declare_atomic_prop(bdd var);
/// Update the variable sets to take a new promise into account.
void declare_promise(bdd prom);
};
}
......
......@@ -7,22 +7,24 @@
namespace spot
{
/// Dictionary of BDD variables.
struct tgba_bdd_dict
{
// Dictionaries for BDD variables.
// formula-to-BDD-variable maps
/// Formula-to-BDD-variable maps.
typedef std::map<const ltl::formula*, int> fv_map;
// BDD-variable-to-formula maps
/// BDD-variable-to-formula maps.
typedef std::map<int, const ltl::formula*> vf_map;
fv_map now_map;
vf_map now_formula_map;
fv_map var_map;
vf_map var_formula_map;
fv_map prom_map;
vf_map prom_formula_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 prom_map; ///< Maps promises to BDD variables.
vf_map prom_formula_map; ///< Maps BDD variables to promises.
/// \brief Dump all variables for debugging.
/// \param os The output stream.
std::ostream& dump(std::ostream& os) const;
};
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment