faudes::CompVerify Class Reference

#include <pev_verify.h>

Classes
class	StateRef

Public Types
typedef TaGenerator< AttributeVoid, StateRef, AttributeVoid, AttributeVoid >	CounterExample

Public Member Functions
	CompVerify (void)
	CompVerify (Generator &goi)
	CompVerify (GeneratorVector &gvoi)
	CompVerify (GeneratorVector &gvoi, const EventSet &pevs)
virtual	~CompVerify (void)
EventSet	AllPevs ()
virtual void	VerifyAll (Generator &trace)
virtual bool	IsNonconflicting ()
bool	IsPreemptive ()
virtual void	GenerateTrace (const Generator &rGen)
virtual bool	ShortestPath (const Generator &rGen, Generator &rRes, Idx begin, Idx end)
virtual void	ClearAttribute (CounterExample &rCE)
virtual void	ExtractParallel (Candidate *cand, CounterExample &rCE)
virtual void	StateMergingExpansion (SynchCandidates *synchCands, Candidate *cand, CounterExample &rCE)
virtual void	CounterExampleRefinement ()

Static Public Member Functions
static StateSet::Iterator	LastState (CounterExample &ce)

Protected Attributes
Generator	mGenFinal
CounterExample	mCounterExp
std::stack< SynchCandidates * >	mAllCandidates
EventSet	mAllPevs
bool	mIsPreemptive = 0

Detailed Description

Definition at line 9 of file pev_verify.h.

Member Typedef Documentation

CounterExample

typedef TaGenerator<AttributeVoid, StateRef, AttributeVoid,AttributeVoid> faudes::CompVerify::CounterExample

Definition at line 44 of file pev_verify.h.

Constructor & Destructor Documentation

CompVerify() [1/4]

faudes::CompVerify::CompVerify ( void  )

inline

Definition at line 11 of file pev_verify.h.

CompVerify() [2/4]

faudes::CompVerify::CompVerify

(

Generator &

goi

)

Definition at line 42 of file pev_verify.cpp.

CompVerify() [3/4]

faudes::CompVerify::CompVerify

(

GeneratorVector &

gvoi

)

Definition at line 47 of file pev_verify.cpp.

CompVerify() [4/4]

faudes::CompVerify::CompVerify	(	GeneratorVector &	gvoi,
		const EventSet &	pevs
	)

Definition at line 57 of file pev_verify.cpp.

~CompVerify()

faudes::CompVerify::~CompVerify ( void  )

virtual

Definition at line 71 of file pev_verify.cpp.

Member Function Documentation

AllPevs()

EventSet faudes::CompVerify::AllPevs ( )

inline

Definition at line 48 of file pev_verify.h.

ClearAttribute()

void faudes::CompVerify::ClearAttribute ( CounterExample &  rCE )

virtual

counter example re-generation algorithm

Clear all state attributes of a counter example. Intended for initialization

Parameters

rCE	counter example

Definition at line 525 of file pev_verify.cpp.

CounterExampleRefinement()

void faudes::CompVerify::CounterExampleRefinement ( )

virtual

wrapper for counter example generation

Definition at line 772 of file pev_verify.cpp.

ExtractParallel()

void faudes::CompVerify::ExtractParallel ( Candidate *  cand, CounterExample &  rCE  )

virtual

Extract state attributes from composed automaton to its original automata

Parameters

cand	the composed camp, i.e. with mMap
rCE	the counter example

Exceptions

599	candidate not composed

Definition at line 532 of file pev_verify.cpp.

GenerateTrace()

void faudes::CompVerify::GenerateTrace ( const Generator &  rGen )

virtual

Generate trace to bad states, i.e. some root in a blocking scc.

Parameters

rGen	the blocking automaton

Definition at line 422 of file pev_verify.cpp.

IsNonconflicting()

bool faudes::CompVerify::IsNonconflicting ( )

virtual

Definition at line 231 of file pev_verify.cpp.

IsPreemptive()

bool faudes::CompVerify::IsPreemptive ( )

inline

Definition at line 51 of file pev_verify.h.

LastState()

StateSet::Iterator faudes::CompVerify::LastState ( CounterExample &  ce )

static

Definition at line 517 of file pev_verify.cpp.

ShortestPath()

bool faudes::CompVerify::ShortestPath ( const Generator &  rGen, Generator &  rRes, Idx  begin, Idx  end  )

virtual

Generate the shortest path between given start and end state in a given automaton

Parameters

rGen	the given automaton
rRes	the shortest path
begin	index of begin state
end	index of end state

Returns

true if there exists a path between begin and end state

Definition at line 467 of file pev_verify.cpp.

StateMergingExpansion()

void faudes::CompVerify::StateMergingExpansion ( SynchCandidates *  synchCands, Candidate *  cand, CounterExample &  rCE  )

virtual

Expand counter example from state merging abstraction

Parameters

synchCands	candidates (i.e. generators with their silentevs)
cand	the candidate which is abstracted
rCE	counter example, which is abstract at begin and shall be expanded to concrete finally w.r.t. cand
isPreemptive	flag, true when consider event preemption

Exceptions

500	concrete bad state can not be reached (this is theoretically impossible. Will only occur in case of implementation bugs)

Definition at line 544 of file pev_verify.cpp.

VerifyAll()

void faudes::CompVerify::VerifyAll ( Generator &  trace )

virtual

Definition at line 186 of file pev_verify.cpp.

Member Data Documentation

mAllCandidates

std::stack<SynchCandidates*> faudes::CompVerify::mAllCandidates

protected

Definition at line 132 of file pev_verify.h.

mAllPevs

EventSet faudes::CompVerify::mAllPevs

protected

Definition at line 133 of file pev_verify.h.

mCounterExp

CounterExample faudes::CompVerify::mCounterExp

protected

Definition at line 131 of file pev_verify.h.

mGenFinal

Generator faudes::CompVerify::mGenFinal

protected

Definition at line 130 of file pev_verify.h.

mIsPreemptive

bool faudes::CompVerify::mIsPreemptive = 0

protected

Definition at line 134 of file pev_verify.h.

---

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

• pev_verify.h
• pev_verify.cpp