X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1fc042e8bc9c51f9267fa1936deaebe59ae01ee7..5ce2cc84f1f1154453e9534505c394fbd2b89e05:/src/mc/mc_state.hpp diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index 8fe92e3dc7..480bdea388 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2007-2017. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2007-2019. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -6,19 +6,16 @@ #ifndef SIMGRID_MC_STATE_HPP #define SIMGRID_MC_STATE_HPP -#include -#include - +#include "src/kernel/activity/CommImpl.hpp" #include "src/mc/Transition.hpp" -#include "src/mc/mc_record.hpp" -#include "src/mc/mc_snapshot.hpp" +#include "src/mc/sosp/Snapshot.hpp" namespace simgrid { namespace mc { enum class PatternCommunicationType { - none = 0, - send = 1, + none = 0, + send = 1, receive = 2, }; @@ -27,37 +24,33 @@ public: int num = 0; simgrid::kernel::activity::CommImpl* comm_addr; PatternCommunicationType type = PatternCommunicationType::send; - unsigned long src_proc = 0; - unsigned long dst_proc = 0; - const char *src_host = nullptr; - const char *dst_host = nullptr; + unsigned long src_proc = 0; + unsigned long dst_proc = 0; + const char* src_host = nullptr; + const char* dst_host = nullptr; std::string rdv; std::vector data; - int tag = 0; + int tag = 0; int index = 0; - PatternCommunication() - { - std::memset(&comm_addr, 0, sizeof(comm_addr)); - } + PatternCommunication() { std::memset(&comm_addr, 0, sizeof(comm_addr)); } PatternCommunication dup() const { simgrid::mc::PatternCommunication res; // num? res.comm_addr = this->comm_addr; - res.type = this->type; + res.type = this->type; // src_proc? // dst_proc? res.dst_proc = this->dst_proc; res.dst_host = this->dst_host; - res.rdv = this->rdv; - res.data = this->data; + res.rdv = this->rdv; + res.data = this->data; // tag? res.index = this->index; return res; } - }; /* On every state, each process has an entry of the following type. @@ -79,28 +72,22 @@ class ProcessState { /** Exploration control information */ InterleavingType state = InterleavingType::disabled; + public: /** Number of times that the process was considered to be executed */ // TODO, make this private unsigned int times_considered = 0; - bool isDisabled() const { - return this->state == InterleavingType::disabled; - } - bool isDone() const { - return this->state == InterleavingType::done; - } - bool isTodo() const { - return this->state == InterleavingType::todo; - } + bool isDisabled() const { return this->state == InterleavingType::disabled; } + bool isDone() const { return this->state == InterleavingType::done; } + bool isTodo() const { return this->state == InterleavingType::todo; } /** Mark that we should try executing this process at some point in the future of the checker algorithm */ - void consider() { + void consider() + { this->state = InterleavingType::todo; this->times_considered = 0; } - void setDone() { - this->state = InterleavingType::done; - } + void setDone() { this->state = InterleavingType::done; } }; /* A node in the exploration graph (kind-of) @@ -116,14 +103,14 @@ public: Transition transition; /** The simcall which was executed, going out of that state */ - s_smx_simcall_t executed_req; + s_smx_simcall executed_req; /* Internal translation of the executed_req simcall * * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT. */ - s_smx_simcall_t internal_req; + s_smx_simcall internal_req; /* Can be used as a copy of the remote synchro object */ simgrid::mc::Remote internal_comm; @@ -135,13 +122,12 @@ public: std::vector> incomplete_comm_pattern; std::vector communicationIndices; - State(unsigned long state_number); + explicit State(unsigned long state_number); std::size_t interleaveSize() const; - void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->pid].consider(); } + void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->get_pid()].consider(); } Transition getTransition() const; }; - } }