NuSMV/code/nusmv/core/compile/FlatHierarchy.h File Reference

#include "nusmv/core/node/node.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/utils/assoc.h"

Go to the source code of this file.

Defines
#define	FLAT_HIERARCHY(x)   ((FlatHierarchy_ptr) x)
#define	FLAT_HIERARCHY_CHECK_INSTANCE(x)   ( nusmv_assert(FLAT_HIERARCHY(x) != FLAT_HIERARCHY(NULL)) )
Functions
void	FlatHierarchy_add_init (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_add_invar (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_add_mirror (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_add_pred (FlatHierarchy_ptr cmp, node_ptr n)
boolean	FlatHierarchy_add_property_name (FlatHierarchy_ptr cmp, node_ptr name)
void	FlatHierarchy_add_property_pattern (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_add_trans (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_add_var (FlatHierarchy_ptr cmp, node_ptr n)
	Add a variable name to the list of variables declared in the given hierarchy.
node_ptr	FlatHierarchy_get_assign (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_compassion (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_compute (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_init (FlatHierarchy_ptr cmp)
	A set of functions accessing the fields of the class.
node_ptr	FlatHierarchy_get_input (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_invar (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_invarspec (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_justice (FlatHierarchy_ptr cmp)
	It is a cons list of constraints.
node_ptr	FlatHierarchy_get_ltlspec (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_mirrors (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_preds (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_property_patterns (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_pslspec (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_spec (FlatHierarchy_ptr cmp)
node_ptr	FlatHierarchy_get_trans (FlatHierarchy_ptr cmp)
Set_t	FlatHierarchy_get_vars (FlatHierarchy_ptr cmp)
	Returns the set of variables declared in the given hierarchy.
void	FlatHierarchy_set_assign (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_compassion (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_compute (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_init (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_input (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_invar (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_invarspec (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_justice (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_ltlspec (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_mirror (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_pred (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_property_patterns (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_pslspec (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_spec (FlatHierarchy_ptr cmp, node_ptr n)
void	FlatHierarchy_set_trans (FlatHierarchy_ptr cmp, node_ptr n)

---

Define Documentation

#define FLAT_HIERARCHY

(

x

)

((FlatHierarchy_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define FLAT_HIERARCHY_CHECK_INSTANCE

(

x

)

( nusmv_assert(FLAT_HIERARCHY(x) != FLAT_HIERARCHY(NULL)) )

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

void FlatHierarchy_add_init	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_invar	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_mirror	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_pred	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

boolean FlatHierarchy_add_property_name	(	FlatHierarchy_ptr	cmp,
		node_ptr	name
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_property_pattern	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_trans	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_add_var	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Add a variable name to the list of variables declared in the given hierarchy.

See also:

FlatHierarchy_get_vars

node_ptr FlatHierarchy_get_assign

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_compassion

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_compute

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_init

(

FlatHierarchy_ptr

cmp

)

A set of functions accessing the fields of the class.

node_ptr FlatHierarchy_get_input

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_invar

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_invarspec

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_justice

(

FlatHierarchy_ptr

cmp

)

It is a cons list of constraints.

node_ptr FlatHierarchy_get_ltlspec

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_mirrors

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_preds

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_property_patterns

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_pslspec

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_spec

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

node_ptr FlatHierarchy_get_trans

(

FlatHierarchy_ptr

cmp

)

Todo:

Missing synopsis

Todo:

Missing description

Set_t FlatHierarchy_get_vars

(

FlatHierarchy_ptr

cmp

)

Returns the set of variables declared in the given hierarchy.

Do not destroy or change returned set

See also:

FlatHierarchy_add_var

void FlatHierarchy_set_assign	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_compassion	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_compute	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_init	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_input	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_invar	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_invarspec	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_justice	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_ltlspec	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Input is a cons list, with elements LTLSPEC nodes

void FlatHierarchy_set_mirror	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_pred	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_property_patterns	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_pslspec	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_spec	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description

void FlatHierarchy_set_trans	(	FlatHierarchy_ptr	cmp,
		node_ptr	n
	)

Todo:

Missing synopsis

Todo:

Missing description