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
  17 namespace simgrid {
  18 namespace mc {
  19
  20 /** A model-checking algorithm
  21  *
  22  *  The goal is to move the data/state/configuration of a model-checking
  23  *  algorihms in subclasses. Implementing this interface will probably
  24  *  not be really mandatory, you might be able to write your
  25  *  model-checking algorithm as plain imperative code instead.
  26  *
  27  *  It works by manipulating a model-checking Session.
  28  */
  29 // abstract
  30 class Checker {
  31   Session* session_;
  32 public:
  33   Checker(Session& session);
  34
  35   // No copy:
  36   Checker(Checker const&) = delete;
  37   Checker& operator=(Checker const&) = delete;
  38
  39   virtual ~Checker();
  40   virtual int run() = 0;
  41
  42   // Give me your internal state:
  43
  44   /** Show the current trace/stack
  45    *
  46    *  Could this be handled in the Session/ModelChecker instead?
  47    */
  48   virtual RecordTrace getRecordTrace();
  49   virtual std::vector<std::string> getTextualTrace();
  50
  51 protected:
  52   Session& getSession() { return *session_; }
  53 };
  54
  55 XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
  56 XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
  57 XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);
  58
  59 }
  60 }
  61
  62 #endif