X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4b0aa1525597fd0800c4d00c6df3f3c49d53ee2c..c4010c537a44b1fb18079401a3635821c86e6fcf:/src/mc/mc_state.hpp diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index 7b4dba0edd..96b59101d5 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2007-2018. 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,14 +6,9 @@ #ifndef SIMGRID_MC_STATE_HPP #define SIMGRID_MC_STATE_HPP -#include -#include - -#include "src/mc/mc_record.hpp" -#include "src/mc/sosp/mc_snapshot.hpp" - #include "src/kernel/activity/CommImpl.hpp" #include "src/mc/Transition.hpp" +#include "src/mc/sosp/Snapshot.hpp" namespace simgrid { namespace mc { @@ -58,18 +53,18 @@ public: } }; -/* On every state, each process has an entry of the following type. - * This represents both the process and its transition because - * a process cannot have more than one enabled transition at a given time. +/* On every state, each actor has an entry of the following type. + * This represents both the actor and its transition because + * an actor cannot have more than one enabled transition at a given time. */ -class ProcessState { - /* Possible exploration status of a process transition in a state. - * Either the checker did not consider the transition, or it was considered and to do, or considered and done. +class ActorState { + /* Possible exploration status of a actor transition in a state. + * Either the checker did not consider the transition, or it was considered and still to do, or considered and done. */ enum class InterleavingType { - /** This process transition is not considered by the checker (yet?) */ + /** This actor transition is not considered by the checker (yet?) */ disabled = 0, - /** The checker algorithm decided that this process transitions should be done at some point */ + /** The checker algorithm decided that this actor transitions should be done at some point */ todo, /** The checker algorithm decided that this should be done, but it was done in the meanwhile */ done, @@ -83,32 +78,31 @@ public: // 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 is_disabled() const { return this->state == InterleavingType::disabled; } + bool is_done() const { return this->state == InterleavingType::done; } + bool is_todo() 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() { this->state = InterleavingType::todo; this->times_considered = 0; } - void setDone() { this->state = InterleavingType::done; } + void set_done() { this->state = InterleavingType::done; } }; -/* A node in the exploration graph (kind-of) - */ +/* A node in the exploration graph (kind-of) */ class XBT_PRIVATE State { public: /** Sequential state number (used for debugging) */ - int num = 0; + int num_ = 0; /** State's exploration status by process */ - std::vector actorStates; + std::vector actor_states_; - Transition transition; + Transition transition_; /** The simcall which was executed, going out of that state */ - s_smx_simcall executed_req; + s_smx_simcall executed_req_; /* Internal translation of the executed_req simcall * @@ -124,14 +118,14 @@ public: std::shared_ptr system_state; // For CommunicationDeterminismChecker - std::vector> incomplete_comm_pattern; - std::vector communicationIndices; + std::vector> incomplete_comm_pattern_; + std::vector communication_indices_; explicit State(unsigned long state_number); - std::size_t interleaveSize() const; - void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->pid_].consider(); } - Transition getTransition() const; + std::size_t interleave_size() const; + void add_interleaving_set(smx_actor_t actor) { this->actor_states_[actor->get_pid()].consider(); } + Transition get_transition() const; }; } }