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

* src/ltlvisit/reduce.cc (reduce): Repeat the reduction as

Browse source 
long as the formula changes, it makes more sense when
combining algorithm.  E.g. basic reductions can help language
containment and vice-versa.
This commit is contained in:
Alexandre Duret-Lutz 2007-04-29 08:31:13 +00:00
parent f57097b991
commit 5d8727258d
2 changed files with 52 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2007-04-29 Alexandre Duret-Lutz <adl@gnu.org>
* src/ltlvisit/reduce.cc (reduce): Repeat the reduction as
long as the formula changes, it makes more sense when
combining algorithm. E.g. basic reductions can help language
containment and vice-versa.
2007-04-20 Alexandre Duret-Lutz <adl@gnu.org> 2007-04-20 Alexandre Duret-Lutz <adl@gnu.org>
* src/tgbatest/spotlbtt.test: Disable formula rewriting during * src/tgbatest/spotlbtt.test: Disable formula rewriting during

83
src/ltlvisit/reduce.cc
View file

@ -1,6 +1,6 @@
// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris 6
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // (LIP6), département Systèmes Répartis Coopératifs (SRC),
// et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -296,54 +296,61 @@ namespace spot
{ {
formula* f1; formula* f1;
formula* f2; formula* f2;
formula* prev = 0;
f1 = unabbreviate_logic(f); int n = 0;
f2 = simplify_f_g(f1);
destroy(f1);
f1 = negative_normal_form(f2);
destroy(f2);
f2 = f1;
if (opt & Reduce_Basics) while (f != prev)
{ {
f1 = basic_reduce(f2); ++n;
destroy(f2); assert(n < 100);
f2 = f1; if (prev)
} {
destroy(prev);
if (opt & (Reduce_Syntactic_Implications prev = const_cast<formula*>(f);
| Reduce_Eventuality_And_Universality)) }
{ else
reduce_visitor v(opt); {
f2->accept(v); prev = clone(f);
f1 = v.result(); }
f1 = unabbreviate_logic(f);
f2 = simplify_f_g(f1);
destroy(f1);
f1 = negative_normal_form(f2);
destroy(f2); destroy(f2);
f2 = f1; f2 = f1;
// Run basic_reduce again.
//
// Consider `FG b & g' were g is an eventual formula rewritten
// as `g = FG c' Then basic_reduce with rewrite it
// as FG(b & c).
if (opt & Reduce_Basics) if (opt & Reduce_Basics)
{ {
f1 = basic_reduce(f2); f1 = basic_reduce(f2);
destroy(f2); destroy(f2);
f2 = f1; f2 = f1;
} }
if (opt & (Reduce_Syntactic_Implications
| Reduce_Eventuality_And_Universality))
{
reduce_visitor v(opt);
f2->accept(v);
f1 = v.result();
destroy(f2);
f2 = f1;
}
if (opt & (Reduce_Containment_Checks
| Reduce_Containment_Checks_Stronger))
{
formula* f1 =
reduce_tau03(f2,
opt & Reduce_Containment_Checks_Stronger);
destroy(f2);
f2 = f1;
}
f = f2;
} }
destroy(prev);
return const_cast<formula*>(f);
if (opt & (Reduce_Containment_Checks
| Reduce_Containment_Checks_Stronger))
{
formula* f1 = reduce_tau03(f2,
opt & Reduce_Containment_Checks_Stronger);
destroy(f2);
f2 = f1;
}
return f2;
} }
} }
} }