MC: simplify initialization and kill api::set_checker()

[simgrid.git] / src / mc / checker / SimcallObserver.cpp

diff --git a/src/mc/checker/SimcallObserver.cpp b/src/mc/checker/SimcallObserver.cpp
index 9c601be80c83b9fdfb540df26adf945b1c44cb92..e4ec65d980934078269da1c595cb55bd3fdb3e4f 100644 (file)
--- a/src/mc/checker/SimcallObserver.cpp
+++ b/src/mc/checker/SimcallObserver.cpp
@@ -57,19 +57,67 @@ std::string MutexUnlockSimcall::dot_label() const
   return SimcallObserver::dot_label() + "Mutex UNLOCK";
 }
 
-std::string MutexTrylockSimcall::to_string(int time_considered) const
+std::string MutexLockSimcall::to_string(int time_considered) const
 {
-  std::string res = SimcallObserver::to_string(time_considered) + "Mutex TRYLOCK";
+  std::string res = SimcallObserver::to_string(time_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
   res += "(locked = " + std::to_string(mutex_->is_locked());
   res += ", owner = " + std::to_string(mutex_->get_owner() ? mutex_->get_owner()->get_pid() : -1);
   res += ", sleeping = n/a)";
   return res;
 }
 
-std::string MutexTrylockSimcall::dot_label() const
+std::string MutexLockSimcall::dot_label() const
 {
-  return SimcallObserver::dot_label() + "Mutex TRYLOCK";
+  return SimcallObserver::dot_label() + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
 }
 
+bool MutexLockSimcall::is_enabled() const
+{
+  return not blocking_ || mutex_->get_owner() == nullptr || mutex_->get_owner() == get_issuer();
+}
+
+std::string ConditionWaitSimcall::to_string(int time_considered) const
+{
+  std::string res = SimcallObserver::to_string(time_considered) + "Condition WAIT";
+  res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
+  return res;
+}
+
+std::string ConditionWaitSimcall::dot_label() const
+{
+  return SimcallObserver::dot_label() + "Condition WAIT";
+}
+
+bool ConditionWaitSimcall::is_enabled() const
+{
+  static bool warned = false;
+  if (not warned) {
+    XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
+    warned = true;
+  }
+  return true;
+}
+
+std::string SemAcquireSimcall::to_string(int time_considered) const
+{
+  std::string res = SimcallObserver::to_string(time_considered) + "Sem ACQUIRE";
+  res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
+  return res;
+}
+
+std::string SemAcquireSimcall::dot_label() const
+{
+  return SimcallObserver::dot_label() + "Sem ACQUIRE";
+}
+
+bool SemAcquireSimcall::is_enabled() const
+{
+  static bool warned = false;
+  if (not warned) {
+    XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
+    warned = true;
+  }
+  return true;
+}
 } // namespace mc
 } // namespace simgrid