NuSMV/code/nusmv/shell/trace/traceCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/trace/traceCmd.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/trace/pkg_trace.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/trace/TraceOpt.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/exec/traceExec.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/utils/ucmd.h"
#include "nusmv/core/utils/ustring.h"
#include "nusmv/shell/bmc/bmcCmd.h"
#include "nusmv/core/trace/loaders/TraceLoader.h"
#include "nusmv/core/trace/loaders/TraceXmlLoader.h"
#include "nusmv/core/trace/exec/BaseTraceExecutor.h"
#include "nusmv/core/trace/exec/CompleteTraceExecutor.h"
#include "nusmv/core/trace/exec/PartialTraceExecutor.h"

Defines
#define	IS_PARTIAL_EXECUTOR   true
	Trace Commands.
Functions
int	CommandExecutePartialTraces (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandExecuteTraces (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandReadTrace (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandShowPlugins (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandShowTraces (NuSMVEnv_ptr env, int argc, char **argv)
void	traceCmd_init (NuSMVEnv_ptr env)
	Module header file for trace shell commands.
int	traceCmd_parse_slice (const NuSMVEnv_ptr env, const char *s, int *trace, int *from, int *to)
	Parse and checks whether the argument 's' contains valid types for trace number and state number/slices 'from' and 'to'.

---

Define Documentation

#define IS_PARTIAL_EXECUTOR   true

Trace Commands.

Author:

Ashutosh Trivedi, Marco Pensallorto This file contains commands related to traces.

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

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

Command:

execute_partial_traces: Executes partial traces on the model FSM

Command arguments: [-h] [-v] [-r] [-m | -o output-file] -e engine [-a | trace_number]

Executes traces stored in the Trace Manager. If no trace is specified, last registered trace is executed. Traces are not required to be complete. Upon succesful termination, a new complete trace is registered in the Trace Manager.

Command Options:

-v

Verbosely prints traces execution steps.

-a

Executes all the currently stored traces.

-r

Performs restart on complete states (deprecated).

-m

Pipes the output through the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command to output-file

-e engine

Selects an engine for trace re-execution. It must be one of 'bdd', 'sat'.

trace_number

The (ordinal) identifier number of the trace to be printed.

See also:

CommandExecuteTraces

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

Command:

execute_traces: Executes complete traces on the model FSM

Command arguments: [-h] [-v] [-m | -o output-file] -e engine [-a | trace_number]

Executes traces stored in the Trace Manager. If no trace is specified, last registered trace is executed. Traces must be complete in order to perform execution.

Command Options:

-v

Verbosely prints traces execution steps

-a

Prints all the currently stored traces.

-m

Pipes the output through the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command to output-file

-e executor

Selects an executor for trace re-execution.

trace_number

The (ordinal) identifier number of the trace to be printed.

See also:

CommandExecutePartialTraces

int CommandReadTrace	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

read_trace: Reads the trace from the specified file into the memory

Command arguments: [-h] | [-i filename] | [-u] [-s] filename

Reads a trace from a specified XML file into the memory.

Command Options:

-h

Prints the usage of the command.

-i filename

Specifies the name of the xml trace file to read (deprecated).

-u

Turns 'undefined symbol' error in a warning.

-s

Turns 'wrong section' error in a warning.

filename

Specifies the name of the xml trace file to read

See also:

show_traces

int CommandShowPlugins	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

show_plugins: Lists out all the available plugins inside the system. In addition, it prints [D] in front of the default plugin.

Command arguments: [ [-h] [-n plugin_index| -a]]

CommandDescription [ Sets the default plugin to print traces.

Command Options:

-h

Prints the usage of the command.

-n plugin_index

Prints the description message of the plugin at specified index only.

-a

Prints all the available plugins with their description.

]

[EXTRACT_DOC_NOTE: * /]

Sets the default plugin to print traces.

Command Options:

-h

Prints the usage of the command.

-n plugin_index

Prints the description message of the plugin at specified index only.

-a

Prints all the available plugins with their description.

int CommandShowTraces	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

show_traces: Shows the traces generated in a NuSMV session

Command arguments: [ [-h] [-v] [-m | -o output-file] [-A] -t | [-d] -a | trace_number[.from_state[:[to_state]]] ]

Shows the traces currently stored in system memory, if any. By default it shows the last generated trace, if any. A trace number can be specified optionally followed by a slice denoting the steps top be shown. Negative numbers can be used to denote steps in a right-to-left fashion. (i.e. -1 denotes last step, -2 is the previous and so forth.)

Command Options:

-v

Verbosely prints traces content (all state variables, otherwise it prints out only those variables that have changed their value from previous state).

-t

Prints only the total number of currently stored traces.

-a

Prints all the currently stored traces.

-A

Prints traces in an anonimized form.

-d

Disables DEFINEs printout in traces

-p trace plugin

Uses the specified trace plugin to explain the trace.

-m

Pipes the output through the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command to output-file

trace_number

The (ordinal) identifier number of the trace to be printed.

from_state

Denotes left end of the trace slice to be printed.

to_state

Denotes right end of the trace slice to be printed.

See also:

pick_state goto_state simulate

void traceCmd_init

(

NuSMVEnv_ptr

env

)

Module header file for trace shell commands.

Author:

Michele Dorigatti Module header file for trace shell commandsAutomaticStart

Todo:

Missing synopsis

Todo:

Missing description

int traceCmd_parse_slice	(	const NuSMVEnv_ptr	env,
		const char *	s,
		int *	trace,
		int *	from,
		int *	to
	)

Parse and checks whether the argument 's' contains valid types for trace number and state number/slices 'from' and 'to'.

Return 0 iff the parse and checks of the argument 's' (format trace.from:to) contains valid types (integer) for trace number and state number/slices 'from' and 'to'. Moreover, the values for 'trace', 'from', and 'to' are assigned.