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