execEngine
TracePkg_execution_engine_from_string(
const char* name
)
- Converts an engine name into an engine identifier.
Returns EXEC_UNDEFINED if no valid name is given.
- Side Effects None
- Defined in
traceExec.c
int
Trace_execute_partial_trace(
Trace_ptr trace,
TraceExecInfo_ptr exec_info
)
- Partial trace re-execution and fill-in.
Tries to complete the given trace using the
chosen incomplete trace re-execution engine.
If succesful, a complete trace is registered
into the Trace Manager.
The "vars" list is only needed if the "restart" flag
is set to true, and should be the set of vars of the model
0 is returned if trace could be succesfully completed.
1 is returned otherwise
- Side Effects None
- Defined in
traceExec.c
int
Trace_execute_trace(
Trace_ptr trace,
TraceExecInfo_ptr exec_info
)
- Complete trace re-execution. Returns 0 if a trace is
executed successfully, and 1 otherwise.
- Side Effects None
- Defined in
traceExec.c
static void
bmc_add_be_into_solver_positively(
SatSolver_ptr solver,
SatSolverGroup group,
be_ptr prob,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time of conversion,
adding, setting polarity and destroying BE.
- Defined in
satExec.c
static Be_Cnf_ptr
bmc_add_be_into_solver(
SatSolver_ptr solver,
SatSolverGroup group,
be_ptr prob,
int polarity,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time of conversion
and adding BE to solver. It is resposibility of the
invoker to destroy returned CNF (with Be_Cnf_Delete)
- Side Effects creates an instance of CNF formula. (do not forget to
delete it)
- Defined in
satExec.c
Trace_ptr
extract_bdd_trace(
BddFsm_ptr fsm,
BddStates goal_states,
node_ptr reachable,
int length,
NodeList_ptr symbols,
const char* trace_name
)
- Extracts a complete trace
Description [This function is a private service of
trace_bdd_execute_partial_trace
- Side Effects None
- Defined in
bddExec.c
int
trace_bdd_execute_partial_trace(
Trace_ptr trace,
TraceExecInfo_ptr exec_info,
int* trace_index
)
- The trace is executed using BDDs, that is a proof
that the fsm is compatible with the trace is
built. Uncomplete traces are filled-in with
compatible values for state variables.
If trace is compatible, a new complete trace is
registered in the TraceManager and its index is written
into new_trace;
Given trace can be either complete or
incomplete.
The number of performed steps (transitions) is
returned. If the initial state is not compatible
-1 is returned.
- Side Effects A complete trace will be registered into the Trace
Manager upon successful completion
- Defined in
bddExec.c
int
trace_bdd_execute_trace(
Trace_ptr trace,
TraceExecInfo_ptr exec_info
)
- The trace is executed using BDDs. Every transition of
the trace is tested for compatibility with the
model. Trace is assumed to be complete and
non-empty (i.e. at least one state exists). The
number of succesfully executed transitions is
returned.
- Side Effects None
- Defined in
bddExec.c
be_ptr
trace_exec_get_initial_state(
BeFsm_ptr be_fsm
)
- Builds the initial state formula
- Side Effects None
- Defined in
satExec.c
be_ptr
trace_exec_get_transition_relation(
BeFsm_ptr be_fsm
)
- Builds the transition relation formula
- Side Effects None
- Defined in
satExec.c
int
trace_sat_execute_trace(
Trace_ptr trace,
TraceExecInfo_ptr exec_info
)
- The trace is executed using SAT solver, that is a proof
that the fsm is compatible with the trace is
built. Trace must be complete in order to
perform execution. If a non complete trace is
given, unpredictable results may occur.
The number of performed steps (transitions) is
returned. If the initial state is not compatible
-1 is returned.
- Side Effects None
- Defined in
satExec.c