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

* src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition):

Do not treat true and false specially.  Otherwise it breaks
translation of F(false).
* src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not
use true as acceptance condition.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as
acceptance condition for Fb, not Acc[Fb].

After this change, degeneralized automata are 40% smaller
parent 440029c1
2004-01-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
After this changes, degeneralized automata are 40% smaller
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition):
Do not treat true and false specially. Otherwise it breaks
translation of F(false).
* src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not
use true as acceptance condition.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as
acceptance condition for Fb, not Acc[Fb].
After this change, degeneralized automata are 40% smaller
in LBTT's statistics.
* src/tgba/tgbatba.cc (state_tba_proxy): Store an iterator,
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
......@@ -260,19 +260,6 @@ namespace spot
bdd
tgba_explicit::get_acceptance_condition(const ltl::formula* f)
{
const ltl::constant* c = dynamic_cast<const ltl::constant*>(f);
if (c)
{
switch (c->val())
{
case ltl::constant::True:
return bddtrue;
case ltl::constant::False:
return bddfalse;
}
/* Unreachable code. */
assert(0);
}
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(has_acceptance_condition(f));
/* If this second assert fails and the first doesn't,
......
......@@ -312,8 +312,9 @@ namespace spot
case unop::F:
{
// r(Fy) = r(y) + a(y)r(XFy)
bdd y = recurse(node->child());
int a = dict_.register_a_variable(node);
const formula* child = node->child();
bdd y = recurse(child);
int a = dict_.register_a_variable(child);
int x = dict_.register_next_variable(node);
res_ = y | (bdd_ithvar(a) & bdd_ithvar(x));
return;
......
......@@ -27,10 +27,10 @@ set -e
cat >input1 <<EOF
acc = p1;
s1, s3, "a", true;
s1, s3, "a", p1;
s1, s2, "b", p1;
s2, s1, "!a", true;
s2, s3, "c", true;
s2, s1, "!a", p1;
s2, s3, "c", p1;
EOF
cat >input2 <<EOF
......
......@@ -27,9 +27,9 @@ set -e
cat >input1 <<EOF
acc = p1;
s1, s3, "a", true;
s1, s3, "a", p1;
s1, s2, "b", p1;
s2, s1, "!a", true;
s2, s1, "!a", p1;
s2, s3, "c",;
EOF
......
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