#ifndef SIMGRID_MC_CHECKER_HPP
#define SIMGRID_MC_CHECKER_HPP
-#include "src/mc/api.hpp"
+#include "simgrid/forward.h"
+#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_record.hpp"
+#include <xbt/Extendable.hpp>
+
+#include <memory>
namespace simgrid::mc {
* `RemoteApp` interface (that is currently not perfectly sufficient to that extend). */
// abstract
class Exploration : public xbt::Extendable<Exploration> {
- RemoteApp* remote_app_;
+ std::unique_ptr<RemoteApp> remote_app_;
public:
- explicit Exploration(RemoteApp* remote_app) : remote_app_(remote_app) {}
+ explicit Exploration(const std::vector<char*>& args);
// No copy:
Exploration(Exploration const&) = delete;
virtual std::vector<std::string> get_textual_trace() = 0;
/** Log additional information about the state of the model-checker */
- virtual void log_state() = 0;
+ virtual void log_state();
- RemoteApp& get_remote_app() { return *remote_app_; }
+ RemoteApp& get_remote_app() { return *remote_app_.get(); }
};
// External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Exploration* create_liveness_checker(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_dfs_exploration(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_udpor_checker(RemoteApp* remote_app);
+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_udpor_checker(const std::vector<char*>& args);
+
+// FIXME: kill this template and use lambdas in boost::range_equal
+struct DerefAndCompareByActorsCountAndUsedHeap {
+ template <class X, class Y> bool operator()(X const& a, Y const& b) const
+ {
+ return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
+ }
+};
+static inline DerefAndCompareByActorsCountAndUsedHeap compare_pair_by_actor_count_and_used_heap()
+{
+ return DerefAndCompareByActorsCountAndUsedHeap();
+}
} // namespace simgrid::mc