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

Last updated on 2010/05/19 15h:56