* iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc,
src/ltlvisit/dump.cc, src/ltlvisit/length.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
Declare private classes and helper function in anonymous namespaces.
* HACKING, src/sanity/style.test: Document and check this.
Also check for trailing { after namespace or class.
* src/ltlast/predecl.hh, src/ltlast/visitor.hh,
src/tgba/tgbareduc.hh: Fix trailing {.
This commit is contained in:
Alexandre Duret-Lutz
parent
5176caf4d2
commit
7d27fd3796
28 changed files with 3128 additions and 3025 deletions
|
|
@ -31,225 +31,228 @@
|
|||
|
||||
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
|
||||
namespace
|
||||
{
|
||||
public:
|
||||
ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
|
||||
: fact_(fact), root_(root)
|
||||
{
|
||||
}
|
||||
using namespace ltl;
|
||||
|
||||
virtual
|
||||
~ltl_trad_visitor()
|
||||
/// \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:
|
||||
ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
|
||||
: fact_(fact), root_(root)
|
||||
{
|
||||
}
|
||||
|
||||
bdd
|
||||
result()
|
||||
{
|
||||
return res_;
|
||||
}
|
||||
virtual
|
||||
~ltl_trad_visitor()
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
visit(const atomic_prop* node)
|
||||
{
|
||||
res_ = bdd_ithvar(fact_.create_atomic_prop(node));
|
||||
}
|
||||
bdd
|
||||
result()
|
||||
{
|
||||
return res_;
|
||||
}
|
||||
|
||||
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 atomic_prop* node)
|
||||
{
|
||||
res_ = bdd_ithvar(fact_.create_atomic_prop(node));
|
||||
}
|
||||
|
||||
void
|
||||
visit(const unop* node)
|
||||
{
|
||||
switch (node->op())
|
||||
{
|
||||
case unop::F:
|
||||
void
|
||||
visit(const constant* node)
|
||||
{
|
||||
switch (node->val())
|
||||
{
|
||||
/*
|
||||
Fx <=> x | XFx
|
||||
In other words:
|
||||
now <=> x | next
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
bdd x = recurse(node->child());
|
||||
fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp));
|
||||
/*
|
||||
`x | next', doesn't actually encode the fact that x
|
||||
should be fulfilled eventually. We ensure this by
|
||||
creating a new generalized Büchi acceptance set, Acc[x],
|
||||
and leave out of this set any transition going off NOW
|
||||
without checking X. Such acceptance conditions are
|
||||
checked for during the emptiness check.
|
||||
*/
|
||||
fact_.declare_acceptance_condition(x | !now, node->child());
|
||||
res_ = now;
|
||||
case constant::True:
|
||||
res_ = bddtrue;
|
||||
return;
|
||||
case constant::False:
|
||||
res_ = bddfalse;
|
||||
return;
|
||||
}
|
||||
case unop::G:
|
||||
{
|
||||
bdd child = recurse(node->child());
|
||||
// If G occurs at the top of the formula we don't
|
||||
// need Now/Next variables. We just constrain
|
||||
// the relation so that the child always happens.
|
||||
// This saves 2 BDD variables.
|
||||
if (root_)
|
||||
{
|
||||
fact_.constrain_relation(child);
|
||||
res_ = child;
|
||||
return;
|
||||
}
|
||||
// Gx <=> x && XGx
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, child & next,
|
||||
bddop_biimp));
|
||||
res_ = now;
|
||||
return;
|
||||
}
|
||||
case unop::Not:
|
||||
{
|
||||
res_ = bdd_not(recurse(node->child()));
|
||||
return;
|
||||
}
|
||||
case unop::X:
|
||||
{
|
||||
int v = fact_.create_state(node->child());
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, recurse(node->child()),
|
||||
bddop_biimp));
|
||||
res_ = next;
|
||||
return;
|
||||
}
|
||||
}
|
||||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
/* 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:
|
||||
void
|
||||
visit(const unop* node)
|
||||
{
|
||||
switch (node->op())
|
||||
{
|
||||
/*
|
||||
f1 U f2 <=> f2 | (f1 & X(f1 U f2))
|
||||
In other words:
|
||||
now <=> f2 | (f1 & next)
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
|
||||
bddop_biimp));
|
||||
/*
|
||||
The rightmost conjunction, f1 & next, doesn't actually
|
||||
encode the fact that f2 should be fulfilled eventually.
|
||||
We declare an acceptance condition for this purpose (see
|
||||
the comment in the unop::F case).
|
||||
*/
|
||||
fact_.declare_acceptance_condition(f2 | !now, node->second());
|
||||
res_ = now;
|
||||
return;
|
||||
case unop::F:
|
||||
{
|
||||
/*
|
||||
Fx <=> x | XFx
|
||||
In other words:
|
||||
now <=> x | next
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
bdd x = recurse(node->child());
|
||||
fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp));
|
||||
/*
|
||||
`x | next', doesn't actually encode the fact that x
|
||||
should be fulfilled eventually. We ensure this by
|
||||
creating a new generalized Büchi acceptance set, Acc[x],
|
||||
and leave out of this set any transition going off NOW
|
||||
without checking X. Such acceptance conditions are
|
||||
checked for during the emptiness check.
|
||||
*/
|
||||
fact_.declare_acceptance_condition(x | !now, node->child());
|
||||
res_ = now;
|
||||
return;
|
||||
}
|
||||
case unop::G:
|
||||
{
|
||||
bdd child = recurse(node->child());
|
||||
// If G occurs at the top of the formula we don't
|
||||
// need Now/Next variables. We just constrain
|
||||
// the relation so that the child always happens.
|
||||
// This saves 2 BDD variables.
|
||||
if (root_)
|
||||
{
|
||||
fact_.constrain_relation(child);
|
||||
res_ = child;
|
||||
return;
|
||||
}
|
||||
// Gx <=> x && XGx
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, child & next,
|
||||
bddop_biimp));
|
||||
res_ = now;
|
||||
return;
|
||||
}
|
||||
case unop::Not:
|
||||
{
|
||||
res_ = bdd_not(recurse(node->child()));
|
||||
return;
|
||||
}
|
||||
case unop::X:
|
||||
{
|
||||
int v = fact_.create_state(node->child());
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, recurse(node->child()),
|
||||
bddop_biimp));
|
||||
res_ = next;
|
||||
return;
|
||||
}
|
||||
}
|
||||
case binop::R:
|
||||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
void
|
||||
visit(const binop* node)
|
||||
{
|
||||
bdd f1 = recurse(node->first());
|
||||
bdd f2 = recurse(node->second());
|
||||
|
||||
switch (node->op())
|
||||
{
|
||||
/*
|
||||
f1 R f2 <=> f2 & (f1 | X(f1 R f2))
|
||||
In other words:
|
||||
now <=> f2 & (f1 | next)
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
|
||||
bddop_biimp));
|
||||
res_ = now;
|
||||
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:
|
||||
{
|
||||
/*
|
||||
f1 U f2 <=> f2 | (f1 & X(f1 U f2))
|
||||
In other words:
|
||||
now <=> f2 | (f1 & next)
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
|
||||
bddop_biimp));
|
||||
/*
|
||||
The rightmost conjunction, f1 & next, doesn't actually
|
||||
encode the fact that f2 should be fulfilled eventually.
|
||||
We declare an acceptance condition for this purpose (see
|
||||
the comment in the unop::F case).
|
||||
*/
|
||||
fact_.declare_acceptance_condition(f2 | !now, node->second());
|
||||
res_ = now;
|
||||
return;
|
||||
}
|
||||
case binop::R:
|
||||
{
|
||||
/*
|
||||
f1 R f2 <=> f2 & (f1 | X(f1 R f2))
|
||||
In other words:
|
||||
now <=> f2 & (f1 | next)
|
||||
*/
|
||||
int v = fact_.create_state(node);
|
||||
bdd now = bdd_ithvar(v);
|
||||
bdd next = bdd_ithvar(v + 1);
|
||||
fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
|
||||
bddop_biimp));
|
||||
res_ = now;
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
void
|
||||
visit(const multop* node)
|
||||
{
|
||||
int op = -1;
|
||||
bool root = false;
|
||||
switch (node->op())
|
||||
{
|
||||
case multop::And:
|
||||
op = bddop_and;
|
||||
res_ = bddtrue;
|
||||
// When the root formula is a conjunction it's ok to
|
||||
// consider all children as root formulae. This allows the
|
||||
// root-G trick to save many more variable. (See the
|
||||
// translation of G.)
|
||||
root = root_;
|
||||
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), root), op);
|
||||
}
|
||||
}
|
||||
void
|
||||
visit(const multop* node)
|
||||
{
|
||||
int op = -1;
|
||||
bool root = false;
|
||||
switch (node->op())
|
||||
{
|
||||
case multop::And:
|
||||
op = bddop_and;
|
||||
res_ = bddtrue;
|
||||
// When the root formula is a conjunction it's ok to
|
||||
// consider all children as root formulae. This allows the
|
||||
// root-G trick to save many more variable. (See the
|
||||
// translation of G.)
|
||||
root = root_;
|
||||
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), root), op);
|
||||
}
|
||||
}
|
||||
|
||||
bdd
|
||||
recurse(const formula* f, bool root = false)
|
||||
{
|
||||
ltl_trad_visitor v(fact_, root);
|
||||
f->accept(v);
|
||||
return v.result();
|
||||
}
|
||||
bdd
|
||||
recurse(const formula* f, bool root = false)
|
||||
{
|
||||
ltl_trad_visitor v(fact_, root);
|
||||
f->accept(v);
|
||||
return v.result();
|
||||
}
|
||||
|
||||
private:
|
||||
bdd res_;
|
||||
tgba_bdd_concrete_factory& fact_;
|
||||
bool root_;
|
||||
};
|
||||
private:
|
||||
bdd res_;
|
||||
tgba_bdd_concrete_factory& fact_;
|
||||
bool root_;
|
||||
};
|
||||
} // anonymous
|
||||
|
||||
tgba_bdd_concrete*
|
||||
ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue