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

simplify: remove an incorrect simplification rule

Browse source 
Fortunately was only enabled with the
ltl_simplifier_options::favor_event_univ option, which cannot yet be
turned on from the command-line tools.

* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/eventuniv.test: Adjust.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2014-05-13 17:26:53 +02:00
parent 362862dace
commit d741d9266d
4 changed files with 8 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -14,9 +14,11 @@ New in spot 1.2.3a (not yet released)
- "ltl2tgta --ta" could crash in certain conditions due to the - "ltl2tgta --ta" could crash in certain conditions due to the
introduction of a simulation-based reduction after introduction of a simulation-based reduction after
degeneralization. degeneralization.
- Fix three incorrect simplifications rules, all related to the - Fix four incorrect formula-simplification rules, three were
factorization of Boolean subformulas in operands of the related to the factorization of Boolean subformulas in
non-length-matching "&" SERE operator. operands of the non-length-matching "&" SERE operator, and
a fourth one could only be enabled by explicitely passing the
favor_event_univ option to the simplifier (not the default).
- Fix incorrect translation of the fusion operator (":") in SERE - Fix incorrect translation of the fusion operator (":") in SERE
such as {xx;1}:yy[*] where the left operand has 1 as tail. such as {xx;1}:yy[*] where the left operand has 1 as tail.

1
doc/tl/tl.tex
View file

@ -1580,7 +1580,6 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\
& & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\ & & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\
\G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\ \G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\
\G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\ \G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\
& & (f\OR u) \W g & \equivEU (f \W g)\OR u \\
\X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\ \X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\
& & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\ & & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\
\end{align*} \end{align*}

6
src/ltltest/eventuniv.test
View file

@ -1,7 +1,7 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement # Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
# de l'Epita (LRDE). # Developpement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -48,7 +48,7 @@ check 'a U (b | Fc)' '(a U b) | Fc'
check 'a W (b | Fc)' '(a W b) | Fc' check 'a W (b | Fc)' '(a W b) | Fc'
check 'a U (b & GFc)' '(a U b) & GFc' check 'a U (b & GFc)' '(a U b) & GFc'
check 'a W (b & GFc)' 'a W (b & GFc)' # Unchanged check 'a W (b & GFc)' 'a W (b & GFc)' # Unchanged
check '(a | Gc) W g' '(a W g) | Gc' check '(a | Gc) W g' '(a | Gc) W g' # Unchanged
check '(a | Gc) U g' '(a | Gc) U g' # Unchanged check '(a | Gc) U g' '(a | Gc) U g' # Unchanged
check '(a & GFc) M b' '(a M b) & GFc' check '(a & GFc) M b' '(a M b) & GFc'

19
src/ltlvisit/simplify.cc
View file

@ -2075,7 +2075,6 @@ namespace spot
// (a W (b|e)) = (a W b)|e // (a W (b|e)) = (a W b)|e
// (a U (b&q)) = (a U b)&q // (a U (b&q)) = (a U b)&q
// ((a&q) M b) = (a M b)&q // ((a&q) M b) = (a M b)&q
// ((a|u) W b) = u|(a W b)
// (a R (b&u)) = (a R b)&u // (a R (b&u)) = (a R b)&u
// (a M (b&u)) = (a M b)&u // (a M (b&u)) = (a M b)&u
if (opt_.favor_event_univ) if (opt_.favor_event_univ)
@ -2099,24 +2098,6 @@ namespace spot
b2->destroy(); b2->destroy();
delete s.res_Event; delete s.res_Event;
} }
if (op == binop::W)
if (const multop* mo = is_Or(a))
{
a->clone();
mospliter s(mospliter::Split_Univ, mo, c_);
const formula* a2 =
multop::instance(multop::Or, s.res_other);
if (a2 != a)
{
a->destroy();
s.res_Univ->push_back(binop::instance(op, a2, b));
result_ = recurse_destroy
(multop::instance(multop::Or, s.res_Univ));
return;
}
a2->destroy();
delete s.res_Univ;
}
if (op == binop::U) if (op == binop::U)
if (const multop* mo = is_And(b)) if (const multop* mo = is_And(b))
{ {