From: Martin Quinson <martin.quinson@loria.fr>
Date: Tue, 7 Feb 2017 15:56:43 +0000 (+0100)
Subject: more info to the user.
X-Git-Tag: v3_15~466
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/da9f5f7a90d30639cf0f1dd8f32ce7040c23c72b?ds=sidebyside

more info to the user.
---

diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc
index 4799993422..90d637c68d 100644
--- a/doc/doxygen/options.doc
+++ b/doc/doxygen/options.doc
@@ -382,7 +382,7 @@ For now, this configuration variable can take 2 values:
  * none: Do not apply any kind of reduction (mandatory for now for
    liveness properties)
  * dpor: Apply Dynamic Partial Ordering Reduction. Only valid if you
-   verify local safety properties.
+   verify local safety properties (default value for safety checks).
 
 \subsection options_modelchecking_visited model-check/visited, Cycle detection
 
diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh
index 201f5d8598..298d92ef7e 100644
--- a/examples/msg/mc/bugged1.tesh
+++ b/examples/msg/mc/bugged1.tesh
@@ -3,7 +3,7 @@
 ! expect return 1
 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
-> [  0.000000] (0:maestro@) Check a safety property
+> [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (2:client@HostB) Sent!
 > [  0.000000] (3:client@HostC) Sent!
 > [  0.000000] (1:server@HostA) OK
diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh
index 518db4c665..ba13938481 100644
--- a/examples/msg/mc/bugged2.tesh
+++ b/examples/msg/mc/bugged2.tesh
@@ -3,7 +3,7 @@
 ! expect return 1
 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
-> [  0.000000] (0:maestro@) Check a safety property
+> [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (2:client@HostB) Send 1
 > [  0.000000] (3:client@HostC) Send 2
 > [  0.000000] (1:server@HostA) Received 1
diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index cf609b4134..d81492c80e 100644
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -308,7 +308,9 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   if (_sg_mc_termination)
     XBT_INFO("Check non progressive cycles");
   else
-    XBT_INFO("Check a safety property");
+    XBT_INFO("Check a safety property. Reduction is: %s.",
+        (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
+            (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
   simgrid::mc::session->initialize();
 
   XBT_DEBUG("Starting the safety algorithm");
diff --git a/teshsuite/mc/random-bug/random-bug-report.tesh b/teshsuite/mc/random-bug/random-bug-report.tesh
index 2ec57351b5..1fec35e7e1 100644
--- a/teshsuite/mc/random-bug/random-bug-report.tesh
+++ b/teshsuite/mc/random-bug/random-bug-report.tesh
@@ -1,7 +1,7 @@
 #!/usr/bin/env tesh
 ! expect return 1
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check/record:1
-> [  0.000000] (0:maestro@) Check a safety property
+> [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************