alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Fix translation of '{(c&!c)[->0..1]}!'.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
the translation of the Goto operator.
(ratexp_trad_visitor::next_to_concat): More comments.
* src/ltltest/reduccmp.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2011-10-30 18:34:49 +01:00
parent 1507dbc63a
commit 58bbaa0859
2 changed files with 52 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ltltest/reduccmp.test
View file

@ -187,6 +187,10 @@ for x in ../reduccmp ../reductaustr; do
# F comes in front when possible...
run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)'
run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)'
# Because reduccmp will translate the formula,
# this also check for an old bug in ltl2tgba_fm.
run 0 $x '{(c&!c)[->0..1]}!' '0'
;;
esac

55
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -326,6 +326,14 @@ namespace spot
bdd next_to_concat()
{
// Encoding X[*0] when there is nothing to concatenate is a
// way to ensure that we distinguish the rational formula "a"
// (encoded as "a&X[*0]") from the rational formula "a;[*]"
// (encoded as "a&X[*]").
//
// It's important that when we do "a && (a;[*])" we do not get
// "a;[*]" as it would occur if we had simply encoded "a" as
// "a".
if (!to_concat_)
to_concat_ = constant::empty_word_instance();
int x = dict_.register_next_variable(to_concat_);
@ -493,18 +501,11 @@ namespace spot
}
return;
case bunop::Equal:
case bunop::Goto:
{
// b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1])
// b[=0..max] == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1])
// Note: b[=0] == (!b)[*] is a trivial identity, so it will
// never occur here.
// b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1])
// b[->0..max] == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1])
// Note: b[->0] == [*0] is a trivial identity, so it will
// never occur here.
formula* f1 = // !b;b[=min..max] or !b;b[->min..max]
multop::instance(multop::Concat,
unop::instance(unop::Not,
@ -524,6 +525,46 @@ namespace spot
res_ |= now_to_concat();
return;
}
case bunop::Goto:
{
// It is important to understand why we do not define Goto
// similarly to equal, i.e.:
//
// b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1])
// b[->0..max] == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1])
// Note: b[->0] == [*0] is a trivial identity, so it will
// never occur here.
//
// The above would be wrong when min=0.
// For instance consider {(c&!c)[->0..1]}<>->1
// This formula is equivalent to {[*0]}<>->1 which is false.
// However with above above rewritings, we get
// {[*0] | !(c&!c);(c&!c)[->0..1] | (c&!c);(c&!c)[->0] }<>->1
// which is equivalent to { 1;[*0] }<>-> 1 which is true. Oops!
//
// We therefore use the following rules instead:
// b[->min..max] == (!b)[*];b;b[->min-1..max-1]
// b[->0..max] == [*0] | (!b)[*];b;b[->min-1..max-1]
formula* f1 = // (!b)[*]
bunop::instance(bunop::Star,
unop::instance(unop::Not,
bo->child()->clone()),
0, bunop::unbounded);
formula* f2 = // b;b[->min-1..max-1]
multop::instance(multop::Concat,
bo->child()->clone(),
bunop::instance(op,
bo->child()->clone(),
min2, max2));
f = multop::instance(multop::Concat, f1, f2);
res_ = recurse_and_concat(f);
f->destroy();
if (min == 0)
res_ |= now_to_concat();
return;
}
}
/* Unreachable code. */
assert(0);