Commit ca2fe4f3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Reimplement basic_reduce()'s rules in ltl_simplifier.

So far I have only checked these rewritings with reduccmp.test.
There are probably a few kinks to iron out.

* src/ltlvisit/simplify.cc: Reimplement most of the basic
rewriting rules, leaving some FIXME comments for dubious ones.
* src/ltlast/multop.cc, src/ltlast/multop.hh: Ignore NULL
pointers in the vector.
* src/ltlvisit/reduce.cc (reduce): Do not call basic_reduce().
* src/ltltest/reduccmp.test: Adjust tests.
parent e3e0f913
......@@ -163,7 +163,7 @@ namespace spot
// We match equivalent formulae modulo "ACI rules"
// (i.e. associativity, commutativity and idempotence of the
// operator). For instance If `+' designate the OR operator and
// operator). For instance if `+' designates the OR operator and
// `0' is false (the neutral element for `+') , then `f+f+0' is
// equivalent to `f'.
formula*
......@@ -178,6 +178,16 @@ namespace spot
vec::iterator i = v->begin();
while (i != v->end())
{
// Some simplification routines erase terms using null
// pointers that we must ignore.
if ((*i) == 0)
{
// FIXME: We should replace the pointer by the
// first non-null value at the end of the array
// instead of calling erase.
i = v->erase(i);
continue;
}
if ((*i)->kind() == MultOp)
{
multop* p = static_cast<multop*>(*i);
......@@ -187,6 +197,7 @@ namespace spot
for (unsigned n = 0; n < ps; ++n)
inlined.push_back(p->nth(n)->clone());
(*i)->destroy();
// FIXME: Do not use erase. See previous FIXME.
i = v->erase(i);
continue;
}
......
......@@ -65,7 +65,8 @@ namespace spot
/// formulae as argument. This vector is acquired by the
/// spot::ltl::multop class, the caller should allocate it with
/// \c new, but not use it (especially not destroy it) after it
/// has been passed to spot::ltl::multop.
/// has been passed to spot::ltl::multop. Inside the vector,
/// null pointers are ignored.
///
/// All operators (Or, And, Concat) are associative, and are
/// automatically inlined. Or and And are commutative, so their
......
......@@ -100,8 +100,10 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
run 0 $x '(a R b) | (c R b)' '(a | c) R b'
run 0 $x 'X(a & GFb)' 'Xa & GFb'
run 0 $x 'X(a | GFb)' 'Xa | GFb'
run 0 $x 'Xa & FGb' 'X(a & FGb)'
run 0 $x 'Xa | FGb' 'Xa | FGb' # We'd prefer 'X(a | FGb)'
run 0 $x 'Xa & GFb' 'Xa & GFb' # 'X(a & GFb)'
run 0 $x 'Xa | GFb' 'X(a | GFb)'
# The following is not reduced to F(a) & GFb. because
# (1) is does not help the translate the formula into a
# smaller automaton, and ...
......@@ -109,10 +111,9 @@ for x in ../reduccmp ../reductaustr; do
# (2) ... it would hinder this useful reduction (that helps to
# produce a smaller automaton)
run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
# FIXME: Don't we want the opposite rewriting
run 0 $x 'Fa & GFb' 'Fa & GFb' # We'd prefer 'F(a & GFb)'
run 0 $x 'G(a | GFb)' 'Ga | GFb'
run 0 $x 'X(a & GFb & c)' 'X(a & c) & GFb'
run 0 $x 'X(a | GFb | c)' 'X(a | c) | GFb'
# The following is not reduced to F(a & c) & GF(b) for the same
# reason as above.
run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
......
......@@ -22,7 +22,6 @@
// 02111-1307, USA.
#include "reduce.hh"
#include "basicreduce.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
......@@ -74,13 +73,6 @@ namespace spot
f2->destroy();
f2 = f1;
if (opt & Reduce_Basics)
{
f1 = basic_reduce(f2);
f2->destroy();
f2 = f1;
}
f1 = simplifier.simplify(f2);
f2->destroy();
f2 = f1;
......
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment