implement NCSB complementation

* spot/twaalgos/isdet.cc,spot/twaalgos/isdet.hh: Two new functions to
highlight deterministic SCCs
* spot/twaalgos/complement.cc,spot/twaalgos/complement.hh:
Implementation of the NCSB complementation algorithm
* tests/Makefile.am, tests/python/complement_semidet.py: Test the
implementation
* NEWS: document function

NEWS

@@ -201,6 +201,12 @@ New in spot 2.5.3.dev  (not yet released)
     looking for differences.  See also
     https://spot.lrde.epita.fr/ipynb/contains.html
 
+  - spot::complement_semidet(aut) is a new function that returns the
+    complement of aut, where aut is a semideterministic automaton. The
+    function uses the NCSB complementation algorithm proposed by
+    F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai
+    (TACAS'16).
+
   - spot::remove_alternation() was slightly improved on very-weak
     alternating automata: the labeling of the outgoing transitions in
     the resulting TGBA makes it more likely that simulation-based

spot/twaalgos/complement.cc

@@ -18,10 +18,12 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+#include <deque>
+#include <map>
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/isdet.hh>
-
+#include <spot/twaalgos/sccinfo.hh>
 
 namespace spot
 {
@@ -34,4 +36,488 @@ namespace spot
 
     return dualize(aut);
   }
+
+  namespace
+  {
+    enum ncsb
+      {
+        ncsb_n = 0,       // non deterministic
+        ncsb_c = 2,       // needs check
+        ncsb_cb = 3,      // needs check AND in breakpoint
+        ncsb_s = 4,       // safe
+        ncsb_m = 1,       // missing
+      };
+
+    typedef std::vector<ncsb> mstate;
+    typedef std::vector<std::pair<unsigned, ncsb>> small_mstate;
+
+    struct small_mstate_hash
+    {
+      size_t
+      operator()(small_mstate s) const noexcept
+      {
+        size_t hash = 0;
+        for (const auto& p: s)
+          {
+            hash = wang32_hash(hash ^ ((p.first<<2) | p.second));
+          }
+        return hash;
+      }
+    };
+
+    class ncsb_complementation
+    {
+    private:
+      // The source automaton.
+      const const_twa_graph_ptr aut_;
+
+      // SCCs information of the source automaton.
+      scc_info si_;
+
+      // Number of states in the input automaton.
+      unsigned nb_states_;
+
+      // The complement being built.
+      twa_graph_ptr res_;
+
+      // Association between NCSB states and state numbers of the
+      // complement.
+      std::unordered_map<small_mstate, unsigned, small_mstate_hash> ncsb2n_;
+
+      // States to process.
+      std::deque<std::pair<mstate, unsigned>> todo_;
+
+      // Support for each state of the source automaton.
+      std::vector<bdd> support_;
+
+      // Propositions compatible with all transitions of a state.
+      std::vector<bdd> compat_;
+
+      // Whether a SCC is deterministic or not
+      std::vector<bool> is_deter_;
+
+      // Whether a state only has accepting transitions
+      std::vector<bool> is_accepting_;
+
+      // State names for graphviz display
+      std::vector<std::string>* names_;
+
+      // Show NCSB states in state name to help debug
+      bool show_names_;
+
+      std::string
+      get_name(const small_mstate& ms)
+      {
+        std::string res = "{";
+
+        bool first_state = true;
+        for (const auto& p: ms)
+          if (p.second == ncsb_n)
+            {
+              if (!first_state)
+                res += ",";
+              first_state = false;
+              res += std::to_string(p.first);
+            }
+
+        res += "},{";
+
+        first_state = true;
+        for (const auto& p: ms)
+          if (p.second & ncsb_c)
+            {
+              if (!first_state)
+                res += ",";
+              first_state = false;
+              res += std::to_string(p.first);
+            }
+
+        res += "},{";
+
+        first_state = true;
+        for (const auto& p: ms)
+          if (p.second == ncsb_s)
+            {
+              if (!first_state)
+                res += ",";
+              first_state = false;
+              res += std::to_string(p.first);
+            }
+
+        res += "},{";
+
+        first_state = true;
+        for (const auto& p: ms)
+          if (p.second == ncsb_cb)
+            {
+              if (!first_state)
+                res += ",";
+              first_state = false;
+              res += std::to_string(p.first);
+            }
+
+        return res + "}";
+      }
+
+      small_mstate
+      to_small_mstate(const mstate& ms)
+      {
+        unsigned count = 0;
+        for (unsigned i = 0; i < nb_states_; ++i)
+          count+= (ms[i] != ncsb_m);
+        small_mstate small;
+        small.reserve(count);
+        for (unsigned i = 0; i < nb_states_; ++i)
+          if (ms[i] != ncsb_m)
+            small.emplace_back(i, ms[i]);
+        return small;
+      }
+
+      // From a NCSB state, looks for a duplicate in the map before
+      // creating a new state if needed.
+      unsigned
+      new_state(mstate&& s)
+      {
+        auto p = ncsb2n_.emplace(to_small_mstate(s), 0);
+        if (p.second) // This is a new state
+          {
+            p.first->second = res_->new_state();
+            if (show_names_)
+              names_->push_back(get_name(p.first->first));
+            todo_.emplace_back(std::move(s), p.first->second);
+          }
+        return p.first->second;
+      }
+
+      void
+      ncsb_successors(mstate&& ms, unsigned origin, bdd letter)
+      {
+        std::vector<mstate> succs;
+        succs.emplace_back(nb_states_, ncsb_m);
+
+        // Handle S states.
+        //
+        // Treated first because we can escape early if the letter
+        // leads to an accepting transition for a Safe state.
+        for (unsigned i = 0; i < nb_states_; ++i)
+          {
+            if (ms[i] != ncsb_s)
+              continue;
+
+            for (const auto& t: aut_->out(i))
+              {
+                if (!bdd_implies(letter, t.cond))
+                  continue;
+                if (t.acc || is_accepting_[t.dst])
+                  // Exit early; transition is forbidden for safe
+                  // state.
+                  return;
+
+                succs[0][t.dst] = ncsb_s;
+
+                // No need to look for other compatible transitions
+                // for this state; it's in the deterministic part of
+                // the automaton
+                break;
+              }
+          }
+
+        // Handle C states.
+        for (unsigned i = 0; i < nb_states_; ++i)
+          {
+            if (!(ms[i] & ncsb_c))
+              continue;
+
+            bool has_succ = false;
+            for (const auto& t: aut_->out(i))
+              {
+                if (!bdd_implies(letter, t.cond))
+                  continue;
+
+                has_succ = true;
+
+                // state can become safe, if transition is accepting
+                // and destination isn't an accepting state
+                if (t.acc)
+                  {
+                    // double all the current possible states
+                    unsigned length = succs.size();
+                    for (unsigned j = 0; j < length; ++j)
+                      {
+                        if (succs[j][t.dst] == ncsb_m)
+                          {
+                            if (!is_accepting_[t.dst])
+                              {
+                                succs.push_back(succs[j]);
+                                succs.back()[t.dst] = ncsb_s;
+                              }
+                            succs[j][t.dst] = ncsb_c;
+                          }
+                      }
+                  }
+                else       // state stays in check
+                  {
+                    auto it = succs.begin();
+                    while (it != succs.end())
+                      {
+                        // remove state if it should stay in s
+                        if ((*it)[t.dst] == ncsb_s)
+                          {
+                            std::iter_swap(it, succs.end() - 1);
+                            succs.pop_back();
+                            continue;
+                          }
+                        (*it)[t.dst] = ncsb_c;
+                        ++it;
+                      }
+                  }
+                // No need to look for other compatible transitions
+                // for this state; it's in the deterministic part of
+                // the automaton
+                break;
+              }
+            if (!has_succ && !is_accepting_[i])
+              return;
+          }
+
+        // Handle N states.
+        for (unsigned i = 0; i < nb_states_; ++i)
+          {
+            if (ms[i] != ncsb_n)
+              continue;
+            for (const auto& t: aut_->out(i))
+              {
+                if (!bdd_implies(letter, t.cond))
+                  continue;
+
+                if (is_deter_[si_.scc_of(t.dst)])
+                  {
+                    // double all the current possible states
+                    unsigned length = succs.size();
+                    for (unsigned j = 0; j < length; ++j)
+                      {
+                        if (succs[j][t.dst] == ncsb_m)
+                          {
+                            // Can become safe if the destination is
+                            // not an accepting state.
+                            if (!is_accepting_[t.dst])
+                              {
+                                succs.push_back(succs[j]);
+                                succs.back()[t.dst] = ncsb_s;
+                              }
+                            succs[j][t.dst] = ncsb_c;
+                          }
+                      }
+                  }
+                else
+                  {
+                    auto it = succs.begin();
+                    while (it != succs.end())
+                      {
+                        // remove state if it should stay in s or c
+                        if ((*it)[t.dst] == ncsb_s
+                            || (*it)[t.dst] == ncsb_c)
+                          {
+                            std::iter_swap(it, succs.end() - 1);
+                            succs.pop_back();
+                            continue;
+                          }
+                        (*it)[t.dst] = ncsb_n;
+                        ++it;
+                      }
+                  }
+              }
+          }
+
+        // Revisit B states to see if they still exist in successors.
+        // This is done at the end because we need to know all of the
+        // states present in C before this stage
+        bool b_empty = true;
+        for (unsigned i = 0; i < nb_states_; ++i)
+          {
+            if (ms[i] != ncsb_cb)
+              continue;
+
+            // The original B set wasn't empty
+            b_empty = false;
+
+            for (const auto& t: aut_->out(i))
+              {
+                if (!bdd_implies(letter, t.cond))
+                  continue;
+
+                for (auto& succ: succs)
+                  {
+                    if (succ[t.dst] == ncsb_c)
+                      succ[t.dst] = ncsb_cb;
+                  }
+
+                // No need to look for other compatible transitions
+                // for this state; it's in the deterministic part of
+                // the automaton
+                break;
+              }
+          }
+
+        // If B was empty, then set every c_not_b to cb in successors
+        if (b_empty)
+          for (auto& succ: succs)
+            for (unsigned i = 0; i < succ.size(); ++i)
+              if (succ[i] == ncsb_c)
+                succ[i] = ncsb_cb;
+
+        // create the automaton states
+        for (auto& succ: succs)
+          {
+            bool b_empty = true;
+            for (const auto& state: succ)
+              if (state == ncsb_cb)
+                {
+                  b_empty = false;
+                  break;
+                }
+            if (b_empty) // becomes accepting
+              {
+                for (unsigned i = 0; i < succ.size(); ++i)
+                  if (succ[i] == ncsb_c)
+                    succ[i] = ncsb_cb;
+                unsigned dst = new_state(std::move(succ));
+                res_->new_edge(origin, dst, letter, {0});
+              }
+            else
+              {
+                unsigned dst = new_state(std::move(succ));
+                res_->new_edge(origin, dst, letter);
+              }
+          }
+      }
+
+    public:
+      ncsb_complementation(const const_twa_graph_ptr& aut, bool show_names)
+        : aut_(aut),
+          si_(aut),
+          nb_states_(aut->num_states()),
+          support_(nb_states_),
+          compat_(nb_states_),
+          is_accepting_(nb_states_),
+          show_names_(show_names)
+      {
+        res_ = make_twa_graph(aut->get_dict());
+        res_->copy_ap_of(aut);
+        res_->set_buchi();
+
+        // Generate bdd supports and compatible options for each state.
+        // Also check if all its transitions are accepting.
+        for (unsigned i = 0; i < nb_states_; ++i)
+          {
+            bdd res_support = bddtrue;
+            bdd res_compat = bddfalse;
+            bool accepting = true;
+            bool has_transitions = false;
+            for (const auto& out: aut->out(i))
+              {
+                has_transitions = true;
+                res_support &= bdd_support(out.cond);
+                res_compat |= out.cond;
+                if (!out.acc)
+                  accepting = false;
+              }
+            support_[i] = res_support;
+            compat_[i] = res_compat;
+            is_accepting_[i] = accepting && has_transitions;
+          }
+
+
+
+        // Compute which SCCs are part of the deterministic set.
+        is_deter_ = semidet_sccs(si_);
+
+        if (show_names_)
+          {
+            names_ = new std::vector<std::string>();
+            res_->set_named_prop("state-names", names_);
+          }
+
+        // Because we only handle one initial state, we assume it
+        // belongs to the N set. (otherwise the automaton would be
+        // deterministic)
+        unsigned init_state = aut->get_init_state_number();
+        mstate new_init_state(nb_states_, ncsb_m);
+        new_init_state[init_state] = ncsb_n;
+        res_->set_init_state(new_state(std::move(new_init_state)));
+      }
+
+      twa_graph_ptr
+      run()
+      {
+        // Main stuff happens here
+
+        while (!todo_.empty())
+          {
+            auto top = todo_.front();
+            todo_.pop_front();
+
+            mstate ms = top.first;
+
+            // Compute support of all available states.
+            bdd msupport = bddtrue;
+            bdd n_s_compat = bddfalse;
+            bdd c_compat = bddtrue;
+            bool c_empty = true;
+            for (unsigned i = 0; i < nb_states_; ++i)
+              if (ms[i] != ncsb_m)
+                {
+                  msupport &= support_[i];
+                  if (ms[i] == ncsb_n || ms[i] == ncsb_s || is_accepting_[i])
+                    n_s_compat |= compat_[i];
+                  else
+                    {
+                      c_empty = false;
+                      c_compat &= compat_[i];
+                    }
+                }
+
+            bdd all;
+            if (!c_empty)
+              all = c_compat;
+            else
+              {
+                all = n_s_compat;
+                if (all != bddtrue)
+                  {
+                    mstate empty_state(nb_states_, ncsb_m);
+                    res_->new_edge(top.second,
+                                   new_state(std::move(empty_state)),
+                                   !all,
+                                   {0});
+                  }
+              }
+            while (all != bddfalse)
+              {
+                bdd one = bdd_satoneset(all, msupport, bddfalse);
+                all -= one;
+
+                // Compute all new states available from the generated
+                // letter.
+                ncsb_successors(std::move(ms), top.second, one);
+              }
+          }
+
+        res_->merge_edges();
+        return res_;
+      }
+    };
+
+  }
+
+  twa_graph_ptr
+  complement_semidet(const const_twa_graph_ptr& aut, bool show_names)
+  {
+    if (!is_semi_deterministic(aut))
+      throw std::runtime_error
+        ("complement_semidet() requires a semi-deterministic input");
+
+    auto ncsb = ncsb_complementation(aut, show_names);
+    return ncsb.run();
+  }
 }

spot/twaalgos/complement.hh

@@ -43,4 +43,13 @@ namespace spot
   SPOT_DEPRECATED("use spot::dualize() instead")
   SPOT_API twa_graph_ptr
   dtwa_complement(const const_twa_graph_ptr& aut);
+
+  /// \brief Complement a semideterministic TωA
+  ///
+  /// The automaton \a aut should be semideterministic.
+  ///
+  /// Uses the NCSB algorithm described by F. Blahoudek, M. Heizmann,
+  /// 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);
 }

spot/twaalgos/isdet.cc

@@ -138,6 +138,24 @@ namespace spot
     aut->prop_universal(universal);
   }
 
+  void highlight_semidet_sccs(scc_info& si, unsigned color)
+  {
+    auto det_sccs = semidet_sccs(si);
+    if (det_sccs.empty())
+      return;
+    auto aut = si.get_aut();
+    auto* highlight = std::const_pointer_cast<twa_graph>(aut)
+      ->get_or_set_named_prop<std::map<unsigned, unsigned>>("highlight-states");
+    for (unsigned scc = 0; scc < si.scc_count(); scc++)
+      {
+        if (det_sccs[scc])
+          {
+            for (auto& t : si.states_of(scc))
+              (*highlight)[t] = color;
+          }
+      }
+  }
+
   bool
   is_complete(const const_twa_graph_ptr& aut)
   {
@@ -238,6 +256,49 @@ namespace spot
     }
   }
 
+  std::vector<bool> semidet_sccs(scc_info& si)
+  {
+    const_twa_graph_ptr aut = si.get_aut();
+    trival sd = aut->prop_semi_deterministic();
+    if (sd.is_known() && sd.is_false())
+      return std::vector<bool>();
+    si.determine_unknown_acceptance();
+    unsigned nscc = si.scc_count();
+    assert(nscc);
+    std::vector<bool> reachable_from_acc(nscc);
+    std::vector<bool> res(nscc);
+    bool semi_det = true;
+    do // iterator of SCCs in reverse topological order
+      {
+        --nscc;
+        if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc])
+          {
+            for (unsigned succ: si.succ(nscc))
+              reachable_from_acc[succ] = true;
+            for (unsigned src: si.states_of(nscc))
+              {
+                bdd available = bddtrue;
+                for (auto& t: aut->out(src))
+                  if (!bdd_implies(t.cond, available))
+                    {
+                      semi_det = false;
+                      goto done;
+                    }
+                  else
+                    {
+                      available -= t.cond;
+                    }
+              }
+            res[nscc] = true;
+          }
+      }
+    while (nscc);
+  done:
+    if (!semi_det)
+      return std::vector<bool>();
+    return res;
+  }
+
   bool
   is_semi_deterministic(const const_twa_graph_ptr& aut)
   {

spot/twaalgos/isdet.hh

@@ -19,6 +19,7 @@
 
 #pragma once
 
+#include <spot/twaalgos/sccinfo.hh>
 #include <spot/twa/twagraph.hh>
 
 namespace spot
@@ -77,6 +78,16 @@ namespace spot
   highlight_nondet_edges(twa_graph_ptr& aut, unsigned color);
   /// @}
 
+  /// \brief Highlight the deterministic part of the automaton
+  ///
+  /// In the case of a semideterministic automaton, highlights the
+  /// states reachable from any accepting SCC.
+  ///
+  /// \param aut the automaton to process
+  /// \param color the color to give to states reachable from accepting SCCs.
+  SPOT_API void
+  highlight_semidet_sccs(scc_info& si, unsigned color);
+
   /// \brief Return true iff \a aut is complete.
   ///
   /// An automaton is complete if its translation relation is total,
@@ -91,6 +102,10 @@ namespace spot
   SPOT_API bool
   is_semi_deterministic(const const_twa_graph_ptr& aut);
 
+  /// \brief Whether an SCC is in the deterministic part of an automaton
+  SPOT_API std::vector<bool>
+  semidet_sccs(scc_info& si);
+
   /// \brief Set the deterministic and semi-deterministic properties
   /// appropriately.
   SPOT_API void check_determinism(twa_graph_ptr aut);

tests/Makefile.am

@@ -366,6 +366,7 @@ TESTS_python = \
   python/bdditer.py \
   python/bddnqueen.py \
   python/bugdet.py \
+  python/complement_semidet.py \
   python/declenv.py \
   python/_word.ipynb \
   python/decompose_scc.py \

tests/python/complement_semidet.py

@@ -0,0 +1,38 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+import spot
+import buddy
+
+
+def complement(aut):
+    return spot.dualize(aut.postprocess('det', 'gen'))
+
+
+n = 10000
+
+for aut in spot.automata(
+        "randltl -n-1 a b "
+        "| ltl2tgba "
+        "| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{} |"
+        .format(n)):
+
+    comp = complement(aut)
+    semidet_comp = spot.complement_semidet(aut, True)
+    assert(comp.equivalent_to(semidet_comp))