Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Don't compute the dependencies locally in the checker, but through the observers...
[simgrid.git] / src / mc / mc_state.hpp
1 /* Copyright (c) 2007-2022. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #ifndef SIMGRID_MC_STATE_HPP
7 #define SIMGRID_MC_STATE_HPP
8
9 #include "src/mc/Transition.hpp"
10 #include "src/mc/sosp/Snapshot.hpp"
11 #include "src/mc/mc_comm_pattern.hpp"
12
13 namespace simgrid {
14 namespace mc {
15
16 /* A node in the exploration graph (kind-of) */
17 class XBT_PRIVATE State {
18 public:
19   /** Sequential state number (used for debugging) */
20   int num_ = 0;
21
22   /** State's exploration status by process */
23   std::vector<ActorState> actor_states_;
24
25   Transition transition_;
26
27   /** The simcall which was executed, going out of that state */
28   s_smx_simcall executed_req_;
29
30   /** Observer of the transition leading to that sate */
31   RemotePtr<kernel::actor::SimcallObserver> remote_observer_;
32
33   /* Internal translation of the executed_req simcall
34    *
35    * Simcall::COMM_TESTANY is translated to a Simcall::COMM_TEST
36    * and Simcall::COMM_WAITANY to a Simcall::COMM_WAIT.
37    */
38   s_smx_simcall internal_req_;
39
40   /* Can be used as a copy of the remote synchro object */
41   simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> internal_comm_;
42
43   /** Snapshot of system state (if needed) */
44   std::shared_ptr<simgrid::mc::Snapshot> system_state_;
45
46   // For CommunicationDeterminismChecker
47   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
48   std::vector<unsigned> communication_indices_;
49
50   explicit State(unsigned long state_number);
51
52   std::size_t count_todo() const;
53   void mark_todo(const simgrid::kernel::actor::ActorImpl* actor) { this->actor_states_[actor->get_pid()].mark_todo(); }
54   Transition get_transition() const;
55
56 private:
57   void copy_incomplete_comm_pattern();
58   void copy_index_comm_pattern();
59 };
60 }
61 }
62
63 #endif