Public Member Functions | Private Member Functions | Private Attributes | List of all members
faudes::HOAConsumerFaudes Class Reference

Detailed Description

Definition at line 237 of file omg_hoa.cpp.

Public Member Functions

 HOAConsumerFaudes (Generator &gen, const SymbolTable &syms)
 
virtual bool parserResolvesAliases () override
 
virtual void notifyHeaderStart (const std::string &version) override
 
virtual void setNumberOfStates (unsigned int numberOfStates) override
 
virtual void addStartStates (const int_list &stateConjunction) override
 
virtual void addAlias (const std::string &name, label_expr::ptr labelExpr) override
 
virtual void setAPs (const std::vector< std::string > &aps) override
 
virtual void setAcceptanceCondition (unsigned int numberOfSets, acceptance_expr::ptr accExpr) override
 
virtual void provideAcceptanceName (const std::string &name, const std::vector< IntOrString > &extraInfo) override
 
virtual void setName (const std::string &name) override
 
virtual void setTool (const std::string &name, std::shared_ptr< std::string > version) override
 
virtual void addProperties (const std::vector< std::string > &properties) override
 
virtual void addMiscHeader (const std::string &name, const std::vector< IntOrString > &content) override
 
virtual void notifyBodyStart () override
 
virtual void addState (unsigned int id, std::shared_ptr< std::string > info, label_expr::ptr labelExpr, std::shared_ptr< int_list > accSignature) override
 
virtual void addEdgeImplicit (unsigned int stateId, const int_list &conjSuccessors, std::shared_ptr< int_list > accSignature) override
 
virtual void addEdgeWithLabel (unsigned int stateId, label_expr::ptr labelExpr, const int_list &conjSuccessors, std::shared_ptr< int_list > accSignature) override
 
virtual void notifyEndOfState (unsigned int stateId) override
 
virtual void notifyEnd () override
 
virtual void notifyAbort () override
 
virtual void notifyWarning (const std::string &warning) override
 

Private Member Functions

std::string bits2event (uint32_t bits)
 
bool evalexpr (label_expr::ptr expr, uint32_t bits)
 
void expr2bits (label_expr::ptr labelExpr, HOAConsumer::int_list &bitslist)
 

Private Attributes

Generator & rGen
 
RabinAutomaton * pRAut =nullptr
 
const SymbolTable & rSymTab
 
bool mRabin =false
 
bool mBuechi =false
 
unsigned int mAccSetCount =0
 
int mApCount =0
 
std::map< int, std::string > mApSymbols
 
std::map< std::string, label_expr::ptr > mAliases
 
ImplicitEdgeHelper mImplEdgeHlp
 
std::map< uint32_t, Idx > mEdgeBitsToEvIdx
 

Constructor & Destructor Documentation

◆ HOAConsumerFaudes()

faudes::HOAConsumerFaudes::HOAConsumerFaudes ( Generator &  gen,
const SymbolTable &  syms 
)
inline

Constructor, holding a reference to the generator to read to

Definition at line 240 of file omg_hoa.cpp.

Member Function Documentation

◆ addAlias()

virtual void faudes::HOAConsumerFaudes::addAlias ( const std::string &  name,
label_expr::ptr  labelExpr 
)
inlineoverridevirtual

Definition at line 262 of file omg_hoa.cpp.

◆ addEdgeImplicit()

virtual void faudes::HOAConsumerFaudes::addEdgeImplicit ( unsigned int  stateId,
const int_list &  conjSuccessors,
std::shared_ptr< int_list >  accSignature 
)
inlineoverridevirtual

Definition at line 368 of file omg_hoa.cpp.

◆ addEdgeWithLabel()

virtual void faudes::HOAConsumerFaudes::addEdgeWithLabel ( unsigned int  stateId,
label_expr::ptr  labelExpr,
const int_list &  conjSuccessors,
std::shared_ptr< int_list >  accSignature 
)
inlineoverridevirtual

Definition at line 390 of file omg_hoa.cpp.

◆ addMiscHeader()

virtual void faudes::HOAConsumerFaudes::addMiscHeader ( const std::string &  name,
const std::vector< IntOrString > &  content 
)
inlineoverridevirtual

Definition at line 300 of file omg_hoa.cpp.

◆ addProperties()

virtual void faudes::HOAConsumerFaudes::addProperties ( const std::vector< std::string > &  properties)
inlineoverridevirtual

Definition at line 297 of file omg_hoa.cpp.

◆ addStartStates()

virtual void faudes::HOAConsumerFaudes::addStartStates ( const int_list &  stateConjunction)
inlineoverridevirtual

Definition at line 257 of file omg_hoa.cpp.

◆ addState()

virtual void faudes::HOAConsumerFaudes::addState ( unsigned int  id,
std::shared_ptr< std::string >  info,
label_expr::ptr  labelExpr,
std::shared_ptr< int_list >  accSignature 
)
inlineoverridevirtual

Definition at line 341 of file omg_hoa.cpp.

◆ bits2event()

std::string faudes::HOAConsumerFaudes::bits2event ( uint32_t  bits)
inlineprivate

bit vector to dummy faudes event name

Definition at line 454 of file omg_hoa.cpp.

◆ evalexpr()

bool faudes::HOAConsumerFaudes::evalexpr ( label_expr::ptr  expr,
uint32_t  bits 
)
inlineprivate

evaluate a label expression

Definition at line 464 of file omg_hoa.cpp.

◆ expr2bits()

void faudes::HOAConsumerFaudes::expr2bits ( label_expr::ptr  labelExpr,
HOAConsumer::int_list &  bitslist 
)
inlineprivate

label expression to list of bit vectors (we'ld need SAT solver or at least a hash/cache to do this efficiently)

Definition at line 491 of file omg_hoa.cpp.

◆ notifyAbort()

virtual void faudes::HOAConsumerFaudes::notifyAbort ( )
inlineoverridevirtual

Definition at line 428 of file omg_hoa.cpp.

◆ notifyBodyStart()

virtual void faudes::HOAConsumerFaudes::notifyBodyStart ( )
inlineoverridevirtual

Definition at line 303 of file omg_hoa.cpp.

◆ notifyEnd()

virtual void faudes::HOAConsumerFaudes::notifyEnd ( )
inlineoverridevirtual

Definition at line 419 of file omg_hoa.cpp.

◆ notifyEndOfState()

virtual void faudes::HOAConsumerFaudes::notifyEndOfState ( unsigned int  stateId)
inlineoverridevirtual

Definition at line 415 of file omg_hoa.cpp.

◆ notifyHeaderStart()

virtual void faudes::HOAConsumerFaudes::notifyHeaderStart ( const std::string &  version)
inlineoverridevirtual

Definition at line 247 of file omg_hoa.cpp.

◆ notifyWarning()

virtual void faudes::HOAConsumerFaudes::notifyWarning ( const std::string &  warning)
inlineoverridevirtual

Definition at line 432 of file omg_hoa.cpp.

◆ parserResolvesAliases()

virtual bool faudes::HOAConsumerFaudes::parserResolvesAliases ( )
inlineoverridevirtual

Definition at line 243 of file omg_hoa.cpp.

◆ provideAcceptanceName()

virtual void faudes::HOAConsumerFaudes::provideAcceptanceName ( const std::string &  name,
const std::vector< IntOrString > &  extraInfo 
)
inlineoverridevirtual

Definition at line 277 of file omg_hoa.cpp.

◆ setAcceptanceCondition()

virtual void faudes::HOAConsumerFaudes::setAcceptanceCondition ( unsigned int  numberOfSets,
acceptance_expr::ptr  accExpr 
)
inlineoverridevirtual

Definition at line 273 of file omg_hoa.cpp.

◆ setAPs()

virtual void faudes::HOAConsumerFaudes::setAPs ( const std::vector< std::string > &  aps)
inlineoverridevirtual

Definition at line 266 of file omg_hoa.cpp.

◆ setName()

virtual void faudes::HOAConsumerFaudes::setName ( const std::string &  name)
inlineoverridevirtual

Definition at line 290 of file omg_hoa.cpp.

◆ setNumberOfStates()

virtual void faudes::HOAConsumerFaudes::setNumberOfStates ( unsigned int  numberOfStates)
inlineoverridevirtual

Definition at line 253 of file omg_hoa.cpp.

◆ setTool()

virtual void faudes::HOAConsumerFaudes::setTool ( const std::string &  name,
std::shared_ptr< std::string >  version 
)
inlineoverridevirtual

Definition at line 294 of file omg_hoa.cpp.

Member Data Documentation

◆ mAccSetCount

unsigned int faudes::HOAConsumerFaudes::mAccSetCount =0
private

Definition at line 446 of file omg_hoa.cpp.

◆ mAliases

std::map<std::string,label_expr::ptr> faudes::HOAConsumerFaudes::mAliases
private

Definition at line 449 of file omg_hoa.cpp.

◆ mApCount

int faudes::HOAConsumerFaudes::mApCount =0
private

Definition at line 447 of file omg_hoa.cpp.

◆ mApSymbols

std::map<int,std::string> faudes::HOAConsumerFaudes::mApSymbols
private

Definition at line 448 of file omg_hoa.cpp.

◆ mBuechi

bool faudes::HOAConsumerFaudes::mBuechi =false
private

Definition at line 445 of file omg_hoa.cpp.

◆ mEdgeBitsToEvIdx

std::map<uint32_t,Idx> faudes::HOAConsumerFaudes::mEdgeBitsToEvIdx
private

Definition at line 451 of file omg_hoa.cpp.

◆ mImplEdgeHlp

ImplicitEdgeHelper faudes::HOAConsumerFaudes::mImplEdgeHlp
private

Definition at line 450 of file omg_hoa.cpp.

◆ mRabin

bool faudes::HOAConsumerFaudes::mRabin =false
private

Payload: intermediate parsing results

Definition at line 444 of file omg_hoa.cpp.

◆ pRAut

RabinAutomaton* faudes::HOAConsumerFaudes::pRAut =nullptr
private

Definition at line 440 of file omg_hoa.cpp.

◆ rGen

Generator& faudes::HOAConsumerFaudes::rGen
private

Payload: automaton to parse to

Definition at line 439 of file omg_hoa.cpp.

◆ rSymTab

const SymbolTable& faudes::HOAConsumerFaudes::rSymTab
private

Definition at line 441 of file omg_hoa.cpp.

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

libFAUDES 2.33l --- 2025.09.16 --- c++ api documentaion by doxygen

>>