> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
-> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
-> [Checker] Backtracking from 1;2;1;2;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
+> [Checker] Backtracking from 1;2;1;2;0
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 7, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
-> [Checker] Backtracking from 2;1;1;2;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
+> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
+> [Checker] Backtracking from 2;1;1;2;0
> [Checker] DFS exploration ended. 9 unique states visited; 2 backtracks (10 transition replays, 0 states visited overall)
$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
-> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;2;3;1;2;3;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;2;3;1;2;3;0
+> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 8, 0 interleaves)
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves)
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves)
-> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves)
-> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
-> [Checker] Backtracking from 1;3;2;1;2;3;0
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
+> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
+> [Checker] Backtracking from 1;3;2;1;2;3;0
> [Checker] DFS exploration ended. 12 unique states visited; 2 backtracks (14 transition replays, 1 states visited overall)
\ No newline at end of file
> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
-> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;1;1;2;2;2;0
-> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
-> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
> [Checker] INDEPENDENT Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
-> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves)
-> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7)
-> [Checker] Backtracking from 1;1;2;1;2;2;0
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
+> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;1;1;2;2;2;0
+> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10)
+> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7)
+> [Checker] Backtracking from 1;1;2;1;2;2;0
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 12, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 13, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13)
> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 14, 0 interleaves)
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
-> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7)
-> [Checker] Backtracking from 2;1;2;2;1;1;0
-> [Checker] Dependent Transitions:
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
+> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=15)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13)
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
+> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7)
+> [Checker] Backtracking from 2;1;2;2;1;1;0
> [Checker] DFS exploration ended. 17 unique states visited; 3 backtracks (21 transition replays, 2 states visited overall)
$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/api/State.hpp"
+#include "src/mc/api/guide/BasicGuide.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
long State::expended_states_ = 0;
-State::State(RemoteApp& remote_app) : num_(++expended_states_)
+State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_unique<BasicGuide>())
{
- remote_app.get_actors_status(actors_to_run_);
+ remote_app.get_actors_status(guide->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
}
State::State(RemoteApp& remote_app, const State* parent_state)
- : num_(++expended_states_), parent_state_(parent_state)
+ : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
{
- remote_app.get_actors_status(actors_to_run_);
+ remote_app.get_actors_status(guide->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
remote_app.get_remote_process_memory());
-
- /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
- if (_sg_mc_sleep_set) {
- /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
- * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
- * it is not explored*/
- for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
-
- if (not parent_state_->get_transition()->depends(&transition)) {
-
- sleep_set_.emplace(aid, transition);
- if (actors_to_run_.count(aid) != 0) {
- XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
-
- actors_to_run_.at(aid).mark_done();
- }
- } else
- XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
- transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str());
- }
+ /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
+ if (_sg_mc_sleep_set) {
+ /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
+ * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
+ * it is not explored*/
+ for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
+
+ if (not parent_state_->get_transition()->depends(&transition)) {
+
+ sleep_set_.emplace(aid, transition);
+ if (guide->actors_to_run_.count(aid) != 0) {
+ XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
+
+ guide->actors_to_run_.at(aid).mark_done();
+ }
+ } else
+ XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
+ transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str());
+ }
}
}
std::size_t State::count_todo() const
{
- return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
-}
-
-void State::mark_all_enabled_todo()
-{
- for (auto const& [aid, _] : this->get_actors_list()) {
- if (this->is_actor_enabled(aid) and not is_actor_done(aid)) {
- this->mark_todo(aid);
- }
- }
+ return boost::range::count_if(this->guide->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
}
Transition* State::get_transition() const
aid_t State::next_transition() const
{
- XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size());
- for (auto const& [aid, actor] : actors_to_run_) {
+ XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide->actors_to_run_.size());
+ for (auto const& [aid, actor] : guide->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()) {
return -1;
}
+std::pair<aid_t, double> State::next_transition_guided() const
+{
+ return guide->next_transition();
+}
+
+// This should be done in GuidedState, or at least interact with it
void State::execute_next(aid_t next, RemoteApp& app)
{
// This actor is ready to be executed. Execution involves three phases:
// 1. Identify the appropriate ActorState to prepare for execution
// when simcall_handle will be called on it
- auto& actor_state = actors_to_run_.at(next);
+ auto& actor_state = guide->actors_to_run_.at(next);
const unsigned times_considered = actor_state.do_consider();
const auto* expected_executed_transition = actor_state.get_transition(times_considered);
xbt_assert(expected_executed_transition != nullptr,
#include "src/mc/api/ActorState.hpp"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/api/guide/GuidedState.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "src/mc/transition/Transition.hpp"
/** Sequential state ID (used for debugging) */
long num_ = 0;
- /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
- * state */
- std::map<aid_t, ActorState> actors_to_run_;
-
/** Snapshot of system state (if needed) */
std::shared_ptr<Snapshot> system_state_;
/** Unique parent of this state. Required both for sleep set computation
and for guided model-checking */
const State* parent_state_;
-
+
+ std::unique_ptr<GuidedState> guide;
+
/* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
* set. With this information, it is check whether it should be removed from it or not when exploring a new
* transition */
std::map<aid_t, Transition> sleep_set_;
-
+
public:
explicit State(RemoteApp& remote_app);
explicit State(RemoteApp& remote_app, const State* parent_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
- aid_t next_transition() const;
+ aid_t next_transition() const; // this function should disapear as it is redundant with the next one
+
+ /* Same as next_transition, but choice is now guided, and a double corresponding to the
+ internal cost of the transition is returned */
+ std::pair<aid_t, double> next_transition_guided() const;
/* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
* next_transition() */
long get_num() const { return num_; }
std::size_t count_todo() const;
- void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
- void mark_all_enabled_todo();
- bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
+
+ void consider_one(aid_t aid) { guide->consider_one(aid); }
+ void consider_best() { guide->consider_best(); }
+ void consider_all() { guide->consider_all(); }
+
+ bool is_actor_done(aid_t actor) const { return guide->actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
- std::map<aid_t, ActorState> const& get_actors_list() const { return actors_to_run_; }
+ std::map<aid_t, ActorState> const& get_actors_list() const { return guide->actors_to_run_; }
- unsigned long get_actor_count() const { return actors_to_run_.size(); }
- bool is_actor_enabled(aid_t actor) { return actors_to_run_.at(actor).is_enabled(); }
+ unsigned long get_actor_count() const { return guide->actors_to_run_.size(); }
+ bool is_actor_enabled(aid_t actor) { return guide->actors_to_run_.at(actor).is_enabled(); }
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
- void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
-
+ void add_sleep_set(Transition* t)
+ {
+ sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
+ }
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
--- /dev/null
+/* Copyright (c) 2007-2023. 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. */
+
+#ifndef SIMGRID_MC_BASICGUIDE_HPP
+#define SIMGRID_MC_BASICGUIDE_HPP
+
+namespace simgrid::mc {
+
+/** Basic MC guiding class which corresponds to no guide at all (random choice) */
+// Not Yet fully implemented
+class BasicGuide : public GuidedState {
+public:
+ std::pair<aid_t, double> 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()) {
+ continue;
+ }
+
+ return std::make_pair(aid, 1.0);
+ }
+ return std::make_pair(-1, 0.0);
+ }
+ void execute_next(aid_t aid, RemoteApp& app) override { return; }
+
+ void consider_best() override
+ {
+ for (auto& [_, actor] : actors_to_run_) {
+ if (actor.is_todo())
+ return;
+ if (actor.is_enabled() and not actor.is_done()) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
--- /dev/null
+/* Copyright (c) 2007-2023. 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. */
+
+#include "xbt/asserts.h"
+
+#ifndef SIMGRID_MC_GUIDEDSTATE_HPP
+#define SIMGRID_MC_GUIDEDSTATE_HPP
+
+namespace simgrid::mc {
+
+class GuidedState {
+protected:
+ /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
+ * state */
+ std::map<aid_t, ActorState> actors_to_run_;
+
+public:
+ virtual std::pair<aid_t, double> next_transition() const = 0;
+ virtual void execute_next(aid_t aid, RemoteApp& app) = 0;
+ virtual void consider_best() = 0;
+
+ // Mark the first enabled and not yet done transition as todo
+ // If there's already a transition marked as todo, does nothing
+ void consider_one(aid_t aid)
+ {
+ xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(),
+ "Tried to mark as TODO actor %ld but it is either not enabled or already done", aid);
+ actors_to_run_.at(aid).mark_todo();
+ }
+ // Matk as todo all actors enabled that are not done yet
+ void consider_all()
+ {
+ for (auto& [_, actor] : actors_to_run_)
+ if (actor.is_enabled() and not actor.is_done())
+ actor.mark_todo();
+ }
+
+ friend class State;
+};
+
+} // namespace simgrid::mc
+
+#endif
}
// Search for the next transition
- aid_t next = state->next_transition();
+ // next_transition returns a pair<aid_t, double> in case we want to consider multiple state
+ auto [next, _] = state->next_transition_guided();
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
-
+
if (state->get_actor_count() == 0) {
get_remote_app().finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
-
}
-
+
this->backtrack();
continue;
}
std::unique_ptr<State> next_state;
next_state = std::make_unique<State>(get_remote_app(), state);
-
on_state_creation_signal(next_state.get(), get_remote_app());
-
+ /* Sleep set procedure:
+ * adding the taken transition to the sleep set of the original state.
+ * <!> Since the parent sleep set is used to compute the child sleep set, this need to be
+ * done after next_state creation */
+ XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
+ state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+ state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
+
+ /* DPOR persistent set procedure:
+ * for each new transition considered, check if it depends on any other previous transition executed before it
+ * on another process. If there exists one, find the more recent, and add its process to the interleave set.
+ * If the process is not enabled at this point, then add every enabled process to the interleave */
+ if (reduction_mode_ == ReductionMode::dpor) {
+ aid_t issuer_id = state->get_transition()->aid_;
+ for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
+ State* prev_state = i->get();
+ if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
+ XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
+ prev_state->get_transition()->to_string().c_str(), issuer_id);
+ continue;
+ } else if (prev_state->get_transition()->depends(state->get_transition())) {
+ XBT_VERB("Dependent Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+
+ if (prev_state->is_actor_enabled(issuer_id)) {
+ if (not prev_state->is_actor_done(issuer_id))
+ prev_state->consider_one(issuer_id);
+ else
+ XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
+ } else {
+ XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
+ "transition as todo",
+ issuer_id);
+ prev_state->consider_all();
+ }
+ break;
+ } else {
+ XBT_VERB("INDEPENDENT Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+ }
+ }
+ }
+
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto const& [aid, _] : next_state->get_actors_list()) {
- if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) {
- next_state->mark_todo(aid);
- if (reduction_mode_ == ReductionMode::dpor)
- break; // With DPOR, we take the first enabled transition
- }
- }
+ if (reduction_mode_ == ReductionMode::dpor)
+ next_state->consider_best(); // Take only one transition if DPOR: others may be considered later if required
+ else
+ next_state->consider_all();
dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
state->get_transition()->dot_string().c_str());
/* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
* In the first case, we need to remove the last transition corresponding to the Finalize */
if (stack_.back()->get_transition()->aid_ == 0)
- stack_.pop_back();
-
+ stack_.pop_back();
+
/* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
- * have it empty in the way. For each deleted state, check if the request that has generated it (from its
- * predecessor state) depends on any other previous request executed before it on another process. If there exists one,
- * find the more recent, and add its process to the interleave set. If the process is not enabled at this point,
- * then add every enabled process to the interleave */
+ * have it empty in the way. */
bool found_backtracking_point = false;
while (not stack_.empty() && not found_backtracking_point) {
std::unique_ptr<State> state = std::move(stack_.back());
stack_.pop_back();
- XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
- state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
- state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
-
- if (reduction_mode_ == ReductionMode::dpor) {
- aid_t issuer_id = state->get_transition()->aid_;
- for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
- State* prev_state = i->get();
- if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
- XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
- prev_state->get_transition()->to_string().c_str(), issuer_id);
- continue;
- } else if (prev_state->get_transition()->depends(state->get_transition())) {
- XBT_VERB("Dependent Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
-
- if (prev_state->is_actor_enabled(issuer_id)) {
- if (not prev_state->is_actor_done(issuer_id))
- prev_state->mark_todo(issuer_id);
- else
- XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
- } else {
- XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
- "transition as todo",
- issuer_id);
- prev_state->mark_all_enabled_todo();
- }
- break;
- } else {
- XBT_VERB("INDEPENDENT Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
- }
- }
- }
if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over
XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
} else {
XBT_DEBUG("Back-tracking to state %ld at depth %zu: %lu transitions left to be explored", state->get_num(),
stack_.size() + 1, state->count_todo());
- stack_.push_back(std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
+ stack_.push_back(
+ std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
found_backtracking_point = true;
}
}
/* Get an enabled actor and insert it in the interleave set of the initial state */
XBT_DEBUG("Initial state. %lu actors to consider", initial_state->get_actor_count());
- for (auto const& [aid, _] : initial_state->get_actors_list()) {
- if (initial_state->is_actor_enabled(aid)) {
- initial_state->mark_todo(aid);
- if (reduction_mode_ == ReductionMode::dpor) {
- XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid);
- break;
- }
- XBT_DEBUG("Actor %ld is TODO", aid);
- }
- }
+ if (reduction_mode_ == ReductionMode::dpor)
+ initial_state->consider_best();
+ else
+ initial_state->consider_all();
stack_.push_back(std::move(initial_state));
}
/* Add all enabled actors to the interleave set of the initial state */
for (auto const& [aid, _] : next_pair->app_state_->get_actors_list())
if (next_pair->app_state_->is_actor_enabled(aid))
- next_pair->app_state_->mark_todo(aid);
+ next_pair->app_state_->consider_one(aid);
next_pair->requests = next_pair->app_state_->count_todo();
/* FIXME : get search_cycle value for each accepting state */
auto next_state = this->get_current_state();
// In UDPOR, we care about all enabled transitions in a given state
- next_state->mark_all_enabled_todo();
+ next_state->consider_all();
return next_state;
}
