diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am
index f463a9e6a..a98d105f2 100644
--- a/spot/mc/Makefile.am
+++ b/spot/mc/Makefile.am
@@ -25,6 +25,6 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
-mc_HEADERS = reachability.hh
+mc_HEADERS = reachability.hh intersect.hh
noinst_LTLIBRARIES = libmc.la
diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh
new file mode 100644
index 000000000..8605ba073
--- /dev/null
+++ b/spot/mc/intersect.hh
@@ -0,0 +1,258 @@
+// -*- 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 .
+
+#pragma once
+
+#include
+#include
+#include
+
+namespace spot
+{
+ /// \brief This class explores (with a DFS) a product between a
+ /// system and a twa. This exploration is performed on-the-fly.
+ /// Since this exploration aims to be a generic we need to define
+ /// hooks to the various emptiness checks.
+ /// Actually, we use "mixins templates" in order to efficiently
+ /// call emptiness check procedure. This means that we add
+ /// a template \a EmptinessCheck that will be called though
+ /// four functions:
+ /// - setup: called before any operation
+ /// - push: called for every new state
+ /// - pop: called every time a state leave the DFS stack
+ /// - update: called for every closing edge
+ /// - trace: must return a counterexample (if exists)
+ ///
+ /// The other template parameters allows to consider any kind
+ /// of state (and so any kind of kripke structures).
+ template
+ class SPOT_API intersect
+ {
+ public:
+ intersect(kripkecube& sys,
+ twacube* twa):
+ sys_(sys), twa_(twa)
+ {
+ assert(is_a_kripkecube(sys));
+ map.reserve(2000000);
+ todo.reserve(100000);
+ }
+
+ ~intersect()
+ {
+ map.clear();
+ }
+
+ /// \brief In order to implement "mixin paradigm", we
+ /// must be abble to access the acual definition of
+ /// the emptiness check that, in turn, has to access
+ /// local variables.
+ EmptinessCheck& self()
+ {
+ return static_cast(*this);
+ }
+
+ /// \brief The main function that will perform the
+ /// product on-the-fly and call the emptiness check
+ /// when necessary.
+ bool run()
+ {
+ self().setup();
+ product_state initial = {sys_.initial(), twa_->get_initial()};
+ if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U)))
+ {
+ todo.push_back({initial, sys_.succ(initial.st_kripke),
+ twa_->succ(initial.st_prop)});
+
+ // Not going further! It's a product with a single state.
+ if (todo.back().it_prop->done())
+ return false;
+
+ forward_iterators(true);
+ map[initial] = ++dfs_number;
+ }
+ while (!todo.empty())
+ {
+ // Check the kripke is enough since it's the outer loop. More
+ // details in forward_iterators.
+ if (todo.back().it_kripke->done())
+ {
+ bool is_init = todo.size() == 1;
+ auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
+ if (SPOT_LIKELY(self().pop_state(todo.back().st,
+ map[todo.back().st],
+ is_init,
+ newtop,
+ map[newtop])))
+ {
+ sys_.recycle(todo.back().it_kripke);
+ // FIXME a local storage for twacube iterator?
+ todo.pop_back();
+ if (SPOT_UNLIKELY(self().counterexample_found()))
+ return true;
+ }
+ }
+ else
+ {
+ ++transitions;
+ product_state dst = {
+ todo.back().it_kripke->state(),
+ twa_->trans_storage(todo.back().it_prop).dst
+ };
+ auto acc = twa_->trans_data(todo.back().it_prop).acc_;
+ forward_iterators(false);
+ auto it = map.find(dst);
+ if (it == map.end())
+ {
+ if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
+ {
+ map[dst] = ++dfs_number;
+ todo.push_back({dst, sys_.succ(dst.st_kripke),
+ twa_->succ(dst.st_prop)});
+ forward_iterators(true);
+ }
+ }
+ else if (SPOT_UNLIKELY(self().update(todo.back().st,
+ dfs_number,
+ dst, map[dst], acc)))
+ return true;
+ }
+ }
+ return false;
+ }
+
+ unsigned int states()
+ {
+ return dfs_number;
+ }
+
+ unsigned int trans()
+ {
+ return transitions;
+ }
+
+ std::string counterexample()
+ {
+ return self().trace();
+ }
+
+
+ virtual std::string stats()
+ {
+ return
+ std::to_string(dfs_number) + " unique states visited\n" +
+ std::to_string(transitions) + " transitions explored\n";
+ }
+
+ protected:
+
+ /// \brief Find the first couple of iterator (from the top of the
+ /// todo stack) that intersect. The \a parameter indicates wheter
+ /// the state has just been pushed since the underlying job
+ /// is slightly different.
+ void forward_iterators(bool just_pushed)
+ {
+ assert(!todo.empty());
+ assert(!(todo.back().it_prop->done() && todo.back().it_kripke->done()));
+
+ // Sometimes kripke state may have no successors.
+ if (todo.back().it_kripke->done())
+ return;
+
+ // The state has just been push and the 2 iterators intersect.
+ // There is no need to move iterators forward.
+ assert(!(todo.back().it_prop->done()));
+ if (just_pushed && twa_->get_cubeset()
+ .intersect(twa_->trans_data(todo.back().it_prop).cube_,
+ todo.back().it_kripke->condition()))
+ return;
+
+ // Otherwise we have to compute the next valid successor (if it exits).
+ // This requires two loops. The most inner one is for the twacube since
+ // its costless
+ if (todo.back().it_prop->done())
+ todo.back().it_prop->reset();
+ else
+ todo.back().it_prop->next();
+
+ while (!todo.back().it_kripke->done())
+ {
+ while (!todo.back().it_prop->done())
+ {
+ if (SPOT_UNLIKELY(twa_->get_cubeset()
+ .intersect(twa_->trans_data(todo.back().it_prop).cube_,
+ todo.back().it_kripke->condition())))
+ return;
+ todo.back().it_prop->next();
+ }
+ todo.back().it_prop->reset();
+ todo.back().it_kripke->next();
+ }
+ }
+
+ public:
+ struct product_state
+ {
+ State st_kripke;
+ unsigned st_prop;
+ };
+
+ struct product_state_equal
+ {
+ bool
+ operator()(const product_state lhs,
+ const product_state rhs) const
+ {
+ StateEqual equal;
+ return (lhs.st_prop == rhs.st_prop) &&
+ equal(lhs.st_kripke, rhs.st_kripke);
+ }
+ };
+
+ struct product_state_hash
+ {
+ size_t
+ operator()(const product_state that) const
+ {
+ // FIXME! wang32_hash(that.st_prop) could have
+ // been pre-calculated!
+ StateHash hasher;
+ return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
+ }
+ };
+
+ struct todo_element
+ {
+ product_state st;
+ SuccIterator* it_kripke;
+ std::shared_ptr it_prop;
+ };
+ kripkecube& sys_;
+ twacube* twa_;
+ std::vector todo;
+ typedef std::unordered_map visited_map;
+ visited_map map;
+ unsigned int dfs_number = 0;
+ unsigned int transitions = 0;
+ };
+}