NuSMV/code/nusmv/shell/simulate/simulateCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/simulate/simulateCmd.h"
#include "nusmv/core/simulate/SimulateState.h"
#include "nusmv/core/simulate/simulate.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/utils/OStream.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/Logger.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/utils/utils_io.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/prop/PropDb.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/parser/symbols.h"
#include "nusmv/core/parser/parser.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/mc/mc.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/trace/pkg_trace.h"
#include "nusmv/core/utils/ucmd.h"

Functions
int	CommandGotoState (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPickState (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintCurrentState (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandSimulate (NuSMVEnv_ptr env, int argc, char **argv)
	Model Checker Simulator Commands.
void	Simulate_Cmd_init (NuSMVEnv_ptr env)
	Module header file for simulate shell commands.
void	Simulate_Cmd_quit (NuSMVEnv_ptr env)
	Deinitialize the simulation shell commands.

---

Function Documentation

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

Command:

goto_state: Goes to a given state of a trace

Command arguments: [-h] state

Makes state the current state. This command is used to navigate alongs traces produced by NuSMV. During the navigation, there is a current state, and the current trace is the trace the current state belongs to. Command options:

state:

The state of a trace (trace.state) to be picked.

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

Command:

pick_state: Picks a state from the set of initial states

Command arguments: [-h] [-v] [-r | -i [-a]] [-c "constraints" | -s trace.state]

Chooses an element from the set of initial states, and makes it the current state (replacing the old one). The chosen state is stored as the first state of a new trace ready to be lengthened by steps states by the simulate command. The state can be chosen according to different policies which can be specified via command line options. By default the state is chosen in a deterministic way.

Command Options:

-v

Verbosely prints out chosen state (all state variables, otherwise it prints out only the label t.1 of the state chosen, where t is the number of the new trace, that is the number of traces so far generated plus one).

-r

Randomly picks a state from the set of initial states.

-i

Enables the user to interactively pick up an initial state. The user is requested to choose a state from a list of possible items (every item in the list doesn't show state variables unchanged with respect to a previous item). If the number of possible states is too high, then the user has to specify some further constraints as "simple expression".

-a

Displays all state variables (changed and unchanged with respect to a previous item) in an interactive picking. This option works only if the -i options has been specified.

-c "constraints"

Uses constraints to restrict the set of initial states in which the state has to be picked.

-s trace.state

Picks state from trace.state label. A new simulation trace will be created by copying prefix of the source trace up to specified state.

See also:

goto_state simulate

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

Command:

print_current_state: Prints out the current state

Command arguments: [-h] [-v]

Prints the name of the current state if defined.

Command options:

-v

Prints the value of all the state variables of the current state.

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

Model Checker Simulator Commands.

Author:

Andrea Morichetti This file contains commands to be used for the simulation feature.

Command:

simulate: Performs a simulation from the current selected state

Command arguments: [-h] [-p | -v] [-r | -i [-a]] [[-c "constraints"] | [-t "constraints"] ] [-k steps]

Generates a sequence of at most steps states (representing a possible execution of the model), starting from the current state. The current state must be set via the pick_state or goto_state commands.

It is possible to run the simulation in three ways (according to different command line policies): deterministic (the default mode), random and interactive.

The resulting sequence is stored in a trace indexed with an integer number taking into account the total number of traces stored in the system. There is a different behavior in the way traces are built, according to how current state is set: current state is always put at the beginning of a new trace (so it will contain at most <it>steps + 1</it> states) except when it is the last state of an existent old trace. In this case the old trace is lengthened by at most <it>steps</it> states.

Command Options:

-p

Prints current generated trace (only those variables whose value changed from the previous state).

-v

Verbosely prints current generated trace (changed and unchanged state variables).

-r

Picks a state from a set of possible future states in a random way.

-i

Enables the user to interactively choose every state of the trace, step by step. If the number of possible states is too high, then the user has to specify some constraints as simple expression. These constraints are used only for a single simulation step and are forgotten in the following ones. They are to be intended in an opposite way with respect to those constraints eventually entered with the pick_state command, or during an interactive simulation session (when the number of future states to be displayed is too high), that are local only to a single step of the simulation and are forgotten in the next one.

-a

Displays all the state variables (changed and unchanged) during every step of an interactive session. This option works only if the -i option has been specified.

-c "constraints"

Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression cannot contain next operators, and is automatically shifted by one state in order to constraint only the next steps

-t "constraints"

Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression can contain next operators, and is NOT automatically shifted by one state as done with option -c

-k steps

Maximum length of the path according to the constraints. The length of a trace could contain less than steps states: this is the case in which simulation stops in an intermediate step because it may not exist any future state satisfying those constraints.

See also:

pick_state goto_state

void Simulate_Cmd_init

(

NuSMVEnv_ptr

env

)

Module header file for simulate shell commands.

Author:

Michele Dorigatti Module header file for simulate shell commandsAutomaticStart

Initializes the simulate shell commands Initializes the simulate shell commands

void Simulate_Cmd_quit

(

NuSMVEnv_ptr

env

)

Deinitialize the simulation shell commands.

Deinitialize the simulation shell commands