model.h

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 /** @file model.h
  11  *  @brief Core model checker.
  12  */
  13
  14 #ifndef __MODEL_H__
  15 #define __MODEL_H__
  16
  17 #include <cstddef>
  18 #include <inttypes.h>
  19 #include "mcexecution.h"
  20 #include "mymemory.h"
  21 #include "hashtable.h"
  22 #include "config.h"
  23 #include "context.h"
  24 #include "params.h"
  25
  26 class MC {
  27 public:
  28         MC(struct model_params params);
  29         ~MC();
  30         MCExecution * get_execution() const { return execution; }
  31         MCScheduler * get_scheduler() const { return execution->get_scheduler(); }
  32         void check();
  33         const model_params params;
  34
  35         MEMALLOC;
  36 private:
  37         MCExecution *execution;
  38         void run_execution();
  39
  40         friend void user_main_wrapper();
  41 };
  42
  43 extern MC *model;
  44 #endif/* __MODEL_H__ */