NuSMV/code/nusmv/core/bmc/sbmc/sbmcStructs.h File Reference

#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/list.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/array.h"

Go to the source code of this file.

Typedefs
typedef struct state_vars_struct_TAG	state_vars_struct
Functions
sbmc_node_info *	sbmc_alloc_node_info (void)
	Creates an empty structure to hold information associated to each subformula.
hash_ptr	sbmc_node_info_assoc_create (void)
	Creates an asociative list for pairs node_ptr sbmc_node_info *.
sbmc_node_info *	sbmc_node_info_assoc_find (hash_ptr a, node_ptr n)
	Return the information associated to a subformula if any.
void	sbmc_node_info_assoc_free (hash_ptr *a)
	Creates an asociative list for pairs node_ptr sbmc_node_info *.
void	sbmc_node_info_assoc_insert (hash_ptr a, node_ptr n, sbmc_node_info *i)
	Insert in the assoc table the infomrnation for the subformula.
void	sbmc_node_info_free (sbmc_node_info *info)
	Frees a structure to hold information associated to each subformula.
node_ptr	sbmc_node_info_get_aux_F_node (sbmc_node_info *h)
array_t *	sbmc_node_info_get_aux_F_trans (sbmc_node_info *h)
node_ptr	sbmc_node_info_get_aux_G_node (sbmc_node_info *h)
array_t *	sbmc_node_info_get_aux_G_trans (sbmc_node_info *h)
unsigned int	sbmc_node_info_get_past_depth (sbmc_node_info *h)
array_t *	sbmc_node_info_get_trans_bes (sbmc_node_info *h)
array_t *	sbmc_node_info_get_trans_vars (sbmc_node_info *h)
void	sbmc_node_info_set_aux_F_node (sbmc_node_info *h, node_ptr s)
void	sbmc_node_info_set_aux_F_trans (sbmc_node_info *h, array_t *s)
void	sbmc_node_info_set_aux_G_node (sbmc_node_info *h, node_ptr s)
void	sbmc_node_info_set_aux_G_trans (sbmc_node_info *h, array_t *s)
void	sbmc_node_info_set_past_depth (sbmc_node_info *h, unsigned int s)
void	sbmc_node_info_set_past_trans_vars (sbmc_node_info *h, array_t *s)
void	sbmc_node_info_set_trans_bes (sbmc_node_info *h, array_t *s)
hash_ptr	sbmc_set_create (void)
	Creates an associtative list to avoid duplicates of node_ptr.
void	sbmc_set_destroy (hash_ptr hash)
	Destroy an associative list used to avoid duplicates of node_ptr.
void	sbmc_set_insert (hash_ptr hash, node_ptr bexp)
	Insert a node in the hash.
int	sbmc_set_is_in (hash_ptr hash, node_ptr bexp)
	Checks if a node_ptr was already inserted.
state_vars_struct *	sbmc_state_vars_create (const NuSMVEnv_ptr env)
	Creates an empty state_vars_struct.
void	sbmc_state_vars_destroy (state_vars_struct *svs)
	state_vars_struct destroyer
lsList	sbmc_state_vars_get_formula_input_vars (const state_vars_struct *ss)
	getter for field \"formula_input_vars\"
lsList	sbmc_state_vars_get_formula_state_vars (const state_vars_struct *ss)
	getter for field \"formula_state_vars\"
node_ptr	sbmc_state_vars_get_l_var (const state_vars_struct *ss)
	getter for field \"l_var\"
node_ptr	sbmc_state_vars_get_LastState_var (const state_vars_struct *ss)
	getter for field \"LastState_var\"
node_ptr	sbmc_state_vars_get_LoopExists_var (const state_vars_struct *ss)
	getter for field \"LoopExists_var\"
lsList	sbmc_state_vars_get_simple_path_system_vars (const state_vars_struct *ss)
	getter for field \"simple_path_system_vars\"
lsList	sbmc_state_vars_get_trans_state_vars (const state_vars_struct *ss)
	getter for field \"trans_state_vars\"
lsList	sbmc_state_vars_get_translation_vars_aux (const state_vars_struct *ss)
	getter for field \"translation_vars_aux\"
lsList	sbmc_state_vars_get_translation_vars_pd0 (const state_vars_struct *ss)
	getter for field \"translation_vars_pd0\"
lsList	sbmc_state_vars_get_translation_vars_pdx (const state_vars_struct *ss)
	getter for field \"translation_vars_pdx\"
void	sbmc_state_vars_print (state_vars_struct *svs, FILE *out)
	Print a state_vars_struct.
void	sbmc_state_vars_set_formula_input_vars (state_vars_struct *ss, lsList f)
	setter for field \"formula_input_vars\"
void	sbmc_state_vars_set_formula_state_vars (state_vars_struct *ss, lsList f)
	setter for field \"formula_state_vars\"
void	sbmc_state_vars_set_l_var (state_vars_struct *ss, node_ptr f)
	setter for field \"l_var\"
void	sbmc_state_vars_set_LastState_var (state_vars_struct *ss, node_ptr f)
	setter for field \"LastState_var\"
void	sbmc_state_vars_set_LoopExists_var (state_vars_struct *ss, node_ptr f)
	setter for field \"LoopExists_var\"
void	sbmc_state_vars_set_simple_path_system_vars (state_vars_struct *ss, lsList f)
	setter for field \"simple_path_system_vars\"
void	sbmc_state_vars_set_trans_state_vars (state_vars_struct *ss, lsList f)
	setter for field \"transition_state_vars\"
void	sbmc_state_vars_set_translation_vars_aux (state_vars_struct *ss, lsList f)
	setter for field \"translation_vars_aux\"
void	sbmc_state_vars_set_translation_vars_pd0 (state_vars_struct *ss, lsList f)
	setter for field \"translation_state_vars_pd0\"
void	sbmc_state_vars_set_translation_vars_pdx (state_vars_struct *ss, lsList f)
	setter for field \"translation_vars_pdx\"

---

Typedef Documentation

typedef struct state_vars_struct_TAG state_vars_struct

---

Function Documentation

sbmc_node_info* sbmc_alloc_node_info

(

void

)

Creates an empty structure to hold information associated to each subformula.

Creates an empty structure to hold information associated to each subformula.

None

hash_ptr sbmc_node_info_assoc_create

(

void

)

Creates an asociative list for pairs node_ptr sbmc_node_info *.

Creates an asociative list for pairs node_ptr sbmc_node_info *

None

sbmc_node_info* sbmc_node_info_assoc_find	(	hash_ptr	a,
		node_ptr	n
	)

Return the information associated to a subformula if any.

Return the information associated to a subformula if any.

None

void sbmc_node_info_assoc_free

(

hash_ptr *

a

)

Creates an asociative list for pairs node_ptr sbmc_node_info *.

Creates an asociative list for pairs node_ptr sbmc_node_info *

None

void sbmc_node_info_assoc_insert	(	hash_ptr	a,
		node_ptr	n,
		sbmc_node_info *	i
	)

Insert in the assoc table the infomrnation for the subformula.

Insert in the assoc table the infomrnation for the subformula.

None

void sbmc_node_info_free

(

sbmc_node_info *

info

)

Frees a structure to hold information associated to each subformula.

Frees a structure to hold information associated to each subformula.

None

node_ptr sbmc_node_info_get_aux_F_node

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

array_t* sbmc_node_info_get_aux_F_trans

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr sbmc_node_info_get_aux_G_node

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

array_t* sbmc_node_info_get_aux_G_trans

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

unsigned int sbmc_node_info_get_past_depth

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

array_t* sbmc_node_info_get_trans_bes

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

array_t* sbmc_node_info_get_trans_vars

(

sbmc_node_info *

h

)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_aux_F_node	(	sbmc_node_info *	h,
		node_ptr	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_aux_F_trans	(	sbmc_node_info *	h,
		array_t *	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_aux_G_node	(	sbmc_node_info *	h,
		node_ptr	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_aux_G_trans	(	sbmc_node_info *	h,
		array_t *	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_past_depth	(	sbmc_node_info *	h,
		unsigned int	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_past_trans_vars	(	sbmc_node_info *	h,
		array_t *	s
	)

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_node_info_set_trans_bes	(	sbmc_node_info *	h,
		array_t *	s
	)

Todo:

Missing synopsis

Todo:

Missing description

hash_ptr sbmc_set_create

(

void

)

Creates an associtative list to avoid duplicates of node_ptr.

An associtative list to avoid duplicates of node_ptr. If a node is in this set, it has a constant 1 associated to it in the associative hash.

None

void sbmc_set_destroy

(

hash_ptr

hash

)

Destroy an associative list used to avoid duplicates of node_ptr.

Destroy an associative list used to avoid duplicates of node_ptr.

None

void sbmc_set_insert	(	hash_ptr	hash,
		node_ptr	bexp
	)

Insert a node in the hash.

Insert a node in the hash associating constant 1

None

int sbmc_set_is_in	(	hash_ptr	hash,
		node_ptr	bexp
	)

Checks if a node_ptr was already inserted.

Checks whether a node_ptr was already inserted. In affermative case return 1, else 0.

None

state_vars_struct* sbmc_state_vars_create

(

const NuSMVEnv_ptr

env

)

Creates an empty state_vars_struct.

AutomaticStart

Creates an empty state_vars_struct

None

void sbmc_state_vars_destroy

(

state_vars_struct *

svs

)

state_vars_struct destroyer

state_vars_struct destroyer

None

lsList sbmc_state_vars_get_formula_input_vars

(

const state_vars_struct *

ss

)

getter for field \"formula_input_vars\"

None

lsList sbmc_state_vars_get_formula_state_vars

(

const state_vars_struct *

ss

)

getter for field \"formula_state_vars\"

None

node_ptr sbmc_state_vars_get_l_var

(

const state_vars_struct *

ss

)

getter for field \"l_var\"

None

node_ptr sbmc_state_vars_get_LastState_var

(

const state_vars_struct *

ss

)

getter for field \"LastState_var\"

None

node_ptr sbmc_state_vars_get_LoopExists_var

(

const state_vars_struct *

ss

)

getter for field \"LoopExists_var\"

None

lsList sbmc_state_vars_get_simple_path_system_vars

(

const state_vars_struct *

ss

)

getter for field \"simple_path_system_vars\"

None

lsList sbmc_state_vars_get_trans_state_vars

(

const state_vars_struct *

ss

)

getter for field \"trans_state_vars\"

lsList sbmc_state_vars_get_translation_vars_aux

(

const state_vars_struct *

ss

)

getter for field \"translation_vars_aux\"

state_vars_struct destroyer

None

lsList sbmc_state_vars_get_translation_vars_pd0

(

const state_vars_struct *

ss

)

getter for field \"translation_vars_pd0\"

None

lsList sbmc_state_vars_get_translation_vars_pdx

(

const state_vars_struct *

ss

)

getter for field \"translation_vars_pdx\"

None

void sbmc_state_vars_print	(	state_vars_struct *	svs,
		FILE *	out
	)

Print a state_vars_struct.

Print a state_vars_struct to 'out'

None

void sbmc_state_vars_set_formula_input_vars	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"formula_input_vars\"

None

void sbmc_state_vars_set_formula_state_vars	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"formula_state_vars\"

None

void sbmc_state_vars_set_l_var	(	state_vars_struct *	ss,
		node_ptr	f
	)

setter for field \"l_var\"

None

void sbmc_state_vars_set_LastState_var	(	state_vars_struct *	ss,
		node_ptr	f
	)

setter for field \"LastState_var\"

None

void sbmc_state_vars_set_LoopExists_var	(	state_vars_struct *	ss,
		node_ptr	f
	)

setter for field \"LoopExists_var\"

None

void sbmc_state_vars_set_simple_path_system_vars	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"simple_path_system_vars\"

None

void sbmc_state_vars_set_trans_state_vars	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"transition_state_vars\"

None

void sbmc_state_vars_set_translation_vars_aux	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"translation_vars_aux\"

None

void sbmc_state_vars_set_translation_vars_pd0	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"translation_state_vars_pd0\"

None

void sbmc_state_vars_set_translation_vars_pdx	(	state_vars_struct *	ss,
		lsList	f
	)

setter for field \"translation_vars_pdx\"

None