NuSMV Developers Manual: NuSMV/code/nusmv/core/utils/bmc

00001 /* ---------------------------------------------------------------------------
00002 
00003   This file is part of the ``utils'' package of NuSMV version 2.
00004   Copyright (C) 1998-2001 by CMU and FBK-irst.
00005 
00006   NuSMV version 2 is free software; you can redistribute it and/or
00007   modify it under the terms of the GNU Lesser General Public
00008   License as published by the Free Software Foundation; either
00009   version 2 of the License, or (at your option) any later version.
00010 
00011   NuSMV version 2 is distributed in the hope that it will be useful,
00012   but WITHOUT ANY WARRANTY; without even the implied warranty of
00013   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00014   Lesser General Public License for more details.
00015 
00016   You should have received a copy of the GNU Lesser General Public
00017   License along with this library; if not, write to the Free Software
00018   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00019 
00020   For more information on NuSMV see <http://nusmv.fbk.eu>
00021   or email to <nusmv-users@fbk.eu>.
00022   Please report bugs to <nusmv-users@fbk.eu>.
00023 
00024   To contact the NuSMV development board, email to <nusmv@fbk.eu>.
00025 
00026 -----------------------------------------------------------------------------*/
00027 
00038 #ifndef __NUSMV_CORE_UTILS_BMC_PROFILER_H__
00039 #define __NUSMV_CORE_UTILS_BMC_PROFILER_H__
00040 
00041 #if HAVE_CONFIG_H
00042 # include "nusmv-config.h"
00043 #endif
00044 
00045 #include "nusmv/core/cinit/NuSMVEnv.h"
00046 #include "nusmv/core/utils/error.h"
00047 
00048 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00049 #include "profiling.h"
00050 #endif
00051 
00052 /*---------------------------------------------------------------------------*/
00053 /* Constant declarations                                                     */
00054 /*---------------------------------------------------------------------------*/
00055 
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Type declarations                                                         */
00059 /*---------------------------------------------------------------------------*/
00060 
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Structure declarations                                                    */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00067 
00073 typedef struct BmcProfilerStruct_TAG
00074 {
00075   boolean enabled;
00076   char* out_file_name;
00077 } BmcProfilerStruct;
00078 
00079 typedef BmcProfilerStruct* BmcProfilerStruct_ptr;
00080 #endif
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Variable declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 
00087 /*---------------------------------------------------------------------------*/
00088 /* Macro declarations                                                        */
00089 /*---------------------------------------------------------------------------*/
00090 
00091 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00092 
00095 #define ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__ "env_bmc_profiler"
00096 #endif
00097 
00104 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00105 #define BMC_PROFILER_INIT_ENV(env)                                      \
00106   nusmv_assert(! NuSMVEnv_has_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__));            \
00107   {                                                                     \
00108      BmcProfilerStruct_ptr prof;                                        \
00109      prof = ALLOC(BmcProfilerStruct, 1);                                \
00110      nusmv_assert((BmcProfilerStruct_ptr) NULL != prof);                \
00111      prof->enabled = false;                                             \
00112      prof->out_file_name = (char*) NULL;                                \
00113      NuSMVEnv_set_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__, prof);                   \
00114   }
00115 #else
00116 #define BMC_PROFILER_INIT_ENV(env)
00117 #endif
00118 
00124 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00125 #define BMC_PROFILER_DEINIT_ENV(env)                                    \
00126   nusmv_assert(NuSMVEnv_has_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__));              \
00127   {                                                                     \
00128     if (BMC_PROFILER_IS_ENABLED(env)) {BMC_PROFILER_DISABLE(env);}       \
00129     BmcProfilerStruct_ptr prof = (BmcProfilerStruct_ptr)                \
00130       NuSMVEnv_remove_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__);                     \
00131     if ( (char*) NULL != prof->out_file_name) {FREE(prof->out_file_name);} \
00132   }
00133 #else
00134 #define BMC_PROFILER_DEINIT_ENV(env)
00135 #endif
00136 
00143 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00144 #define BMC_PROFILER_IS_ENABLED(env)                                    \
00145   ((BmcProfilerStruct_ptr) NuSMVEnv_get_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__))->enabled
00146 #else
00147 #define BMC_PROFILER_IS_ENABLED(env) false
00148 #endif
00149 
00156 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00157 #define BMC_PROFILER_GET_OUT_FILE(env)                                  \
00158   ((BmcProfilerStruct_ptr) NuSMVEnv_get_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__))->out_file_name
00159 #else
00160 #define BMC_PROFILER_GET_OUT_FILE(env) (char*) NULL
00161 #endif
00162 
00163 
00170 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00171 #define BMC_PROFILER_INITIALIZE(env)                                \
00172   if (BMC_PROFILER_IS_ENABLED(env)) {                               \
00173     profiler_initialize();                                          \
00174   }
00175 #else
00176 #define BMC_PROFILER_INITIALIZE(env)
00177 #endif
00178 
00190 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00191 #define BMC_PROFILER_ENABLE(env, filename)                              \
00192   nusmv_assert(NuSMVEnv_has_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__));              \
00193   {                                                                     \
00194     BmcProfilerStruct_ptr prof;                                         \
00195     prof = (BmcProfilerStruct_ptr) NuSMVEnv_get_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__); \
00196     nusmv_assert(! prof->enabled);                                      \
00197     if ( (char*) NULL != prof->out_file_name) {                         \
00198       FREE(prof->out_file_name);                                        \
00199     }                                                                   \
00200     prof->enabled = true;                                               \
00201     prof->out_file_name = util_strsav(filename);                        \
00202     /* actual call to the library */                                    \
00203     profiler_enable(prof->out_file_name);                               \
00204   }
00205 #else
00206 #define BMC_PROFILER_ENABLE(env, file)
00207 #endif
00208 
00219 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00220 #define BMC_PROFILER_DISABLE(env)                                       \
00221   nusmv_assert(NuSMVEnv_has_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__));              \
00222   {                                                                     \
00223     BmcProfilerStruct_ptr prof;                                         \
00224     prof = (BmcProfilerStruct_ptr) NuSMVEnv_get_value(env, ENV__NUSMV_CORE_UTILS_BMC_PROFILER_H__); \
00225     nusmv_assert(prof->enabled);                                        \
00226     if ( (char*) NULL != prof->out_file_name) {                         \
00227       FREE(prof->out_file_name);                                        \
00228       prof->out_file_name = (char*) NULL;                               \
00229     }                                                                   \
00230     prof->enabled = false;                                              \
00231     /* actual call to the library */                                    \
00232     profiler_disable();                                                 \
00233   }
00234 #else
00235 #define BMC_PROFILER_DISABLE(env)
00236 #endif
00237 
00252 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00253 #define BMC_PROFILER_SAMPLING_SOLVE_START(env, bmc_step)                \
00254   if (BMC_PROFILER_IS_ENABLED(env)) {                                   \
00255     profiler_output_message("\n-- start of problem solving for bound", bmc_step); \
00256   }
00257 #else
00258 #define BMC_PROFILER_SAMPLING_SOLVE_START(env, bmc_step)
00259 #endif
00260 
00275 #if NUSMV_HAVE__NUSMV_CORE_UTILS_BMC_PROFILER_H___LIBRARY
00276 #define BMC_PROFILER_SAMPLING_SOLVE_END(env, bmc_step)                  \
00277   if (BMC_PROFILER_IS_ENABLED(env)) {                                   \
00278     profiler_output_message("\n-- end of problem solving for bound", bmc_step); \
00279     profiler_sampling(bmc_step);                                        \
00280   }
00281 #else
00282 #define BMC_PROFILER_SAMPLING_SOLVE_END(env, bmc_step)
00283 #endif
00284 
00285 
00288 /*---------------------------------------------------------------------------*/
00289 /* Function prototypes                                                       */
00290 /*---------------------------------------------------------------------------*/
00291 
00294 #endif /* __NUSMV_CORE_UTILS_BMC_PROFILER_H__ */
NuSMV/code/nusmv/core/utils/bmc_profiler.h
