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

Disable LTL reductions on SERE formulae.

Browse source 
* src/ltlvisit/contain.cc (recurse, reduce_tau03): Do not
run on non-PSL formulae.
* src/ltlvisit/reduce.cc (reduce_visitor::visit): Skip
multop::Fusion operators, and do not run syntactic_implication_neg
on SERE formulae.
* src/ltlvisit/syntimpl.cc (inf_right_recurse_visitor::visit):
Skip [*0].
This commit is contained in:
Alexandre Duret-Lutz 2011-02-20 17:15:37 +01:00
parent 459921ef60
commit 6e6b6b1e01
3 changed files with 36 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ltlvisit/contain.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -30,6 +30,7 @@
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/save.hh"
namespace spot
{
namespace ltl
@ -381,6 +382,9 @@ namespace spot
formula*
recurse(formula* f)
{
if (!f->is_psl_formula())
return f->clone();
reduce_tau03_visitor v(stronger, lcc);
const_cast<formula*>(f)->accept(v);
return v.result();
@ -391,6 +395,9 @@ namespace spot
formula*
reduce_tau03(const formula* f, bool stronger)
{
if (!f->is_psl_formula())
return f->clone();
bdd_dict b;
reduce_tau03_visitor v(stronger,
new language_containment_checker(&b,

46
src/ltlvisit/reduce.cc
View file

@ -325,7 +325,8 @@ namespace spot
res->push_back(recurse(mo->nth(i)));
if ((opt_ & Reduce_Syntactic_Implications)
&& (mo->op() != multop::Concat))
&& (mo->op() != multop::Concat)
&& (mo->op() != multop::Fusion))
{
bool removed = true;
@ -369,25 +370,30 @@ namespace spot
}
}
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (f1 = res->begin(); f1 != res->end(); f1++)
for (f2 = res->begin(); f2 != res->end(); f2++)
if (f1 != f2 &&
c_->syntactic_implication_neg(*f1, *f2,
mo->op() != multop::Or))
{
for (multop::vec::iterator j = res->begin();
j != res->end(); j++)
(*j)->destroy();
res->clear();
delete res;
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
return;
}
// We cannot run syntactic_implication_neg on SERE
// formulae, unless they are just Boolean formulae.
if (mo->is_boolean() || !mo->is_sere_formula())
{
bool is_and = mo->op() != multop::Or;
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (f1 = res->begin(); f1 != res->end(); f1++)
for (f2 = res->begin(); f2 != res->end(); f2++)
if (f1 != f2 &&
c_->syntactic_implication_neg(*f1, *f2, is_and))
{
for (multop::vec::iterator j = res->begin();
j != res->end(); j++)
(*j)->destroy();
res->clear();
delete res;
if (is_and)
result_ = constant::false_instance();
else
result_ = constant::true_instance();
return;
}
}
}

4
src/ltlvisit/syntimpl.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -76,7 +76,7 @@ namespace spot
result_ = false;
return;
case constant::EmptyWord:
result_ = true;
result_ = false;
}
}