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
  13 #include "src/mc/mc_forward.hpp"
  14
  15 namespace simgrid {
  16 namespace mc {
  17
  18 /** A model-checking algorithm
  19  *
  20  *  The goal is to move the data/state/configuration of a model-checking
  21  *  algorihms in subclasses. Implementing this interface will probably
  22  *  not be really mandatory, you might be able to write your
  23  *  model-checking algorithm as plain imperative code instead.
  24  *
  25  *  It works by manipulating a model-checking Session.
  26  */
  27 // abstract
  28 class Checker {
  29   Session* session_;
  30 public:
  31   Checker(Session& session) : session_(&session) {}
  32
  33   // No copy:
  34   Checker(Checker const&) = delete;
  35   Checker& operator=(Checker const&) = delete;
  36
  37   virtual ~Checker();
  38   virtual int run() = 0;
  39
  40 protected:
  41   Session& getSession() { return *session_; }
  42 };
  43
  44 }
  45 }
  46
  47 #endif