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_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

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

inline static Expr_ptr 
trace_evaluate_define(
  const Trace_ptr  trace, 
  const TraceIter  step, 
  node_ptr  define, 
  hash_ptr  cache 
)
Evaluates a define in a given environment. Missing dependencies are represented by FAILURE nodes. This function is a private service of Trace_evaluate_defines

Side Effects None

See Also Trace_evaluate_defines
Defined in traceEval.c

Expr_ptr 
trace_evaluate_expr_recur(
  const Trace_ptr  trace, 
  const TraceIter  step, 
  Expr_ptr  expr, 
  boolean  in_next, 
  hash_ptr  cache 
)
This function is a private service of Trace_evaluate_expr

Side Effects None

See Also Trace_evaluate_expr
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

Expr_ptr 
trace_simplify_expr(
  const SymbTable_ptr  st, 
  Expr_ptr  expr 
)
MathSAT is currently required to evaluate expressions over reals

Defined in traceEval.c

void 
trace_step_evaluate_defines(
  Trace_ptr  self, 
  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 2010/05/19 15h:56