NuSMV/code/nusmv/core/opt/OptsHandler.h File Reference

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

Go to the source code of this file.

Data Structures
struct	Opts_EnumRec
Defines
#define	OPTS_DEFAULT_VALUE_TRUE   true
#define	OPTS_FALSE_VALUE   "0"
#define	OPTS_FOREACH_OPTION(h, name, value)   for (Opts_Gen_init(h); Opts_Gen_next(h, name, value) || (Opts_Gen_deinit(h), 0); )
	Operates on each entry of the option handler.
#define	OPTS_HANDLER(self)   ((OptsHandler_ptr) self)
	To cast and check instances of class ModelSimplifier.
#define	OPTS_HANDLER_CHECK_INSTANCE(self)   (nusmv_assert(OPTS_HANDLER(self) != OPTS_HANDLER(NULL)))
#define	OPTS_IS_PUBLIC   true
#define	OPTS_TRUE_VALUE   "1"
#define	OPTS_VALUE_ERROR   (void *)-9999
Typedefs
typedef boolean(*	Opts_CheckFnType )(OptsHandler_ptr, const char *, void *)
typedef void *(*	Opts_ReturnFnType )(OptsHandler_ptr, const char *, void *)
typedef boolean(*	Opts_TriggerFnType )(OptsHandler_ptr, const char *, const char *, Trigger_Action, void *)
Enumerations
enum	Option_Type {   GENERIC_OPTION, USER_OPTION, INTEGER_OPTION, ENUM_OPTION,   BOOL_OPTION }
	Generic handler of options. More...
enum	Trigger_Action { ACTION_SET, ACTION_RESET, ACTION_GET }
Functions
void	OptsHandler_copy (OptsHandler_ptr src_opts, OptsHandler_ptr dst_opts)
	Copy src_opts to dst_opts.
void	OptsHandler_destroy (OptsHandler_ptr h)
	Frees an option handler.
boolean	OptsHandler_register_bool_option (OptsHandler_ptr self, const char *name, boolean value, boolean is_public)
	Registers a boolean option in an option handler.

---

Define Documentation

#define OPTS_DEFAULT_VALUE_TRUE   true

Todo:

Missing synopsis

Todo:

Missing description

#define OPTS_FALSE_VALUE   "0"

Todo:

Missing synopsis

Todo:

Missing description

#define OPTS_FOREACH_OPTION	(	h,
		name,
		value		)	for (Opts_Gen_init(h); Opts_Gen_next(h, name, value) || (Opts_Gen_deinit(h), 0); )

Operates on each entry of the option handler.

Operates on each entry of the option handler. name and value must be declared to be char **.

See also:

Opts_GenInit Opts_Gen Opts_GenFree

#define OPTS_HANDLER

(

self

)

((OptsHandler_ptr) self)

To cast and check instances of class ModelSimplifier.

These macros must be used respectively to cast and to check instances of class ModelSimplifier

#define OPTS_HANDLER_CHECK_INSTANCE

(

self

)

(nusmv_assert(OPTS_HANDLER(self) != OPTS_HANDLER(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define OPTS_IS_PUBLIC   true

Todo:

Missing synopsis

Todo:

Missing description

#define OPTS_TRUE_VALUE   "1"

Todo:

Missing synopsis

Todo:

Missing description

#define OPTS_VALUE_ERROR   (void *)-9999

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef boolean(* Opts_CheckFnType)(OptsHandler_ptr, const char *, void *)

Todo:

Missing synopsis

Todo:

Missing description

typedef void*(* Opts_ReturnFnType)(OptsHandler_ptr, const char *, void *)

Todo:

Missing synopsis

Todo:

Missing description

typedef boolean(* Opts_TriggerFnType)(OptsHandler_ptr, const char *, const char *, Trigger_Action, void *)

---

Enumeration Type Documentation

enum Option_Type

Generic handler of options.

Author:

Marco Roveri, Alessandro Mariotti Generic handler of options. An option is uniquely identified in an option handler by:

• a name (it is the string of its name).
• a default value (it is the string of its name).
• a value (it is the string of its name).

When registering an option the user must specify two functions. The first is responsible of checking that the value passed while setting a value is a valid value for the given option. The second function is a function that transforms the stroed value in a value suitable to be used in the calling program.

For boolean options are provided special methods to register the option and for setting and getting a value associated to it.

For enumerative options are provided special methods to register the option and for setting and getting a value associated to it. An enumertive option is registered by providing an array of structures of type Opts_EnumRec. Similarly to the below declaration:

typedef enum {foo1, ...., fooN} fooenumtype;
   Opts_EnumRec foo[] = {"foo1", foo1,
   "foo2", foo2,
   ....
   "fooN", fooN};
   ....
   handler = OptsHandler_create();
   OptsHandler_register_enum_option(handler, "foooption", "foo1", foo, N);

   if (OptsHandler_get_enum_option_value(handler, "foooption") == foo2) {
   ...
   }

   ...

   switch(OptsHandler_get_enum_option_value(handler, "foooption")) {
   case foo1:
   ...
   case fooN:
   ...
   default:
   ...
   }
   

Todo:

Missing synopsis

Todo:

Missing description

Enumerator:

GENERIC_OPTION
USER_OPTION
INTEGER_OPTION
ENUM_OPTION
BOOL_OPTION

enum Trigger_Action

Todo:

Missing synopsis

Todo:

Missing description

Enumerator:

ACTION_SET
ACTION_RESET
ACTION_GET

---

Function Documentation

void OptsHandler_copy	(	OptsHandler_ptr	src_opts,
		OptsHandler_ptr	dst_opts
	)

Copy src_opts to dst_opts.

Copy src_opts to dst_opts.

Note that:

• dst_opts can have a different environment from src_opts
• triggers and args are not copied

void OptsHandler_destroy

(

OptsHandler_ptr

h

)

Frees an option handler.

Frees an option handler.

None

See also:

OptsHandler_create

boolean OptsHandler_register_bool_option	(	OptsHandler_ptr	self,
		const char *	name,
		boolean	value,
		boolean	is_public
	)

Registers a boolean option in an option handler.

Registers a boolean option in an option handler. The user is not required to provide any function to check and return a value. Returns true if the registration of the option succeeds, false otherwise.

None