Prop_Rewriter Struct Reference

Public interface of class 'Prop_Rewriter'. More...

#include <Prop_Rewriter_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
BddEnc_ptr	bddenc
WffRewriterExpectedProperty	expprop
FsmType	fsm_type
boolean	is_status_consistent
SymbLayer_ptr	layer
boolean	ltl2invar_negate_property
WffRewriteMethod	method
boolean	monitor_variable_initialized_to_true
boolean	monitor_visible_in_traces
Prop_ptr	original
Prop_Rewriter_rewrite_method	rewrite
Prop_ptr	rewritten
SymbTable_ptr	symb_table
Related Functions
(Note that these are not member functions.)
Prop_Rewriter_ptr	Prop_Rewriter_create (NuSMVEnv_ptr env, Prop_ptr prop, WffRewriteMethod method, WffRewriterExpectedProperty expprop, FsmType fsm_type, BddEnc_ptr bddenc)
	The Prop_Rewriter class constructor.
void	prop_rewriter_deinit (Prop_Rewriter_ptr self)
	The Prop_Rewriter class private deinitializer.
void	Prop_Rewriter_destroy (Prop_Rewriter_ptr self)
	The Prop_Rewriter class destructor.
Prop_ptr	Prop_Rewriter_get_original_property (Prop_Rewriter_ptr self)
	Getter for original property.
void	prop_rewriter_init (Prop_Rewriter_ptr self, NuSMVEnv_ptr env, Prop_ptr original, WffRewriteMethod method, WffRewriterExpectedProperty expprop, FsmType fsm_type, BddEnc_ptr enc, SymbLayer_ptr layer)
	The Prop_Rewriter class private initializer.
void	Prop_Rewriter_initialize_monitor_vars_to_false (Prop_Rewriter_ptr self)
	Makes the monitor variables initialized to False.
void	Prop_Rewriter_initialize_monitor_vars_to_true (Prop_Rewriter_ptr self)
	Makes the monitor variables initialized to True.
void	Prop_Rewriter_ltl2invar_negate_property_to_false (Prop_Rewriter_ptr self)
	Do not negate the property before building the monitor. Only when converting LTL to invar.
void	Prop_Rewriter_ltl2invar_negate_property_to_true (Prop_Rewriter_ptr self)
	Negates the property before building the monitor. Only when converting LTL to invar.
void	Prop_Rewriter_make_monitor_vars_invisible (Prop_Rewriter_ptr self)
	Makes the monitor variables invisible in traces.
void	Prop_Rewriter_make_monitor_vars_visible (Prop_Rewriter_ptr self)
	Makes the monitor variables visible in traces.
Prop_ptr	prop_rewriter_rewrite (Prop_Rewriter_ptr self)
	the internal rewrite function
Prop_ptr	Prop_Rewriter_rewrite (Prop_Rewriter_ptr self)
	Rewrites self->original and stores the result in self->rewritten.
void	Prop_Rewriter_update_original_property (Prop_Rewriter_ptr self)
	Copy the results in self->rewritten to self->original.

---

Detailed Description

Public interface of class 'Prop_Rewriter'.

Author:

Michele Dorigatti

Todo:

: Missing description

Definition of the public accessor for class Prop_Rewriter

---

Member Function Documentation

Prop_Rewriter::INHERITS_FROM

(

EnvObject

)

---

Friends And Related Function Documentation

Prop_Rewriter_ptr Prop_Rewriter_create	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		WffRewriteMethod	method,
		WffRewriterExpectedProperty	expprop,
		FsmType	fsm_type,
		BddEnc_ptr	bddenc
	)			[related]

The Prop_Rewriter class constructor.

AutomaticStart

All the parameters are just referenced.

Parameters:

fsm_type

can be a bitwise disjuction (example: FSM_TYPE_BE | FSM_TYPE_BDD)

See also:

Prop_Rewriter_destroy

void prop_rewriter_deinit

(

Prop_Rewriter_ptr

self

)

[related]

The Prop_Rewriter class private deinitializer.

The Prop_Rewriter class private deinitializer

See also:

Prop_Rewriter_destroy

void Prop_Rewriter_destroy

(

Prop_Rewriter_ptr

self

)

[related]

The Prop_Rewriter class destructor.

The Prop_Rewriter class destructor

See also:

Prop_Rewriter_create

Prop_ptr Prop_Rewriter_get_original_property

(

Prop_Rewriter_ptr

self

)

[related]

Getter for original property.

Getter for original property

void prop_rewriter_init	(	Prop_Rewriter_ptr	self,
		NuSMVEnv_ptr	env,
		Prop_ptr	original,
		WffRewriteMethod	method,
		WffRewriterExpectedProperty	expprop,
		FsmType	fsm_type,
		BddEnc_ptr	enc,
		SymbLayer_ptr	layer
	)			[related]

The Prop_Rewriter class private initializer.

Assumption: the property must contain an Fsm

See also:

Prop_Rewriter_create

void Prop_Rewriter_initialize_monitor_vars_to_false

(

Prop_Rewriter_ptr

self

)

[related]

Makes the monitor variables initialized to False.

When the WFF_REWRITE_METHOD_DEADLOCK_FREE is selected, then the monitor variable if created is initialized to be FALSE.

void Prop_Rewriter_initialize_monitor_vars_to_true

(

Prop_Rewriter_ptr

self

)

[related]

Makes the monitor variables initialized to True.

When the WFF_REWRITE_METHOD_DEADLOCK_FREE is selected, then the monitor variable if created is initialized to be TRUE (default).

void Prop_Rewriter_ltl2invar_negate_property_to_false

(

Prop_Rewriter_ptr

self

)

[related]

Do not negate the property before building the monitor. Only when converting LTL to invar.

void Prop_Rewriter_ltl2invar_negate_property_to_true

(

Prop_Rewriter_ptr

self

)

[related]

Negates the property before building the monitor. Only when converting LTL to invar.

void Prop_Rewriter_make_monitor_vars_invisible

(

Prop_Rewriter_ptr

self

)

[related]

Makes the monitor variables invisible in traces.

Makes the monitor variables invisible in traces. By default they are invisible. Must be set right after initialization of the rewriter.

void Prop_Rewriter_make_monitor_vars_visible

(

Prop_Rewriter_ptr

self

)

[related]

Makes the monitor variables visible in traces.

Makes the monitor variables visible in traces. Must be set right after initialization of the rewriter.

Prop_ptr prop_rewriter_rewrite

(

Prop_Rewriter_ptr

self

)

[related]

the internal rewrite function

The returned property will contain an FSM of the type self->fsm_type, plus any other FSM needed for building the target one.

Prop_ptr Prop_Rewriter_rewrite

(

Prop_Rewriter_ptr

self

)

[related]

Rewrites self->original and stores the result in self->rewritten.

This is the most important method of the class. Here the property is rewritten. The returned property must be freed by the caller.

void Prop_Rewriter_update_original_property

(

Prop_Rewriter_ptr

self

)

[related]

Copy the results in self->rewritten to self->original.

Copy the results in self->rewritten to self->original

---

Field Documentation

BddEnc_ptr Prop_Rewriter::bddenc

WffRewriterExpectedProperty Prop_Rewriter::expprop

FsmType Prop_Rewriter::fsm_type

boolean Prop_Rewriter::is_status_consistent

SymbLayer_ptr Prop_Rewriter::layer

boolean Prop_Rewriter::ltl2invar_negate_property

WffRewriteMethod Prop_Rewriter::method

boolean Prop_Rewriter::monitor_variable_initialized_to_true

boolean Prop_Rewriter::monitor_visible_in_traces

Prop_ptr Prop_Rewriter::original

Prop_Rewriter_rewrite_method Prop_Rewriter::rewrite

Prop_ptr Prop_Rewriter::rewritten

SymbTable_ptr Prop_Rewriter::symb_table

---

The documentation for this struct was generated from the following files:

• NuSMV/code/nusmv/core/prop/Prop_Rewriter_private.h
• NuSMV/code/nusmv/core/prop/Prop_Rewriter.h