mc: rework and test conversion into twa

* spot/mc/Makefile.am,
spot/mc/reachability.hh,
spot/mc/utils.hh,
tests/Makefile.am,
tests/ltsmin/.gitignore,
tests/ltsmin/testconvert.cc,
tests/ltsmin/testconvert.test: Here.

spot/mc/Makefile.am

@@ -21,8 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 mcdir = $(pkgincludedir)/mc
-mc_HEADERS = reachability.hh intersect.hh lpar13.hh unionfind.hh utils.hh\
+mc_HEADERS = intersect.hh lpar13.hh unionfind.hh utils.hh mc.hh\
-	mc.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh
+	mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh
 
 noinst_LTLIBRARIES = libmc.la
 

spot/mc/reachability.hh

@@ -1,126 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2019 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/kripke/kripke.hh>
-
-namespace spot
-{
-  /// \brief This template class provide a sequential reachability
-  /// of a kripkecube. The algorithm uses a single DFS since it
-  /// is the most efficient in a sequential setting
-  template<typename State, typename SuccIterator,
-           typename StateHash, typename StateEqual,
-           typename Visitor>
-  class SPOT_API seq_reach_kripke
-  {
-  public:
-    seq_reach_kripke(kripkecube<State, SuccIterator>& sys, unsigned tid):
-      sys_(sys), tid_(tid)
-  {
-      static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
-                                             State, SuccIterator>::value,
-                    "error: does not match the kripkecube requirements");
-      visited.reserve(2000000);
-      todo.reserve(100000);
-    }
-
-    ~seq_reach_kripke()
-      {
-        // States will be destroyed by the system, so just clear map
-        visited.clear();
-      }
-
-    Visitor& self()
-    {
-      return static_cast<Visitor&>(*this);
-    }
-
-    void run()
-    {
-      self().setup();
-      State initial = sys_.initial(tid_);
-      if (SPOT_LIKELY(self().push(initial, dfs_number)))
-        {
-          todo.push_back({initial, sys_.succ(initial, tid_)});
-          visited[initial] = ++dfs_number;
-        }
-      while (!todo.empty())
-        {
-          if (todo.back().it->done())
-            {
-              if (SPOT_LIKELY(self().pop(todo.back().s)))
-                {
-                  sys_.recycle(todo.back().it, tid_);
-                  todo.pop_back();
-                }
-            }
-          else
-            {
-              ++transitions;
-              State dst = todo.back().it->state();
-              auto it  = visited.insert({dst, dfs_number+1});
-              if (it.second)
-                {
-                  ++dfs_number;
-                  if (SPOT_LIKELY(self().push(dst, dfs_number)))
-                    {
-                      todo.back().it->next();
-                      todo.push_back({dst, sys_.succ(dst, tid_)});
-                    }
-                }
-              else
-                {
-                  self().edge(visited[todo.back().s], visited[dst]);
-                  todo.back().it->next();
-                }
-            }
-        }
-      self().finalize();
-    }
-
-    unsigned int states()
-    {
-      return dfs_number;
-    }
-
-    unsigned int trans()
-    {
-      return transitions;
-    }
-
-  protected:
-    struct todo_element
-    {
-      State s;
-      SuccIterator* it;
-    };
-    kripkecube<State, SuccIterator>& sys_;
-    std::vector<todo_element> todo;
-    // FIXME: The system already handle a set of visited states so
-    // this map is redundant: an we avoid this new map?
-    typedef std::unordered_map<const State, int,
-                               StateHash, StateEqual> visited_map;
-    visited_map visited;
-    unsigned int dfs_number = 0;
-    unsigned int transitions = 0;
-    unsigned int tid_;
-  };
-}

spot/mc/utils.hh

@@ -19,68 +19,119 @@
 
 #pragma once
 
-#include <spot/mc/reachability.hh>
 #include <spot/mc/intersect.hh>
 #include <spot/twa/twa.hh>
 #include <spot/twacube_algos/convert.hh>
 
 namespace spot
 {
+  /// \brief convert a (cube) model  into a twa.
+  /// Note that this algorithm cannot be run in parallel but could.
   template<typename State, typename SuccIterator,
            typename StateHash, typename StateEqual>
-  class SPOT_API kripke_to_twa :
+  class SPOT_API kripkecube_to_twa
-    public seq_reach_kripke<State, SuccIterator,
-                            StateHash, StateEqual,
-                            kripke_to_twa<State, SuccIterator,
-                                          StateHash, StateEqual>>
   {
   public:
-    kripke_to_twa(kripkecube<State, SuccIterator>& sys, bdd_dict_ptr dict)
-      : seq_reach_kripke<State, SuccIterator, StateHash, StateEqual,
-                         kripke_to_twa<State, SuccIterator,
-                                       StateHash, StateEqual>>(sys),
-      dict_(dict)
-      {}
 
-    ~kripke_to_twa()
+  kripkecube_to_twa(kripkecube<State, SuccIterator>& sys, bdd_dict_ptr dict):
+    sys_(sys), dict_(dict)
     {
+     static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
+                   State, SuccIterator>::value,
+                   "error: does not match the kripkecube requirements");
+    }
+
+    ~kripkecube_to_twa()
+    {
+     visited_.clear();
+    }
+
+    void run()
+    {
+     setup();
+     State initial = sys_.initial(0);
+     if (SPOT_LIKELY(push(initial, dfs_number_+1)))
+       {
+         visited_[initial] = dfs_number_++;
+         todo_.push_back({initial, sys_.succ(initial, 0)});
+       }
+     while (!todo_.empty())
+       {
+         if (todo_.back().it->done())
+           {
+             if (SPOT_LIKELY(pop(todo_.back().s)))
+               {
+                 sys_.recycle(todo_.back().it, 0);
+                 todo_.pop_back();
+               }
+           }
+         else
+           {
+             ++transitions_;
+             State dst = todo_.back().it->state();
+             auto it = visited_.find(dst);
+             if (it == visited_.end())
+               {
+                 if (SPOT_LIKELY(push(dst, dfs_number_+1)))
+                   {
+                     visited_[dst] = dfs_number_++;
+                     todo_.back().it->next();
+                     todo_.push_back({dst, sys_.succ(dst, 0)});
+                   }
+               }
+             else
+               {
+                 edge(visited_[todo_.back().s], visited_[dst]);
+                 todo_.back().it->next();
+               }
+           }
+       }
+     finalize();
     }
 
     void setup()
     {
-      res_ = make_twa_graph(dict_);
+     auto d = spot::make_bdd_dict();
+     res_ = make_twa_graph(d);
      names_ = new std::vector<std::string>();
 
-      // padding to simplify computation.
+     int i = 0;
-      res_->new_state();
+     for (auto ap : sys_.ap())
-
-      // Compute the reverse binder.
-      auto aps = this->sys_.ap();
-      for (unsigned i = 0; i < aps.size(); ++i)
        {
-          auto k = res_->register_ap(aps[i]);
+         auto idx = res_->register_ap(ap);
-          reverse_binder_.insert({i, k});
+         reverse_binder_[i++] = idx;
        }
     }
 
-    void push(State s, unsigned i)
+    bool push(State s, unsigned i)
     {
+
       unsigned st = res_->new_state();
-      names_->push_back(this->sys_.to_string(s));
+      names_->push_back(sys_.to_string(s));
-      SPOT_ASSERT(st == i);
+      if (!todo_.empty())
+        {
+          edge(visited_[todo_.back().s], st);
+        }
+
+      SPOT_ASSERT(st+1 == i);
+      return true;
+    }
+
+    bool pop(State)
+    {
+      return true;
     }
 
     void edge(unsigned src, unsigned dst)
     {
-      cubeset cs(this->sys_.ap().size());
+     cubeset cs(sys_.ap().size());
-      bdd cond = cube_to_bdd(this->todo.back().it->condition(),
+     bdd cond = cube_to_bdd(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<std::vector<std::string>>("state-names", names_);
     }
@@ -90,15 +141,27 @@ namespace spot
      return res_;
     }
 
-  private:
+  protected:
+    struct todo__element
+    {
+      State s;
+      SuccIterator* it;
+    };
+
+    typedef std::unordered_map<const State, int,
+                               StateHash, StateEqual> visited__map;
+
+    kripkecube<State, SuccIterator>& sys_;
+    std::vector<todo__element> todo_;
+    visited__map visited_;
+    unsigned int dfs_number_ = 0;
+    unsigned int transitions_ = 0;
     spot::twa_graph_ptr res_;
     std::vector<std::string>* names_;
     bdd_dict_ptr dict_;
     std::unordered_map<int, int> reverse_binder_;
   };
 
-
-
   /// \brief convert a (cube) product automaton into a twa
   /// Note that this algorithm cannot be run in parallel.
   template<typename State, typename SuccIterator,
@@ -128,6 +191,7 @@ namespace spot
       size_t
       operator()(const product_state lhs) const noexcept
       {
+        StateHash hash;
         unsigned u = hash(lhs.st_kripke) % (1<<30);
         u = wang32_hash(lhs.st_prop) ^ u;
         u = u % (1<<30);
@@ -217,6 +281,7 @@ namespace spot
 
     twa_graph_ptr twa()
     {
+      res_->purge_unreachable_states();
       res_->set_named_prop<std::vector<std::string>>("state-names", names_);
       return res_;
     }
@@ -228,7 +293,7 @@ namespace spot
       names_ = new std::vector<std::string>();
 
       int i = 0;
-      for (auto ap : this->twa_->ap())
+      for (auto ap : sys_.ap())
         {
           auto idx = res_->register_ap(ap);
           reverse_binder_[i++] = idx;
@@ -237,24 +302,25 @@ namespace spot
 
     bool push_state(product_state s, unsigned i, acc_cond::mark_t)
     {
-      // push also implies edge (when it's not the initial state)
+      unsigned st = res_->new_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(),
+      if (!todo_.empty())
+        {
+          auto c = twa_->get_cubeset()
+            .intersection(twa_->trans_data
+                          (todo_.back().it_prop).cube_,
+                          todo_.back().it_kripke->condition());
+
+          bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
                                     reverse_binder_);
-          this->twa_->get_cubeset().release(c);
+          twa_->get_cubeset().release(c);
-          res_->new_edge(this->map[this->todo_.back().st]-1, i-1, x,
+          res_->new_edge(map[todo_.back().st]-1, st, x,
-                         this->twa_->trans_data
+                         twa_->trans_data
-                         (this->todo_.back().it_prop).acc_);
+                         (todo_.back().it_prop).acc_);
         }
 
-      unsigned st = res_->new_state();
+
-      names_->push_back(this->sys_.to_string(s.st_kripke) +
+      names_->push_back(sys_.to_string(s.st_kripke) +
                         ('*' + std::to_string(s.st_prop)));
       SPOT_ASSERT(st+1 == i);
       return true;
@@ -264,14 +330,14 @@ namespace spot
                 product_state, unsigned dst,
                 acc_cond::mark_t cond)
     {
-      auto c = this->twa_->get_cubeset()
+      auto c = twa_->get_cubeset()
-        .intersection(this->twa_->trans_data
+        .intersection(twa_->trans_data
-                      (this->todo_.back().it_prop).cube_,
+                      (todo_.back().it_prop).cube_,
-                      this->todo_.back().it_kripke->condition());
+                      todo_.back().it_kripke->condition());
 
-      bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
+      bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
                                 reverse_binder_);
-      this->twa_->get_cubeset().release(c);
+      twa_->get_cubeset().release(c);
       res_->new_edge(src-1, dst-1, x, cond);
       return false;
     }

tests/Makefile.am

@@ -458,6 +458,7 @@ EXTRA_DIST = \
 
 if USE_LTSMIN
 check_PROGRAMS += ltsmin/modelcheck
+check_PROGRAMS += ltsmin/testconvert
 ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
 	$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
 ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread
@@ -468,6 +469,17 @@ ltsmin_modelcheck_LDADD =  \
   $(top_builddir)/spot/libspot.la              \
   $(top_builddir)/spot/ltsmin/libspotltsmin.la
 
+ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
+	$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
+ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread
+ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc
+ltsmin_testconvert_LDADD =  \
+  $(top_builddir)/bin/libcommon.a		\
+  $(top_builddir)/lib/libgnu.la			\
+  $(top_builddir)/spot/libspot.la              \
+  $(top_builddir)/spot/ltsmin/libspotltsmin.la
+
+
 check_SCRIPTS += ltsmin/defs
 
 ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
@@ -480,7 +492,8 @@ TESTS_ltsmin = \
   ltsmin/finite.test  \
   ltsmin/finite2.test \
   ltsmin/finite3.test \
-  ltsmin/kripke.test
+  ltsmin/kripke.test  \
+  ltsmin/testconvert.test
 
 EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \
   ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal

tests/ltsmin/.gitignore

@@ -1,2 +1,3 @@
 defs
 modelcheck
+testconvert

tests/ltsmin/testconvert.cc

@@ -0,0 +1,133 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2020 Laboratoire de Recherche et Développement 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 "config.h"
+#include <bddx.h>
+#include "bin/common_conv.hh"
+#include "bin/common_setup.hh"
+#include "bin/common_output.hh"
+
+#include <spot/ltsmin/ltsmin.hh>
+#include <spot/ltsmin/spins_kripke.hh>
+#include <spot/mc/mc_instanciator.hh>
+#include <spot/twaalgos/dot.hh>
+#include <spot/tl/defaultenv.hh>
+#include <spot/tl/parse.hh>
+#include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/emptiness.hh>
+#include <spot/twa/twaproduct.hh>
+
+#include <algorithm>
+#include <thread>
+#include <spot/twacube/twacube.hh>
+#include <spot/twacube_algos/convert.hh>
+#include <spot/mc/utils.hh>
+
+// FIXME (1) model (2)formula
+int main(int argc, char** argv)
+{
+  // Build the formula
+  char* formula = argv[2];
+  spot::formula f = nullptr;
+  spot::default_environment& env = spot::default_environment::instance();
+  spot::atomic_prop_set ap;
+  spot::const_twa_graph_ptr prop = nullptr;
+  auto dict = spot::make_bdd_dict();
+  {
+    auto pf = spot::parse_infix_psl(formula, env, false);
+    f = pf.f;
+    spot::translator trans(dict);
+    prop = trans.run(&f);
+  }
+
+  atomic_prop_collect(f, &ap);
+
+  auto propcube = spot::twa_to_twacube(prop);
+
+  // Load model
+  spot::ltsmin_kripkecube_ptr modelcube = nullptr;
+  try
+    {
+      modelcube = spot::ltsmin_model::load(argv[1])
+        .kripkecube(propcube->ap(), spot::formula::tt(), 0, 1);
+    }
+  catch (const std::runtime_error& e)
+    {
+      std::cerr << e.what() << '\n';
+    }
+
+  // ------------------------------------------------------------------
+  // check that cube and bdd approaches agree for the size of the model
+  // ------------------------------------------------------------------
+  auto result0 =
+    spot::ec_instanciator<spot::ltsmin_kripkecube_ptr, spot::cspins_state,
+                          spot::cspins_iterator, spot::cspins_state_hash,
+                          spot::cspins_state_equal>
+    (spot::mc_algorithm::REACHABILITY, modelcube, propcube, false);
+  std::cout << "[CUBE] Model: "
+            << result0.states[0] << ','
+            << result0.transitions[0]
+            << '\n';
+
+
+  spot::kripkecube_to_twa<spot::cspins_state,
+                          spot::cspins_iterator,
+                          spot::cspins_state_hash,
+                          spot::cspins_state_equal> ktt(*modelcube, dict);
+  ktt.run();
+  auto twa_from_model = ktt.twa();
+  std::cout << "[BDD]  Model: "
+            << twa_from_model->num_states() << ','
+            << twa_from_model->num_edges() << '\n';
+
+
+
+  // ------------------------------------------------------------------
+  // check that cube and bdd approaches agree for the emptiness and the
+  // size of the synchronous product
+  // ------------------------------------------------------------------
+  auto result1 =
+    spot::ec_instanciator<spot::ltsmin_kripkecube_ptr, spot::cspins_state,
+                          spot::cspins_iterator, spot::cspins_state_hash,
+                          spot::cspins_state_equal>
+    (spot::mc_algorithm::BLOEMEN_EC, modelcube, propcube, false);
+  auto result2 =
+    spot::ec_instanciator<spot::ltsmin_kripkecube_ptr, spot::cspins_state,
+                          spot::cspins_iterator, spot::cspins_state_hash,
+                          spot::cspins_state_equal>
+    (spot::mc_algorithm::REACHABILITY, modelcube, propcube, false);
+
+  std::cout << "[CUBE] Product: "
+            << result1.value[0] << ','
+            << result1.states[0] << ','
+            << result1.transitions[0]
+            << '\n';
+
+  spot::product_to_twa<spot::cspins_state,
+                       spot::cspins_iterator,
+                       spot::cspins_state_hash,
+                       spot::cspins_state_equal> ptt(*modelcube, propcube);
+  ptt.run();
+  auto twa_from_product = ptt.twa();
+  std::cout << "[BDD]  Product: "
+            << (twa_from_product->is_empty() ? "empty" : "not_empty")
+            << ','
+            << twa_from_product->num_states() << ','
+            << twa_from_product->num_edges()
+            << '\n';
+}

tests/ltsmin/testconvert.test

@@ -0,0 +1,54 @@
+ #! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2020 Laboratoire de Recherche et Developpement
+# 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/>.
+
+
+
+. ./defs
+
+divine compile > output 2>&1
+
+if grep -i 'ltsmin ' output; then
+  :
+else
+  echo "divine not installed, or no ltsmin interface"
+  exit 77
+fi
+
+set -e
+
+run 0 ../testconvert $srcdir/finite.dve 'true' > output
+cat << EOF > expected
+[CUBE] Model: 15,24
+[BDD]  Model: 15,24
+[CUBE] Product: not_empty,4,4
+[BDD]  Product: not_empty,15,24
+EOF
+
+cmp output expected
+
+run 0 ../testconvert $srcdir/finite.dve 'G "P.a==5"' > output
+cat << EOF > expected
+[CUBE] Model: 15,24
+[BDD]  Model: 15,24
+[CUBE] Product: empty,1,0
+[BDD]  Product: empty,1,0
+EOF
+
+cmp output expected