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

More LTL reductions for W and M.

Browse source 
* src/ltlvisit/basicreduce.cc: Perform the following reductions:
(a U b) & (c W b) = (a & c) U b
(a W b) & (c W b) = (a & c) W b
(a R b) | (c M b) = (a | c) R b
(a M b) | (c M b) = (a | c) M b
* src/ltltest/reduccmp.test: Test them.
This commit is contained in:
Alexandre Duret-Lutz 2010-04-12 15:26:48 +02:00
parent f003c3d16f
commit e6809b8c66
3 changed files with 42 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
More LTL reductions for W and M.
* src/ltlvisit/basicreduce.cc: Perform the following reductions:
(a U b) & (c W b) = (a & c) U b
(a W b) & (c W b) = (a & c) W b
(a R b) | (c M b) = (a | c) R b
(a M b) | (c M b) = (a | c) M b
* src/ltltest/reduccmp.test: Test them.
2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add LTL reductions for strong release.

5
src/ltltest/reduccmp.test
View file

@ -125,6 +125,11 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'a R (F(a))' 'Fa'
run 0 $x '(a R b) & (a M c)' 'a M (b & c)'
run 0 $x '(a R b) & Fa' 'a M b'
run 0 $x '(a U b) & (c W b)' '(a & c) U b'
run 0 $x '(a W b) & (c W b)' '(a & c) W b'
run 0 $x '(a R b) | (c M b)' '(a | c) R b'
run 0 $x '(a M b) | (c M b)' '(a | c) M b'
;;
esac

41
src/ltlvisit/basicreduce.cc
View file

@ -495,22 +495,27 @@ namespace spot
}
else if (bo)
{
if (bo->op() == binop::U)
if (bo->op() == binop::U || bo->op() == binop::W)
{
// (a U b) & (c U b) = (a & c) U b
// (a U b) & (c W b) = (a & c) U b
// (a W b) & (c W b) = (a & c) W b
bool weak = true;
formula* ftmp = dynamic_cast<binop*>(*i)->second();
multop::vec* tmpUright = new multop::vec;
multop::vec* right = new multop::vec;
for (multop::vec::iterator j = i; j != res->end();
j++)
{
if (!*j)
continue;
binop* bo2 = dynamic_cast<binop*>(*j);
if (bo2 && bo2->op() == binop::U
if (bo2 && (bo2->op() == binop::U
|| bo2->op() == binop::W)
&& ftmp == bo2->second())
{
tmpUright
->push_back(bo2->first()->clone());
if (bo2->op() == binop::U)
weak = false;
right->push_back(bo2->first()->clone());
if (j != i)
{
(*j)->destroy();
@ -519,11 +524,11 @@ namespace spot
}
}
tmpU
->push_back(binop::instance(binop::U,
->push_back(binop::instance(weak ?
binop::W : binop::U,
multop::
instance(multop::
And,
tmpUright),
And, right),
ftmp->clone()));
}
else if (bo->op() == binop::R || bo->op() == binop::M)
@ -690,22 +695,27 @@ namespace spot
instance(multop::Or,
right)));
}
else if (bo->op() == binop::R)
else if (bo->op() == binop::R || bo->op() == binop::M)
{
// (a R b) | (c R b) = (a | c) R b
// (a R b) | (c M b) = (a | c) R b
// (a M b) | (c M b) = (a | c) M b
bool weak = false;
formula* ftmp = dynamic_cast<binop*>(*i)->second();
multop::vec* tmpRright = new multop::vec;
multop::vec* right = new multop::vec;
for (multop::vec::iterator j = i; j != res->end();
j++)
{
if (!*j)
continue;
binop* bo2 = dynamic_cast<binop*>(*j);
if (bo2 && bo2->op() == binop::R
if (bo2 && (bo2->op() == binop::R
|| bo2->op() == binop::M)
&& ftmp == bo2->second())
{
tmpRright
->push_back(bo2->first()->clone());
if (bo2->op() == binop::R)
weak = true;
right->push_back(bo2->first()->clone());
if (j != i)
{
(*j)->destroy();
@ -714,10 +724,11 @@ namespace spot
}
}
tmpR
->push_back(binop::instance(binop::R,
->push_back(binop::instance(weak ?
binop::R : binop::M,
multop::
instance(multop::Or,
tmpRright),
right),
ftmp->clone()));
}
else