#include "simgrid/forward.h"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_record.hpp"
#include <xbt/Extendable.hpp>
FILE* dot_output_ = nullptr;
public:
- explicit Exploration(const std::vector<char*>& args, bool need_memory_introspection);
+ explicit Exploration(const std::vector<char*>& args);
virtual ~Exploration();
static Exploration* get_instance() { return instance_; }
// No copy:
- Exploration(Exploration const&) = delete;
+ Exploration(Exploration const&) = delete;
Exploration& operator=(Exploration const&) = delete;
/** Main function of this algorithm */
* to get and display information about the current state of the
* model-checking algorithm: */
- /** Show the current trace/stack
- *
- * Could this be handled in the Session/ModelChecker instead? */
+ /** Retrieve the current stack to build an execution trace */
virtual RecordTrace get_record_trace() = 0;
/** Generate a textual execution trace of the simulated application */
- virtual std::vector<std::string> get_textual_trace() = 0;
+ std::vector<std::string> get_textual_trace(int max_elements = -1);
/** Log additional information about the state of the model-checker */
virtual void log_state();
};
// External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Exploration* create_liveness_checker(const std::vector<char*>& args);
-XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor);
+XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, ReductionMode mode);
XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
} // namespace simgrid::mc