PartialTraceExecutor Struct Reference

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

#include <PartialTraceExecutor_private.h>

Public Member Functions
	INHERITS_FROM (BaseTraceExecutor)
Data Fields
VIRTUAL Trace_ptr(*	execute )(const PartialTraceExecutor_ptr self, const Trace_ptr trace, NodeList_ptr language, int *n_steps)
Related Functions
(Note that these are not member functions.)
boolean	partial_trace_executor_check_loopbacks (const PartialTraceExecutor_ptr self, const Trace_ptr orig_trace, const Trace_ptr complete_trace)
	Private service for loopback checking.
void	partial_trace_executor_deinit (PartialTraceExecutor_ptr self)
	The PartialTraceExecutor class private deinitializer.
void	partial_trace_executor_init (PartialTraceExecutor_ptr self, const NuSMVEnv_ptr env)
	The PartialTraceExecutor class private initializer.
boolean	partial_trace_executor_is_complete_state (const PartialTraceExecutor_ptr self, const Trace_ptr trace, const TraceIter step)
	Returns true iff the given step is a complete assignment to state vars in the given trace.
Trace_ptr	PartialTraceExecutor_execute (const PartialTraceExecutor_ptr self, const Trace_ptr trace, const NodeList_ptr language, int *n_steps)
	Executes a partial trace.

---

Detailed Description

Private and protected interface of class 'PartialTraceExecutor'.

Public interface of class 'PartialTraceExecutor'.

Author:

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

PartialTraceExecutor class definition derived from class TraceExecutor

See also:

Base class TraceExecutor

Author:

Marco Pensallorto

Todo:

: Missing description

Definition of the public accessor for class PartialTraceExecutor

---

Member Function Documentation

PartialTraceExecutor::INHERITS_FROM

(

BaseTraceExecutor

)

---

Friends And Related Function Documentation

boolean partial_trace_executor_check_loopbacks	(	const PartialTraceExecutor_ptr	self,
		const Trace_ptr	orig_trace,
		const Trace_ptr	complete_trace
	)			[related]

Private service for loopback checking.

Returns true iff all loopback information for partial_trace applies to the complete trace as well

none

See also:

complete_trace_executor_check_loopbacks

void partial_trace_executor_deinit

(

PartialTraceExecutor_ptr

self

)

[related]

The PartialTraceExecutor class private deinitializer.

The PartialTraceExecutor class private deinitializer

See also:

PartialTraceExecutor_destroy

void partial_trace_executor_init	(	PartialTraceExecutor_ptr	self,
		const NuSMVEnv_ptr	env
	)			[related]

The PartialTraceExecutor class private initializer.

The PartialTraceExecutor class private initializer

See also:

PartialTraceExecutor_create

boolean partial_trace_executor_is_complete_state	(	const PartialTraceExecutor_ptr	self,
		const Trace_ptr	trace,
		const TraceIter	step
	)			[related]

Returns true iff the given step is a complete assignment to state vars in the given trace.

Returns true iff the given step is a complete assignment to state vars in the given trace

Trace_ptr PartialTraceExecutor_execute	(	const PartialTraceExecutor_ptr	self,
		const Trace_ptr	trace,
		const NodeList_ptr	language,
		int *	n_steps
	)			[related]

Executes a partial trace.

AutomaticStart

Tries to execute a partial trace on FSM provided at construction time. If execution is succesfully completed, a valid complete trace is built on language and returned. A NULL Trace is retured otherwise.

The number of performed steps is stored in *n_steps, if n_steps is non-NULL. This is -1 if given trace has no feasible initial state.

A complete Trace on language is created upon successful completion

See also:

CompleteTraceExecutor_execute

---

Field Documentation

VIRTUAL Trace_ptr(* PartialTraceExecutor::execute)(const PartialTraceExecutor_ptr self, const Trace_ptr trace, NodeList_ptr language, int *n_steps)

---

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

• NuSMV/code/nusmv/core/trace/exec/PartialTraceExecutor_private.h
• NuSMV/code/nusmv/core/trace/exec/PartialTraceExecutor.h