Revalidate the tesh outputs after cosmetics to the output in mc_dfs

diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
index 4e1450d..2e610e7 100644 (file)
--- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
+++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
@@ -4,6 +4,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Start a DFS exploration. Reduction is: dpor.
 > [Checker] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Execution came to an end at 1;1;0 (state: 3, depth: 3)
 > [Checker] Backtracking from 1;1;0
 > [Checker] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
 
@@ -13,6 +14,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 2: BARRIER_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
 > [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)
@@ -34,6 +36,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
 > [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)

diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
index 10c30de..e7dedc4 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
+++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
@@ -11,6 +11,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 2: MUTEX_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] INDEPENDENT Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3)
@@ -27,6 +28,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:1) (stack depth: 4, state: 10, 0 interleaves)
 > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 5, state: 11, 0 interleaves)
 > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 12, 0 interleaves)
+> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 13, depth: 7)
 > [Checker] Backtracking from 2;1;2;2;1;1;0
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 0, owner:1) (state=10)
@@ -55,6 +57,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 10, 0 interleaves)
 > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 11, 0 interleaves)
 > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 12, 0 interleaves)
+> [Checker] Execution came to an end at 1;1;1;2;2;2;3;3;3;4;4;4;0 (state: 13, depth: 13)
 > [Checker] Backtracking from 1;1;1;2;2;2;3;3;3;4;4;4;0
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 1, owner:-1) (state=9)
@@ -89,6 +92,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:3) (stack depth: 10, state: 16, 0 interleaves)
 > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 11, state: 17, 0 interleaves)
 > [Checker] Execute 3: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 18, 0 interleaves)
+> [Checker] Execution came to an end at 1;1;1;2;2;2;4;3;4;4;3;3;0 (state: 19, depth: 13)
 > [Checker] Backtracking from 1;1;1;2;2;2;4;3;4;4;3;3;0
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 1, owner:3) (state=16)
@@ -139,6 +143,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 28, 0 interleaves)
 > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 29, 0 interleaves)
 > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 30, 0 interleaves)
+> [Checker] Execution came to an end at 2;1;2;2;1;1;3;3;3;4;4;4;0 (state: 31, depth: 13)
 > [Checker] Backtracking from 2;1;2;2;1;1;3;3;3;4;4;4;0
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 1, owner:-1) (state=27)
@@ -173,6 +178,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:3) (stack depth: 10, state: 34, 0 interleaves)
 > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 11, state: 35, 0 interleaves)
 > [Checker] Execute 3: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 36, 0 interleaves)
+> [Checker] Execution came to an end at 2;1;2;2;1;1;4;3;4;4;3;3;0 (state: 37, depth: 13)
 > [Checker] Backtracking from 2;1;2;2;1;1;4;3;4;4;3;3;0
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 1, owner:3) (state=34)

diff --git a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
index eb2a5e1..d63b175 100644 (file)
--- a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
+++ b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
@@ -26,6 +26,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] Execute 2: SEM_LOCK(semaphore: 1) (stack depth: 22, state: 22, 0 interleaves)
 > [Checker] Execute 2: SEM_WAIT(semaphore: 1, granted: yes) (stack depth: 23, state: 23, 0 interleaves)
 > [Checker] Execute 2: SEM_UNLOCK(semaphore: 0) (stack depth: 24, state: 24, 0 interleaves)
+> [Checker] Execution came to an end at 1;1;1;1;2;2;2;1;1;1;2;2;2;1;1;1;2;2;2;1;1;2;2;2;0 (state: 25, depth: 25)
 > [Checker] Backtracking from 1;1;1;1;2;2;2;1;1;1;2;2;2;1;1;1;2;2;2;1;1;2;2;2;0
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   SEM_UNLOCK(semaphore: 1) (state=21)

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index c310c05..286c3f7 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -131,7 +131,7 @@ void DFSExplorer::run()
 
       if (mc_model_checker->get_remote_process().actors().empty()) {
         mc_model_checker->finalize_app();
-        XBT_INFO("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
+        XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
                  state->num_, stack_.size());
       }
       this->backtrack();