#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/mc/Session.hpp"
+#include "src/mc/checker/Checker.hpp"
#include "src/mc/checker/SimcallObserver.hpp"
#include "src/mc/mc_comm_pattern.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_pattern.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/remote/RemoteSimulation.hpp"
+#include "src/mc/remote/RemoteProcess.hpp"
#include <xbt/asserts.h>
#include <xbt/log.h>
if (mc_model_checker == nullptr)
return actor->get_host()->get_name();
- const simgrid::mc::RemoteSimulation* process = &mc_model_checker->get_remote_simulation();
+ const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_simulation();
// Read the simgrid::xbt::string in the MCed process:
simgrid::mc::ActorInformation* info = actor_info_cast(actor);
simgrid::mc::ActorInformation* info = actor_info_cast(actor);
if (info->name.empty()) {
- const simgrid::mc::RemoteSimulation* process = &mc_model_checker->get_remote_simulation();
+ const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_simulation();
simgrid::xbt::string_data string_data = simgrid::xbt::string::to_string_data(actor->name_);
info->name = process->read_string(remote(string_data.data), string_data.len);
return res;
}
-void Api::initialize(char** argv) const
+simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
{
simgrid::mc::session = new simgrid::mc::Session([argv] {
int i = 1;
execvp(argv[i], argv + i);
xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
});
+
+ simgrid::mc::Checker* checker;
+ switch (algo) {
+ case CheckerAlgorithm::CommDeterminism:
+ checker = simgrid::mc::createCommunicationDeterminismChecker();
+ break;
+
+ case CheckerAlgorithm::UDPOR:
+ checker = simgrid::mc::createUdporChecker();
+ break;
+
+ case CheckerAlgorithm::Safety:
+ checker = simgrid::mc::createSafetyChecker();
+ break;
+
+ case CheckerAlgorithm::Liveness:
+ checker = simgrid::mc::createLivenessChecker();
+ break;
+
+ default:
+ THROW_IMPOSSIBLE;
+ }
+
+ mc_model_checker->setChecker(checker);
+ return checker;
}
std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
std::size_t Api::get_remote_heap_bytes() const
{
- RemoteSimulation& process = mc_model_checker->get_remote_simulation();
+ RemoteProcess& process = mc_model_checker->get_remote_simulation();
auto heap_bytes_used = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info());
return heap_bytes_used;
}
return mc_model_checker->getChecker();
}
-void Api::set_checker(Checker* const checker) const
-{
- xbt_assert(mc_model_checker);
- xbt_assert(mc_model_checker->getChecker() == nullptr);
- mc_model_checker->setChecker(checker);
-}
-
void Api::handle_simcall(Transition const& transition) const
{
mc_model_checker->handle_simcall(transition);