translate: improve handling of Xor and Equiv at top-level for -G -D

* spot/tl/formula.hh: Add variant of formula::is that support 4
arguments.
* spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
to preserve Xor and Equiv at the top-level.
* spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
Equiv for the -D -G case.
* NEWS: Mention that.
* tests/core/ltl2tgba2.test: Add test case.
* tests/python/simstate.py: Adjust expected result.

NEWS

@@ -1,5 +1,12 @@
 New in spot 2.9.0.dev (not yet released)
 
+  Command-line tools:
+
+  - 'ltl2tgba -G -D' is now better at handling formulas that use
+    '<->' and 'xor' operators at the top level.   For instance
+         ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
+    now produces a 16-state automaton (instead of 31 in Spot 2.9).
+
   Library:
 
   - product_xor() and product_xnor() are two new versions of the
@@ -8,6 +15,11 @@ New in spot 2.9.0.dev (not yet released)
     respectively the symmetric difference of the operands, and the
     complement of that.
 
+  - tl_simplifier_options::keep_top_xor is a new option to keep Xor
+    and Equiv operator that appear at the top of LTL formulas (maybe
+    below other Boolean or X operators).  This is used by the
+    spot::translator class when creating deterministic automata with
+    generic acceptance.
 
 New in spot 2.9 (2020-04-30)
 

spot/tl/formula.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -186,18 +186,27 @@ namespace spot
       std::string kindstr() const;
 
       /// \see formula::is
+      /// @{
       bool is(op o) const
       {
         return op_ == o;
       }
 
-      /// \see formula::is
       bool is(op o1, op o2) const
       {
         return op_ == o1 || op_ == o2;
       }
 
-      /// \see formula::is
+      bool is(op o1, op o2, op o3) const
+      {
+        return op_ == o1 || op_ == o2 || op_ == o3;
+      }
+
+      bool is(op o1, op o2, op o3, op o4) const
+      {
+        return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
+      }
+
       bool is(std::initializer_list<op> l) const
       {
         const fnode* n = this;
@@ -209,6 +218,7 @@ namespace spot
         }
         return true;
       }
+      /// @}
 
       /// \see formula::get_child_of
       const fnode* get_child_of(op o) const
@@ -1333,6 +1343,19 @@ namespace spot
       return ptr_->is(o1, o2);
     }
 
+    /// Return true if the formula is of kind \a o1 or \a o2 or \a o3
+    bool is(op o1, op o2, op o3) const
+    {
+      return ptr_->is(o1, o2, o3);
+    }
+
+    /// Return true if the formula is of kind \a o1 or \a o2 or \a o3
+    /// or \a a4.
+    bool is(op o1, op o2, op o3, op o4) const
+    {
+      return ptr_->is(o1, o2, o3, o4);
+    }
+
     /// Return true if the formulas nests all the operators in \a l.
     bool is(std::initializer_list<op> l) const
     {

spot/tl/simplify.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2019 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -417,22 +417,25 @@ namespace spot
     //////////////////////////////////////////////////////////////////////
 
     formula
-    nenoform_rec(formula f, bool negated, tl_simplifier_cache* c);
+    nenoform_rec(formula f, bool negated, tl_simplifier_cache* c,
+                 bool deep);
 
     formula equiv_or_xor(bool equiv, formula f1, formula f2,
-                         tl_simplifier_cache* c)
+                         tl_simplifier_cache* c, bool deep)
     {
-      auto rec = [c](formula f, bool negated)
+      auto rec = [c, deep](formula f, bool negated)
         {
-          return nenoform_rec(f, negated, c);
+          return nenoform_rec(f, negated, c, deep);
         };
 
       if (equiv)
         {
           // Rewrite a<=>b as (a&b)|(!a&!b)
           auto recurse_f1_true = rec(f1, true);
-          auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_true = rec(f2, true);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Equiv(recurse_f1_true, recurse_f2_true);
+          auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
           auto left = formula::And({recurse_f1_false, recurse_f2_false});
           auto right = formula::And({recurse_f1_true, recurse_f2_true});
@@ -442,8 +445,10 @@ namespace spot
         {
           // Rewrite a^b as (a&!b)|(!a&b)
           auto recurse_f1_true = rec(f1, true);
-          auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_true = rec(f2, true);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Xor(recurse_f1_true, recurse_f2_true);
+          auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
           auto left = formula::And({recurse_f1_false, recurse_f2_true});
           auto right = formula::And({recurse_f1_true, recurse_f2_false});
@@ -451,8 +456,11 @@ namespace spot
         }
     }
 
+    // The deep argument indicate whether we are under a temporal
+    // operator (except X).
     formula
-    nenoform_rec(formula f, bool negated, tl_simplifier_cache* c)
+    nenoform_rec(formula f, bool negated, tl_simplifier_cache* c,
+                 bool deep)
     {
       if (f.is(op::Not))
         {
@@ -474,9 +482,9 @@ namespace spot
         }
       else
         {
-          auto rec = [c](formula f, bool neg)
+          auto rec = [c, &deep](formula f, bool neg)
             {
-              return nenoform_rec(f, neg, c);
+              return nenoform_rec(f, neg, c, deep);
             };
 
           switch (op o = f.kind())
@@ -504,21 +512,25 @@ namespace spot
               break;
             case op::F:
               // !Fa == G!a
+              deep = true;
               result = formula::unop(negated ? op::G : op::F,
                                      rec(f[0], negated));
               break;
             case op::G:
               // !Ga == F!a
+              deep = true;
               result = formula::unop(negated ? op::F : op::G,
                                      rec(f[0], negated));
               break;
             case op::Closure:
+              deep = true;
               result = formula::unop(negated ?
                                      op::NegClosure : op::Closure,
                                      rec(f[0], false));
               break;
             case op::NegClosure:
             case op::NegClosureMarked:
+              deep = true;
               result = formula::unop(negated ? op::Closure : o,
                                      rec(f[0], false));
               break;
@@ -539,17 +551,18 @@ namespace spot
             case op::Xor:
               {
                 // !(a ^ b) == a <=> b
-                result = equiv_or_xor(negated, f[0], f[1], c);
+                result = equiv_or_xor(negated, f[0], f[1], c, deep);
                 break;
               }
             case op::Equiv:
               {
                 // !(a <=> b) == a ^ b
-                result = equiv_or_xor(!negated, f[0], f[1], c);
+                result = equiv_or_xor(!negated, f[0], f[1], c, deep);
                 break;
               }
             case op::U:
               {
+                deep = true;
                 // !(a U b) == !a R !b
                 auto f1 = rec(f[0], negated);
                 auto f2 = rec(f[1], negated);
@@ -558,6 +571,7 @@ namespace spot
               }
             case op::R:
               {
+                deep = true;
                 // !(a R b) == !a U !b
                 auto f1 = rec(f[0], negated);
                 auto f2 = rec(f[1], negated);
@@ -566,6 +580,7 @@ namespace spot
               }
             case op::W:
               {
+                deep = true;
                 // !(a W b) == !a M !b
                 auto f1 = rec(f[0], negated);
                 auto f2 = rec(f[1], negated);
@@ -574,6 +589,7 @@ namespace spot
               }
             case op::M:
               {
+                deep = true;
                 // !(a M b) == !a W !b
                 auto f1 = rec(f[0], negated);
                 auto f2 = rec(f[1], negated);
@@ -604,15 +620,16 @@ namespace spot
               // !(a*) etc. should never occur.
               {
                 assert(!negated);
-                result = f.map([c](formula f)
+                result = f.map([c, deep](formula f)
                                {
-                                 return nenoform_rec(f, false, c);
+                                 return nenoform_rec(f, false, c, deep);
                                });
                 break;
               }
             case op::EConcat:
             case op::EConcatMarked:
               {
+                deep = true;
                 // !(a <>-> b) == a[]-> !b
                 auto f1 = f[0];
                 auto f2 = f[1];
@@ -622,6 +639,7 @@ namespace spot
               }
             case op::UConcat:
               {
+                deep = true;
                 // !(a []-> b) == a<>-> !b
                 auto f1 = f[0];
                 auto f2 = f[1];
@@ -4048,9 +4066,9 @@ namespace spot
     if (f2.is_sere_formula() && !f2.is_boolean())
       return false;
     if (right)
-      f2 = nenoform_rec(f2, true, this);
+      f2 = nenoform_rec(f2, true, this, false);
     else
-      f1 = nenoform_rec(f1, true, this);
+      f1 = nenoform_rec(f1, true, this, false);
     return syntactic_implication(f1, f2);
   }
 
@@ -4085,7 +4103,7 @@ namespace spot
   formula
   tl_simplifier::negative_normal_form(formula f, bool negated)
   {
-    return nenoform_rec(f, negated, cache_);
+    return nenoform_rec(f, negated, cache_, false);
   }
 
   bool

spot/tl/simplify.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2017, 2019 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011-2017, 2019, 2020 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -37,7 +37,8 @@ namespace spot
                           bool nenoform_stop_on_boolean = false,
                           bool reduce_size_strictly = false,
                           bool boolean_to_isop = false,
-                           bool favor_event_univ = false)
+                          bool favor_event_univ = false,
+                          bool keep_top_xor = false)
       : reduce_basics(basics),
         synt_impl(synt_impl),
         event_univ(event_univ),
@@ -46,7 +47,8 @@ namespace spot
         nenoform_stop_on_boolean(nenoform_stop_on_boolean),
         reduce_size_strictly(reduce_size_strictly),
         boolean_to_isop(boolean_to_isop),
-        favor_event_univ(favor_event_univ)
+        favor_event_univ(favor_event_univ),
+        keep_top_xor(keep_top_xor)
     {
     }
 
@@ -87,6 +89,10 @@ namespace spot
     bool boolean_to_isop;
     // Try to isolate subformulae that are eventual and universal.
     bool favor_event_univ;
+    // Keep Xor and Equiv at the top of the formula, possibly under
+    // &,|, and X operators.  Only rewrite Xor and Equiv under
+    // temporal operators.
+    bool keep_top_xor;
   };
 
   // fwd declaration to hide technical details.

spot/twaalgos/translate.cc

@@ -108,6 +108,8 @@ namespace spot
         }
     if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
       options.favor_event_univ = true;
+    if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
+      options.keep_top_xor = true;
     simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
   }
 
@@ -167,15 +169,16 @@ namespace spot
                 r2 = formula::multop(op2, susp);
               }
           }
-        if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or) ||
+        if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or,
+                                                   op::Xor, op::Equiv) ||
             // For TGBA/BA we only do conjunction.  There is nothing wrong
             // with disjunction, but it seems to generate larger automata
             // in many cases and it needs to be further investigated.  Maybe
             // this could be relaxed in the case of deterministic output.
-            (r2.is(op::Or) && (type_ == TGBA || type_ == BA)))
+            (!r2.is(op::And) && (type_ == TGBA || type_ == BA)))
           goto nosplit;
 
-        bool is_and = r2.is(op::And);
+        op topop = r2.kind();
         // Let's classify subformulas.
         std::vector<formula> oblg;
         std::vector<formula> susp;
@@ -270,10 +273,16 @@ namespace spot
             twa_graph_ptr rest_aut = transrun(rest_f);
             if (aut == nullptr)
               aut = rest_aut;
-            else if (is_and)
+            else if (topop == op::And)
               aut = product(aut, rest_aut);
-            else
+            else if (topop == op::Or)
               aut = product_or(aut, rest_aut);
+            else if (topop == op::Xor)
+              aut = product_xor(aut, rest_aut);
+            else if (topop == op::Equiv)
+              aut = product_xnor(aut, rest_aut);
+            else
+              SPOT_UNREACHABLE();
           }
         if (!susp.empty())
           {
@@ -285,10 +294,16 @@ namespace spot
                 twa_graph_ptr one = transrun(f);
                 if (!susp_aut)
                   susp_aut = one;
-                else if (is_and)
+                else if (topop == op::And)
                   susp_aut = product(susp_aut, one);
-                else
+                else if (topop == op::Or)
                   susp_aut = product_or(susp_aut, one);
+                else if (topop == op::Xor)
+                  susp_aut = product_xor(susp_aut, one);
+                else if (topop == op::Equiv)
+                  susp_aut = product_xnor(susp_aut, one);
+                else
+                  SPOT_UNREACHABLE();
               }
             if (susp_aut->prop_universal().is_true())
               {
@@ -311,10 +326,14 @@ namespace spot
               }
             if (aut == nullptr)
               aut = susp_aut;
-            else if (is_and)
+            else if (topop == op::And)
               aut = product_susp(aut, susp_aut);
-            else
+            else if (topop == op::Or)
               aut = product_or_susp(aut, susp_aut);
+            else if (topop == op::Xor) // No suspension here
+              aut = product_xor(aut, susp_aut);
+            else if (topop == op::Equiv) // No suspension here
+              aut = product_xnor(aut, susp_aut);
             //if (aut && susp_aut)
             //  {
             //    print_hoa(std::cerr << "AUT\n", aut) << '\n';

tests/core/ltl2tgba2.test

@@ -451,4 +451,11 @@ f='(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)'
 test 1,8,3 = `ltl2tgba -G -D "$f" --stats=%s,%e,%a`
 test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a`
 
+# Handling of Xor and <-> by ltl-split and -D -G.
+res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'`
+test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
+res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
+test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
+ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
+
 :

tests/python/simstate.py

@@ -178,13 +178,13 @@ b.copy_state_names_from(a)
 assert b.to_str() == """HOA: v1
 States: 1
 Start: 0
-AP: 2 "p0" "p1"
+AP: 2 "p1" "p0"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0 "[1,7]"
-[!1] 0 {0}
+[!0] 0 {0}
-[1] 0
+[0] 0
 --END--"""