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

@@ -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()
     {
+      if (compute_deadlock)
         return "deadlock";
+      return "reachability";
     }
 
     int sccs()
@@ -244,7 +252,9 @@ namespace spot
 
     mc_rvalue result()
     {
+      if (compute_deadlock)
         return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
+      return mc_rvalue::SUCCESS;
     }
 
     std::string trace()

spot/mc/mc.hh

@@ -32,6 +32,7 @@ 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
+     REACHABILITY,  ///< \brief Only perform a reachability algorithm
      SWARMING,      ///< \brief Holzmann.11.ieee applied to renault.13.lpar
     };
 
@@ -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;
       }

spot/mc/mc_instanciator.hh

@@ -187,7 +187,13 @@ namespace spot
             kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
 
       case mc_algorithm::DEADLOCK:
-        return instanciate<spot::swarmed_deadlock<State, Iterator, Hash, Equal>,
+        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:

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 },