NuSMV/code/nusmv/core/utils/range.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"

Go to the source code of this file.

Functions
boolean	Utils_check_subrange (node_ptr subrange)
	Checks that in given subrange n..m, n<=m.
boolean	Utils_check_subrange_not_negative (node_ptr subrange)
	Checks that in given subrange n..m, n<=m, and that n,m are not negative.
void	Utils_failure_node_check (const NuSMVEnv_ptr env, node_ptr n)
	Checks if the values of n does not contains FAILURE node. If they do then report and terminate.
boolean	Utils_is_in_range (node_ptr s, node_ptr d)
	Checks if the first argument is contained in the second.
void	Utils_range_check (const NuSMVEnv_ptr env, node_ptr n)
	Checks if the values of n is in the range allowed for the variable.
void	Utils_set_data_for_range_check (const NuSMVEnv_ptr env, node_ptr var, node_ptr range)
	External header of the utils package.
void	Utils_set_mode_for_range_check (const NuSMVEnv_ptr env, boolean is_fatal)
	Called before using Utils_range_check callback function.

---

Function Documentation

boolean Utils_check_subrange

(

node_ptr

subrange

)

Checks that in given subrange n..m, n<=m.

Returns True if in given subrange n..m n <= m. Given node_ptr must be of TWODOTS type

See also:

Utils_check_subrange_not_negative

boolean Utils_check_subrange_not_negative

(

node_ptr

subrange

)

Checks that in given subrange n..m, n<=m, and that n,m are not negative.

Check for correct positive (or zero) range

See also:

Utils_check_subrange

void Utils_failure_node_check	(	const NuSMVEnv_ptr	env,
		node_ptr	n
	)

Checks if the values of n does not contains FAILURE node. If they do then report and terminate.

Utils_set_data_for_range_check

boolean Utils_is_in_range	(	node_ptr	s,
		node_ptr	d
	)

Checks if the first argument is contained in the second.

Returns true if the first argument is contained in the set represented by the second, false otherwise. If the first argument is not a CONS, then it is considered to be a singleton.

None

See also:

in_list

void Utils_range_check	(	const NuSMVEnv_ptr	env,
		node_ptr	n
	)

Checks if the values of n is in the range allowed for the variable.

Checks if the values of n is in the range allowed for the variable. The allowed values are stored in the global variable the_range, which should be set before invocation of this function. An error occure if: 1. the value is not in the range (all FAILURE node are, of course, irgnored)

Utils_set_data_for_range_check

void Utils_set_data_for_range_check	(	const NuSMVEnv_ptr	env,
		node_ptr	var,
		node_ptr	range
	)

External header of the utils package.

Author:

Roberto Cavada External header of the utils package.

Called before using Utils_range_check callback function Utils_range_check

void Utils_set_mode_for_range_check	(	const NuSMVEnv_ptr	env,
		boolean	is_fatal
	)

Called before using Utils_range_check callback function.

Utils_range_check