Remove option 'model-check/record': paths are recorded in any cases

diff --git a/ChangeLog b/ChangeLog
index a967110..91fbb8c 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -12,6 +12,9 @@ SMPI:
  - MPI/IO is now supported over the Storage API (no files are written or read, storage is simulated). Supported calls are all synchronous ones.
  - MPI interface is now const correct for input parameters
 
  - MPI/IO is now supported over the Storage API (no files are written or read, storage is simulated). Supported calls are all synchronous ones.
  - MPI interface is now const correct for input parameters
 

+Model-checker:
+ - Remove option 'model-check/record': Paths are recorded in any cases now.
+

 Fixed bugs (GH=GitHub; FG=FramaGit):
  - FG#10: Can not use MSG_process_set_data from SMPI any more
  - FG#11: Auto-restart actors forget their on_exit behavior
 Fixed bugs (GH=GitHub; FG=FramaGit):
  - FG#10: Can not use MSG_process_set_data from SMPI any more
  - FG#11: Auto-restart actors forget their on_exit behavior

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index 7a59994..ac9affc 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -110,7 +110,6 @@ Existing Configuration Items
 - **model-check/hash:** :ref:`cfg=model-checker/hash`
 - **model-check/max-depth:** :ref:`cfg=model-check/max-depth`
 - **model-check/property:** :ref:`cfg=model-check/property`
 - **model-check/hash:** :ref:`cfg=model-checker/hash`
 - **model-check/max-depth:** :ref:`cfg=model-check/max-depth`
 - **model-check/property:** :ref:`cfg=model-check/property`

-- **model-check/record:** :ref:`cfg=model-check/record`

 - **model-check/reduction:** :ref:`cfg=model-check/reduction`
 - **model-check/replay:** :ref:`cfg=model-check/replay`
 - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`
 - **model-check/reduction:** :ref:`cfg=model-check/reduction`
 - **model-check/replay:** :ref:`cfg=model-check/replay`
 - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`


@@ -681,11 +680,10 @@ Currently most of the state is not included in the hash because the
 implementation was found to be buggy and this options is not as useful as
 it could be. For this reason, it is currently disabled by default.
 
 implementation was found to be buggy and this options is not as useful as
 it could be. For this reason, it is currently disabled by default.
 

-.. _cfg=model-check/record:

 .. _cfg=model-check/replay:
 
 .. _cfg=model-check/replay:
 

-Recording and replaying verifications
-.....................................
+Replaying buggy execution paths out of the model-checker
+........................................................

 
 Debugging the problems reported by the model-checker is challenging: First, the
 application under verification cannot be debugged with gdb because the
 
 Debugging the problems reported by the model-checker is challenging: First, the
 application under verification cannot be debugged with gdb because the


@@ -697,11 +695,7 @@ enabling the usage of classical debugging tools.
 
 When the model-checker finds an interesting path in the application
 execution graph (where a safety or liveness property is violated), it
 
 When the model-checker finds an interesting path in the application
 execution graph (where a safety or liveness property is violated), it

-can generate an identifier for this path. To enable this behavious the
-``model-check/record`` must be set to **yes**, which is the case
-by default.
-
-Here is an example of output:
+generates an identifier for this path. Here is an example of output:

 
 .. code-block:: shell
 
 
 .. code-block:: shell
 


@@ -717,11 +711,11 @@ Here is an example of output:
    [  0.000000] (0:@) Visited states = 68
    [  0.000000] (0:@) Executed transitions = 46
 
    [  0.000000] (0:@) Visited states = 68
    [  0.000000] (0:@) Executed transitions = 46
 

-This path can then be replayed outside of the model-checker (and even
-in non-MC build of simgrid) by setting the ``model-check/replay`` item
-to the given path. The other options should be the same (but the
-model-checker should be disabled). Note that format and meaning of the
-path may change between different releases.
+The interesting line is ``Path = 1/3;1/4``, which means that you should use
+`--cfg=model-check/replay:1/3;1/4`` to replay your application on the buggy
+execution path. The other options should be the same (but the model-checker
+should be disabled). Note that format and meaning of the path may change between
+different releases.

 
 Configuring the User Code Virtualization
 ----------------------------------------
 
 Configuring the User Code Virtualization
 ----------------------------------------

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index ed3220f..584d0ba 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -54,8 +54,6 @@ simgrid::config::Flag<bool> _sg_mc_timeout{
 int _sg_do_model_check = 0;
 int _sg_mc_max_visited_states = 0;
 
 int _sg_do_model_check = 0;
 int _sg_mc_max_visited_states = 0;
 

-simgrid::config::Flag<bool> _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", true};
-

 simgrid::config::Flag<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
                               "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "
 simgrid::config::Flag<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
                               "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 6ee0daf..ffc0c2e 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -11,7 +11,6 @@
 /********************************** Configuration of MC **************************************/
 extern "C" XBT_PUBLIC int _sg_do_model_check;
 extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_record_path;
 /********************************** Configuration of MC **************************************/
 extern "C" XBT_PUBLIC int _sg_do_model_check;
 extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_record_path;

-extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_do_model_check_record;

 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_ksm;
 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_ksm;

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index dd19a66..115695c 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -18,8 +18,7 @@
 #include "src/mc/mc_state.hpp"
 #endif
 
 #include "src/mc/mc_state.hpp"
 #endif
 

-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
-  " Logging specific to MC record/replay facility");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, "Logging specific to MC record/replay facility");

 
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {


@@ -99,10 +98,8 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace)
 
 void dumpRecordPath()
 {
 
 void dumpRecordPath()
 {

-  if (MC_record_is_active()) {
-    RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace();
-    XBT_INFO("Path = %s", traceToString(trace).c_str());
-  }
+  RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace();
+  XBT_INFO("Path = %s", traceToString(trace).c_str());

 }
 
 #endif
 }
 
 #endif

diff --git a/src/mc/mc_record.hpp b/src/mc/mc_record.hpp
index df5285e..d4ead6f 100644 (file)
--- a/src/mc/mc_record.hpp
+++ b/src/mc/mc_record.hpp
@@ -6,9 +6,8 @@
 /** \file mc_record.hpp
  *
  *  This file contains the MC replay/record functionnality.
 /** \file mc_record.hpp
  *
  *  This file contains the MC replay/record functionnality.

- *  A MC path may be recorded by using ``-cfg=model-check/record:1`'`.
- *  The path is written in the log output and an be replayed with MC disabled
- *  (even with an non-MC build) with `--cfg=model-check/replay:$replayPath`.
+ *  The recorded path is written in the log output and can be replayed with MC disabled
+ *  (even with an non-MC build) using `--cfg=model-check/replay:$replayPath`.

  *
  *  The same version of Simgrid should be used and the same arguments should be
  *  passed to the application (without the MC specific arguments).
  *
  *  The same version of Simgrid should be used and the same arguments should be
  *  passed to the application (without the MC specific arguments).


@@ -39,13 +38,6 @@ XBT_PRIVATE void replay(const std::string& trace);
 }
 }
 
 }
 }
 

-/** Whether the MC record mode is enabled
- *
- *  The behaviour is not changed. The only real difference is that
- *  the path is writtent in the log when an interesting path is found.
- */
-#define MC_record_is_active() _sg_do_model_check_record
-

 // **** Data conversion
 
 #endif
 // **** Data conversion
 
 #endif