Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Documentation cleanup
[simgrid.git] / src / mc / Checker.hpp
1 /* Copyright (c) 2016. 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_CHECKER_HPP
8 #define SIMGRID_MC_CHECKER_HPP
9
10 #include <functional>
11 #include <memory>
12 #include <string>
13
14 #include "src/mc/mc_forward.hpp"
15 #include "src/mc/mc_record.h"
16 #include "src/mc/Session.hpp"
17
18 namespace simgrid {
19 namespace mc {
20
21 /** A model-checking algorithm
22  *
23  *  This is an abstract base class used to group the data, state, configuration
24  *  of a model-checking algorithm.
25  *
26  *  Implementing this interface will probably not be really mandatory,
27  *  you might be able to write your model-checking algorithm as plain
28  *  imperative code instead.
29  *
30  *  It is expected to interact with the model-checking core through the
31  * `Session` interface (but currently the `Session` interface does not
32  *  have all the necessary features). */
33 // abstract
34 class Checker {
35   Session* session_;
36 public:
37   Checker(Session& session);
38
39   // No copy:
40   Checker(Checker const&) = delete;
41   Checker& operator=(Checker const&) = delete;
42
43   virtual ~Checker();
44
45   /** Main function of this algorithm */
46   virtual int run() = 0;
47
48   /* These methods are callbacks called by the model-checking engine
49    * to get and display information about the current state of the
50    * model-checking algorithm: */
51
52   /** Show the current trace/stack
53    *
54    *  Could this be handled in the Session/ModelChecker instead? */
55   virtual RecordTrace getRecordTrace();
56
57   /** Generate a textual execution trace of the simulated application */
58   virtual std::vector<std::string> getTextualTrace();
59
60   /** Log additional information about the state of the model-checker */
61   virtual void logState();
62
63 protected:
64   Session& getSession() { return *session_; }
65 };
66
67 XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
68 XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
69 XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);
70
71 }
72 }
73
74 #endif