CompleteTraceExecutor Struct Reference

Private and protected interface of class 'CompleteTraceExecutor'. More...

#include <CompleteTraceExecutor_private.h>

Public Member Functions
	INHERITS_FROM (BaseTraceExecutor)
Data Fields
VIRTUAL boolean(*	execute )(const CompleteTraceExecutor_ptr self, const Trace_ptr trace, int *n_steps)
Related Functions
(Note that these are not member functions.)
boolean	complete_trace_executor_check_loopbacks (const CompleteTraceExecutor_ptr self, const Trace_ptr trace)
	Private service for loopback checking.
void	complete_trace_executor_deinit (CompleteTraceExecutor_ptr self)
	The CompleteTraceExecutor class private deinitializer.
void	complete_trace_executor_init (CompleteTraceExecutor_ptr self, const NuSMVEnv_ptr env)
	The CompleteTraceExecutor class private initializer.
CompleteTraceExecutor_ptr	CompleteTraceExecutor_create (const NuSMVEnv_ptr env)
	The CompleteTraceExecutor class constructor.
void	CompleteTraceExecutor_destroy (CompleteTraceExecutor_ptr self)
	The CompleteTraceExecutor class destructor.
boolean	CompleteTraceExecutor_execute (const CompleteTraceExecutor_ptr self, const Trace_ptr trace, int *n_steps)
	Executes a complete trace.

---

Detailed Description

Private and protected interface of class 'CompleteTraceExecutor'.

Public interface of class 'CompleteTraceExecutor'.

Author:

Marco Pensallorto This file can be included only by derived and friend classes

CompleteTraceExecutor class definition derived from class TraceExecutor

See also:

Base class TraceExecutor

Author:

Marco Pensallorto

Todo:

: Missing description

Definition of the public accessor for class CompleteTraceExecutor

---

Member Function Documentation

CompleteTraceExecutor::INHERITS_FROM

(

BaseTraceExecutor

)

---

Friends And Related Function Documentation

boolean complete_trace_executor_check_loopbacks	(	const CompleteTraceExecutor_ptr	self,
		const Trace_ptr	trace
	)			[related]

Private service for loopback checking.

Returns true iff all loopback information for trace applies to the trace itself

none

See also:

partial_trace_executor_check_loopbacks

void complete_trace_executor_deinit

(

CompleteTraceExecutor_ptr

self

)

[related]

The CompleteTraceExecutor class private deinitializer.

The CompleteTraceExecutor class private deinitializer

See also:

CompleteTraceExecutor_destroy

void complete_trace_executor_init	(	CompleteTraceExecutor_ptr	self,
		const NuSMVEnv_ptr	env
	)			[related]

The CompleteTraceExecutor class private initializer.

The CompleteTraceExecutor class private initializer

See also:

CompleteTraceExecutor_create

CompleteTraceExecutor_ptr CompleteTraceExecutor_create

(

const NuSMVEnv_ptr

env

)

[related]

The CompleteTraceExecutor class constructor.

AutomaticStart

The CompleteTraceExecutor class constructor

See also:

CompleteTraceExecutor_destroy

void CompleteTraceExecutor_destroy

(

CompleteTraceExecutor_ptr

self

)

[related]

The CompleteTraceExecutor class destructor.

The CompleteTraceExecutor class destructor

See also:

CompleteTraceExecutor_create

boolean CompleteTraceExecutor_execute	(	const CompleteTraceExecutor_ptr	self,
		const Trace_ptr	trace,
		int *	n_steps
	)			[related]

Executes a complete trace.

Tries to execute a complete on FSM provided at construction time and returns true iff the trace is compatible with the fsm given at construction time. The number of performed steps is stored in *n_steps if a non-NULL pointer is given. This is -1 is if the Trace has no feasible initial state.

none

See also:

PartialTraceExecutor_execute

---

Field Documentation

VIRTUAL boolean(* CompleteTraceExecutor::execute)(const CompleteTraceExecutor_ptr self, const Trace_ptr trace, int *n_steps)

---

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

• NuSMV/code/nusmv/core/trace/exec/CompleteTraceExecutor_private.h
• NuSMV/code/nusmv/core/trace/exec/CompleteTraceExecutor.h