NuSMV/code/nusmv/core/simulate/simulateInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include "nusmv/core/simulate/simulate.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/fsm/bdd/BddFsm.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include <setjmp.h>
#include <assert.h>

Go to the source code of this file.

Defines
#define	CHOICE_LENGTH   8
	Internal Header File for the simulate package.
Functions
int	Simulate_CmdPickOneState (NuSMVEnv_ptr, BddFsm_ptr, Simulation_Mode, int, bdd_ptr)
	Picks one state, to be used for BDD simulation.
Variables
cmp_struct_ptr	cmps
FsmBuilder_ptr	global_fsm_builder
TraceMgr_ptr	global_trace_manager
char *	simulation_buffer
size_t	simulation_buffer_size
int	trace_number

---

Define Documentation

#define CHOICE_LENGTH   8

Internal Header File for the simulate package.

Author:

Andrea Morichetti Internal Header File for the simulate package

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

int Simulate_CmdPickOneState	(	NuSMVEnv_ptr	,
		BddFsm_ptr	,
		Simulation_Mode	,
		int	,
		bdd_ptr
	)

Picks one state, to be used for BDD simulation.

Returns the trace index on success, -1 otherwise

required

See also:

optional

---

Variable Documentation

cmp_struct_ptr cmps

FsmBuilder_ptr global_fsm_builder

TraceMgr_ptr global_trace_manager

char* simulation_buffer

size_t simulation_buffer_size

int trace_number