+ /* This is actually a map from int to int. We could use
+ * std::map here, but looking up a value there costs O(log(n)).
+ * For a vector, this costs O(1). We hence go with the vector.
+ */
+ std::vector<simgrid::s4u::ActorPtr> rank_to_actor_map_;
+ std::map<simgrid::s4u::ActorPtr, int> actor_to_rank_map_;
+ std::vector<int> index_to_rank_map_;
+