Simulation

Functions for handling Simulations. More...

Macros
#define	NUXMV_VALID_SIMULATION(simulation)   ((simulation).repr != NULL)
	Valid simulation.
#define	NUXMV_MAKE_SIMULATION_CONSTRAINT( simple_constraint_, trans_constraint_, trace_, trace_start_, ltl_formula_)
	Helper macro to construct a simulation constraint.

Functions
nuxmv_simulation	nuxmv_create_simulation (nuxmv_env env, nuxmv_model model, nuxmv_simulation_constraint constraint, const nuxmv_opt *opts, size_t opt_num)
	Create a new simulation for a model.
nuxmv_status_code	nuxmv_destroy_simulation (nuxmv_env env, nuxmv_simulation simulation)
	Destroy a simulation.
nuxmv_status_code	nuxmv_extend_simulation (nuxmv_env env, nuxmv_simulation simulation, size_t k, nuxmv_simulation_constraint constraint)
	Extend the simulation by k steps.
nuxmv_result	nuxmv_simulation_get_result (nuxmv_env env, nuxmv_simulation simulation)
	Get the result out of a simulation.

Detailed Description

Functions for handling Simulations.

---

Macro Definition Documentation

NUXMV_MAKE_SIMULATION_CONSTRAINT

#define NUXMV_MAKE_SIMULATION_CONSTRAINT	(		simple_constraint_,
			trans_constraint_,
			trace_,
			trace_start_,
			ltl_formula_
	)

Value:

    ((nuxmv_simulation_constraint){.simple_constraint = (simple_constraint_),  \
                                   .trans_constraint = (trans_constraint_),    \
                                   .trace = (trace_),                          \
                                   .trace_start = (trace_start_),              \
                                   .ltl_formula = (ltl_formula_)})

Helper macro to construct a simulation constraint.

Parameters

[in]	simple_constraint_	An nuxmv_expr.
[in]	trans_constraint_	An nuxmv_expr.
[in]	trace_	An nuxmv_trace.
[in]	trace_start_	An integer representing the starting step of the trace.
[in]	ltl_formula_	An nuxmv_expr.

NUXMV_VALID_SIMULATION

#define NUXMV_VALID_SIMULATION

(

simulation

)

((simulation).repr != NULL)

Valid simulation.

This macro checks whether simulation is a valid nuxmv_simulation.

Parameters

[in]

simulation

The simulation to inspect.

Returns

true if the option is valid, false otherwise.

Function Documentation

nuxmv_create_simulation()

nuxmv_simulation nuxmv_create_simulation	(	nuxmv_env	env,
		nuxmv_model	model,
		nuxmv_simulation_constraint	constraint,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Create a new simulation for a model.

When no longer needed, the simulation can be freed using nuxmv_destroy_simulation().

Parameters

[in]	env	The environment to modify.
[in]	model	The model to simulate.
[in]	constraint	The constraint to apply to the simulation.
[in]	opts	A list of options to apply. If no list shall be used it is safe to use NULL or the result of malloc(0), provided that opt_num=0.
[in]	opt_num	The number of options in the list. If no list shall be passed, use 0 as actual value of opt_num.

Returns

The newly created simulation. In case of error, NUXMV_VALID_SIMULATION() evaluates to false.

See also

• nuxmv_extend_simulation()
• nuxmv_simulation_get_result()
• nuxmv_destroy_simulation()
• nuxmv_env_get_last_error_message()

Requirements: 02.002

Attention

This function has not been implemented, yet.

nuxmv_destroy_simulation()

nuxmv_status_code nuxmv_destroy_simulation	(	nuxmv_env	env,
		nuxmv_simulation	simulation
	)

Destroy a simulation.

With this function, the user notifies the environment that the selected simulation is no more needed.

Parameters

[in]	env	The environment to modify.
[in]	simulation	A simulation to destroy.

Returns

NUXMV_SUCCESS if the simulation was destroyed, NUXMV_FAILURE in case of error.

See also

• nuxmv_create_simulation()
• nuxmv_env_get_last_error_message()

Requirements: 02.002

Attention

This function has not been implemented, yet.

nuxmv_extend_simulation()

nuxmv_status_code nuxmv_extend_simulation	(	nuxmv_env	env,
		nuxmv_simulation	simulation,
		size_t	k,
		nuxmv_simulation_constraint	constraint
	)

Extend the simulation by k steps.

Parameters

[in]	env	The environment to modify.
[in,out]	simulation	The simulation to extend.
[in]	k	The number of steps to extend the simulation by.
[in]	constraint	The constraint to apply to the simulation.

Returns

NUXMV_SUCCESS if the simulation was extended, NUXMV_FAILURE in case of error.

See also

• nuxmv_create_simulation()
• nuxmv_env_get_last_error_message()

Requirements: 02.002

Attention

This function has not been implemented, yet.

nuxmv_simulation_get_result()

nuxmv_result nuxmv_simulation_get_result	(	nuxmv_env	env,
		nuxmv_simulation	simulation
	)

Get the result out of a simulation.

Parameters

[in]	env	The environment to modify.
[in]	simulation	The simulation to inspect.

Returns

The result of the simulation. In case of error, NUXMV_VALID_RESULT() evaluates to false.

See also

• nuxmv_property_check_satisfiability()
• nuxmv_trace_check_property()
• nuxmv_model_check_deadlock()
• nuxmv_model_check_receptiveness()
• nuxmv_env_get_last_error_message()

Requirements: 02.002

Attention

This function has not been implemented, yet.