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

Explicit automata can now have arbitrary logic formula on their

arcs.  ltl2tgba_fm benefits from this and join multiple arcs with
the same destination and acceptance conditions.
* src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula,
bdd_format_formula): New functions.
* src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition,
tgba_explicit::add_condition, tgba_explicit::add_neg_condition,
tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition,
tgba_explicit::get_accepting_condition,
tgba_explicit::add_accepting_condition): Take a const formula*.
* src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition):
Rewrite using formula_to_bdd.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use
bdd_print_formula to display conditions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Likewise.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula):
New function.
(translate_dict::conj_bdd_to_atomic_props): Remove.
(ltl_to_tgba_fm): Factor successors on accepting conditions
and destinations, not conditions.  Use bdd_to_formula to translate
the conditions.
* src/tgbaparse/tgbaparse.yy: Expect conditions as a formula
in a string, call the LTL parser for this.
* src/tgbaparse/tgbascan.ll: Process " and \ escapes in
strings.
* src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust to new syntax for explicit
automata.
parent 3126e49b
2003-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
Explicit automata can now have arbitrary logic formula on their
arcs. ltl2tgba_fm benefits from this and join multiple arcs with
the same destination and acceptance conditions.
* src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula,
bdd_format_formula): New functions.
* src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition,
tgba_explicit::add_condition, tgba_explicit::add_neg_condition,
tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition,
tgba_explicit::get_accepting_condition,
tgba_explicit::add_accepting_condition): Take a const formula*.
* src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition):
Rewrite using formula_to_bdd.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use
bdd_print_formula to display conditions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Likewise.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula):
New function.
(translate_dict::conj_bdd_to_atomic_props): Remove.
(ltl_to_tgba_fm): Factor successors on accepting conditions
and destinations, not conditions. Use bdd_to_formula to translate
the conditions.
* src/tgbaparse/tgbaparse.yy: Expect conditions as a formula
in a string, call the LTL parser for this.
* src/tgbaparse/tgbascan.ll: Process \" and \\ escapes in
strings.
* src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust to new syntax for explicit
automata.
* src/misc/minato.hh (minato_isop(bdd,bdd)): New constructor variant.
(minato_isop::local_vars::vars): New attribute.
(minato_isop::local_vars::local_vars): Add the vars arguments.
......
......@@ -27,6 +27,7 @@ tgbadir = $(pkgincludedir)/tgba
tgba_HEADERS = \
bdddict.hh \
bddprint.hh \
formula2bdd.hh \
public.hh \
state.hh \
statebdd.hh \
......@@ -46,6 +47,7 @@ noinst_LTLIBRARIES = libtgba.la
libtgba_la_SOURCES = \
bdddict.cc \
bddprint.cc \
formula2bdd.cc \
statebdd.cc \
succiterconcrete.cc \
tgba.cc \
......
......@@ -23,6 +23,8 @@
#include <cassert>
#include "bddprint.hh"
#include "ltlvisit/tostring.hh"
#include "formula2bdd.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
......@@ -163,6 +165,23 @@ namespace spot
return os.str();
}
std::ostream&
bdd_print_formula(std::ostream& os, const bdd_dict* d, bdd b)
{
const ltl::formula* f = bdd_to_formula(b, d);
to_string(f, os);
destroy(f);
return os;
}
std::string
bdd_format_formula(const bdd_dict* d, bdd b)
{
std::ostringstream os;
bdd_print_formula(os, d, b);
return os.str();
}
std::ostream&
bdd_print_dot(std::ostream& os, const bdd_dict* d, bdd b)
{
......
......@@ -69,6 +69,18 @@ namespace spot
/// \return The BDD formated as a string.
std::string bdd_format_set(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a formula.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream& bdd_print_formula(std::ostream& os,
const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a formula.
/// \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_formula(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.
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "formula2bdd.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include "misc/minato.hh"
#include "ltlvisit/clone.hh"
namespace spot
{
using namespace ltl;
class formula_to_bdd_visitor : public ltl::const_visitor
{
public:
formula_to_bdd_visitor(bdd_dict* d, void* owner)
: d_(d), owner_(owner)
{
}
virtual
~formula_to_bdd_visitor()
{
}
virtual void
visit(const atomic_prop* node)
{
res_ = bdd_ithvar(d_->register_proposition(node, owner_));
}
virtual void
visit(const constant* node)
{
switch (node->val())
{
case constant::True:
res_ = bddtrue;
return;
case constant::False:
res_ = bddfalse;
return;
}
/* Unreachable code. */
assert(0);
}
virtual void
visit(const unop* node)
{
switch (node->op())
{
case unop::F:
case unop::G:
case unop::X:
assert(!"unsupported operator");
case unop::Not:
{
res_ = bdd_not(recurse(node->child()));
return;
}
}
/* Unreachable code. */
assert(0);
}
virtual 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:
case binop::R:
assert(!"unsupported operator");
}
/* Unreachable code. */
assert(0);
}
virtual void
visit(const multop* node)
{
int op = -1;
switch (node->op())
{
case multop::And:
op = bddop_and;
res_ = bddtrue;
break;
case multop::Or:
op = bddop_or;
res_ = bddfalse;
break;
}
assert(op != -1);
unsigned s = node->size();
for (unsigned n = 0; n < s; ++n)
{
res_ = bdd_apply(res_, recurse(node->nth(n)), op);
}
}
bdd
result() const
{
return res_;
}
bdd
recurse(const formula* f) const
{
return formula_to_bdd(f, d_, owner_);
}
private:
bdd_dict* d_;
void* owner_;
bdd res_;
};
bdd
formula_to_bdd(const formula* f, bdd_dict* d, void* for_me)
{
formula_to_bdd_visitor v(d, for_me);
f->accept(v);
return v.result();
}
// Convert a BDD which is known to be a conjonction into a formula.
static ltl::formula*
conj_to_formula(bdd b, const bdd_dict* d)
{
if (b == bddfalse)
return constant::false_instance();
multop::vec* v = new multop::vec;
while (b != bddtrue)
{
int var = bdd_var(b);
bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var);
assert(isi != d->var_formula_map.end());
formula* res = clone(isi->second);
bdd high = bdd_high(b);
if (high == bddfalse)
{
res = unop::instance(unop::Not, res);
b = bdd_low(b);
}
else
{
// If bdd_low is not false, then b was not a conjunction.
assert(bdd_low(b) == bddfalse);
b = high;
}
assert(b != bddfalse);
v->push_back(res);
}
return multop::instance(multop::And, v);
}
const formula*
bdd_to_formula(bdd f, const bdd_dict* d)
{
if (f == bddfalse)
return constant::false_instance();
multop::vec* v = new multop::vec;
minato_isop isop(f);
bdd cube;
while ((cube = isop.next()) != bddfalse)
v->push_back(conj_to_formula(cube, d));
return multop::instance(multop::Or, v);
}
}
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBA_FORMULA2BDD_HH
# define SPOT_TGBA_FORMULA2BDD_HH
# include "bdddict.hh"
# include "ltlast/formula.hh"
namespace spot
{
// \brief Convert a formula into a BDD.
//
// Convert formula \a f into a Bdd, using existing variables from \a
// d, and registering new one as necessary. \a for_me is the
// address to use as owner of the variables used in the BDD.
bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
// Convert a BDD into a formula.
const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
}
#endif // SPOT_TGBA_FORMULA2BDD_HH
......@@ -23,6 +23,7 @@
#include "ltlast/constant.hh"
#include "ltlvisit/destroy.hh"
#include "tgbaexplicit.hh"
#include "tgba/formula2bdd.hh"
#include <cassert>
namespace spot
......@@ -171,22 +172,23 @@ namespace spot
}
bdd
tgba_explicit::get_condition(ltl::formula* f)
tgba_explicit::get_condition(const ltl::formula* f)
{
assert(dynamic_cast<ltl::atomic_prop*>(f));
assert(dynamic_cast<const ltl::atomic_prop*>(f));
int v = dict_->register_proposition(f, this);
ltl::destroy(f);
return bdd_ithvar(v);
}
void
tgba_explicit::add_condition(transition* t, ltl::formula* f)
tgba_explicit::add_condition(transition* t, const ltl::formula* f)
{
t->condition &= get_condition(f);
t->condition &= formula_to_bdd(f, dict_, this);
ltl::destroy(f);
}
void
tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
tgba_explicit::add_neg_condition(transition* t, const ltl::formula* f)
{
t->condition -= get_condition(f);
}
......@@ -199,7 +201,7 @@ namespace spot
}
void
tgba_explicit::declare_accepting_condition(ltl::formula* f)
tgba_explicit::declare_accepting_condition(const ltl::formula* f)
{
int v = dict_->register_accepting_variable(f, this);
ltl::destroy(f);
......@@ -234,15 +236,15 @@ namespace spot
}
bool
tgba_explicit::has_accepting_condition(ltl::formula* f) const
tgba_explicit::has_accepting_condition(const ltl::formula* f) const
{
return dict_->is_registered_accepting_variable(f, this);
}
bdd
tgba_explicit::get_accepting_condition(ltl::formula* f)
tgba_explicit::get_accepting_condition(const ltl::formula* f)
{
ltl::constant* c = dynamic_cast<ltl::constant*>(f);
const ltl::constant* c = dynamic_cast<const ltl::constant*>(f);
if (c)
{
switch (c->val())
......@@ -267,7 +269,7 @@ namespace spot
}
void
tgba_explicit::add_accepting_condition(transition* t, ltl::formula* f)
tgba_explicit::add_accepting_condition(transition* t, const ltl::formula* f)
{
bdd c = get_accepting_condition(f);
t->accepting_conditions |= c;
......
......@@ -55,13 +55,13 @@ namespace spot
transition*
create_transition(const std::string& source, const std::string& dest);
void add_condition(transition* t, ltl::formula* f);
void add_neg_condition(transition* t, ltl::formula* f);
void add_condition(transition* t, const ltl::formula* f);
void add_neg_condition(transition* t, const ltl::formula* f);
/// This assumes that all variables in \a f are known from dict.
void add_conditions(transition* t, bdd f);
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 declare_accepting_condition(const ltl::formula* f);
bool has_accepting_condition(const ltl::formula* f) const;
void add_accepting_condition(transition* t, const ltl::formula* f);
/// This assumes that all accepting conditions in \a f are known from dict.
void add_accepting_conditions(transition* t, bdd f);
void complement_all_accepting_conditions();
......@@ -84,8 +84,8 @@ namespace spot
virtual bdd compute_support_variables(const spot::state* state) const;
state* add_state(const std::string& name);
bdd get_condition(ltl::formula* f);
bdd get_accepting_condition(ltl::formula* f);
bdd get_condition(const ltl::formula* f);
bdd get_accepting_condition(const ltl::formula* f);
typedef Sgi::hash_map<const std::string, tgba_explicit::state*,
string_hash> ns_map;
......
......@@ -60,8 +60,8 @@ namespace spot
process_link(int in, int out, const tgba_succ_iterator* si)
{
os_ << " " << in << " -> " << out << " [label=\"";
bdd_print_set(os_, automata_->get_dict(),
si->current_condition()) << "\\n";
bdd_print_formula(os_, automata_->get_dict(),
si->current_condition()) << "\\n";
bdd_print_set(os_, automata_->get_dict(),
si->current_accepting_conditions()) << "\"]" << std::endl;
}
......
......@@ -208,6 +208,7 @@ namespace spot
}
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
assert(b != bddfalse);
......@@ -216,30 +217,21 @@ namespace spot
return ltl::multop::instance(ltl::multop::And, v);
}
void
conj_bdd_to_atomic_props(tgba_explicit* a, bdd b,
tgba_explicit::transition* t)
const formula*
bdd_to_formula(bdd f)
{
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);
}
}
if (f == bddfalse)
return ltl::constant::false_instance();
multop::vec* v = new multop::vec;
minato_isop isop(f);
bdd cube;
while ((cube = isop.next()) != bddfalse)
v->push_back(conj_bdd_to_formula(cube));
return multop::instance(multop::Or, v);
}
void
conj_bdd_to_acc(tgba_explicit* a, bdd b, tgba_explicit::transition* t)
......@@ -462,7 +454,7 @@ namespace spot
std::string now = to_string(f);
minato_isop isop(res);
minato_isop isop(res, d.next_set & d.a_set);
bdd cube;
while ((cube = isop.next()) != bddfalse)
{
......@@ -473,7 +465,8 @@ namespace spot
tgba_explicit::transition* t = a->create_transition(now, next);
d.conj_bdd_to_atomic_props(a, bdd_existcomp(cube, d.var_set), t);
a->add_condition(t,
d.bdd_to_formula(bdd_existcomp(cube, d.var_set)));
d.conj_bdd_to_acc(a, bdd_existcomp(cube, d.a_set), t);
if (formulae_seen.find(dest) == formulae_seen.end())
......
......@@ -77,8 +77,8 @@ namespace spot
{
state* dest = si->current_state();
os_ << "\"" << cur << "\", \""
<< automata_->format_state(dest) << "\", ";
bdd_print_sat(os_, d, si->current_condition()) << ",";
<< automata_->format_state(dest) << "\", \"";
bdd_print_formula(os_, d, si->current_condition()) << "\",";
bdd_print_acc(os_, d, si->current_accepting_conditions());
os_ << ";" << std::endl;
}
......
......@@ -40,6 +40,7 @@
%{
#include "ltlast/constant.hh"
#include "ltlvisit/destroy.hh"
#include "ltlparse/public.hh"
/* tgbaparse.hh and parsedecl.hh include each other recursively.
We mut ensure that YYSTYPE is declared (by the above %union)
......@@ -55,9 +56,9 @@ using namespace spot::ltl;
typedef std::pair<bool, spot::ltl::formula*> pair;
%}
%token <str> STRING
%token <str> STRING UNTERMINATED_STRING
%token <str> IDENT
%type <str> strident
%type <str> strident string
%type <listp> cond_list
%type <list> acc_list
%token ACC_DEF
......@@ -92,17 +93,37 @@ line: strident ',' strident ',' cond_list ',' acc_list ';'
}
;
strident: STRING | IDENT;
string: STRING
| UNTERMINATED_STRING
{
error_list.push_back(spot::tgba_parse_error(@1,
"unterminated string"));
}
strident: string | IDENT
cond_list:
{
$$ = new std::list<pair>;
}
| cond_list strident
| cond_list string
{
if (*$2 != "")
{
$1->push_back(pair(false, parse_environment.require(*$2)));
parse_error_list pel;
formula* f = spot::ltl::parse(*$2, pel, parse_environment);
for (parse_error_list::iterator i = pel.begin();
i != pel.end(); ++i)
{
// Adjust the diagnostic to the current position.
Location here = @2;
here.begin.line += i->first.begin.line;
here.begin.column += i->first.begin.column;
here.end.line = here.begin.line + i->first.begin.line;
here.end.column = here.begin.column + i->first.begin.column;
error_list.push_back(spot::tgba_parse_error(here, i->second));
}
$1->push_back(pair(false, f));
}
delete $2;
$$ = $1;
......