X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b487d5a9259b88670b8cd97e9c16e4b000c11008..7f0845ec805dc9b93cab3adb223eadd20aa1f169:/src/mc/mc_model_checker.h diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 74df0d7cec..0b07e8e71c 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -3,11 +3,19 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef MC_MODEL_CHECKER_H +#define MC_MODEL_CHECKER_H + +#include #include +#include -#ifndef MC_MODEL_CHECKER_H -#define MC_MODEL_CHECKER_H +#include "mc_forward.h" +#include "mc_process.h" +#include "mc_page_store.h" +#include "mc_protocol.h" SG_BEGIN_DECL() @@ -18,18 +26,27 @@ SG_BEGIN_DECL() * By moving as much state as possible in this structure allocated * on the model-chercker heap, we avoid those issues. */ -typedef struct s_mc_model_checker { +struct s_mc_model_checker { // This is the parent snapshot of the current state: mc_snapshot_t parent_snapshot; mc_pages_store_t pages; int fd_clear_refs; int fd_pagemap; xbt_dynar_t record; -} s_mc_model_checker_t, *mc_model_checker_t; + s_mc_process_t process; + /** String pool for host names */ + xbt_dict_t /* */ hosts; +}; -mc_model_checker_t MC_model_checker_new(void); +mc_model_checker_t MC_model_checker_new(pid_t pid, int socket); void MC_model_checker_delete(mc_model_checker_t mc); -extern mc_model_checker_t mc_model_checker; + +static inline +int MC_smx_get_maxpid(void) +{ + // Currently we use the same variable in STANDALONE and in SERVER mode: + return simix_process_maxpid; +} SG_END_DECL()