tl: add some implication-based rewritings for "<->", "->", and "xor"

This prevents an exception from being raised if NNF is not performed
on Boolean properties and implication-based checks are used.

* NEWS: Mention the issue.
* spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules.
* tests/python/ltlsimple.py: Test them.

NEWS

@@ -52,6 +52,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:

doc/tl/tl.tex

@@ -1770,6 +1770,10 @@ are counted as one.
 \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                  \\

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:
-              case op::Implies:
-                SPOT_UNIMPLEMENTED();
+                {
+                  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:
+                {
+                  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))

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))