X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/95da4b54779cd1eae048f8d1207e45231e5599da..42ec07cc0c4fb24df86b22c97bfbeab2f0a21c8e:/src/mc/api.hpp diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 7cc6276a59..36730ee219 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -7,7 +7,6 @@ #include "simgrid/forward.h" #include "src/mc/mc_forward.hpp" #include "src/mc/mc_record.hpp" -#include "src/mc/mc_request.hpp" #include "src/mc/mc_state.hpp" #include "xbt/automaton.hpp" #include "xbt/base.h" @@ -15,6 +14,8 @@ namespace simgrid { namespace mc { +XBT_DECLARE_ENUM_CLASS(CheckerAlgorithm, Safety, UDPOR, Liveness, CommDeterminism); + /** * @brief Maintains the transition's information. */ @@ -46,7 +47,7 @@ private: } }; - simgrid::kernel::activity::CommImpl* get_comm(smx_simcall_t const r) const; + simgrid::kernel::activity::CommImpl* get_comm_or_nullptr(smx_simcall_t const r) const; bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) const; simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor) const; std::string get_actor_name(smx_actor_t actor) const; @@ -64,17 +65,15 @@ public: return api; } - void initialize(char** argv) const; + simgrid::mc::Checker* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const; // ACTOR APIs std::vector& get_actors() const; - bool actor_is_enabled(aid_t pid) const; unsigned long get_maxpid() const; int get_actors_size() const; // COMMUNICATION APIs RemotePtr get_comm_isend_raw_addr(smx_simcall_t request) const; - RemotePtr get_comm_wait_raw_addr(smx_simcall_t request) const; RemotePtr get_comm_waitany_raw_addr(smx_simcall_t request, int value) const; std::string get_pattern_comm_rdv(RemotePtr const& addr) const; unsigned long get_pattern_comm_src_proc(RemotePtr const& addr) const; @@ -98,7 +97,6 @@ public: void mc_check_deadlock() const; bool mc_is_null() const; Checker* mc_get_checker() const; - void set_checker(Checker* const checker) const; void handle_simcall(Transition const& transition) const; void mc_wait_for_requests() const; XBT_ATTRIB_NORETURN void mc_exit(int status) const; @@ -124,14 +122,12 @@ public: // STATE APIs void restore_state(std::shared_ptr system_state) const; void log_state() const; - void restore_initial_state() const; // SNAPSHOT APIs bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const; simgrid::mc::Snapshot* take_snapshot(int num_state) const; // SESSION APIs - void session_initialize() const; void s_close() const; void execute(Transition& transition, smx_simcall_t simcall) const;