1 /* Copyright (c) 2014-2015. The SimGrid Team.
2 * All rights reserved. */
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. */
8 * This file contains the MC replay/record functionnality.
9 * A MC path may be recorded by using ``-cfg=model-check/record:1`'`.
10 * The path is written in the log output and an be replayed with MC disabled
11 * (even with an non-LC build) with `--cfg=model-check/replay:$replayPath`.
13 * The same version of Simgrid should be used and the same arguments should be
14 * passed to the application (without the MC specific arguments).
17 #ifndef SIMGRID_MC_RECORD_H
18 #define SIMGRID_MC_RECORD_H
24 /** Whether the MC record mode is enabled
26 * The behaviour is not changed. The only real difference is that
27 * the path is writtent in the log when an interesting path is found.
29 #define MC_record_is_active() _sg_do_model_check_record
31 // **** Data conversion
33 /** An element in the recorded path
35 * At each decision point, we need to record which process transition
36 * is trigerred and potentially which value is associated with this
37 * transition. The value is used to find which communication is triggerred
38 * in things like waitany and for associating a given value of MC_random()
41 typedef struct s_mc_record_item {
44 } s_mc_record_item_t, *mc_record_item_t;
46 /** Convert a string representation of the path into a array of `s_mc_record_item_t`
48 XBT_PRIVATE xbt_dynar_t MC_record_from_string(const char* data);
50 /** Generate a string representation
52 * The current format is a ";"-delimited list of pairs:
53 * "pid0,value0;pid2,value2;pid3,value3". The value can be
54 * omitted is it is null.
56 XBT_PRIVATE char* MC_record_stack_to_string(xbt_fifo_t stack);
58 /** Dump the path represented by a given stack in the log
60 XBT_PRIVATE void MC_record_dump_path(xbt_fifo_t stack);
64 /** Replay a path represented by the record items
66 * \param start Array of record item
67 * \item count Number of record items
69 XBT_PRIVATE void MC_record_replay(mc_record_item_t start, size_t count);
71 /** Replay a path represented by a string
73 * \param data String representation of the path
75 XBT_PRIVATE void MC_record_replay_from_string(const char* data);
77 XBT_PRIVATE void MC_record_replay_init(void);