src/mc/mc_record.h

   1 /* Copyright (c) 2014-2015. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 /** \file mc_record.h
   8  *
   9  *  This file contains the MC replay/record functionnality.
  10  *  A MC path may be recorded by using ``-cfg=model-check/record:1`'`.
  11  *  The path is written in the log output and an be replayed with MC disabled
  12  *  (even with an non-LC build) with `--cfg=model-check/replay:$replayPath`.
  13  *
  14  *  The same version of Simgrid should be used and the same arguments should be
  15  *  passed to the application (without the MC specific arguments).
  16  */
  17
  18 #ifndef SIMGRID_MC_RECORD_H
  19 #define SIMGRID_MC_RECORD_H
  20
  21 #include <string>
  22 #include <vector>
  23
  24 #include <xbt/base.h>
  25
  26 #include "src/mc/Transition.hpp"
  27
  28 namespace simgrid {
  29 namespace mc {
  30
  31 typedef std::vector<Transition> RecordTrace;
  32
  33 /** Convert a string representation of the path into a array of `simgrid::mc::Transition`
  34  */
  35 XBT_PRIVATE RecordTrace parseRecordTrace(const char* data);
  36 XBT_PRIVATE std::string traceToString(simgrid::mc::RecordTrace const& trace);
  37 XBT_PRIVATE void dumpRecordPath();
  38
  39 XBT_PRIVATE void replay(RecordTrace const& trace);
  40 XBT_PRIVATE void replay(const char* trace);
  41
  42 }
  43 }
  44
  45 SG_BEGIN_DECL()
  46
  47 /** Whether the MC record mode is enabled
  48  *
  49  *  The behaviour is not changed. The only real difference is that
  50  *  the path is writtent in the log when an interesting path is found.
  51  */
  52 #define MC_record_is_active() _sg_do_model_check_record
  53
  54 // **** Data conversion
  55
  56 SG_END_DECL()
  57
  58 #endif