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

* src/tgba/bddprint.cc, src/tgba/bddprint.hh,

src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
Add Doxygen comments.
parent ddf05b5d
2003-05-27 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
Add Doxygen comments.
* 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
......
......@@ -4,9 +4,10 @@
namespace spot
{
/// Global dictionary used by print_handler() to lookup variables.
const tgba_bdd_dict* dict;
/// Stream handler used by Buddy to display BDD variables.
static void
print_handler(std::ostream& o, int var)
{
......
......@@ -9,13 +9,29 @@
namespace spot
{
/// \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);
/// \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);
/// \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);
/// \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);
......
......@@ -5,6 +5,7 @@
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);
}
......
......@@ -3,11 +3,15 @@
#include "tgbabddconcretefactory.hh"
#include "ltl2tgba.hh"
// FIXME: Add ref to Couvreur's paper.
namespace spot
{
using namespace ltl;
/// \brief Recursively translate a formula into a BDD.
///
/// The algorithm used here is adapted from Jean-Michel Couvreur's
/// Probataf tool.
class ltl_trad_visitor: public const_visitor
{
public:
......@@ -171,7 +175,7 @@ namespace spot
};
tgba_bdd_concrete
ltl_to_tgba(const formula* f)
ltl_to_tgba(const ltl::formula* f)
{
tgba_bdd_concrete_factory fact;
ltl_trad_visitor v(fact);
......
......@@ -6,8 +6,8 @@
namespace spot
{
/// Build a spot::tgba_bdd_concrete from an LTL formula.
tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f);
}
#endif // SPOT_TGBA_LTL2TGBA_HH
......@@ -5,26 +5,53 @@
#include "bddfactory.hh"
#include "tgbabddfactory.hh"
namespace spot
namespace spot
{
/// Helper class to build a spot::tgba_bdd_concrete object.
class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory
{
public:
virtual ~tgba_bdd_concrete_factory();
int create_state(const ltl::formula* f);
/// Create a state variable for formula \a f.
///
/// \param f The formula to create a state for.
/// \return The variable number for this state.
///
/// The state is not created if it already exists. Instead its
/// existing variable number is returned. Variable numbers
/// can be turned into BDD using ithvar().
int create_state(const ltl::formula* f);
/// Create an atomic proposition variable for formula \a f.
///
/// \param f The formula to create an aotmic proposition for.
/// \return The variable number for this state.
///
/// The atomic proposition is not created if it already exists.
/// Instead its existing variable number is returned. Variable numbers
/// can be turned into BDD using ithvar().
int create_atomic_prop(const ltl::formula* f);
/// Create a promise variable for formula \a f.
///
/// \param f The formula to create a promise for.
/// \return The variable number for this state.
///
/// The promise is not created if it already exists. Instead its
/// existing variable number is returned. Variable numbers
/// can be turned into BDD using ithvar().
int create_promise(const ltl::formula* f);
const tgba_bdd_core_data& get_core_data() const;
const tgba_bdd_dict& get_dict() const;
/// Add a new constraint to the relation.
void add_relation(bdd new_rel);
private:
tgba_bdd_core_data data_;
tgba_bdd_dict dict_;
tgba_bdd_core_data data_; ///< Core data for the new automata.
tgba_bdd_dict dict_; ///< Dictionary for the new automata.
};
}
......
......@@ -4,6 +4,11 @@
namespace spot
{
/// \brief Helper class for product().
///
/// As both automata are encoded using BDD, we just have
/// to homogenize the variable numbers before ANDing the
/// relations and initial states.
class tgba_bdd_product_factory: public tgba_bdd_factory
{
public:
......@@ -11,36 +16,36 @@ namespace spot
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())
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())
{
}
virtual
~tgba_bdd_product_factory()
{
}
const tgba_bdd_core_data&
get_core_data() const
{
return data_;
}
const tgba_bdd_dict&
get_dict() const
{
return dict_;
}
bdd
get_init_state() const
{
return init_;
}
private:
tgba_bdd_dict dict_;
tgba_bdd_translate_factory fact_left_;
......@@ -48,11 +53,11 @@ namespace spot
tgba_bdd_core_data data_;
bdd init_;
};
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());
}
......
......@@ -5,6 +5,10 @@
namespace spot
{
/// \brief Multiplies two tgba::tgba_bdd_concrete automata.
///
/// This function build the resulting product, as another
/// tgba::tgba_bdd_concrete automaton.
tgba_bdd_concrete
product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right);
}
......
......@@ -6,10 +6,16 @@
namespace spot
{
/// \brief Abstract class for spot::tgba_bdd_concrete factories.
///
/// A spot::tgba_bdd_concrete can be constructed from anything that
/// supplies core data and their associated dictionary.
class tgba_bdd_factory
{
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;
};
}
......
......@@ -6,28 +6,37 @@
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();
bddPair* compute_pairs(const tgba_bdd_dict& from);
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_;
bdd init_;
};
/// Reorder the variables of an automata.
tgba_bdd_concrete defrag(const tgba_bdd_concrete& a);
}
......
......@@ -7,6 +7,7 @@ namespace spot
{
typedef std::map<state*, int, state_ptr_less_than> seen_map;
/// Output and record a state.
static bool
dotty_state(std::ostream& os,
const tgba& g, state* st, seen_map& m, int& node)
......@@ -28,6 +29,7 @@ namespace spot
return true;
}
/// Process successors.
static void
dotty_rec(std::ostream& os,
const tgba& g, state* st, seen_map& m, int father)
......
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