> [0.000000] [mc_explo/INFO] Counter-example execution trace:
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 930 unique states visited; 207 backtracks (2195 transition replays, 3332 states visited overall)
+> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;3;3;2;1;1;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 662 unique states visited; 144 backtracks (1540 transition replays, 2346 states visited overall)
! expect return 1
! timeout 20
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 173 unique states visited; 29 backtracks (286 transition replays, 488 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 64 unique states visited; 5 backtracks (23 transition replays, 92 states visited overall)
\ No newline at end of file
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;1;1;1;2;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 5 backtracks (17 transition replays, 51 states visited overall)
+> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall)
! expect return 1
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;1;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall)
-
-! expect return 1
-! timeout 300
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42'
-> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none.
-> [0.000000] [mc_explo/INFO] **************************
-> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
-> [0.000000] [mc_explo/INFO] **************************
-> [0.000000] [mc_explo/INFO] Counter-example execution trace:
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;2;1;3;1;1;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 7 backtracks (19 transition replays, 70 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;2;1;1;3;1;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (0 transition replays, 25 states visited overall)
\ No newline at end of file
! timeout 20
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
-> [ 0.000000] (1:server@Boivin) OK
> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (1:server@Boivin) OK
+> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;1;1'
-> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall)
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;3;1;1'
+> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 3 backtracks (1 transition replays, 22 states visited overall)
! expect return 1
! timeout 20
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
-> [ 0.000000] (1:server@Boivin) OK
> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (1:server@Boivin) OK
+> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
-> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall)
\ No newline at end of file
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1'
+> [ 0.000000] (0:maestro@) DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall)
\ No newline at end of file
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (49 transition replays, 126 states visited overall)
-
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '3'
-> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 647 unique states visited; 122 backtracks (871 transition replays, 1640 states visited overall)
\ No newline at end of file
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 103 unique states visited; 16 backtracks (163 transition replays, 282 states visited overall)
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -c 2 -C 1 -p 2 -P 1
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42'
-> [0.000000] [sthread/INFO] Starting the simulation.
-> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 91 unique states visited; 11 backtracks (116 transition replays, 218 states visited overall)
\ No newline at end of file
/** Basic MC guiding class which corresponds to no guide. When asked for different states
* it will follow a depth first search politics to minize the number of opened states. */
class BasicStrategy : public Strategy {
- int depth_ = 100000; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer
+ int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer
public:
void copy_from(const Strategy* strategy) override
{
- const BasicStrategy* cast_strategy = static_cast<BasicStrategy const*>(strategy);
+ const BasicStrategy* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
xbt_assert(cast_strategy != nullptr);
depth_ = cast_strategy->depth_ - 1;
xbt_assert(depth_ > 0, "The exploration reached a depth greater than 100000. We will stop here to prevent weird interaction with DFSExplorer.");
BasicStrategy() = default;
~BasicStrategy() override = default;
- std::pair<aid_t, int> next_transition() const override
- {
- for (auto const& [aid, actor] : actors_to_run_) {
- /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
- if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
+ std::pair<aid_t, int> best_transition(bool must_be_todo) const override {
+ for (auto const& [aid, actor] : actors_to_run_) {
+ /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
+ if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) {
continue;
}
return std::make_pair(aid, depth_);
}
return std::make_pair(-1, depth_);
+
}
+
- void consider_best() override
- {
- for (auto& [_, actor] : actors_to_run_)
- if (actor.is_todo())
- return;
-
- for (auto& [_, actor] : actors_to_run_)
- if (actor.is_enabled() and not actor.is_done())
- actor.mark_todo();
-
+ void execute_next(aid_t aid, RemoteApp& app) override { return; }
- }
};
} // namespace simgrid::mc
public:
void copy_from(const Strategy* strategy) override
{
- const MaxMatchComm* cast_strategy = static_cast<MaxMatchComm const*>(strategy);
+ const MaxMatchComm* cast_strategy = dynamic_cast<MaxMatchComm const*>(strategy);
xbt_assert(cast_strategy != nullptr);
for (auto& [id, val] : cast_strategy->mailbox_)
mailbox_[id] = val;
MaxMatchComm() = default;
~MaxMatchComm() override = default;
- std::pair<aid_t, int> next_transition() const override
+ std::pair<aid_t, int> best_transition(bool must_be_todo) const override
{
- std::pair<aid_t, int> if_no_match = std::make_pair(-1, 0);
+ std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_+2);
for (auto const& [aid, actor] : actors_to_run_) {
- if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
- continue;
+ if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done())
+ continue;
+ int aid_value = value_of_state_;
const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
-
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) > 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting send corresponding to this recv
-
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) < 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting recv corresponding to this send
-
- if (if_no_match.first == -1)
- if_no_match = std::make_pair(aid, value_of_state_);
+
+ const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr) {
+ if (mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) > 0) {
+ aid_value--; // This means we have waiting recv corresponding to this recv
+ } else {
+ aid_value++;
+
+ }
+ }
+
+ const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr) {
+ if (mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) < 0) {
+ aid_value--; // This means we have waiting recv corresponding to this send
+ }else {
+ aid_value++;
+ }
+ }
+
+ if (aid_value < min_found.second)
+ min_found = std::make_pair(aid, aid_value);
}
- return if_no_match;
+ return min_found;
}
+
void execute_next(aid_t aid, RemoteApp& app) override
{
const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
last_transition_ = transition->type_;
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
if (cast_recv != nullptr)
last_mailbox_ = cast_recv->get_mailbox();
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
if (cast_send != nullptr)
last_mailbox_ = cast_send->get_mailbox();
}
- void consider_best() override
- {
- for (auto& [aid, actor] : actors_to_run_)
- if (actor.is_todo())
- return;
-
- for (auto& [aid, actor] : actors_to_run_) {
- if (not actor.is_enabled() || actor.is_done())
- continue;
-
- const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
-
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) > 0) {
- actor.mark_todo();
- return;
- }
-
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) < 0) {
- actor.mark_todo();
- return;
- }
- }
- for (auto& [_, actor] : actors_to_run_) {
- if (actor.is_enabled() and not actor.is_done()) {
- actor.mark_todo();
- return;
- }
- }
- }
};
} // namespace simgrid::mc
* Negative number means that much recv are waiting on that mailbox, while
* a positiv number means that much send are waiting there. */
std::map<unsigned, int> mailbox_;
- int value_of_state_ = 100000; // used to valuate the state. Corresponds to the number of in-fly communications
+ /** Used to valuate the state. Corresponds to a maximum minus the number of in-fly communications.
+ * Maximum should be set in order not to reach 0.*/
+ int value_of_state_ = _sg_mc_max_depth;
+
// The two next values are used to save the operation we execute so the next strategy can update its field accordingly
Transition::Type last_transition_;
unsigned last_mailbox_ = 0;
public:
void copy_from(const Strategy* strategy) override
{
- const MinMatchComm* cast_strategy = static_cast<MinMatchComm const*>(strategy);
+ const MinMatchComm* cast_strategy = dynamic_cast<MinMatchComm const*>(strategy);
xbt_assert(cast_strategy != nullptr);
for (auto& [id, val] : cast_strategy->mailbox_)
mailbox_[id] = val;
for (auto const& [_, val] : mailbox_)
value_of_state_ -= std::abs(val);
- if (value_of_state_ < 0)
- value_of_state_ = 0;
+ xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0");
}
MinMatchComm() = default;
~MinMatchComm() override = default;
- std::pair<aid_t, int> next_transition() const override
+ std::pair<aid_t, int> best_transition(bool must_be_todo) const override
{
- std::pair<aid_t, int> if_no_match = std::make_pair(-1, 0);
+ std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_+2);
for (auto const& [aid, actor] : actors_to_run_) {
- if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
- continue;
+ if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done())
+ continue;
+ int aid_value = value_of_state_;
const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) <= 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this recv
-
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) >= 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this send
-
- if (if_no_match.first == -1)
- if_no_match = std::make_pair(aid, value_of_state_);
+ const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr) {
+ if ((mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) <= 0) or mailbox_.count(cast_recv->get_mailbox()) == 0)
+ aid_value--; // This means we don't have waiting recv corresponding to this recv
+ else
+ aid_value++;
+ }
+ const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr) {
+ if ((mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) >= 0) or mailbox_.count(cast_send->get_mailbox()) == 0)
+ aid_value--;
+ else
+ aid_value++;
+ }
+
+ if (aid_value < min_found.second)
+ min_found = std::make_pair(aid, aid_value);
}
- return if_no_match;
+ return min_found;
}
+
void execute_next(aid_t aid, RemoteApp& app) override
{
const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
last_transition_ = transition->type_;
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
if (cast_recv != nullptr)
last_mailbox_ = cast_recv->get_mailbox();
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
if (cast_send != nullptr)
last_mailbox_ = cast_send->get_mailbox();
}
- void consider_best() override
- {
- for (auto& [aid, actor] : actors_to_run_)
- if (actor.is_todo())
- return;
-
- for (auto& [aid, actor] : actors_to_run_) {
- if (not actor.is_enabled() || actor.is_done())
- continue;
-
- const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
-
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) <= 0) {
- actor.mark_todo();
- return;
- }
-
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) >= 0) {
- actor.mark_todo();
- return;
- }
- }
- for (auto& [_, actor] : actors_to_run_) {
- if (actor.is_enabled() and not actor.is_done()) {
- actor.mark_todo();
- return;
- }
- }
- }
};
} // namespace simgrid::mc
#include "simgrid/forward.h"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_config.hpp"
#include "xbt/asserts.h"
#include <map>
#include <utility>
Strategy() = default;
virtual ~Strategy() = default;
- virtual std::pair<aid_t, int> next_transition() const = 0;
+ virtual std::pair<aid_t, int> best_transition(bool must_be_todo) const = 0;
+
+ std::pair<aid_t, int> next_transition() { return best_transition(true); }
virtual void execute_next(aid_t aid, RemoteApp& app) = 0;
// Mark the first enabled and not yet done transition as todo
// If there's already a transition marked as todo, does nothing
- virtual void consider_best() = 0;
+ void consider_best() {
+ for (auto& [_, actor] :actors_to_run_)
+ if (actor.is_todo())
+ return;
+ aid_t best_aid = best_transition(false).first;
+ if (best_aid != -1)
+ actors_to_run_.at(best_aid).mark_todo();
+ }
// Mark aid as todo. If it makes no sense, ie. if it is already done or not enabled,
// raise an error
#include "src/mc/transition/Transition.hpp"
+#define MAX_RAND 100000
+
namespace simgrid::mc {
/** Guiding strategy that valuate states randomly */
UniformStrategy()
{
for (long aid = 0; aid < 10; aid++)
- valuation[aid] = rand() % 1000;
+ valuation[aid] = rand() % 10000;
}
void copy_from(const Strategy* strategy) override
{
for (auto& [aid, _] : actors_to_run_)
- valuation[aid] = rand() % 1000;
+ valuation[aid] = rand() % 10000;
}
- std::pair<aid_t, int> next_transition() const override
+ std::pair<aid_t, int> best_transition(bool must_be_todo) const override
{
int possibilities = 0;
// Consider only valid actors
for (auto const& [aid, actor] : actors_to_run_) {
- if (actor.is_todo() and (not actor.is_done()) and actor.is_enabled())
+ if ((actor.is_todo() or not must_be_todo) and (not actor.is_done()) and actor.is_enabled())
possibilities++;
}
int chosen;
if (possibilities == 0)
- return std::make_pair(-1, 100000);
+ return std::make_pair(-1, 0);
if (possibilities == 1)
chosen = 0;
else
chosen = rand() % possibilities;
for (auto const& [aid, actor] : actors_to_run_) {
- if ((not actor.is_todo()) or actor.is_done() or (not actor.is_enabled()))
+ if (((not actor.is_todo()) and must_be_todo) or actor.is_done() or (not actor.is_enabled()))
continue;
if (chosen == 0) {
return std::make_pair(aid, valuation.at(aid));
chosen--;
}
- return std::make_pair(-1, 100000);
+ return std::make_pair(-1, 0);
}
+
void execute_next(aid_t aid, RemoteApp& app) override {}
-
- void consider_best() override
- {
-
- int possibilities = 0;
- // Consider only valid actors
- // If some actor are already considered as todo, skip
- for (auto const& [aid, actor] : actors_to_run_) {
- if (valuation.count(aid) == 0)
- for (auto& [aid, _] : actors_to_run_)
- valuation[aid] = rand() % 1000;
- if (actor.is_todo())
- return;
- if (actor.is_enabled() and not actor.is_done())
- possibilities++;
- }
-
- int chosen;
- if (possibilities == 0)
- return;
- if (possibilities == 1)
- chosen = 0;
- else
- chosen = rand() % possibilities;
-
- for (auto& [aid, actor] : actors_to_run_) {
- if (not actor.is_enabled() or actor.is_done())
- continue;
- if (chosen == 0) {
- actor.mark_todo();
- return;
- }
- chosen--;
- }
- THROW_IMPOSSIBLE; // One actor should be marked as todo before
- }
+
};
} // namespace simgrid::mc
