X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7dc2c17f1e4a76b7fc5be51a4cad40354ebeaf2e..0b0dbda8d509d4c0e2d583d20f014163f0fb7230:/src/mc/mc_pattern.hpp

diff --git a/src/mc/mc_pattern.hpp b/src/mc/mc_pattern.hpp
index 385224d653..6a8f735161 100644
--- a/src/mc/mc_pattern.hpp
+++ b/src/mc/mc_pattern.hpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2007-2021. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2007-2022. 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. */
@@ -7,53 +7,16 @@
 #define SIMGRID_MC_PATTERN_H
 
 #include "src/kernel/activity/CommImpl.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
-namespace simgrid {
-namespace mc {
-
-enum class PatternCommunicationType {
-  none    = 0,
-  send    = 1,
-  receive = 2,
-};
-
-class PatternCommunication {
-public:
-  int num = 0;
-  RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr{nullptr};
-  PatternCommunicationType type = PatternCommunicationType::send;
-  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<char> data;
-  int tag   = 0;
-  int index = 0;
-
-  PatternCommunication dup() const
-  {
-    simgrid::mc::PatternCommunication res;
-    // num?
-    res.comm_addr = this->comm_addr;
-    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;
-    // tag?
-    res.index = this->index;
-    return res;
-  }
-};
+namespace simgrid::mc {
 
 /* 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 ActorState {
+
   /* Possible exploration status of an 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.
    */
@@ -67,26 +30,46 @@ class ActorState {
   };
 
   /** Exploration control information */
-  InterleavingType state = InterleavingType::disabled;
+  InterleavingType state_ = InterleavingType::disabled;
+
+  /** Number of times that the actor was considered to be executed in previous explorations of the state space */
+  unsigned int times_considered_ = 0;
+  /** Maximal amount of times that the actor can be considered for execution in this state.
+   * If times_considered==max_consider, we fully explored that part of the state space */
+  unsigned int max_consider_ = 0;
+
+  /** Whether that actor is initially enabled in this state */
+  bool enabled_;
 
 public:
-  /** Number of times that the process was considered to be executed */
-  // TODO, make this private
-  unsigned int times_considered = 0;
+  ActorState(aid_t aid, bool enabled, unsigned int max_consider)
+      : aid_(aid), max_consider_(max_consider), enabled_(enabled)
+  {
+  }
+
+  unsigned int do_consider()
+  {
+    if (max_consider_ <= times_considered_ + 1)
+      set_done();
+    return times_considered_++;
+  }
+  unsigned int get_times_considered() const { return times_considered_; }
 
-  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; }
+  /* returns whether the actor is marked as enabled in the application side */
+  bool is_enabled() const { return enabled_; }
+  /* returns whether the actor is marked as disabled by the exploration algorithm */
+  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 mark_todo()
   {
-    this->state            = InterleavingType::todo;
-    this->times_considered = 0;
+    this->state_            = InterleavingType::todo;
+    this->times_considered_ = 0;
   }
-  void set_done() { this->state = InterleavingType::done; }
+  void set_done() { this->state_ = InterleavingType::done; }
 };
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc
 
 #endif