Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
objectifies surf::Action::State
[simgrid.git] / src / mc / mc_safety.h
1 /* Copyright (c) 2007-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 #ifndef SIMGRID_MC_SAFETY_H
8 #define SIMGRID_MC_SAFETY_H
9
10 #include <stdint.h>
11
12 #include <vector>
13 #include <memory>
14
15 #include <simgrid_config.h>
16
17 #include <xbt/base.h>
18 #include <xbt/dynar.h>
19
20 #include "src/mc/mc_forward.hpp"
21 #include "src/mc/mc_state.h"
22
23 namespace simgrid {
24 namespace mc {
25
26 enum class ReductionMode {
27   unset,
28   none,
29   dpor,
30 };
31
32 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
33
34 int modelcheck_safety(void);
35
36 struct XBT_PRIVATE VisitedState {
37   simgrid::mc::Snapshot* system_state = nullptr;
38   size_t heap_bytes_used = 0;
39   int nb_processes = 0;
40   int num = 0;
41   int other_num = 0; // dot_output for
42
43   VisitedState();
44   ~VisitedState();
45 };
46
47 extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
48 XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state);
49
50 }
51 }
52
53 #endif