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

#include "nusmv/core/utils/defs.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Data Structures
struct	Ssiter
Defines
#define	SSET(x)   ((Sset_ptr) x)
#define	SSET_CHECK_INSTANCE(x)   ( nusmv_assert(SSET(x) != SSET(NULL)) )
#define	SSET_FOREACH(sset, iter)
Typedefs
typedef void *	Sset_key
typedef struct Sset_TAG *	Sset_ptr
typedef struct Ssnode_TAG *	Ssnode_ptr
Functions
void	Sset_test (const NuSMVEnv_ptr env)
void *	Ssiter_element (Ssiter iter)
	Returns a value stored in an element pointed by a provided iterator.
boolean	Ssiter_is_valid (Ssiter iter)
	Returns true iff an iterator points a valid node of a set, i.e. not past the last element or before the first element of a set.
Sset_key	Ssiter_key (Ssiter iter)
	Returns a key stored in an element pointed by a provided iterator (and which was used to order the elements).
Ssiter	Ssiter_next (Ssiter iter)
	Returns an iterator pointing to the next element of a set w.r.t. the element pointed by a provided iterator, i.e. element with a greater key.
Ssiter	Ssiter_prev (Ssiter iter)
	Returns an iterator pointing to the previous element of a set w.r.t. the element pointed by a provided iterator, i.e. element with a smaller key.
void	Ssiter_set_element (Ssiter iter, void *element)
	Sets up a value stored in an element pointed by a provided iterator.

---

Define Documentation

#define SSET

(

x

)

((Sset_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define SSET_CHECK_INSTANCE

(

x

)

( nusmv_assert(SSET(x) != SSET(NULL)) )

Todo:

Missing synopsis

Todo:

Missing description

#define SSET_FOREACH	(	sset,
		iter		)

Value:

for (iter=SSet_first(sset); SSiter_is_valid(iter); \
        iter=SSiter_next(iter))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef void* Sset_key

Todo:

Missing synopsis

Todo:

Missing description

typedef struct Sset_TAG* Sset_ptr

typedef struct Ssnode_TAG* Ssnode_ptr

---

Function Documentation

void Sset_test

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

void* Ssiter_element

(

Ssiter

iter

)

Returns a value stored in an element pointed by a provided iterator.

Precondition: this function can be applied only if Ssiter_is_valid(iter) returns true

See also:

Sset_first, Sset_next, Ssiter_is_valid, Ssiter_next

boolean Ssiter_is_valid

(

Ssiter

iter

)

Returns true iff an iterator points a valid node of a set, i.e. not past the last element or before the first element of a set.

The iterator must have been created with function Sset_first, Sset_last, Sset_next or Sset_prev. NOTE: the function is constant time. WARNING: if the function returns false no other function should be invoked on the given iterator!

See also:

Sset_first, Ssiter_next, Ssiter_element

Sset_key Ssiter_key

(

Ssiter

iter

)

Returns a key stored in an element pointed by a provided iterator (and which was used to order the elements).

Precondition: this function can be applied only if Ssiter_is_valid(iter) returns true

See also:

Sset_first, Sset_next, Ssiter_is_valid, Ssiter_next

Ssiter Ssiter_next

(

Ssiter

iter

)

Returns an iterator pointing to the next element of a set w.r.t. the element pointed by a provided iterator, i.e. element with a greater key.

Precondition: this function can be applied only if Ssiter_is_valid(iter) returns true.

See also:

Sset_first, Ssiter_is_end, Ssiter_element

Ssiter Ssiter_prev

(

Ssiter

iter

)

Returns an iterator pointing to the previous element of a set w.r.t. the element pointed by a provided iterator, i.e. element with a smaller key.

Precondition: this function can be applied only if Ssiter_is_valid(iter) returns true.

See also:

Sset_first, Ssiter_is_valid, Ssiter_element

void Ssiter_set_element	(	Ssiter	iter,
		void *	element
	)

Sets up a value stored in an element pointed by a provided iterator.

Precondition: this function can be applied only if Ssiter_is_valid(iter) returns true

See also:

Sset_first, Sset_next, Ssiter_is_valid, Ssiter_next