File inter-aut.hh

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

class FormulaGraph

#include <inter-aut.hh>

Structure representing a transition formula using a graph.

A node of graph consists of node itself and set of children nodes. Nodes are operators and operands of the formula. E.g., a formula q1 & s1 will be transformed to a tree with & as a root node and q1 and s2 being children nodes of the root.

Public Functions

FormulaGraph() = default

inline explicit FormulaGraph(const FormulaNode &n)

inline explicit FormulaGraph(FormulaNode &&n)

inline FormulaGraph(const FormulaGraph &g)

inline FormulaGraph(FormulaGraph &&g) noexcept

FormulaGraph &operator=(const mata::FormulaGraph&) = default

FormulaGraph &operator=(mata::FormulaGraph&&) noexcept = default

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

void print_tree(std::ostream &os) const

Public Members

FormulaNode node = {}

std::vector<FormulaGraph> children = {}

Private Static Attributes

static size_t MAX_NUM_OF_CHILDREN = {2}

Maximal number of FormulaNode children in any FormulaGraph node (for AND, OR nodes). Only one (NOT node) or zero (FormulaNode node) children may be used. Used as an optimalization by preallocating children at node initialization.

struct FormulaNode

#include <inter-aut.hh>

A node of graph representing transition formula.

A node could be operator (!,&,|) or operand (symbol, state, node). Each node has a name (in case of marking naming, an initial character defining type of node is removed and stored in name), raw (name including potential type marker), and information about its type.

Public Types

enum class OperandType

Values:

enumerator SYMBOL

enumerator STATE

enumerator NODE

enumerator TRUE

enumerator FALSE

enumerator NOT_OPERAND

enum class OperatorType

Values:

enumerator NEG

enumerator AND

enumerator OR

enumerator NOT_OPERATOR

enum class Type

Values:

enumerator OPERAND

enumerator OPERATOR

enumerator LEFT_PARENTHESIS

enumerator RIGHT_PARENTHESIS

enumerator UNKNOWN

Public Functions

inline bool is_operand() const

inline bool is_operator() const

inline bool is_rightpar() const

inline bool is_leftpar() const

inline bool is_state() const

inline bool is_symbol() const

inline bool is_and() const

inline bool is_neg() const

inline bool is_constant() const

inline bool is_true() const

inline bool is_false() const

inline FormulaNode()

inline FormulaNode(Type t, std::string raw, std::string name, OperatorType operator_t)

inline FormulaNode(Type t, std::string raw, std::string name, OperandType operand)

inline FormulaNode(Type t, const std::string &raw)

inline FormulaNode(const FormulaNode &n)

FormulaNode(FormulaNode&&) noexcept = default

FormulaNode &operator=(const FormulaNode &other) = default

FormulaNode &operator=(FormulaNode &&other) noexcept = default

Public Members

Type type

Define whether a node is operand or operator.

std::string raw

Raw name of node as it was specified in input text, i.e., including type marker.

std::string name

Parsed name, i.e., a potential type marker (first character) is removed.

OperatorType operator_type

if a node is operator, it defines which one

OperandType operand_type

if a node is operand, it defines which one

class IntermediateAut

#include <inter-aut.hh>

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

inline bool are_states_enum_type() const

inline bool are_symbols_enum_type() const

inline bool are_nodes_enum_type() const

inline bool is_bitvector() const

inline bool is_nft() const

inline bool is_nfa() const

inline bool is_afa() const

inline std::unordered_set<std::string> get_enumerated_initials() const

inline std::unordered_set<std::string> get_enumerated_finals() const

inline bool are_final_states_conjunction_of_negation() const

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.

size_t get_number_of_disjuncts() const

void add_transition(const FormulaNode &lhs, const FormulaNode &symbol, const FormulaGraph &rhs)

void add_transition(const FormulaNode &lhs, const FormulaNode &rhs)

void print_transitions_trees(std::ostream&) const

Public Members

Naming state_naming = Naming::MARKED

Naming symbol_naming = Naming::MARKED

Naming node_naming = Naming::MARKED

AlphabetType alphabet_type = {}

AutomatonType automaton_type = {}

std::vector<std::string> states_names = {}

std::vector<std::string> symbols_names = {}

std::vector<std::string> nodes_names = {}

FormulaGraph initial_formula = {}

FormulaGraph final_formula = {}

bool initial_enumerated = false

bool final_enumerated = false

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.

static bool is_graph_conjunction_of_negations(const FormulaGraph &graph)

static void parse_transition(mata::IntermediateAut &aut, const std::vector<std::string> &tokens)

struct transitions

#include <inter-aut.hh>

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).

namespace std

Functions

std::ostream &operator<<(std::ostream &os, const mata::IntermediateAut &inter_aut)