diff --git a/NEWS b/NEWS index 8993cb368..0c687ce22 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,13 @@ New in spot 2.6.0.dev (not yet released) - scc_info::split_on_sets() did not correctly register the atomic propositions of the returned automata. + - The spot::tl_simplifier class could raise an exception while + attempting to reduce formulas containing unsimplified <->, -> or + xor, if options nenoform_stop_on_boolean and synt_impl are both + set. (This combinations of options is not available from + command-line tools.) + + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 08f597a28..7dd243292 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1744,58 +1744,62 @@ are counted as one. \begingroup \allowdisplaybreaks \begin{alignat*}{3} -\text{if~} & f\simp \NOT g && \text{~then~} & f\OR g & \equiv \1 \\ -\text{if~} & f\simp \NOT g && \text{~then~} & f\AND g & \equiv \0 \\ -\text{if~} & \flessg && \text{~then~} & f\OR g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\OR g & \equiv g \\ -\text{if~} & \glessf && \text{~then~} & f\AND g & \equiv g \\ -\text{if~} & f\simp g && \text{~then~} & f\AND g & \equiv f \\ -\text{if~} & \flessg && \text{~then~} & f\U g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\U g & \equiv g \\ -\text{if~} & (f\U g)\Simp g && \text{~then~} & f\U g & \equiv g \\ -\text{if~} & (\NOT f)\simp g && \text{~then~} & f\U g & \equiv \F g \\ -\text{if~} & g\simp e && \text{~then~} & e\U g & \equiv \F g \\ -\text{if~} & f\simp g && \text{~then~} & f\U (g \U h) & \equiv g \U h \\ -\text{if~} & f\simp g && \text{~then~} & f\U (g \W h) & \equiv g \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\U (g \U h) & \equiv f \U h \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ -\text{if~} & f\simp h && \text{~then~} & (f\U g) \U h & \equiv g \U h \\ -\text{if~} & f\simp h && \text{~then~} & (f\W g) \U h & \equiv g \U h \\ -\text{if~} & g\simp h && \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ -\text{if~} & (\NOT f)\simp g && \text{~then~} & f\W g & \equiv \1 \\ -\text{if~} & \flessg && \text{~then~} & f\W g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\W g & \equiv g \\ -\text{if~} & (f\W g)\Simp g && \text{~then~} & f\W g & \equiv g \\ -\text{if~} & f\simp g && \text{~then~} & f\W (g \W h) & \equiv g \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\W (g \U h) & \equiv f \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\W (g \W h) & \equiv f \W h \\ -\text{if~} & f\simp h && \text{~then~} & (f\U g) \W h & \equiv g \W h \\ -\text{if~} & f\simp h && \text{~then~} & (f\W g) \W h & \equiv g \W h \\ -\text{if~} & g\simp h && \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ -\text{if~} & g\simp h && \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ -\text{if~} & \flessg && \text{~then~} & f\R g & \equiv f \\ -\text{if~} & g\simp f && \text{~then~} & f\R g & \equiv g \\ -\text{if~} & g\simp \NOT f && \text{~then~} & f\R g & \equiv \G g \\ -\text{if~} & u\simp g && \text{~then~} & u\R g & \equiv \G g \\ -\text{if~} & g\simp f && \text{~then~} & f\R (g \R h) & \equiv g \R h \\ -\text{if~} & g\simp f && \text{~then~} & f\R (g \M h) & \equiv g \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\R (g \R h) & \equiv f \R h \\ -\text{if~} & h\simp f && \text{~then~} & (f\R g) \R h & \equiv g \R h \\ -\text{if~} & h\simp f && \text{~then~} & (f\M g) \R h & \equiv g \R h \\ -\text{if~} & g\simp h && \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ -\text{if~} & g\simp h && \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ -\text{if~} & \flessg && \text{~then~} & f\M g & \equiv f \\ -\text{if~} & g\simp f && \text{~then~} & f\M g & \equiv g \\ -\text{if~} & g\simp \NOT f && \text{~then~} & f\M g & \equiv \0 \\ -\text{if~} & g\simp f && \text{~then~} & f\M (g \M h) & \equiv g \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\M (g \M h) & \equiv f \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\M (g \R h) & \equiv f \M h \\ -\text{if~} & h\simp f && \text{~then~} & (f\M g) \M h & \equiv g \M h \\ -\text{if~} & h\simp f && \text{~then~} & (f\R g) \M h & \equiv g \M h \\ -\text{if~} & g\simp h && \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ +\text{if~} & f\simp \NOT g & & \text{~then~} & f\OR g & \equiv \1 \\ +\text{if~} & f\simp \NOT g & & \text{~then~} & f\AND g & \equiv \0 \\ +\text{if~} & \flessg & & \text{~then~} & f\OR g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\OR g & \equiv g \\ +\text{if~} & \glessf & & \text{~then~} & f\AND g & \equiv g \\ +\text{if~} & f\simp g & & \text{~then~} & f\AND g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\EQUIV g & \equiv g\IMPLIES f \\ +\text{if~} & f\simp g & & \text{~then~} & f\IMPLIES g & \equiv \1 \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\XOR g & \equiv g\IMPLIES \NOT f \\ +\text{if~} & f\simp\NOT g & & \text{~then~} & f\XOR g & \equiv (\NOT g)\IMPLIES f \\ +\text{if~} & \flessg & & \text{~then~} & f\U g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (f\U g)\Simp g & & \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\U g & \equiv \F g \\ +\text{if~} & g\simp e & & \text{~then~} & e\U g & \equiv \F g \\ +\text{if~} & f\simp g & & \text{~then~} & f\U (g \U h) & \equiv g \U h \\ +\text{if~} & f\simp g & & \text{~then~} & f\U (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\U (g \U h) & \equiv f \U h \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ +\text{if~} & f\simp h & & \text{~then~} & (f\U g) \U h & \equiv g \U h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\W g) \U h & \equiv g \U h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\W g & \equiv \1 \\ +\text{if~} & \flessg & & \text{~then~} & f\W g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\W g & \equiv g \\ +\text{if~} & (f\W g)\Simp g & & \text{~then~} & f\W g & \equiv g \\ +\text{if~} & f\simp g & & \text{~then~} & f\W (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\W (g \U h) & \equiv f \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\W (g \W h) & \equiv f \W h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\U g) \W h & \equiv g \W h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\W g) \W h & \equiv g \W h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ +\text{if~} & \flessg & & \text{~then~} & f\R g & \equiv f \\ +\text{if~} & g\simp f & & \text{~then~} & f\R g & \equiv g \\ +\text{if~} & g\simp \NOT f & & \text{~then~} & f\R g & \equiv \G g \\ +\text{if~} & u\simp g & & \text{~then~} & u\R g & \equiv \G g \\ +\text{if~} & g\simp f & & \text{~then~} & f\R (g \R h) & \equiv g \R h \\ +\text{if~} & g\simp f & & \text{~then~} & f\R (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\R (g \R h) & \equiv f \R h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\R g) \R h & \equiv g \R h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\M g) \R h & \equiv g \R h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & \flessg & & \text{~then~} & f\M g & \equiv f \\ +\text{if~} & g\simp f & & \text{~then~} & f\M g & \equiv g \\ +\text{if~} & g\simp \NOT f & & \text{~then~} & f\M g & \equiv \0 \\ +\text{if~} & g\simp f & & \text{~then~} & f\M (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\M (g \M h) & \equiv f \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\M (g \R h) & \equiv f \M h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\M g) \M h & \equiv g \M h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\R g) \M h & \equiv g \M h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ \end{alignat*} \endgroup diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index ddb90c776..422529fc6 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1775,12 +1775,38 @@ namespace spot trace << "bo: trying inclusion-based rules" << std::endl; switch (o) { - case op::Xor: case op::Equiv: + { + if (c_->implication(a, b)) + return recurse(formula::Implies(b, a)); + if (c_->implication(b, a)) + return recurse(formula::Implies(a, b)); + break; + } case op::Implies: - SPOT_UNIMPLEMENTED(); - break; - + { + if (c_->implication(a, b)) + return formula::tt(); + break; + } + case op::Xor: + { + // if (!a)->b then a xor b = b->!a = a->!b + if (c_->implication_neg(a, b, false)) + { + if (b.is(op::Not)) + return recurse(formula::Implies(a, b[0])); + return recurse(formula::Implies(b, formula::Not(a))); + } + // if a->!b then a xor b = (!b)->a = (!a)->b + if (c_->implication_neg(a, b, true)) + { + if (b.is(op::Not)) + return recurse(formula::Implies(b[0], a)); + return recurse(formula::Implies(formula::Not(a), b)); + } + break; + } case op::U: // if a => b, then a U b = b if (c_->implication(a, b)) diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index 9eb9f909f..96ebcda17 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2015, 2018 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systemes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -116,3 +116,21 @@ Default for shell: echo 'a U (b U "$strange[0]=name")' | ... LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ... Default for CSV: ...,"a U (b U ""$strange[0]=name"")",... Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""" + + +opt = spot.tl_simplifier_options(False, True, True, + True, True, True, + False, False, False) + +for (input, output) in [('(a&b)<->b', 'b->(a&b)'), + ('b<->(a&b)', 'b->(a&b)'), + ('(a&b)->b', '1'), + ('b->(a&b)', 'b->(a&b)'), + ('(!(a&b)) xor b', 'b->(a&b)'), + ('(a&b) xor !b', 'b->(a&b)'), + ('b xor (!(a&b))', 'b->(a&b)'), + ('!b xor (a&b)', 'b->(a&b)')]: + f = spot.tl_simplifier(opt).simplify(input) + print(input, f, output) + assert(f == output) + assert(spot.are_equivalent(input, output))