diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am
index 2bc3291b2..35f90e11f 100644
--- a/spot/mc/Makefile.am
+++ b/spot/mc/Makefile.am
@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
-mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh
+mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh
noinst_LTLIBRARIES = libmc.la
diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh
new file mode 100644
index 000000000..d3468365b
--- /dev/null
+++ b/spot/mc/utils.hh
@@ -0,0 +1,214 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 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
+#include
+
+namespace spot
+{
+ template
+ class SPOT_API kripke_to_twa :
+ public seq_reach_kripke>
+ {
+ public:
+ kripke_to_twa(kripkecube& sys, bdd_dict_ptr dict)
+ : seq_reach_kripke>(sys),
+ dict_(dict)
+ {}
+
+ ~kripke_to_twa()
+ {
+ }
+
+ void setup()
+ {
+ res_ = make_twa_graph(dict_);
+ names_ = new std::vector();
+
+ // padding to simplify computation.
+ res_->new_state();
+
+ // Compute the reverse binder.
+ auto aps = this->sys_.get_ap();
+ for (unsigned i = 0; i < aps.size(); ++i)
+ {
+ auto k = res_->register_ap(aps[i]);
+ reverse_binder_.insert({i, k});
+ }
+ }
+
+ void push(State s, unsigned i)
+ {
+ unsigned st = res_->new_state();
+ names_->push_back(this->sys_.to_string(s));
+ assert(st == i);
+ }
+
+ void edge(unsigned src, unsigned dst)
+ {
+ cubeset cs(this->sys_.get_ap().size());
+ bdd cond = cube_to_bdd(this->todo.back().it->condition(),
+ cs, reverse_binder_);
+ res_->new_edge(src, dst, cond);
+ }
+
+ void finalize()
+ {
+ res_->set_init_state(1);
+ res_->purge_unreachable_states();
+ res_->set_named_prop>("state-names", names_);
+ }
+
+ twa_graph_ptr twa()
+ {
+ return res_;
+ }
+
+ private:
+ spot::twa_graph_ptr res_;
+ std::vector* names_;
+ bdd_dict_ptr dict_;
+ std::unordered_map reverse_binder_;
+
+ };
+
+
+
+ template
+ class SPOT_API product_to_twa :
+ public intersect>
+ {
+ // Ease the manipulation
+ using typename intersect>::product_state;
+
+ public:
+ product_to_twa(kripkecube& sys,
+ twacube* twa)
+ : intersect>(sys, twa)
+ {
+ }
+
+ ~product_to_twa()
+ {
+ }
+
+ twa_graph_ptr twa()
+ {
+ res_->set_named_prop>("state-names", names_);
+ return res_;
+ }
+
+ void setup()
+ {
+ auto d = spot::make_bdd_dict();
+ res_ = make_twa_graph(d);
+ names_ = new std::vector();
+
+ int i = 0;
+ for (auto ap : this->twa_->get_ap())
+ {
+ auto idx = res_->register_ap(ap);
+ std::cout << ap << idx << std::endl;
+ reverse_binder_[i++] = idx;
+ }
+ }
+
+ bool push_state(product_state s, unsigned i, acc_cond::mark_t)
+ {
+ // push also implies edge (when it's not the initial state)
+ if (this->todo.size())
+ {
+ auto c = this->twa_->get_cubeset()
+ .intersection(this->twa_->trans_data
+ (this->todo.back().it_prop).cube_,
+ this->todo.back().it_kripke->condition());
+
+ bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
+ reverse_binder_);
+ this->twa_->get_cubeset().release(c);
+ res_->new_edge(this->map[this->todo.back().st]-1, i-1, x,
+ this->twa_->trans_data
+ (this->todo.back().it_prop).acc_);
+ }
+
+ unsigned st = res_->new_state();
+ names_->push_back(this->sys_.to_string(s.st_kripke) +
+ ('*' + std::to_string(s.st_prop)));
+ assert(st+1 == i);
+ return true;
+ }
+
+
+ bool update(product_state, unsigned src,
+ product_state, unsigned dst,
+ acc_cond::mark_t cond)
+ {
+ auto c = this->twa_->get_cubeset()
+ .intersection(this->twa_->trans_data
+ (this->todo.back().it_prop).cube_,
+ this->todo.back().it_kripke->condition());
+
+ bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
+ reverse_binder_);
+ this->twa_->get_cubeset().release(c);
+ res_->new_edge(src-1, dst-1, x, cond);
+ return false;
+ }
+
+ // These callbacks are useless here
+ bool counterexample_found()
+ {
+ return false;
+ }
+
+ std::string trace()
+ {
+ return "";
+ }
+
+ bool pop_state(product_state, unsigned, bool, product_state, unsigned)
+ {
+ return true;
+ }
+
+ private:
+ spot::twa_graph_ptr res_;
+ std::vector* names_;
+ std::unordered_map reverse_binder_;
+ };
+}