From 369a8b8b142b04e3327152db4aecf971bc6c11bc Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Wed, 13 May 2020 13:51:09 +0200
Subject: [PATCH] mc: merge deadlock and reachabilty algorithms

* spot/mc/deadlock.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here.
---
 spot/mc/deadlock.hh        | 18 ++++++++++++++----
 spot/mc/mc.hh              |  5 ++++-
 spot/mc/mc_instanciator.hh | 10 ++++++++--
 tests/ltsmin/modelcheck.cc |  6 ++++++
 4 files changed, 32 insertions(+), 7 deletions(-)

diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh
index cdf2d47af..bb2e2dab4 100644
--- a/spot/mc/deadlock.hh
+++ b/spot/mc/deadlock.hh
@@ -35,8 +35,11 @@ namespace spot
   /// \brief This class aims to explore a model to detect wether it
   /// contains a deadlock. This deadlock detection performs a DFS traversal
   /// sharing information shared among multiple threads.
+  /// If Deadlock equals std::true_type performs dealock algorithm,
+  /// otherwise perform a simple reachability.
   template<typename State, typename SuccIterator,
-           typename StateHash, typename StateEqual>
+           typename StateHash, typename StateEqual,
+           typename Deadlock>
   class SPOT_API swarmed_deadlock
   {
     /// \brief Describes the status of a state
@@ -79,6 +82,9 @@ namespace spot
       }
     };
 
+    static constexpr bool compute_deadlock =
+       std::is_same<std::true_type, Deadlock>::value;
+
   public:
 
     ///< \brief Shortcut to ease shared map manipulation
@@ -132,7 +138,7 @@ namespace spot
               if (SPOT_LIKELY(pop()))
                 {
                   deadlock_ = todo_.back().current_tr == transitions_;
-                  if (deadlock_)
+                  if (compute_deadlock && deadlock_)
                     break;
                   sys_.recycle(todo_.back().it, tid_);
                   todo_.pop_back();
@@ -234,7 +240,9 @@ namespace spot
 
     std::string name()
     {
-      return "deadlock";
+      if (compute_deadlock)
+        return "deadlock";
+      return "reachability";
     }
 
     int sccs()
@@ -244,7 +252,9 @@ namespace spot
 
     mc_rvalue result()
     {
-      return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
+      if (compute_deadlock)
+        return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
+      return mc_rvalue::SUCCESS;
     }
 
     std::string trace()
diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh
index 2cabd17a7..f73233690 100644
--- a/spot/mc/mc.hh
+++ b/spot/mc/mc.hh
@@ -32,7 +32,8 @@ namespace spot
      BLOEMEN_SCC,   ///< \brief Bloemen.16.ppopp SCC computation
      CNDFS,         ///< \brief Evangelista.12.atva emptiness check
      DEADLOCK,      ///< \brief Check wether there is a deadlock
-     SWARMING,       ///< \brief Holzmann.11.ieee applied to renault.13.lpar
+     REACHABILITY,  ///< \brief Only perform a reachability algorithm
+     SWARMING,      ///< \brief Holzmann.11.ieee applied to renault.13.lpar
     };
 
   enum SPOT_API class mc_rvalue
@@ -70,6 +71,8 @@ namespace spot
         os << "cndfs";  break;
       case mc_algorithm::DEADLOCK:
         os << "deadlock";  break;
+      case mc_algorithm::REACHABILITY:
+        os << "reachability";  break;
       case mc_algorithm::SWARMING:
         os << "swarming";  break;
       }
diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh
index 160117bb6..4333a87cc 100644
--- a/spot/mc/mc_instanciator.hh
+++ b/spot/mc/mc_instanciator.hh
@@ -187,8 +187,14 @@ namespace spot
             kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
 
       case mc_algorithm::DEADLOCK:
-        return instanciate<spot::swarmed_deadlock<State, Iterator, Hash, Equal>,
-            kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
+        return instanciate
+         <spot::swarmed_deadlock<State, Iterator, Hash, Equal, std::true_type>,
+           kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
+
+      case mc_algorithm::REACHABILITY:
+        return instanciate
+         <spot::swarmed_deadlock<State, Iterator, Hash, Equal, std::false_type>,
+           kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
 
       case mc_algorithm::SWARMING:
         return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc
index 0d1dffc50..efa4930d8 100644
--- a/tests/ltsmin/modelcheck.cc
+++ b/tests/ltsmin/modelcheck.cc
@@ -134,6 +134,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
       mc_options.nb_threads = to_unsigned(arg, "-p/--parallel");
       mc_options.force_parallel = true;
       break;
+    case 'r':
+      mc_options.algorithm = spot::mc_algorithm::REACHABILITY;
+      mc_options.force_parallel = true;
+      break;
     case 's':
       mc_options.dead_ap = arg;
       break;
@@ -184,6 +188,8 @@ static const argp_option options[] =
       "is found."
       , 0 },
     { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
+    { "reachability", 'r', nullptr, 0, "performs a traversal of the model "
+      , 0 },
     { "selfloopize", 's', "STRING", 0,
       "use STRING as property for marking deadlock "
       "states (by default selfloopize is activated with STRING='true')", 0 },