more info to the user.

diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc
index 4799993..90d637c 100644 (file)
--- 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
  * 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
 
 
 \subsection options_modelchecking_visited model-check/visited, Cycle detection
 

diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh
index 201f5d8..298d92e 100644 (file)
--- 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
 ! 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
 > [  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 518db4c..ba13938 100644 (file)
--- 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
 ! 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
 > [  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 cf609b4..d81492c 100644 (file)
--- 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
   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");
   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 2ec5735..1fec35e 100644 (file)
--- 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
 #!/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@) **************************
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************