X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5a97de8c98502af9f74cfceb924fa02e0fd80925..756df47074b2d7b0721f234077f5ef8d75e13932:/src/mc/mc_liveness.h diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h index e0f102f458..f33cc5428e 100644 --- a/src/mc/mc_liveness.h +++ b/src/mc/mc_liveness.h @@ -1,11 +1,11 @@ -/* Copyright (c) 2007-2014. The SimGrid Team. +/* Copyright (c) 2007-2015. The SimGrid Team. * All rights reserved. */ /* 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_LIVENESS_H -#define MC_LIVENESS_H +#ifndef SIMGRID_MC_LIVENESS_H +#define SIMGRID_MC_LIVENESS_H #include @@ -13,13 +13,13 @@ #include #include #include -#include "mc_state.h" +#include "src/mc/mc_state.h" SG_BEGIN_DECL() -extern xbt_automaton_t _mc_property_automaton; +extern XBT_PRIVATE xbt_automaton_t _mc_property_automaton; -typedef struct s_mc_pair{ +typedef struct XBT_PRIVATE s_mc_pair { int num; int search_cycle; mc_state_t graph_state; /* System state included */ @@ -31,7 +31,7 @@ typedef struct s_mc_pair{ int visited_pair_removed; } s_mc_pair_t, *mc_pair_t; -typedef struct s_mc_visited_pair{ +typedef struct XBT_PRIVATE s_mc_visited_pair{ int num; int other_num; /* Dot output for */ int acceptance_pair; @@ -44,19 +44,17 @@ typedef struct s_mc_visited_pair{ int visited_removed; } s_mc_visited_pair_t, *mc_visited_pair_t; -mc_pair_t MC_pair_new(void); -void MC_pair_delete(mc_pair_t); -void mc_pair_free_voidp(void *p); -mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); -void MC_visited_pair_delete(mc_visited_pair_t p); +XBT_PRIVATE mc_pair_t MC_pair_new(void); +XBT_PRIVATE void MC_pair_delete(mc_pair_t); +XBT_PRIVATE mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); +XBT_PRIVATE void MC_visited_pair_delete(mc_visited_pair_t p); -void MC_pre_modelcheck_liveness(void); -void MC_modelcheck_liveness(void); -void MC_show_stack_liveness(xbt_fifo_t stack); -void MC_dump_stack_liveness(xbt_fifo_t stack); +int MC_modelcheck_liveness(void); +XBT_PRIVATE void MC_show_stack_liveness(xbt_fifo_t stack); +XBT_PRIVATE void MC_dump_stack_liveness(xbt_fifo_t stack); -extern xbt_dynar_t visited_pairs; -int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair); +XBT_PRIVATE extern xbt_dynar_t visited_pairs; +XBT_PRIVATE int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair); SG_END_DECL()