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

Improve a reduction rule for "a M b".

Browse source 
* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
to "a & b" if "a" is a pure eventual formula, remove the
constraint on "b".
* src/ltltest/reduccmp.test: Add two tests.
This commit is contained in:
Alexandre Duret-Lutz 2011-03-17 11:55:56 +01:00
parent b51b7ab8b9
commit 1878bfd0fc
3 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2011-03-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Improve a reduction rule for "a M b".
* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
to "a & b" if "a" is a pure eventual formula, remove the
constraint on "b".
* src/ltltest/reduccmp.test: Add two tests.
2011-03-11 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-03-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Mention recent changes to dotty_reachable. * NEWS: Mention recent changes to dotty_reachable.

8
src/ltltest/reduccmp.test
View file

@ -1,5 +1,5 @@
#! /bin/sh #! /bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -153,6 +153,10 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'a M ((a & b) M c)' '(a & b)M c' run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
run 0 $x '(a & b) M (a R c)' '(a & b)M c' run 0 $x '(a & b) M (a R c)' '(a & b)M c'
run 0 $x '(a & b) M (a M c)' '(a & b)M c' run 0 $x '(a & b) M (a M c)' '(a & b)M c'
# Eventuality and universality class reductions
run 0 $x 'Fa M b' 'Fa & b'
run 0 $x 'GFa M b' 'GFa & b'
;; ;;
esac esac
@ -161,7 +165,7 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced. run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced. run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
# Eventuality and universality class reduction # Eventuality and universality class reductions
run 0 $x 'FFa' 'Fa' run 0 $x 'FFa' 'Fa'
run 0 $x 'FGFa' 'GFa' run 0 $x 'FGFa' 'GFa'
run 0 $x 'b U Fa' 'Fa' run 0 $x 'b U Fa' 'Fa'

6
src/ltlvisit/reduce.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -285,9 +285,9 @@ namespace spot
eu_info f1i = { recurse_eu(f1) }; eu_info f1i = { recurse_eu(f1) };
if (opt_ & Reduce_Eventuality_And_Universality) if (opt_ & Reduce_Eventuality_And_Universality)
{ {
/* If a&b is a pure eventuality formula then a M b = a & b. /* If a is a pure eventuality formula then a M b = a & b.
If a is a pure universality formula a W b = a|b. */ If a is a pure universality formula a W b = a|b. */
if (f1i.is.eventual && f2i.is.eventual && (op == binop::M)) if (f1i.is.eventual && (op == binop::M))
{ {
result_ = multop::instance(multop::And, f1, f2); result_ = multop::instance(multop::And, f1, f2);
return; return;