int 
CommandExecutePartialTraces(
  int  argc, 
  char** argv 
)
CommandExecutePartialTraces

See Also CommandExecuteTraces
Defined in traceCmd.c

int 
CommandExecuteTraces(
  int  argc, 
  char** argv 
)
CommandExecuteTraces

See Also CommandExecutePartialTraces
Defined in traceCmd.c

int 
CommandReadTrace(
  int  argc, 
  char** argv 
)
read_trace

See Also show_traces
Defined in traceCmd.c

int 
CommandShowPlugins(
  int  argc, 
  char** argv 
)
Lists out all the available plugins inside the system.

Defined in traceCmd.c

int 
CommandShowTraces(
  int  argc, 
  char** argv 
)
Shows the traces generated in a NuSMV session

See Also pick_state goto_state simulate
Defined in traceCmd.c

bdd_ptr 
TraceUtils_fetch_as_bdd(
  Trace_ptr  trace, 
  TraceIter  step, 
  TraceIteratorType  iter_type, 
  BddEnc_ptr  bdd_enc 
)
Builds a bdd representing the assignments from a given step in trace. The symbols to be assigned are picked according to "iter_type". Refer to documentation of the TraceIteratorType for possible sets. Remarks: returned bdd is referenced

Defined in traceUtils.c

be_ptr 
TraceUtils_fetch_as_be(
  Trace_ptr  trace, 
  TraceIter  step, 
  TraceIteratorType  iter_type, 
  BeEnc_ptr  be_enc, 
  BddEnc_ptr  bdd_enc 
)
Builds a be representing the assignments from a given step in trace. The symbols to be assigned are picked according to "iter_type". Refer to documentation of the TraceIteratorType for possible sets.

Defined in traceUtils.c

Expr_ptr 
TraceUtils_fetch_as_big_and(
  Trace_ptr  trace, 
  TraceIter  step, 
  TraceIteratorType  iter_type 
)
Do the same thing as TraceUtils_fetch_as_sexp, but do not simplify or reorder the pointers of expressions created.

See Also TraceUtils_fetch_as_sexp
Defined in traceUtils.c

Expr_ptr 
TraceUtils_fetch_as_sexp(
  Trace_ptr  trace, 
  TraceIter  step, 
  TraceIteratorType  iter_type 
)
Builds a sexp representing the assignments from a given step in trace. The symbols to be assigned are picked according to "iter_type". Refer to documentation of the TraceIteratorType for possible sets. Remarks: returned expression is find-node'd

See Also TraceUtils_fetch_as_big_and
Defined in traceUtils.c

static int 
UsageExecuteTraces(
    
)
UsageExecuteTraces

Defined in traceCmd.c

static int 
UsageReadTrace(
    
)
UsageReadTrace

Defined in traceCmd.c

static int 
UsageShowPlugins(
    
)
UsageShowPlugins

Defined in traceCmd.c

static int 
UsageShowTraces(
    
)
UsageShowTraces

Defined in traceCmd.c

int 
trace_cmd_parse_slice(
  const char* s, 
  int* trace, 
  int* from, 
  int* to 
)
Private service of top level trace execution functions

Defined in traceCmd.c

hash_ptr 
trace_eval_make_environment(
  Trace_ptr  trace, 
  TraceIter  step 
)
This function builds a local environment for constant expressions evaluation

Side Effects none

Defined in traceEval.c

node_ptr 
trace_make_failure(
  const char* tmpl, 
  node_ptr  symbol 
)
Private service of trace_evaluate_expr_recur

See Also Private service of trace_evaluate_expr_recur
Defined in traceEval.c

void 
trace_step_evaluate_defines(
  Trace_ptr  trace, 
  const TraceIter  step 
)
Evaluates define for a trace, based on assignments to state, frozen and input variables. If a previous value exists for a define, The mismatch is reported to the caller by appending a failure node describing the error to the "failures" list. If "failures" is NULL failures are silently discarded. If no previous value exists for a given define, assigns the define to the calculated value according to vars assignments. The "failures" list must be either NULL or a valid, empty list. 0 is returned if no mismatching were detected, 1 otherwise

Side Effects The trace is filled with defines, failures list is populated as necessary.

Defined in traceEval.c

 
(
    
)
UsageExecutePartialTrace

Defined in traceCmd.c

Last updated on 2012/11/18 14h:16