Classes
struct	Trans
	A transition. More...

class	Alphabet

class	OnTheFlyAlphabet

class	DirectAlphabet

class	CharAlphabet

class	EnumAlphabet

struct	Nfa
	An NFA. More...

Typedefs
using	State = uintptr_t

using	Symbol = uintptr_t

using	StateSet = std::set< State >

using	PostSymb = std::unordered_map< Symbol, StateSet >
	set of states More...

using	StateToPostMap = std::unordered_map< State, PostSymb >
	post over a symbol More...

using	ProductMap = std::unordered_map< std::pair< State, State >, State >
	transitions More...

using	SubsetMap = std::unordered_map< StateSet, State >

using	Path = std::vector< State >

using	Word = std::vector< Symbol >
	a finite-length path through automaton More...

using	StringToStateMap = std::unordered_map< std::string, State >
	a finite-length word More...

using	StringToSymbolMap = std::unordered_map< std::string, Symbol >

using	StateToStringMap = std::unordered_map< State, std::string >

using	SymbolToStringMap = std::unordered_map< Symbol, std::string >

using	StringDict = std::unordered_map< std::string, std::string >

Functions
Vata2::Parser::ParsedSection	serialize (const Nfa &aut, const SymbolToStringMap symbol_map=nullptr, const StateToStringMap state_map=nullptr)
	serializes Nfa into a ParsedSection More...

bool	are_state_disjoint (const Nfa &lhs, const Nfa &rhs)
	Do the automata have disjoint sets of states? More...

bool	is_lang_empty (const Nfa &aut, Path *cex=nullptr)
	Is the language of the automaton empty? More...

bool	is_lang_empty_cex (const Nfa &aut, Word *cex)

bool	is_universal (const Nfa &aut, const Alphabet &alphabet, Word *cex=nullptr, const StringDict &params={})
	Is the language of the automaton universal? More...

bool	is_universal (const Nfa &aut, const Alphabet &alphabet, const StringDict &params)

bool	is_incl (const Nfa &smaller, const Nfa &bigger, const Alphabet &alphabet, Word *cex=nullptr, const StringDict &params={})
	Checks inclusion of languages of two automata (smaller <= bigger)? More...

bool	is_incl (const Nfa &smaller, const Nfa &bigger, const Alphabet &alphabet, const StringDict &params)

void	union_norename (Nfa *result, const Nfa &lhs, const Nfa &rhs)
	Compute union of a pair of automata Assumes that sets of states of lhs, rhs, and result are disjoint. More...

Nfa	union_norename (const Nfa &lhs, const Nfa &rhs)
	Compute union of a pair of automata. More...

void	intersection (Nfa result, const Nfa &lhs, const Nfa &rhs, ProductMap prod_map=nullptr)
	Compute intersection of a pair of automata. More...

Nfa	intersection (const Nfa &lhs, const Nfa &rhs, ProductMap *prod_map=nullptr)

void	determinize (Nfa result, const Nfa &aut, SubsetMap subset_map=nullptr, State *last_state_num=nullptr)
	Determinize an automaton. More...

Nfa	determinize (const Nfa &aut, SubsetMap subset_map=nullptr, State last_state_num=nullptr)

void	make_complete (Nfa *aut, const Alphabet &alphabet, State sink_state)
	makes the transition relation complete More...

void	complement (Nfa result, const Nfa &aut, const Alphabet &alphabet, SubsetMap subset_map=nullptr)
	Complement. More...

Nfa	complement (const Nfa &aut, const Alphabet &alphabet, SubsetMap *subset_map=nullptr)

void	revert (Nfa *result, const Nfa &aut)
	Reverting the automaton. More...

Nfa	revert (const Nfa &aut)

bool	is_deterministic (const Nfa &aut)
	Test whether an automaton is deterministic, i.e., whether it has exactly one initial state and every state has at most one outgoing transition over every symbol. Checks the whole automaton, not only the reachable part. More...

bool	is_complete (const Nfa &aut, const Alphabet &alphabet)
	Test for automaton completeness wrt an alphabet. An automaton is complete if every reachable state has at least one outgoing transition over every symbol. More...

void	construct (Nfa aut, const Vata2::Parser::ParsedSection &parsec, StringToSymbolMap symbol_map=nullptr, StringToStateMap *state_map=nullptr)
	Loads an automaton from Parsed object. More...

Nfa	construct (const Vata2::Parser::ParsedSection &parsec, StringToSymbolMap symbol_map=nullptr, StringToStateMap state_map=nullptr)
	Loads an automaton from Parsed object. More...

void	construct (Nfa aut, const Vata2::Parser::ParsedSection &parsec, Alphabet alphabet, StringToStateMap *state_map=nullptr)
	Loads an automaton from Parsed object. More...

Nfa	construct (const Vata2::Parser::ParsedSection &parsec, Alphabet alphabet, StringToStateMap state_map=nullptr)
	Loads an automaton from Parsed object. More...

std::pair< Word, bool >	get_word_for_path (const Nfa &aut, const Path &path)
	Obtains a word corresponding to a path in an automaton (or sets a flag) More...

bool	is_in_lang (const Nfa &aut, const Word &word)
	Checks whether a string is in the language of an automaton. More...

bool	is_prfx_in_lang (const Nfa &aut, const Word &word)
	Checks whether the prefix of a string is in the language of an automaton. More...

Word	encode_word (const StringToSymbolMap &symbol_map, const std::vector< std::string > &input)
	Encodes a vector of strings (each corresponding to one symbol) into a `Word` instance. More...

std::ostream &	operator<< (std::ostream &strm, const Nfa &nfa)
	operator<< More...

void	init ()
	global constructor to be called at program startup (from vm-dispatch) More...

Variables
const PostSymb	EMPTY_POST {}

Typedef Documentation

using Path = std::vector<State>

Definition at line 47 of file nfa.hh.

using PostSymb = std::unordered_map<Symbol, StateSet>

set of states

Definition at line 42 of file nfa.hh.

using ProductMap = std::unordered_map<std::pair<State, State>, State>

transitions

Definition at line 45 of file nfa.hh.

using State = uintptr_t

Definition at line 39 of file nfa.hh.

using StateSet = std::set<State>

Definition at line 41 of file nfa.hh.

using StateToPostMap = std::unordered_map<State, PostSymb>

post over a symbol

Definition at line 43 of file nfa.hh.

using StateToStringMap = std::unordered_map<State, std::string>

Definition at line 52 of file nfa.hh.

using StringDict = std::unordered_map<std::string, std::string>

Definition at line 55 of file nfa.hh.

using StringToStateMap = std::unordered_map<std::string, State>

a finite-length word

Definition at line 50 of file nfa.hh.

using StringToSymbolMap = std::unordered_map<std::string, Symbol>

Definition at line 51 of file nfa.hh.

using SubsetMap = std::unordered_map<StateSet, State>

Definition at line 46 of file nfa.hh.

using Symbol = uintptr_t

Definition at line 40 of file nfa.hh.

using SymbolToStringMap = std::unordered_map<Symbol, std::string>

Definition at line 53 of file nfa.hh.

using Word = std::vector<Symbol>

a finite-length path through automaton

Definition at line 48 of file nfa.hh.

Function Documentation

bool Vata2::Nfa::are_state_disjoint	(	const Nfa &	lhs,
		const Nfa &	rhs
	)

Do the automata have disjoint sets of states?

void Vata2::Nfa::complement	(	Nfa *	result,
		const Nfa &	aut,
		const Alphabet &	alphabet,
		SubsetMap *	subset_map = `nullptr`
	)

Complement.

Referenced by complement().

Nfa Vata2::Nfa::complement	(	const Nfa &	aut,
		const Alphabet &	alphabet,
		SubsetMap *	subset_map = `nullptr`
	)

inline

Definition at line 427 of file nfa.hh.

References complement().

void Vata2::Nfa::construct	(	Nfa *	aut,
		const Vata2::Parser::ParsedSection &	parsec,
		StringToSymbolMap *	symbol_map = `nullptr`,
		StringToStateMap *	state_map = `nullptr`
	)

Loads an automaton from Parsed object.

Referenced by construct().

Nfa Vata2::Nfa::construct	(	const Vata2::Parser::ParsedSection &	parsec,
		StringToSymbolMap *	symbol_map = `nullptr`,
		StringToStateMap *	state_map = `nullptr`
	)

inline

Loads an automaton from Parsed object.

Definition at line 466 of file nfa.hh.

References construct().

void Vata2::Nfa::construct	(	Nfa *	aut,
		const Vata2::Parser::ParsedSection &	parsec,
		Alphabet *	alphabet,
		StringToStateMap *	state_map = `nullptr`
	)

Loads an automaton from Parsed object.

Nfa Vata2::Nfa::construct	(	const Vata2::Parser::ParsedSection &	parsec,
		Alphabet *	alphabet,
		StringToStateMap *	state_map = `nullptr`
	)

inline

Loads an automaton from Parsed object.

Definition at line 484 of file nfa.hh.

References construct().

void Vata2::Nfa::determinize	(	Nfa *	result,
		const Nfa &	aut,
		SubsetMap *	subset_map = `nullptr`,
		State *	last_state_num = `nullptr`
	)

Determinize an automaton.

Referenced by determinize().

Nfa Vata2::Nfa::determinize	(	const Nfa &	aut,
		SubsetMap *	subset_map = `nullptr`,
		State *	last_state_num = `nullptr`
	)

inline

Definition at line 404 of file nfa.hh.

References determinize().

Word Vata2::Nfa::encode_word	(	const StringToSymbolMap &	symbol_map,
		const std::vector< std::string > &	input
	)

inline

Encodes a vector of strings (each corresponding to one symbol) into a Word instance.

Definition at line 521 of file nfa.hh.

std::pair<Word, bool> Vata2::Nfa::get_word_for_path	(	const Nfa &	aut,
		const Path &	path
	)

Obtains a word corresponding to a path in an automaton (or sets a flag)

Returns a word that is consistent with path of states in automaton aut, or sets a flag to false if such a word does not exist. Note that there may be several words with the same path (in case some pair of states is connected by transitions over more than one symbol).

Parameters

[in]	aut	The automaton
[in]	path	The path of states

Returns: A pair (word, bool) where if bool is true, then word is a word consistent with path, and if bool is false, this denotes that the path is invalid in aut

void Vata2::Nfa::init ( )

global constructor to be called at program startup (from vm-dispatch)

void Vata2::Nfa::intersection	(	Nfa *	result,
		const Nfa &	lhs,
		const Nfa &	rhs,
		ProductMap *	prod_map = `nullptr`
	)

Compute intersection of a pair of automata.

Referenced by intersection().

Nfa Vata2::Nfa::intersection	(	const Nfa &	lhs,
		const Nfa &	rhs,
		ProductMap *	prod_map = `nullptr`
	)

inline

Definition at line 387 of file nfa.hh.

References intersection().

bool Vata2::Nfa::is_complete	(	const Nfa &	aut,
		const Alphabet &	alphabet
	)

Test for automaton completeness wrt an alphabet. An automaton is complete if every reachable state has at least one outgoing transition over every symbol.

bool Vata2::Nfa::is_deterministic ( const Nfa & aut )

Test whether an automaton is deterministic, i.e., whether it has exactly one initial state and every state has at most one outgoing transition over every symbol. Checks the whole automaton, not only the reachable part.

bool Vata2::Nfa::is_in_lang	(	const Nfa &	aut,
		const Word &	word
	)

Checks whether a string is in the language of an automaton.

bool Vata2::Nfa::is_incl	(	const Nfa &	smaller,
		const Nfa &	bigger,
		const Alphabet &	alphabet,
		Word *	cex = `nullptr`,
		const StringDict &	params = `{}`
	)

Checks inclusion of languages of two automata (smaller <= bigger)?

Referenced by is_incl().

bool Vata2::Nfa::is_incl	(	const Nfa &	smaller,
		const Nfa &	bigger,
		const Alphabet &	alphabet,
		const StringDict &	params
	)

inline

Definition at line 354 of file nfa.hh.

References is_incl().

bool Vata2::Nfa::is_lang_empty	(	const Nfa &	aut,
		Path *	cex = `nullptr`
	)

Is the language of the automaton empty?

bool Vata2::Nfa::is_lang_empty_cex	(	const Nfa &	aut,
		Word *	cex
	)

bool Vata2::Nfa::is_prfx_in_lang	(	const Nfa &	aut,
		const Word &	word
	)

Checks whether the prefix of a string is in the language of an automaton.

bool Vata2::Nfa::is_universal	(	const Nfa &	aut,
		const Alphabet &	alphabet,
		Word *	cex = `nullptr`,
		const StringDict &	params = `{}`
	)

Is the language of the automaton universal?

Referenced by is_universal().

bool Vata2::Nfa::is_universal	(	const Nfa &	aut,
		const Alphabet &	alphabet,
		const StringDict &	params
	)

inline

Definition at line 338 of file nfa.hh.

References is_universal().

void Vata2::Nfa::make_complete	(	Nfa *	aut,
		const Alphabet &	alphabet,
		State	sink_state
	)

makes the transition relation complete

std::ostream& Vata2::Nfa::operator<<	(	std::ostream &	strm,
		const Nfa &	nfa
	)

operator<<

void Vata2::Nfa::revert	(	Nfa *	result,
		const Nfa &	aut
	)

Reverting the automaton.

Referenced by revert().

Nfa Vata2::Nfa::revert ( const Nfa & aut )

inline

Definition at line 440 of file nfa.hh.

References revert().

Vata2::Parser::ParsedSection Vata2::Nfa::serialize	(	const Nfa &	aut,
		const SymbolToStringMap *	symbol_map = `nullptr`,
		const StateToStringMap *	state_map = `nullptr`
	)