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
Move SDPOR core computation into a method
[simgrid.git]
/
src
/
mc
/
explo
/
DFSExplorer.hpp
diff --git
a/src/mc/explo/DFSExplorer.hpp
b/src/mc/explo/DFSExplorer.hpp
index 087e06f13c0c9889f78bc8a07cbff6893b264e9f..320754dc3595510a69a8428cb5ec1fb7cec99ccd 100644
(file)
--- a/
src/mc/explo/DFSExplorer.hpp
+++ b/
src/mc/explo/DFSExplorer.hpp
@@
-9,11
+9,13
@@
#include "src/mc/api/ClockVector.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/api/ClockVector.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/VisitedState.hpp"
#endif
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/VisitedState.hpp"
#endif
+#include <deque>
#include <list>
#include <memory>
#include <set>
#include <list>
#include <memory>
#include <set>
@@
-23,7
+25,7
@@
namespace simgrid::mc {
namespace simgrid::mc {
-using stack_t = std::
list
<std::shared_ptr<State>>;
+using stack_t = std::
deque
<std::shared_ptr<State>>;
class XBT_PRIVATE DFSExplorer : public Exploration {
XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor);
class XBT_PRIVATE DFSExplorer : public Exploration {
XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor);
@@
-96,6
+98,12
@@
private:
/** Stack representing the position in the exploration graph */
stack_t stack_;
/** Stack representing the position in the exploration graph */
stack_t stack_;
+ /**
+ * Provides additional metadata about the position in the exploration graph
+ * which is used by SDPOR and ODPOR
+ */
+ odpor::Execution execution_seq_;
+
/** Per-actor clock vectors used to compute the "happens-before" relation */
std::unordered_map<aid_t, ClockVector> per_actor_clocks_;
/** Per-actor clock vectors used to compute the "happens-before" relation */
std::unordered_map<aid_t, ClockVector> per_actor_clocks_;