ec: Renault et al LPAR'13 emptiness check

In order to reuse the computation of the
intersection between kripke and twa efficiently,
we use template inheritance through the
"mixin templates" technique.

* spot/Makefile.am, spot/mc/Makefile.am,
spot/mc/ec.hh, spot/mc/unionfind.cc,
spot/mc/unionfind.hh: here.

spot/Makefile.am

@@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects
 # end, after building '.' (since the current directory contains
 # libspot.la needed by the tests)
 SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \
-          twacube_algos parseaut parsetl . ltsmin gen
+          twacube_algos mc parseaut parsetl . ltsmin gen
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
@@ -44,6 +44,7 @@ libspot_la_LIBADD =  \
   twa/libtwa.la \
   twacube_algos/libtwacube_algos.la \
   twacube/libtwacube.la \
+  mc/libmc.la \
   ../lib/libgnu.la \
   ../picosat/libpico.la
 

spot/mc/Makefile.am

 ## -*- coding: utf-8 -*-
-## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
-## de Recherche et Développement de l'Epita (LRDE).
-## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
-## et Marie Curie.
+## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
+## l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -24,7 +21,9 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 mcdir = $(pkgincludedir)/mc
-
-mc_HEADERS = reachability.hh intersect.hh
+mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh
 
 noinst_LTLIBRARIES = libmc.la
+
+libmc_la_SOURCES = \
+  unionfind.cc

spot/mc/ec.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et
+// Developpement de l'Epita
+//
+// 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/>.
+
+#pragma once
+
+#include <spot/twa/acc.hh>
+#include <spot/mc/unionfind.hh>
+#include <spot/mc/intersect.hh>
+
+namespace spot
+{
+  /// \brief This class implements the sequential emptiness check as
+  /// presented in "Three SCC-based Emptiness Checks for Generalized
+  /// B\¨uchi Automata" (Renault et al, LPAR 2013). Among the three
+  /// emptiness check that has been proposed we opted to implement
+  /// the Gabow's one.
+  template<typename State, typename SuccIterator,
+	   typename StateHash, typename StateEqual>
+  class ec_renault13lpar  : public intersect<State, SuccIterator,
+				       StateHash, StateEqual,
+				       ec_renault13lpar<State, SuccIterator,
+							StateHash, StateEqual>>
+  {
+    // Ease the manipulation
+    using typename intersect<State, SuccIterator, StateHash, StateEqual,
+			     ec_renault13lpar<State, SuccIterator,
+					      StateHash,
+					      StateEqual>>::product_state;
+
+  public:
+    ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
+                     twacube* twa)
+      : intersect<State, SuccIterator, StateHash, StateEqual,
+		  ec_renault13lpar<State, SuccIterator,
+				   StateHash, StateEqual>>(sys, twa),
+      acc_(twa->acc())
+      {
+      }
+
+    virtual ~ec_renault13lpar()
+    {
+
+    }
+
+    /// \brief This method is called at the begining of the exploration.
+    /// here we do not need to setup any information.
+    void setup()
+    {
+    }
+
+    /// \brief This method is called to notify the emptiness checks
+    /// that a new state has been discovered. If this method return
+    /// false, the state will not be explored. The parameter \a dfsnum
+    /// specify an unique id for the state \a s. Parameter \a cond represents
+    /// The value on the ingoing edge to \a s.
+    bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond)
+    {
+      uf_.makeset(dfsnum);
+      roots_.push_back({dfsnum, cond, 0U});
+      return true;
+    }
+
+    /// \brief This method is called to notify the emptiness checks
+    /// that a state will be popped. If the method return false, then
+    /// the state will be popped. Otherwise the state \a newtop will
+    /// become the new top of the DFS stack. If the state \a top is
+    /// the only one in the DFS stak, the parameter \a is_initial is set
+    /// to true and both \a newtop and \a  newtop_dfsnum have inconsistency
+    /// values.
+    bool pop_state(product_state, unsigned top_dfsnum, bool,
+  		   product_state, unsigned)
+    {
+      if (top_dfsnum == roots_.back().dfsnum)
+  	{
+  	  roots_.pop_back();
+  	  uf_.markdead(top_dfsnum);
+  	}
+      return true;
+    }
+
+    /// \brief This method is called for every closing, back, or forward edge.
+    /// Return true if a counterexample has been found.
+    bool update(product_state, unsigned,
+                product_state, unsigned dst_dfsnum,
+                acc_cond::mark_t cond)
+    {
+      if (uf_.isdead(dst_dfsnum))
+  	return false;
+
+      while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
+        {
+          auto& el = roots_.back();
+          roots_.pop_back();
+          uf_.unite(dst_dfsnum, el.dfsnum);
+          cond |= el.acc | el.ingoing;
+        }
+      roots_.back().acc |= cond;
+      found_ = acc_.accepting(roots_.back().acc);
+      return found_;
+    }
+
+    bool counterexample_found()
+    {
+      return found_;
+    }
+
+    std::string trace()
+    {
+      assert(counterexample_found());
+      std::string res = "Prefix:\n";
+
+       // Compute the prefix of the accepting run
+      for (auto& s : this->todo)
+      	res += "  " + std::to_string(s.st.st_prop) +
+      	  + "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
+
+      // Compute the accepting cycle
+      res += "Cycle:\n";
+
+      struct ctrx_element
+      {
+	const product_state* prod_st;
+	ctrx_element* parent_st;
+	SuccIterator* it_kripke;
+	std::shared_ptr<trans_index> it_prop;
+      };
+      std::queue<ctrx_element*> bfs;
+
+      acc_cond::mark_t acc = 0U;
+
+      bfs.push(new ctrx_element({&this->todo.back().st, nullptr,
+              this->sys_.succ(this->todo.back().st.st_kripke),
+              this->twa_->succ(this->todo.back().st.st_prop)}));
+      while (true)
+	{
+	here:
+	  auto* front = bfs.front();
+	  bfs.pop();
+	  // PUSH all successors of the state.
+	  while (!front->it_kripke->done())
+	    {
+	      while (!front->it_prop->done())
+		{
+		  if (this->twa_->get_cubeset().intersect
+		      (this->twa_->trans_data(front->it_prop).cube_,
+		       front->it_kripke->condition()))
+		    {
+		      const product_state dst = {
+			front->it_kripke->state(),
+			this->twa_->trans_storage(front->it_prop).dst
+		      };
+
+		      // Skip Unknown states or not same SCC
+		      auto it  = this->map.find(dst);
+		      if (it == this->map.end() ||
+			  !uf_.sameset(it->second,
+				       this->map[this->todo.back().st]))
+			{
+			  front->it_prop->next();
+			  continue;
+			}
+
+		      // This is a valid transition. If this transition
+		      // is the one we are looking for, update the counter-
+		      // -example and flush the bfs queue.
+		      auto mark = this->twa_->trans_data(front->it_prop).acc_;
+		      if (!acc.has(mark))
+			{
+			  ctrx_element* current = front;
+			  while (current != nullptr)
+			    {
+			      // FIXME also display acc?
+			      res = res + "  " +
+				std::to_string(current->prod_st->st_prop) +
+				+ "*" +
+				this->sys_. to_string(current->prod_st
+						      ->st_kripke) +
+				"\n";
+			      current = current->parent_st;
+			    }
+
+			  // empty the queue
+			  while (!bfs.empty())
+			    {
+			      auto* e = bfs.front();
+			      bfs.pop();
+			      delete e;
+			    }
+
+			  // update acceptance
+			  acc |= mark;
+			  if (this->twa_->acc().accepting(acc))
+			    return res;
+
+                          const product_state* q = &(it->first);
+                          ctrx_element* root = new ctrx_element({
+                              q , nullptr,
+                              this->sys_.succ(q->st_kripke),
+                              this->twa_->succ(q->st_prop)
+                          });
+                          bfs.push(root);
+                          goto here;
+                        }
+
+                      // Otherwise increment iterator and push successor.
+                      const product_state* q = &(it->first);
+                      ctrx_element* root = new ctrx_element({
+                          q , nullptr,
+                          this->sys_.succ(q->st_kripke),
+                          this->twa_->succ(q->st_prop)
+                      });
+                      bfs.push(root);
+                    }
+                  front->it_prop->next();
+                }
+              front->it_prop->reset();
+              front->it_kripke->next();
+            }
+        }
+
+      // never reach here;
+      return res;
+    }
+
+    // Refine stats to display
+    virtual std::string stats() override
+    {
+      return
+	std::to_string(this->dfs_number) + " unique states visited\n" +
+	std::to_string(roots_.size()) +
+	" strongly connected components in search stack\n" +
+	std::to_string(this->transitions) + " transitions explored\n";
+    }
+
+  private:
+
+    bool found_ = false;	///< \brief A counterexample is detected?
+
+    struct root_element {
+      unsigned dfsnum;
+      acc_cond::mark_t ingoing;
+      acc_cond::mark_t acc;
+    };
+
+    /// \brief the root stack.
+    std::vector<root_element> roots_;
+    int_unionfind uf_;
+    acc_cond acc_;
+  };
+}

spot/mc/unionfind.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et
+// Developpement de l'Epita
+//
+// 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/>.
+
+#include <spot/mc/unionfind.hh>
+#include <assert.h>
+
+namespace spot
+{
+  int int_unionfind::root(int i)
+  {
+    assert(i > 0);
+    int p = id[i];
+    if (p == DEAD)
+      return DEAD;
+    if (p < 0)
+      return i;
+    int gp = id[p];
+    if (gp == DEAD)
+      return DEAD;
+    if (gp < 0)
+      return p;
+    p = root(p);
+    id[i] = p;
+    return p;
+  }
+
+  int_unionfind::int_unionfind() : id()
+  {
+    id.push_back(DEAD);
+  }
+
+  void int_unionfind::makeset(int e)
+  {
+    assert(e == (int) id.size());
+    id.push_back(-1);
+  }
+
+  bool int_unionfind::unite(int e1, int e2)
+  {
+    // IPC - Immediate Parent Check
+    int p1 = id[e1];
+    int p2 = id[e2];
+    if ((p1 < 0 ? e1 : p1) == (p2 < 0 ? e2 : p2))
+      return false;
+    int root1 = root(e1);
+    int root2 = root(e2);
+    if (root1 == root2)
+      return false;
+    int rk1 = -id[root1];
+    int rk2 = -id[root2];
+    if (rk1 < rk2)
+      id[root1] = root2;
+    else {
+      id[root2] = root1;
+      if (rk1 == rk2)
+	id[root1] = -(rk1 + 1);
+    }
+    return true;
+  }
+
+  void int_unionfind::markdead(int e)
+  {
+    id[root(e)] = DEAD;
+  }
+
+  bool int_unionfind::sameset(int e1, int e2)
+  {
+    assert(e1 < (int)id.size() && e2 < (int)id.size());
+    return root(e1) == root(e2);
+  }
+
+  bool int_unionfind::isdead(int e)
+  {
+    assert(e < (int)id.size());
+    return root(e) == DEAD;
+  }
+}

spot/mc/unionfind.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et
+// Developpement de l'Epita
+//
+// 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/>.
+
+#pragma once
+
+#include <spot/misc/common.hh>
+#include <vector>
+
+namespace spot
+{
+
+  /// \brief This Union-Find data structure is a particular
+  /// union-find, dedicated for emptiness checks below, see ec.hh. The
+  /// key of this union-find is int. Moreover, we suppose that only
+  /// consecutive int are inserted. This union-find includes most of
+  /// the classical optimisations (IPC, LR, PC, MS).
+  class SPOT_API int_unionfind final
+  {
+  private:
+    // Store the parent relation, i.e. -1 or x < id.size()
+    std::vector<int> id;
+
+    // id of a specially managed partition of "dead" elements
+    const int DEAD = 0;
+
+    int root(int i);
+
+  public:
+    int_unionfind();
+    void makeset(int e);
+    bool unite(int e1, int e2);
+    void markdead(int e);
+    bool sameset(int e1, int e2);
+    bool isdead(int e);
+  };
+}