1 /* Copyright (c) 2014. 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).
22 #include "simgrid_config.h"
26 /** Whether the MC record mode is enabled
28 * The behaviour is not changed. The only real difference is that
29 * the path is writtent in the log when an interesting path is found.
31 #define MC_record_is_active() _sg_do_model_check_record
33 // **** Data conversion
35 /** An element in the recorded path
37 * At each decision point, we need to record which process transition
38 * is trigerred and potentially which value is associated with this
39 * transition. The value is used to find which communication is triggerred
40 * in things like waitany and for associating a given value of MC_random()
43 typedef struct s_mc_record_item {
46 } s_mc_record_item_t, *mc_record_item_t;
48 /** Convert a string representation of the path into a array of `s_mc_record_item_t`
50 xbt_dynar_t MC_record_from_string(const char* data);
52 /** Generate a string representation
54 * The current format is a ";"-delimited list of pairs:
55 * "pid0,value0;pid2,value2;pid3,value3". The value can be
56 * omitted is it is null.
58 char* MC_record_stack_to_string(xbt_fifo_t stack);
60 /** Dump the path represented by a given stack in the log
62 void MC_record_dump_path(xbt_fifo_t stack);
66 /** Replay a path represented by the record items
68 * \param start Array of record item
69 * \item count Number of record items
71 void MC_record_replay(mc_record_item_t start, size_t count);
73 /** Replay a path represented by a string
75 * \param data String representation of the path
77 void MC_record_replay_from_string(const char* data);
79 void MC_record_replay_init(void);