X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/cde2aca7feb21f861c3f2da5fa5ae957ff15bb8e..ff420e1906d916322427488153e45bf82d5c03dd:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index fcc85efd39..3ca696bef4 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2015. The SimGrid Team.
+/* Copyright (c) 2008-2018. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -19,16 +19,16 @@
 #include "xbt/log.h"
 #include "xbt/system_error.hpp"
 
-#include "simgrid/sg_config.h"
+#include "simgrid/sg_config.hpp"
 
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/PageStore.hpp"
 #include "src/mc/Transition.hpp"
 #include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
+#include "src/mc/mc_exit.hpp"
+#include "src/mc/mc_private.hpp"
+#include "src/mc/mc_record.hpp"
 #include "src/mc/remote/mc_protocol.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
@@ -46,13 +46,13 @@ using simgrid::mc::remote;
 namespace simgrid {
 namespace mc {
 
-ModelChecker::ModelChecker(std::unique_ptr<Process> process) :
-  base_(nullptr),
-  socket_event_(nullptr),
-  signal_event_(nullptr),
-  page_store_(500),
-  process_(std::move(process)),
-  parent_snapshot_(nullptr)
+ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
+    : base_(nullptr)
+    , socket_event_(nullptr)
+    , signal_event_(nullptr)
+    , page_store_(500)
+    , process_(std::move(process))
+    , parent_snapshot_(nullptr)
 {
 
 }
@@ -96,7 +96,7 @@ void ModelChecker::start()
 
   process_->init();
 
-  if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
+  if (not _sg_mc_dot_output_file.get().empty())
     MC_init_dot_output();
 
   setup_ignore();
@@ -131,7 +131,7 @@ static const std::pair<const char*, const char*> ignored_local_variables[] = {
 
 void ModelChecker::setup_ignore()
 {
-  Process& process = this->process();
+  RemoteClient& process = this->process();
   for (std::pair<const char*, const char*> const& var :
       ignored_local_variables)
     process.ignore_local_variable(var.first, var.second);
@@ -144,15 +144,15 @@ void ModelChecker::shutdown()
 {
   XBT_DEBUG("Shuting down model-checker");
 
-  simgrid::mc::Process* process = &this->process();
+  simgrid::mc::RemoteClient* process = &this->process();
   if (process->running()) {
     XBT_DEBUG("Killing process");
-    kill(process->pid(), SIGTERM);
+    kill(process->pid(), SIGKILL);
     process->terminate();
   }
 }
 
-void ModelChecker::resume(simgrid::mc::Process& process)
+void ModelChecker::resume(simgrid::mc::RemoteClient& process)
 {
   int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
   if (res)
@@ -175,7 +175,7 @@ static void MC_report_crash(int status)
     XBT_INFO("No core dump was generated by the system.");
   XBT_INFO("Counter-example execution trace:");
   simgrid::mc::dumpRecordPath();
-  for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
   simgrid::mc::session->logState();
   XBT_INFO("Stack trace:");
@@ -189,14 +189,14 @@ static void MC_report_assertion_error()
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
   simgrid::mc::dumpRecordPath();
-  for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
   simgrid::mc::session->logState();
 }
 
 bool ModelChecker::handle_message(char* buffer, ssize_t size)
 {
-  mc_message_t base_message;
+  s_mc_message_t base_message;
   if (size < (ssize_t) sizeof(base_message))
     xbt_die("Broken message");
   memcpy(&base_message, buffer, sizeof(base_message));
@@ -251,26 +251,23 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
 
   case MC_MESSAGE_REGISTER_SYMBOL:
     {
-      s_mc_register_symbol_message_t message;
-      if (size != sizeof(message))
-        xbt_die("Broken message");
-      memcpy(&message, buffer, sizeof(message));
-      if (message.callback)
-        xbt_die("Support for client-side function proposition is not implemented.");
-      XBT_DEBUG("Received symbol: %s", message.name);
-
-      if (simgrid::mc::property_automaton == nullptr)
-        simgrid::mc::property_automaton = xbt_automaton_new();
-
-      simgrid::mc::Process* process = &this->process();
-      simgrid::mc::RemotePtr<int> address
-        = simgrid::mc::remote((int*) message.data);
-      simgrid::xbt::add_proposition(simgrid::mc::property_automaton,
-        message.name,
-        [process, address]() { return process->read(address); }
-        );
-
-      break;
+    s_mc_message_register_symbol_t message;
+    if (size != sizeof(message))
+      xbt_die("Broken message");
+    memcpy(&message, buffer, sizeof(message));
+    if (message.callback)
+      xbt_die("Support for client-side function proposition is not implemented.");
+    XBT_DEBUG("Received symbol: %s", message.name);
+
+    if (simgrid::mc::property_automaton == nullptr)
+      simgrid::mc::property_automaton = xbt_automaton_new();
+
+    simgrid::mc::RemoteClient* process  = &this->process();
+    simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
+    simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
+                                  [process, address]() { return process->read(address); });
+
+    break;
     }
 
   case MC_MESSAGE_WAITING:
@@ -378,25 +375,20 @@ void ModelChecker::handle_waitpid()
 
 void ModelChecker::on_signal(int signo)
 {
-  switch(signo) {
-  case SIGCHLD:
+  if (signo == SIGCHLD)
     this->handle_waitpid();
-    break;
-  default:
-    break;
-  }
 }
 
-void ModelChecker::wait_client(simgrid::mc::Process& process)
+void ModelChecker::wait_for_requests()
 {
-  this->resume(process);
+  this->resume(process());
   if (this->process().running())
     event_base_dispatch(base_);
 }
 
 void ModelChecker::handle_simcall(Transition const& transition)
 {
-  s_mc_message_simcall_handle m;
+  s_mc_message_simcall_handle_t m;
   memset(&m, 0, sizeof(m));
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = transition.pid;
@@ -412,7 +404,7 @@ bool ModelChecker::checkDeadlock()
   int res;
   if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
     xbt_die("Could not check deadlock state");
-  mc_message_int_t message;
+  s_mc_message_int_t message;
   ssize_t s = mc_model_checker->process().getChannel().receive(message);
   if (s == -1)
     xbt_die("Could not receive message");