A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
MC further cleanups (let it compile, this time)
[simgrid.git]
/
src
/
mc
/
api.cpp
diff --git
a/src/mc/api.cpp
b/src/mc/api.cpp
index
71969e1
..
f854af4
100644
(file)
--- a/
src/mc/api.cpp
+++ b/
src/mc/api.cpp
@@
-12,7
+12,6
@@
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_base.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_base.hpp"
#include "src/mc/mc_exit.hpp"
-#include "src/mc/mc_pattern.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#include "src/surf/HostImpl.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#include "src/surf/HostImpl.hpp"
@@
-28,17
+27,20
@@
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Api, mc, "Logging specific to MC Facade APIs ");
XBT_LOG_EXTERNAL_CATEGORY(mc_global);
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Api, mc, "Logging specific to MC Facade APIs ");
XBT_LOG_EXTERNAL_CATEGORY(mc_global);
-using Simcall = simgrid::simix::Simcall;
+namespace simgrid::mc {
-namespace simgrid {
-namespace mc {
-
-simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo)
+simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<std::string, std::string>& env,
+ simgrid::mc::ExplorationAlgorithm algo)
{
{
- session_ = std::make_unique<simgrid::mc::Session>([argv] {
+ session_ = std::make_unique<simgrid::mc::Session>([argv
, &env
] {
int i = 1;
while (argv[i] != nullptr && argv[i][0] == '-')
i++;
int i = 1;
while (argv[i] != nullptr && argv[i][0] == '-')
i++;
+
+ for (auto const& [key, val] : env) {
+ XBT_INFO("setenv '%s'='%s'", key.c_str(), val.c_str());
+ setenv(key.c_str(), val.c_str(), 1);
+ }
xbt_assert(argv[i] != nullptr,
"Unable to find a binary to exec on the command line. Did you only pass config flags?");
execvp(argv[i], argv + i);
xbt_assert(argv[i] != nullptr,
"Unable to find a binary to exec on the command line. Did you only pass config flags?");
execvp(argv[i], argv + i);
@@
-47,19
+49,19
@@
simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgor
simgrid::mc::Exploration* explo;
switch (algo) {
simgrid::mc::Exploration* explo;
switch (algo) {
- case
Checker
Algorithm::CommDeterminism:
+ case
Exploration
Algorithm::CommDeterminism:
explo = simgrid::mc::create_communication_determinism_checker(session_.get());
break;
explo = simgrid::mc::create_communication_determinism_checker(session_.get());
break;
- case
Checker
Algorithm::UDPOR:
+ case
Exploration
Algorithm::UDPOR:
explo = simgrid::mc::create_udpor_checker(session_.get());
break;
explo = simgrid::mc::create_udpor_checker(session_.get());
break;
- case
Checker
Algorithm::Safety:
- explo = simgrid::mc::create_
safety_checker
(session_.get());
+ case
Exploration
Algorithm::Safety:
+ explo = simgrid::mc::create_
dfs_exploration
(session_.get());
break;
break;
- case
Checker
Algorithm::Liveness:
+ case
Exploration
Algorithm::Liveness:
explo = simgrid::mc::create_liveness_checker(session_.get());
break;
explo = simgrid::mc::create_liveness_checker(session_.get());
break;
@@
-71,11
+73,6
@@
simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgor
return explo;
}
return explo;
}
-std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
-{
- return mc_model_checker->get_remote_process().actors();
-}
-
unsigned long Api::get_maxpid() const
{
return mc_model_checker->get_remote_process().get_maxpid();
unsigned long Api::get_maxpid() const
{
return mc_model_checker->get_remote_process().get_maxpid();
@@
-90,12
+87,12
@@
std::size_t Api::get_remote_heap_bytes() const
void Api::mc_inc_visited_states() const
{
void Api::mc_inc_visited_states() const
{
- mc_model_checker->
visited_states++
;
+ mc_model_checker->
inc_visited_states()
;
}
unsigned long Api::mc_get_visited_states() const
{
}
unsigned long Api::mc_get_visited_states() const
{
- return mc_model_checker->
visited_states
;
+ return mc_model_checker->
get_visited_states()
;
}
void Api::mc_exit(int status) const
}
void Api::mc_exit(int status) const
@@
-103,7
+100,7
@@
void Api::mc_exit(int status) const
mc_model_checker->exit(status);
}
mc_model_checker->exit(status);
}
-void Api::restore_state(
std::shared_ptr<simgrid::mc::Snapshot>
system_state) const
+void Api::restore_state(
const simgrid::mc::Snapshot*
system_state) const
{
system_state->restore(&mc_model_checker->get_remote_process());
}
{
system_state->restore(&mc_model_checker->get_remote_process());
}
@@
-185,5
+182,4
@@
xbt_automaton_state_t Api::get_automaton_transition_dst(xbt_dynar_t const& dynar
return transition->dst;
}
return transition->dst;
}
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc