#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. |
int CommandGotoState | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
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:
int CommandPickState | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
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
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
-i
-a
-i
options has been specified. -c "constraints"
constraints
to restrict the set of initial states in which the state has to be picked. -s trace.state
int CommandPrintCurrentState | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
int CommandSimulate | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
Model Checker Simulator Commands.
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
-v
-r
-i
-a
-i
option has been specified. -c "constraints"
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"
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
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. void Simulate_Cmd_init | ( | NuSMVEnv_ptr | env | ) |
Module header file for simulate shell commands.
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