nfa.hh File Reference

#include <algorithm>
#include <cassert>
#include <cstdint>
#include <set>
#include <unordered_map>
#include <vector>
#include <vata2/parser.hh>
#include <vata2/util.hh>

Go to the source code of this file.

Classes
struct	Trans
	A transition. More...
class	Alphabet
class	OnTheFlyAlphabet
class	DirectAlphabet
class	CharAlphabet
class	EnumAlphabet
struct	Nfa
	An NFA. More...
struct	Nfa::const_iterator
	number of transitions; has linear time complexity More...
struct	hash< Vata2::Nfa::Trans >

Namespaces
	Vata2
	Vata2::Nfa

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...
std::ostream &	operator<< (std::ostream &strm, const Vata2::Nfa::Trans &trans)

Variables
const PostSymb	EMPTY_POST {}