00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00038 #ifndef __NUSMV_CORE_BMC_BMC_SIMULATE_H__
00039 #define __NUSMV_CORE_BMC_BMC_SIMULATE_H__
00040
00041 #include "cudd/util.h"
00042 #include "nusmv/core/utils/utils.h"
00043 #include "nusmv/core/bmc/bmcInt.h"
00044 #include "nusmv/core/bmc/bmcUtils.h"
00045 #include "nusmv/core/bmc/bmcConv.h"
00046 #include "nusmv/core/trace/pkg_trace.h"
00047 #include "nusmv/core/trace/Trace.h"
00048 #include "nusmv/core/simulate/simulate.h"
00049 #include "nusmv/core/compile/compile.h"
00050 #include "nusmv/core/sat/sat.h"
00051 #include "nusmv/core/utils/Olist.h"
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067
00068
00069
00070
00071
00072
00073
00074
00075
00076
00077
00080
00081
00082
00083
00093 int
00094 Bmc_Simulate(NuSMVEnv_ptr env,
00095 const BeFsm_ptr be_fsm,
00096 BddEnc_ptr bdd_enc,
00097 be_ptr constraints,
00098 boolean time_shift,
00099 const int k,
00100 const boolean print_trace,
00101 const boolean changes_only,
00102 Simulation_Mode mode);
00103
00132 int
00133 Bmc_StepWiseSimulation(NuSMVEnv_ptr env,
00134 BeFsm_ptr be_fsm,
00135 BddEnc_ptr bdd_enc,
00136 TraceMgr_ptr trace_manager,
00137 int target_steps,
00138 be_ptr constraints,
00139 boolean time_shift,
00140 boolean printtrace,
00141 boolean changes_only,
00142 Simulation_Mode mode,
00143 boolean display_all);
00144
00163 Olist_ptr
00164 Bmc_simulate_check_feasible_constraints(NuSMVEnv_ptr env,
00165 BeFsm_ptr be_fsm,
00166 BddEnc_ptr bdd_enc,
00167 Olist_ptr constraints,
00168 be_ptr from_state);
00169
00180 int
00181 Bmc_pick_state_from_constr(NuSMVEnv_ptr env,
00182 BeFsm_ptr fsm, BddEnc_ptr bdd_enc,
00183 be_ptr constr, Simulation_Mode mode,
00184 boolean display_all);
00185
00191 int
00192 Bmc_Simulate_bmc_pick_state(const NuSMVEnv_ptr env,
00193 TraceLabel label,
00194 be_ptr be_constr,
00195 int tr_number,
00196 const Simulation_Mode mode,
00197 const int display_all,
00198 const boolean verbose);
00199
00207 int
00208 Bmc_Simulate_bmc_simulate_check_feasible_constraints(const NuSMVEnv_ptr env,
00209 const Olist_ptr str_constraints,
00210 const Olist_ptr be_constraints,
00211 const Olist_ptr expr_constraints,
00212 const boolean human_readable);
00213
00216 #endif