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

This implements Couvreur's FM'99 ltl2tgba translation.

* src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...
(bdd_dict::is_registered_proposition, bdd_dict::is_registered_state,
bdd_dict::is_registered_accepting_variable): ... these.
* src/tgba/bdddict.hh: Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method.
(tgba_explicit::declare_accepting_condition): Arrange so that this
function can be called during the construction of the automaton.
(tgba_explicit::complement_all_accepting_conditions): New method.
(tgba_explicit::has_accepting_condition): Adjust to call
bdd_dict::is_registered_accepting_variable.
* src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state,
tgba_explicit::complement_all_accepting_conditions): New methods.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt
and tbalbtt.
(tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove.
* src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t".
* src/tgbatest/ltl2tgba.cc: Implement the -f and -F options.
* src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of
"spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add
also check the ltl2tgba_fm translator.
* wrap/python/spot.i: Wrap ltl2tgba_fm.
* wrap/python/cgi/ltl2tgba.in: Add radio buttons to select
between ltl2tgba and ltl2tgba_fm.
* wrap/python/tests/ltl2tgba.py: Add support for the -f option.
* wrap/python/tests/ltl2tgba.test: Try the -f option.
parent 256d8005
2003-08-15 Alexandre Duret-Lutz <adl@gnu.org>
This implements Couvreur's FM'99 ltl2tgba translation.
* src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...
(bdd_dict::is_registered_proposition, bdd_dict::is_registered_state,
bdd_dict::is_registered_accepting_variable): ... these.
* src/tgba/bdddict.hh: Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method.
(tgba_explicit::declare_accepting_condition): Arrange so that this
function can be called during the construction of the automaton.
(tgba_explicit::complement_all_accepting_conditions): New method.
(tgba_explicit::has_accepting_condition): Adjust to call
bdd_dict::is_registered_accepting_variable.
* src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state,
tgba_explicit::complement_all_accepting_conditions): New methods.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt
and tbalbtt.
(tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove.
* src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t".
* src/tgbatest/ltl2tgba.cc: Implement the -f and -F options.
* src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of
"spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add
also check the ltl2tgba_fm translator.
* wrap/python/spot.i: Wrap ltl2tgba_fm.
* wrap/python/cgi/ltl2tgba.in: Add radio buttons to select
between ltl2tgba and ltl2tgba_fm.
* wrap/python/tests/ltl2tgba.py: Add support for the -f option.
* wrap/python/tests/ltl2tgba.test: Try the -f option.
varnum can be augmented by other allocator. Keep track
of a local varnum (lvarnum) in each allocator.
* src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize
lvarnum.
(bdd_allocator::extvarnum): New method.
(bdd_allocator::allocate_variables): Use lvarnum and extvarnum.
* src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod.
(bdd_allocator::lvarnum): New variable.
2003-08-14 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/statebdd.cc:
......
......@@ -161,30 +161,33 @@ namespace spot
}
bool
bdd_dict::is_registered(const ltl::formula* f, const void* by_me)
bdd_dict::is_registered_proposition(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;
if (fi == var_map.end())
return false;
ref_set& s = var_refs[fi->second];
return s.find(by_me) != s.end();
}
else
{
fi = now_map.find(f);
if (fi != now_map.end())
bool
bdd_dict::is_registered_state(const ltl::formula* f, const void* by_me)
{
var = fi->second;
fv_map::iterator fi = now_map.find(f);
if (fi == now_map.end())
return false;
ref_set& s = var_refs[fi->second];
return s.find(by_me) != s.end();
}
else
bool
bdd_dict::is_registered_accepting_variable(const ltl::formula* f,
const void* by_me)
{
fi = acc_map.find(f);
fv_map::iterator fi = acc_map.find(f);
if (fi == acc_map.end())
return false;
var = fi->second;
}
}
ref_set& s = var_refs[var];
ref_set& s = var_refs[fi->second];
return s.find(by_me) != s.end();
}
......
......@@ -91,8 +91,13 @@ namespace spot
/// 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);
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_accepting_variable(const ltl::formula* f,
const void* by_me);
/// @}
/// \brief Dump all variables for debugging.
/// \param os The output stream.
......
......@@ -111,6 +111,7 @@ namespace spot
state_name_map_[s] = name;
// The first state we add is the inititial state.
// It can also be overridden with set_init_state().
if (! init_)
init_ = s;
......@@ -119,6 +120,14 @@ namespace spot
return i->second;
}
void
tgba_explicit::set_init_state(const std::string& state)
{
tgba_explicit::state* s = add_state(state);
init_ = s;
}
tgba_explicit::transition*
tgba_explicit::create_transition(const std::string& source,
const std::string& dest)
......@@ -159,13 +168,40 @@ namespace spot
{
int v = dict_->register_accepting_variable(f, this);
ltl::destroy(f);
neg_accepting_conditions_ &= bdd_nithvar(v);
bdd neg = bdd_nithvar(v);
neg_accepting_conditions_ &= neg;
// Append neg to all acceptance conditions.
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->accepting_conditions &= neg;
}
all_accepting_conditions_computed_ = false;
}
void
tgba_explicit::complement_all_accepting_conditions()
{
bdd all = all_accepting_conditions();
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
(*i2)->accepting_conditions = all - (*i2)->accepting_conditions;
}
}
}
bool
tgba_explicit::has_accepting_condition(ltl::formula* f) const
{
return dict_->is_registered(f, this);
return dict_->is_registered_accepting_variable(f, this);
}
bdd
......@@ -185,6 +221,9 @@ namespace spot
assert(0);
}
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(has_accepting_condition(f));
/* If this second assert fails and the first doesn't,
things are badly broken. This has already happened. */
assert(i != dict_->acc_map.end());
ltl::destroy(f);
bdd v = bdd_ithvar(i->second);
......
......@@ -29,6 +29,8 @@ namespace spot
state* dest;
};
void set_init_state(const std::string& state);
transition*
create_transition(const std::string& source, const std::string& dest);
......@@ -37,6 +39,7 @@ namespace spot
void declare_accepting_condition(ltl::formula* f);
bool has_accepting_condition(ltl::formula* f) const;
void add_accepting_condition(transition* t, ltl::formula* f);
void complement_all_accepting_conditions();
// tgba interface
virtual ~tgba_explicit();
......
......@@ -8,6 +8,7 @@ tgbaalgos_HEADERS = \
dotty.hh \
lbtt.hh \
ltl2tgba.hh \
ltl2tgba_fm.hh \
magic.hh \
save.hh
......@@ -17,5 +18,6 @@ libtgbaalgos_la_SOURCES = \
dotty.cc \
lbtt.cc \
ltl2tgba.cc \
ltl2tgba_fm.cc \
magic.cc \
save.cc
......@@ -7,6 +7,23 @@
namespace spot
{
/// Build a spot::tgba_bdd_concrete from an LTL formula.
///
/// This is based on the following paper.
/// \verbatim
/// @InProceedings{ couvreur.00.lacim,
/// author = {Jean-Michel Couvreur},
/// title = {Un point de vue symbolique sur la logique temporelle
/// lin{\'e}aire},
/// booktitle = {Actes du Colloque LaCIM 2000},
/// month = {August},
/// year = {2000},
/// pages = {131--140},
/// volume = {27},
/// series = {Publications du LaCIM},
/// publisher = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al},
/// editor = {Pierre Leroux}
/// }
/// \endverbatim
tgba_bdd_concrete* ltl_to_tgba(const ltl::formula* f, bdd_dict* dict);
}
......
#include "misc/bddalloc.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh"
#include "ltlvisit/destroy.hh"
#include "ltlvisit/tostring.hh"
#include <cassert>
#include "tgba/tgbabddconcretefactory.hh"
#include "ltl2tgba_fm.hh"
namespace spot
{
using namespace ltl;
namespace
{
// Helper dictionary. We represent formula using a BDD to simplify
// them, and them translate the BDD back into formulae.
//
// The name of the variables are inspired from Couvreur's FM paper.
// "a" variables are promises (written "a" in the paper)
// "next" variables are X's operands (the "r_X" variables from the paper)
// "var" variables are atomic propositions.
class translate_dict: public bdd_allocator
{
public:
translate_dict()
: bdd_allocator(),
a_set(bddtrue),
var_set(bddtrue),
next_set(bddtrue)
{
}
~translate_dict()
{
fv_map::iterator i;
for (i = a_map.begin(); i != a_map.end(); ++i)
ltl::destroy(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::destroy(i->first);
for (i = next_map.begin(); i != next_map.end(); ++i)
ltl::destroy(i->first);
}
/// 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 a_map; ///< Maps formulae to "a" BDD variables
vf_map a_formula_map; ///< Maps "a" 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 next_map; ///< Maps "Next" variables to BDD variables
vf_map next_formula_map; ///< Maps BDD variables to "Next" variables
bdd a_set;
bdd var_set;
bdd next_set;
int
register_proposition(const ltl::formula* f)
{
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_set &= bdd_ithvar(num);
return num;
}
int
register_a_variable(const ltl::formula* f)
{
int num;
// Do not build an accepting variable that already exists.
fv_map::iterator sii = a_map.find(f);
if (sii != a_map.end())
{
num = sii->second;
}
else
{
f = clone(f);
num = allocate_variables(1);
a_map[f] = num;
a_formula_map[num] = f;
}
a_set &= bdd_ithvar(num);
return num;
}
int
register_next_variable(const ltl::formula* f)
{
int num;
// Do not build a Next variable that already exists.
fv_map::iterator sii = next_map.find(f);
if (sii != next_map.end())
{
num = sii->second;
}
else
{
f = clone(f);
num = allocate_variables(1);
next_map[f] = num;
next_formula_map[num] = f;
}
next_set &= bdd_ithvar(num);
return num;
}
std::ostream&
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 << ": ";
to_string(fi->first, os) << std::endl;
}
os << "a Variables:" << std::endl;
for (fi = a_map.begin(); fi != a_map.end(); ++fi)
{
os << " " << fi->second << ": a[";
to_string(fi->first, os) << "]" << std::endl;
}
os << "Next Variables:" << std::endl;
for (fi = next_map.begin(); fi != next_map.end(); ++fi)
{
os << " " << fi->second << ": Next[";
to_string(fi->first, os) << "]" << std::endl;
}
return os;
}
ltl::formula*
var_to_formula(int var) const
{
vf_map::const_iterator isi = next_formula_map.find(var);
if (isi != next_formula_map.end())
return ltl::clone(isi->second);
isi = a_formula_map.find(var);
if (isi != a_formula_map.end())
return ltl::clone(isi->second);
isi = var_formula_map.find(var);
if (isi != var_formula_map.end())
return ltl::clone(isi->second);
assert(0);
}
ltl::formula*
conj_bdd_to_formula(bdd b)
{
if (b == bddfalse)
return ltl::constant::false_instance();
ltl::multop::vec* v = new ltl::multop::vec;
while (b != bddtrue)
{
int var = bdd_var(b);
ltl::formula* res = var_to_formula(var);
bdd high = bdd_high(b);
if (high == bddfalse)
{
res = ltl::unop::instance(ltl::unop::Not, res);
b = bdd_low(b);
}
else
{
b = high;
}
assert(b != bddfalse);
v->push_back(res);
}
return ltl::multop::instance(ltl::multop::And, v);
}
void
conj_bdd_to_atomic_props(tgba_explicit* a, bdd b,
tgba_explicit::transition* t)
{
assert(b != bddfalse);
while (b != bddtrue)
{
int var = bdd_var(b);
ltl::formula* ap = var_to_formula(var);
bdd high = bdd_high(b);
if (high == bddfalse)
{
a->add_neg_condition(t, ap);
b = bdd_low(b);
}
else
{
a->add_condition(t, ap);
b = high;
}
assert(b != bddfalse);
}
}
void
conj_bdd_to_acc(tgba_explicit* a, bdd b, tgba_explicit::transition* t)
{
assert(b != bddfalse);
while (b != bddtrue)
{
int var = bdd_var(b);
bdd high = bdd_high(b);
if (high == bddfalse)
{
// Simply ignore negated accepting variables.
b = bdd_low(b);
}
else
{
ltl::formula* ac = var_to_formula(var);
if (! a->has_accepting_condition(ac))
a->declare_accepting_condition(ltl::clone(ac));
a->add_accepting_condition(t, ac);
ltl::atomic_prop::instance_count();
b = high;
}
assert(b != bddfalse);
}
}
};
// The rewrite rules used here are adapted from Jean-Michel
// Couvreur's FM paper.
class ltl_trad_visitor: public const_visitor
{
public:
ltl_trad_visitor(translate_dict& dict)
: dict_(dict)
{
}
virtual
~ltl_trad_visitor()
{
}
bdd result() const
{
return res_;
}
void
visit(const atomic_prop* node)
{
res_ = bdd_ithvar(dict_.register_proposition(node));
}
void
visit(const constant* node)
{
switch (node->val())
{
case constant::True:
res_ = bddtrue;
return;
case constant::False:
res_ = bddfalse;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const unop* node)
{
switch (node->op())
{
case unop::F:
{
// r(Fy) = r(y) + a(y)r(XFy)
bdd y = recurse(node->child());
int a = dict_.register_a_variable(node);
int x = dict_.register_next_variable(node);
res_ = y | (bdd_ithvar(a) & bdd_ithvar(x));
return;
}
case unop::G:
{
// r(Gy) = r(y)r(XGy)
bdd y = recurse(node->child());
int x = dict_.register_next_variable(node);
res_ = y & bdd_ithvar(x);
return;
}
case unop::Not:
{
res_ = bdd_not(recurse(node->child()));
return;
}
case unop::X:
{
int x = dict_.register_next_variable(node->child());
res_ = bdd_ithvar(x);
return;
}
}
/* Unreachable code. */
assert(0);
}
void
visit(const binop* node)
{
bdd f1 = recurse(node->first());
bdd f2 = recurse(node->second());
switch (node->op())
{
case binop::Xor:
res_ = bdd_apply(f1, f2, bddop_xor);
return;
case binop::Implies:
res_ = bdd_apply(f1, f2, bddop_imp);
return;
case binop::Equiv:
res_ = bdd_apply(f1, f2, bddop_biimp);
return;
case binop::U:
{
// r(f1 U f2) = r(f2) + a(f2)r(f1)r(X(f1 U f2))
int a = dict_.register_a_variable(node->second());
int x = dict_.register_next_variable(node);
res_ = f2 | (bdd_ithvar(a) & f1 & bdd_ithvar(x));
return;
}
case binop::R:
{
// r(f1 R f2) = r(f1)r(f2) + r(f2)r(X(f1 U f2))
int x = dict_.register_next_variable(node);
res_ = (f1 & f2) | (f2 & bdd_ithvar(x));
return;
}
}
/* Unreachable code. */
assert(0);
}
void
visit(const multop* node)
{
int op = -1;
switch (node->op())
{
case multop::And:
op = bddop_and;