Class mata::IntermediateAut

class IntermediateAut

Structure for a general intermediate representation of parsed automaton.

It contains information about type of automata, type of naming of nodes, symbols and states and type of alphabet. It contains also the transitions formula and formula for initial and final states. The formulas are represented as tree where nodes are either operands or operators.

Public Types

enum class AutomatonType

Type of automaton.

So far we support nondeterministic finite automata (NFA) and alternating finite automata (AFA)

Values:

enumerator NFA

enumerator AFA

enumerator NFT

enum class Naming

The possible kinds of naming of items in sets of states, nodes, or symbols.

It implies how the given set is defined. Naming could be automatic (all things in formula not belonging to other sets will be assigned to a set with automatic naming), marker based (everything beginning with q is a state, with s is a symbol, with n is a node), or enumerated (the given set is defined by enumeration). There are two special cases used for alphabet - symbols could be any character (CHARS) or anything from utf (UTF).

Values:

enumerator AUTO

enumerator MARKED

enumerator ENUM

enumerator CHARS

enumerator UTF

enum class AlphabetType

Type of alphabet.

We can have explicit alphabet (containing explicit symbols), or bitvector, or class of symbols (e.g., alphabet is everything in utf), or intervals. So far, only explicit representation is supported.

Values:

enumerator EXPLICIT

enumerator BITVECTOR

enumerator CLASS

enumerator INTERVALS

Public Functions

const FormulaGraph &get_symbol_part_of_transition(const std::pair<FormulaNode, FormulaGraph> &trans) const

Returns symbolic part of transition.

That may be just a symbol or bitvector formula. This function is supported only for NFA where transitions have a rhs state at the end of right handed side of transition.

Parameters:

transition – Transition from which symbol is returned

Returns:

Graph representing symbol. It maybe just an explicit symbol or graph representing bitvector formula

std::unordered_set<std::string> get_positive_finals() const

Method returns a set of final states in the case that they were entered as a conjunction of negated states.

It collects all negated states and subtracts them from set of all states.

Public Static Functions

static std::vector<IntermediateAut> parse_from_mf(const mata::parser::Parsed &parsed)

A method for building a vector of IntermediateAut for a parsed input.

For each section in input is created one IntermediateAut. It parses basic information about type of automata, its naming conventions etc. Then it parses input and final formula of automaton. Finally, transition formulas are transformed to graph representation by turning an input stream of tokens to postfix notation and then a tree representing the formula is built from it.

Parameters:

parsed – Parsed input in MATA format.

Returns:

A vector of InterAutomata from each section in parsed input.

struct transitions

Transitions are pairs where the first member is left-hand side of transition (i.e., a state) and the second item is a graph representing transition formula (which can contain symbols, nodes, and states).