complement: add a complement() function

* spot/twaalgos/complement.cc,
spot/twaalgos/complement.hh (complement): New function.
* bin/autfilt.cc, spot/twa/twa.cc, spot/twaalgos/contains.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/stutter.cc: Use it.
* tests/core/complement.test: Adjust.
* NEWS: Mention it.

NEWS

@@ -39,6 +39,10 @@ New in spot 2.7.2.dev (not yet released)
     helpful to display automata as "graphs", e.g., when illustrating
     algorithms that do not care about labels.
 
+  - A new complement() function that return automata with unspecified
+    acceptance condition.  The output can be alternating only if the
+    input was alternating.
+
   Bugs fixed:
 
   - When processing CSV files with MSDOS-style \r\n line endings,

bin/autfilt.cc

@@ -49,6 +49,7 @@
 #include <spot/twaalgos/canonicalize.hh>
 #include <spot/twaalgos/cobuchi.hh>
 #include <spot/twaalgos/cleanacc.hh>
+#include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/contains.hh>
 #include <spot/twaalgos/degen.hh>
 #include <spot/twaalgos/dtwasat.hh>
@@ -318,7 +319,7 @@ static const argp_option options[] =
     { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
       "remove unused acceptance sets from the automaton", 0 },
     { "complement", OPT_COMPLEMENT, nullptr, 0,
-      "complement each automaton (currently via determinization)", 0 },
+      "complement each automaton (different strategies are used)", 0 },
     { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
       "complement the acceptance condition (without touching the automaton)",
       0 },
@@ -1500,7 +1501,7 @@ namespace
 
       if (opt_complement)
         {
-          aut = spot::dualize(ensure_deterministic(aut));
+          aut = spot::complement(aut);
           aut->merge_edges();
         }
 

spot/twa/twa.cc

@@ -28,8 +28,7 @@
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/alternation.hh>
 #include <spot/twa/twaproduct.hh>
-#include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/complement.hh>
-#include <spot/twaalgos/postproc.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/genem.hh>
@@ -172,20 +171,13 @@ namespace spot
   namespace
   {
     static const_twa_graph_ptr
-    ensure_deterministic(const const_twa_ptr& aut_in)
+    ensure_graph(const const_twa_ptr& aut_in)
     {
       const_twa_graph_ptr aut =
         std::dynamic_pointer_cast<const twa_graph>(aut_in);
-      if (!aut)
+      if (aut)
-        aut = make_twa_graph(aut_in, twa::prop_set::all());
-
-      if (is_deterministic(aut))
         return aut;
-      postprocessor p;
+      return make_twa_graph(aut_in, twa::prop_set::all());
-      p.set_type(postprocessor::Generic);
-      p.set_pref(postprocessor::Deterministic);
-      p.set_level(postprocessor::Low);
-      return p.run(std::const_pointer_cast<twa_graph>(aut));
     }
   }
   twa_run_ptr
@@ -199,9 +191,9 @@ namespace spot
     if (auto aa = std::dynamic_pointer_cast<const twa_graph>(a))
       if (is_deterministic(aa))
         std::swap(a, b);
-    if (auto run = a->intersecting_run(dualize(ensure_deterministic(b))))
+    if (auto run = a->intersecting_run(complement(ensure_graph(b))))
       return run;
-    return b->intersecting_run(dualize(ensure_deterministic(a)));
+    return b->intersecting_run(complement(ensure_graph(a)));
   }
 
   twa_word_ptr
@@ -215,9 +207,9 @@ namespace spot
     if (auto aa = std::dynamic_pointer_cast<const twa_graph>(a))
       if (is_deterministic(aa))
         std::swap(a, b);
-    if (auto word = a->intersecting_word(dualize(ensure_deterministic(b))))
+    if (auto word = a->intersecting_word(complement(ensure_graph(b))))
       return word;
-    return b->intersecting_word(dualize(ensure_deterministic(a)));
+    return b->intersecting_word(complement(ensure_graph(a)));
   }
 
   void

spot/twaalgos/complement.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2015, 2017-2018 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2017-2019 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -23,6 +23,9 @@
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/isdet.hh>
+#include <spot/twaalgos/alternation.hh>
+#include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/strength.hh>
 #include <spot/twaalgos/sccinfo.hh>
 
 namespace spot
@@ -506,4 +509,19 @@ namespace spot
     auto ncsb = ncsb_complementation(aut, show_names);
     return ncsb.run();
   }
+
+  twa_graph_ptr
+  complement(const const_twa_graph_ptr& aut)
+  {
+    if (!aut->is_existential() || is_universal(aut))
+      return dualize(aut);
+    if (is_very_weak_automaton(aut))
+      return remove_alternation(dualize(aut));
+    // Determinize
+    spot::postprocessor p;
+    p.set_type(spot::postprocessor::Generic);
+    p.set_pref(spot::postprocessor::Deterministic);
+    p.set_level(spot::postprocessor::Low);
+    return dualize(p.run(std::const_pointer_cast<twa_graph>(aut)));
+  }
 }

spot/twaalgos/complement.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2017, 2019 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -52,4 +52,26 @@ namespace spot
   /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16).
   SPOT_API twa_graph_ptr
   complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false);
+
+
+  /// \brief Complement a TωA
+  ///
+  /// This employs different complementation strategies depending
+  /// on the type of the automaton.
+  ///
+  /// If the input is alternating, the output may be alternating and
+  /// is simply the result of calling dualize().
+  ///
+  /// If the input is not alternating, the output will not be
+  /// alternating, but could have any acceptance condition.
+  /// - deterministic inputs are passed to dualize()
+  /// - very weak automata are also dualized, and then
+  ///   passed to remove_alternation() to obtain a TGBA
+  /// - any other type of input is determized before
+  ///   complementation.
+  ///
+  /// complement_semidet() is not yet used.
+  SPOT_API twa_graph_ptr
+  complement(const const_twa_graph_ptr& aut);
+
 }

spot/twaalgos/contains.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2018 Laboratoire de Recherche et Développement de
+// Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
 // l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -19,27 +19,14 @@
 
 #include "config.h"
 #include <spot/twaalgos/contains.hh>
-#include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/isdet.hh>
-#include <spot/twaalgos/dualize.hh>
 
 namespace spot
 {
   namespace
   {
-    static spot::const_twa_graph_ptr
-    ensure_deterministic(const spot::const_twa_graph_ptr& aut)
-    {
-      if (spot::is_deterministic(aut))
-        return aut;
-      spot::postprocessor p;
-      p.set_type(spot::postprocessor::Generic);
-      p.set_pref(spot::postprocessor::Deterministic);
-      p.set_level(spot::postprocessor::Low);
-      return p.run(std::const_pointer_cast<twa_graph>(aut));
-    }
-
     static spot::const_twa_graph_ptr
     translate(formula f, const bdd_dict_ptr& dict)
     {
@@ -49,25 +36,22 @@ namespace spot
 
   bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right)
   {
-    return !right->intersects(dualize(ensure_deterministic(left)));
+    return !complement(left)->intersects(right);
   }
 
   bool contains(const_twa_graph_ptr left, formula right)
   {
-    auto right_aut = translate(right, left->get_dict());
+    return contains(left, translate(right, left->get_dict()));
-    return !right_aut->intersects(dualize(ensure_deterministic(left)));
   }
 
   bool contains(formula left, const_twa_graph_ptr right)
   {
-    return !right->intersects(translate(formula::Not(left), right->get_dict()));
+    return !translate(formula::Not(left), right->get_dict())->intersects(right);
   }
 
   bool contains(formula left, formula right)
   {
-    auto dict = make_bdd_dict();
+    return contains(left, translate(right, make_bdd_dict()));
-    auto right_aut = translate(right, dict);
-    return !right_aut->intersects(translate(formula::Not(left), dict));
   }
 
   bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right)

spot/twaalgos/powerset.cc

@@ -463,12 +463,9 @@ namespace spot
         neg_aut = scc_filter(neg_aut, true);
       }
 
-    if (product(det, neg_aut)->is_empty())
+    if (!det->intersects(neg_aut) && !aut->intersects(dualize(det)))
-      // Complement the DBA.
+      // Determinization was safe.
-      if (product(aut, remove_fin(dualize(det)))->is_empty())
+      return det;
-        // Finally, we are now sure that it was safe
-        // to determinize the automaton.
-        return det;
 
     return aut;
   }

spot/twaalgos/stutter.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de
+// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -28,9 +28,8 @@
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/isdet.hh>
-#include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/remfin.hh>
-#include <spot/twaalgos/postproc.hh>
 #include <spot/twaalgos/sccinfo.hh>
 #include <spot/twa/twaproduct.hh>
 #include <spot/twa/bddprint.hh>
@@ -602,16 +601,7 @@ namespace spot
       bool own_nf = false;
       if (!aut_nf)
         {
-          twa_graph_ptr tmp = aut_f;
+          aut_nf = complement(aut_f);
-          if (!is_deterministic(aut_f))
-            {
-              spot::postprocessor p;
-              p.set_type(spot::postprocessor::Generic);
-              p.set_pref(spot::postprocessor::Deterministic);
-              p.set_level(spot::postprocessor::Low);
-              tmp = p.run(aut_f);
-            }
-          aut_nf = dualize(std::move(tmp));
           own_nf = true;
         }
       bool res = do_si_check(aut_f, own_f,
@@ -709,13 +699,7 @@ namespace spot
       return res;
 
     if (neg == nullptr)
-      {
+      neg = complement(pos);
-        spot::postprocessor p;
-        p.set_type(spot::postprocessor::Generic);
-        p.set_pref(spot::postprocessor::Deterministic);
-        p.set_level(spot::postprocessor::Low);
-        neg = dualize(p.run(std::const_pointer_cast<twa_graph>(pos)));
-      }
 
     auto product_states = [](const const_twa_graph_ptr& a)
       {
@@ -782,13 +766,7 @@ namespace spot
       return res;
 
     if (neg == nullptr)
-      {
+      neg = complement(pos);
-        spot::postprocessor p;
-        p.set_type(spot::postprocessor::Generic);
-        p.set_pref(spot::postprocessor::Deterministic);
-        p.set_level(spot::postprocessor::Low);
-        neg = dualize(p.run(std::const_pointer_cast<twa_graph>(pos)));
-      }
 
     auto product_states = [](const const_twa_graph_ptr& a)
       {

tests/core/complement.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -105,17 +105,17 @@ HOA: v1
 States: 2
 Start: 0
 AP: 2 "a" "b"
-acc-name: parity min even 2
+acc-name: Buchi
-Acceptance: 2 Inf(0) | Fin(1)
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0
-[!0 | !1] 0
+[!0 | !1] 0 {0}
-[0&1] 1 {1}
+[0&1] 1
 State: 1
 [!0 | !1] 0 {0}
-[0&1] 1 {1}
+[0&1] 1
 --END--
 EOF
 diff out expected
@@ -128,17 +128,17 @@ HOA: v1
 States: 2
 Start: 0
 AP: 1 "a"
-acc-name: parity min even 2
+acc-name: Buchi
-Acceptance: 2 Inf(0) | Fin(1)
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0
-[!0] 0
+[!0] 0 {0}
-[0] 1 {1}
+[0] 1
 State: 1
 [!0] 0 {0}
-[0] 1 {1}
+[0] 1
 --END--
 EOF
 diff out expected