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

FM: Simplify promises of U, M, and F formulae.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Simplify promises by replacing P(a U b), P(b M a), and P(Fb), by P(b).
This commit is contained in:
Alexandre Duret-Lutz 2012-05-20 12:43:02 +02:00
parent cb068599dc
commit 31b3a22805
1 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -236,6 +236,36 @@ namespace spot
int
register_a_variable(const formula* f)
{
// A promise of 'x', noted P(x) is pretty much like the F(x)
// LTL formula, it ensure that 'x' will be fulfilled (= not
// promised anymore) eventually.
// So a U b = ((a&Pb) W b)
// a U (b U c) = (a&P(b U c)) W (b&P(c) W c)
// the latter encoding may be simplified to
// a U (b U c) = (a&P(c)) W (b&P(c) W c)
//
// Similarly
// a M b = (a R (b&P(a)))
// (a M b) M c = (a R (b & Pa)) R (c & P(a M b))
// = (a R (b & Pa)) R (c & P(a))
// The rules also apply to F:
// P(F(a)) = P(a)
again:
while (const binop* b = is_binop(f))
{
binop::type op = b->op();
if (op == binop::U)
f = b->second();
else if (op == binop::M)
f = b->first();
else
break;
}
if (const unop* u = is_unop(f, unop::F))
{
f = u->child();
goto again;
}
int num = dict->register_acceptance_variable(f, this);
a_set &= bdd_ithvar(num);
return num;