Commit 93b8bb72 authored by Etienne Renault's avatar Etienne Renault

mc: merge deadlock and reachabilty algorithms

* spot/mc/deadlock.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here.
parent 8b0ffb74
......@@ -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()
......
......@@ -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;
}
......
......@@ -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>,
......
......@@ -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 },
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment