From f7e8a86c0520ec724ef4892ad00e55c89a4c232f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Tue, 19 Sep 2023 09:45:46 +0200 Subject: [PATCH] Remove AFA implementation --- README.md | 3 +- doc/afa.rst | 11 - doc/index.rst | 1 - doc/overview.rst | 2 - examples/example05-parsing-afa.cc | 46 -- include/mata/afa/afa.hh | 507 ------------ src/CMakeLists.txt | 1 - src/afa/afa.cc | 1200 ----------------------------- tests/CMakeLists.txt | 1 - tests/afa/afa.cc | 741 ------------------ tests/mintermization.cc | 379 +-------- 11 files changed, 6 insertions(+), 2886 deletions(-) delete mode 100644 doc/afa.rst delete mode 100644 examples/example05-parsing-afa.cc delete mode 100644 include/mata/afa/afa.hh delete mode 100644 src/afa/afa.cc delete mode 100644 tests/afa/afa.cc diff --git a/README.md b/README.md index eaffe16a1..a39e3c13b 100644 --- a/README.md +++ b/README.md @@ -5,8 +5,7 @@ [![Python-Binding (build-&-test)](https://github.com/VeriFIT/mata/actions/workflows/python-binding.yml/badge.svg?branch=devel)](https://github.com/VeriFIT/mata/actions/workflows/python-binding.yml) [![codecov](https://codecov.io/gh/VeriFIT/mata/branch/devel/graph/badge.svg?token=9VAVD19N4D)](https://codecov.io/gh/VeriFIT/mata) -Mata is an open source automata library that offers interface for different kinds of automata (NFA, -AFA, etc.). Currently, Mata offers two interfaces: +Mata is an open source automata library that offers interface for different kinds of automata (NFA, etc.). Currently, Mata offers two interfaces: 1. An efficient library implemented in C/C++ 2. A flexible wrapper implemented in Python that uses the efficient library diff --git a/doc/afa.rst b/doc/afa.rst deleted file mode 100644 index 42aeaae4d..000000000 --- a/doc/afa.rst +++ /dev/null @@ -1,11 +0,0 @@ -Alternating Finite automata -================================== - -Structures ----------- - -.. doxygenstruct:: mata::afa::Afa - :members: - -Operations ----------- diff --git a/doc/index.rst b/doc/index.rst index 43cad38e8..221c183a8 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -13,7 +13,6 @@ Welcome to automata-library's documentation! introduction overview nfa - afa Indices and tables diff --git a/doc/overview.rst b/doc/overview.rst index df7452b48..c3104bfbb 100644 --- a/doc/overview.rst +++ b/doc/overview.rst @@ -5,5 +5,3 @@ Supported Classes of Automata ----------------------------- .. doxygenstruct:: mata::nfa::Nfa - -.. doxygenstruct:: mata::afa::Afa diff --git a/examples/example05-parsing-afa.cc b/examples/example05-parsing-afa.cc deleted file mode 100644 index e7d259011..000000000 --- a/examples/example05-parsing-afa.cc +++ /dev/null @@ -1,46 +0,0 @@ -// example5-parsing-afa.cc - parsing AFA from file - -#include "mata/afa/afa.hh" -#include "mata/parser/inter-aut.hh" - -#include -#include - -using namespace mata::afa; - -int main(int argc, char *argv[]) { - if (argc != 2) { - std::cerr << "Input file missing\n"; - return EXIT_FAILURE; - } - - std::string filename = argv[1]; - - std::fstream fs(filename, std::ios::in); - if (!fs) { - std::cerr << "Could not open file \'" << filename << "'\n"; - return EXIT_FAILURE; - } - - mata::parser::Parsed parsed; - Afa aut; - try { - parsed = mata::parser::parse_mf(fs, true); - fs.close(); - - std::vector inter_auts = mata::IntermediateAut::parse_from_mf(parsed); - for (const auto& ia : inter_auts) - std::cout << ia << '\n'; - - if (inter_auts[0].is_afa()) - aut = construct(inter_auts[0]); - std::cout << aut << '\n'; - } - catch (const std::exception& ex) { - fs.close(); - std::cerr << "libMATA error: " << ex.what() << "\n"; - return EXIT_FAILURE; - } - - return EXIT_SUCCESS; -} diff --git a/include/mata/afa/afa.hh b/include/mata/afa/afa.hh deleted file mode 100644 index 1def81874..000000000 --- a/include/mata/afa/afa.hh +++ /dev/null @@ -1,507 +0,0 @@ -/* afa.hh -- alternating finite automaton (over finite words) - * - * Copyright (c) TODO - * - * This file is a part of libmata. - * - * This program is free software; you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation; either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - */ - -#ifndef MATA_AFA_HH_ -#define MATA_AFA_HH_ - -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include "mata/alphabet.hh" -#include "mata/nfa/nfa.hh" -#include "mata/parser/parser.hh" -#include "mata/utils/utils.hh" -#include "mata/utils/ord-vector.hh" -#include "mata/utils/closed-set.hh" -#include "mata/nfa/builder.hh" - -/** - * Alternating Finite Automata including structures, transitions and algorithms. - * - * In particular, this includes: - * 1. Structures (Automaton, Transitions, Results), - * 2. Algorithms (operations, checks, tests), - * 3. Constructions. - */ -namespace mata::afa { -extern const std::string TYPE_AFA; - -using State = mata::nfa::State; - -using SymbolToStringMap = std::unordered_map; - -template using OrdVec = mata::utils::OrdVector; - -using Node = OrdVec; -using Nodes = OrdVec; - -using StateNameMap = std::unordered_map; -using NameStateMap = nfa::builder::NameStateMap; - -using Path = std::vector; -using Word = std::vector; - -using StringDict = mata::nfa::ParameterMap; - -using StateSet = OrdVec; -using StateClosedSet = mata::ClosedSet; - -/* -* A node is an ordered vector of states of the automaton. -* A transition consists of a source state, a symbol on the transition -* and a vector of nodes (which are the destination of the transition). -* -* In context of an AFA, the transition relation maps a state and a symbol -* to the positive Boolean formula over states, which is a Boolean formula -* using states in positive form, conjunctions and disjunctions. Since such -* a formula can be converted to the DNF, we can represent it as an ordered vector -* of nodes. The ordered vector represents a set of disjuncts. Each node corresponds -* to a single disjunct of a formula in DNF (states connected by conjunctions). -* -*/ -struct Trans -{ - State src; // source state - Symbol symb; // transition symbol - Nodes dst; // a vector of vectors of states - - Trans() : src(), symb(), dst() { } - Trans(const State src, const Symbol symb, const Node& dst) : src(src), symb(symb), dst(Nodes{ dst }) {} - Trans(const State src, const Symbol symb, Nodes dst) : src(src), symb(symb), dst(std::move(dst)) {} - - bool operator==(const Trans& rhs) const - { // {{{ - return src == rhs.src && symb == rhs.symb && dst == rhs.dst ; - } // operator== }}} - bool operator!=(const Trans& rhs) const { return !this->operator==(rhs); } - -}; // struct Trans - -using TransList = std::vector; -using TransRelation = std::vector; - -/* A tuple (result_node, precondition). The node result_node is a predecessor -* of a given node 'N' if the node 'precondition' is its subset. */ -struct InverseResults{ - - Node result_node{}; - Node precondition{}; - - InverseResults() : result_node(), precondition() {} - InverseResults(State state, Node precondition) - : result_node(Node(state)), precondition(std::move(precondition)) {} - InverseResults(Node result_node, Node precondition) - : result_node(std::move(result_node)), precondition(std::move(precondition)) {} - - bool operator==(const InverseResults& rhs) const - { // {{{ - return precondition == rhs.precondition && result_node == rhs.result_node; - } // operator== }}} - - bool operator!=(const InverseResults& rhs) const - { // {{{ - return !this->operator==(rhs); - } // operator!= }}} - - bool operator<(const InverseResults& rhs) const - { // {{{ - return precondition < rhs.precondition || - (precondition == rhs.precondition && result_node < rhs.result_node); - } // operator< }}} - -}; // struct InverseResults - -/** - * A tuple (state, symb, inverseResults). The structure inverseResults contains tuples (inverseResult, - * precondition). If a node is a subset of 'precondition', the 'inverseResult' is a predecessor - * of the given node which is accessible through the symbol 'symb'. - * The state 'state' is always part of all 'preconditions' and it is a minimal element of them. - */ -struct InverseTrans { - State state{}; - Symbol symb{}; - std::vector inverseResults{}; - - InverseTrans() = default; - explicit InverseTrans(Symbol symb) : symb(symb), inverseResults(std::vector()) { } - InverseTrans(Symbol symb, const InverseResults& inverseResults_) : symb(symb) { inverseResults.push_back(inverseResults_); } - InverseTrans(State state, Symbol symb, const InverseResults& inverseResults_) - : state(state), symb(symb) { inverseResults.push_back(inverseResults_); } -}; // struct InverseTrans - -using InverseTransRelation = std::vector>; - -struct Afa; - -/// serializes Afa into a ParsedSection -mata::parser::ParsedSection serialize( - const Afa& aut, - const SymbolToStringMap* symbol_map = nullptr, - const StateNameMap* state_map = nullptr); - - -/// An AFA -struct Afa -{ // {{{ -private: - TransRelation transitionrelation{}; - InverseTransRelation inverseTransRelation{}; - -public: - - Afa() : transitionrelation(), inverseTransRelation() {} - - explicit Afa(const unsigned long num_of_states, const Nodes& initial_states = Nodes{}, - const StateSet& final_states = StateSet{}) - : transitionrelation(num_of_states), inverseTransRelation(num_of_states), - initialstates(initial_states), finalstates(final_states) {} - -public: - - Nodes initialstates = {}; - StateSet finalstates = {}; - - State add_new_state(); - - auto get_num_of_states() const { return transitionrelation.size(); } - - void add_initial(State state) { this->initialstates.insert(Node({state})); } - void add_initial(Node node) { this->initialstates.insert(node); } - void add_initial(const std::vector& vec) - { // {{{ - Node node{}; - for (const State& st : vec) { node.insert(st); } - this->initialstates.insert(node); - } // }}} - bool has_initial(State state) const - { // {{{ - return has_initial(Node({state})); - } // }}} - bool has_initial(Node node) const - { // {{{ - return StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1, initialstates).contains(node); - } // }}} - void add_final(State state) { this->finalstates.insert(state); } - void add_final(const std::vector vec) - { // {{{ - for (const State& st : vec) { this->add_final(st); } - } // }}} - bool has_final(State state) const - { // {{{ - return mata::utils::haskey(this->finalstates, state); - } // }}} - - void add_trans(const Trans& trans); - void add_trans(State src, Symbol symb, State dst) - { // {{{ - this->add_trans({src, symb, Nodes(Node(dst))}); - } // }}} - void add_trans(State src, Symbol symb, Node dst) - { // {{{ - this->add_trans({src, symb, Nodes(dst)}); - } // }}} - void add_trans(State src, Symbol symb, Nodes dst) - { // {{{ - this->add_trans({src, symb, dst}); - } // }}} - - void add_inverse_trans(const Trans& trans); - void add_inverse_trans(State src, Symbol symb, Node dst) - { // {{{ - this->add_inverse_trans({src, symb, Nodes(dst)}); - } // }}} - void add_inverse_trans(State src, Symbol symb, Nodes dst) - { // {{{ - this->add_inverse_trans({src, symb, dst}); - } // }}} - - std::vector perform_inverse_trans(State src, Symbol symb) const; - std::vector perform_inverse_trans(const Node& src, Symbol symb) const; - - bool has_trans(const Trans& trans) const; - bool has_trans(State src, Symbol symb, Node dst) const - { // {{{ - return this->has_trans({src, symb, Nodes(dst)}); - } // }}} - bool has_trans(State src, Symbol symb, Nodes dst) const - { // {{{ - return this->has_trans({src, symb, dst}); - } // }}} - - std::vector get_trans_from_state(State state) const; - Trans get_trans_from_state(State state, Symbol symbol) const; - - bool trans_empty() const { return transitionrelation.empty(); }// no transitions - size_t trans_size() const;/// number of transitions; has linear time complexity - - - StateClosedSet post(State state, Symbol symb) const; - StateClosedSet post(const Node& node, Symbol symb) const; - StateClosedSet post(const Nodes& nodes, Symbol symb) const; - StateClosedSet post(const StateClosedSet& closed_set, Symbol symb) const; - - StateClosedSet post(const Node& node) const; - StateClosedSet post(const Nodes& nodes) const; - - StateClosedSet post(const StateClosedSet& closed_set) const; - - StateClosedSet pre(const Node& node, Symbol symb) const; - StateClosedSet pre(const State state, const Symbol symb) const { return pre(Node(state), symb); }; - StateClosedSet pre(const Nodes& nodes, Symbol symb) const; - StateClosedSet pre(const StateClosedSet& closed_set, Symbol symb) const; - - StateClosedSet pre(const Node& node) const; - StateClosedSet pre(const Nodes& nodes) const; - - StateClosedSet pre(StateClosedSet closed_set) const { return pre(closed_set.antichain()); }; - - StateClosedSet get_initial_nodes() const; - - StateClosedSet get_non_initial_nodes() const { - return StateClosedSet{ ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1, initialstates }.complement(); - }; - StateClosedSet get_final_nodes() const { - return { ClosedSetType::downward_closed_set, 0, transitionrelation.size()-1, finalstates }; - }; - - /** - * @brief This function returns an upward-closed set of all the nodes which are non-final. - * @return Closed set of non-final nodes. - */ - StateClosedSet get_non_final_nodes() const; - -}; // Afa }}} - -/// a wrapper encapsulating @p Afa for higher-level use -struct AfaWrapper -{ // {{{ - /// the AFA - Afa afa; - - /// the alphabet - Alphabet* alphabet; - - /// mapping of state names (as strings) to their numerical values - NameStateMap state_dict; -}; // AfaWrapper }}} - -/// Do the automata have disjoint sets of states? -bool are_state_disjoint(const Afa& lhs, const Afa& rhs); -/// Is the language of the automaton empty? -bool is_lang_empty(const Afa& aut, Path* cex = nullptr); -bool is_lang_empty_cex(const Afa& aut, Word* cex); - -bool antichain_concrete_forward_emptiness_test_old(const Afa& aut); -bool antichain_concrete_backward_emptiness_test_old(const Afa& aut); - -bool antichain_concrete_forward_emptiness_test_new(const Afa& aut); -bool antichain_concrete_backward_emptiness_test_new(const Afa& aut); - -/// Retrieves the states reachable from initial states -std::unordered_set get_fwd_reach_states(const Afa& aut); - -/// Is the language of the automaton universal? -bool is_universal( - const Afa& aut, - const Alphabet& alphabet, - Word* cex = nullptr, - const StringDict& params = {{"algorithm", "antichains"}}); - -inline bool is_universal( - const Afa& aut, - const Alphabet& alphabet, - const StringDict& params) -{ // {{{ - return is_universal(aut, alphabet, nullptr, params); -} // }}} - -/// Does the language of the automaton contain epsilon? -bool accepts_epsilon(const Afa& aut); - -/// Checks inclusion of languages of two automata (smaller <= bigger)? -bool is_incl( - const Afa& smaller, - const Afa& bigger, - const Alphabet& alphabet, - Word* cex = nullptr, - const StringDict& params = {{"algorithm", "antichains"}}); - -inline bool is_incl( - const Afa& smaller, - const Afa& bigger, - const Alphabet& alphabet, - const StringDict& params) -{ // {{{ - return is_incl(smaller, bigger, alphabet, nullptr, params); -} // }}} - -/// Compute union of a pair of automata -/// Assumes that sets of states of lhs, rhs, and result are disjoint -void union_norename( - Afa* result, - const Afa& lhs, - const Afa& rhs); - -/// Compute union of a pair of automata -inline Afa union_norename( - const Afa& lhs, - const Afa& rhs) -{ // {{{ - Afa result; - union_norename(&result, lhs, rhs); - return result; -} // union_norename }}} - -/// Compute union of a pair of automata -/// The states of the automata do not need to be disjoint; renaming will be done -Afa union_rename( - const Afa& lhs, - const Afa& rhs); - - -/// makes the transition relation complete -void make_complete( - Afa* aut, - const Alphabet& alphabet, - State sink_state); - -/// Reverting the automaton -void revert(Afa* result, const Afa& aut); - -inline Afa revert(const Afa& aut) { - Afa result; - revert(&result, aut); - return result; -} - -/// Removing epsilon transitions -void remove_epsilon(Afa* result, const Afa& aut, Symbol epsilon); - -inline Afa remove_epsilon(const Afa& aut, Symbol epsilon) { - Afa result{}; - remove_epsilon(&result, aut, epsilon); - return result; -} - -/// Minimizes an AFA. The method can be set using @p params -void minimize( - Afa* result, - const Afa& aut, - const StringDict& params = {}); - - -inline Afa minimize( - const Afa& aut, - const StringDict& params = {}) -{ // {{{ - Afa result; - minimize(&result, aut, params); - return result; -} // minimize }}} - - -/// 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 is_deterministic(const Afa& aut); - -/// 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 is_complete(const Afa& aut, const Alphabet& alphabet); - -/** Loads an automaton from Parsed object */ -Afa construct(const mata::parser::ParsedSection& parsec, Alphabet* alphabet, NameStateMap* state_map = nullptr); -/** Loads automaton from intermediate automaton */ -Afa construct(const mata::IntermediateAut& inter_aut, Alphabet* alphabet, NameStateMap* state_map = nullptr); - -/** - * @brief Loads automaton from parsed object (either ParsedSection or Intermediate automaton. - * - * If user does not provide symbol map or state map, it allocates its own ones. - */ -template -Afa construct(const ParsedObject& parsed, Alphabet* alphabet = nullptr, NameStateMap* state_map = nullptr) { - mata::OnTheFlyAlphabet tmp_alphabet{}; - if (!alphabet) { - alphabet = &tmp_alphabet; - } - return construct(parsed, alphabet, state_map);; -} - -/** Loads an automaton from Parsed object */ -template void construct(Afa* result, const ParsedObject& parsed, - Alphabet* alphabet = nullptr, NameStateMap* state_map = nullptr) { - mata::OnTheFlyAlphabet tmp_alphabet{}; - if (!alphabet) { - alphabet = &tmp_alphabet; - } - *result = construct(parsed, alphabet, state_map); -} - -/** - * @brief Obtains a word corresponding to a path in an automaton (or sets a flag) - * - * Returns a word that is consistent with @p path of states in automaton @p - * aut, or sets a flag to @p 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). - * - * @param[in] aut The automaton - * @param[in] path The path of states - * - * @returns A pair (word, bool) where if @p bool is @p true, then @p word is a - * word consistent with @p path, and if @p bool is @p false, this - * denotes that the path is invalid in @p aut - */ -std::pair get_word_for_path(const Afa& aut, const Path& path); - -/// Checks whether a string is in the language of an automaton -bool is_in_lang(const Afa& aut, const Word& word); - -/// Checks whether the prefix of a string is in the language of an automaton -bool is_prfx_in_lang(const Afa& aut, const Word& word); - -/** Encodes a vector of strings (each corresponding to one symbol) into a @c Word instance. */ -inline Word encode_word(const Alphabet& alphabet, const std::vector& input); - -std::ostream& operator<<(std::ostream& os, const Afa& afa); - -/// global constructor to be called at program startup (from vm-dispatch) -void init(); - -} // namespace mata::afa. - -namespace std { - -template <> struct hash { - inline size_t operator()(const mata::afa::Trans& trans) const; -}; - -std::ostream& operator<<(std::ostream& os, const mata::afa::Trans& trans); -std::ostream& operator<<(std::ostream& os, const mata::afa::AfaWrapper& afa_wrap); - -} // namespace std. - -#endif /* MATA_AFA_HH_ */ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3f93c481d..c3b5bbea0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -4,7 +4,6 @@ configure_file("${CMAKE_CURRENT_SOURCE_DIR}/config.cc.in" "${CMAKE_CURRENT_BINAR add_library(libmata STATIC # add_library(libmata SHARED alphabet.cc - afa/afa.cc "${CMAKE_CURRENT_BINARY_DIR}/config.cc" inter-aut.cc mintermization.cc diff --git a/src/afa/afa.cc b/src/afa/afa.cc deleted file mode 100644 index b1e5c7603..000000000 --- a/src/afa/afa.cc +++ /dev/null @@ -1,1200 +0,0 @@ -/* afa.cc -- operations for AFA - * - * Copyright (c) TODO TODO - * - * This file is a part of libmata. - * - * This program is free software; you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation; either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - */ - -// NOTE: AFA implementation is in an unmaintained state at the moment. -// We hide warnings from the AFA implementation until we rewrite the whole AFA module from scratch. - -#pragma GCC diagnostic push -#pragma GCC diagnostic ignored "-Wpragmas" -#pragma GCC diagnostic ignored "-Wunused-parameter" -#pragma GCC diagnostic ignored "-Wreturn-type" -#pragma GCC diagnostic ignored "-Wstring-conversion" - -#include -#include -#include -#include -#include - -// MATA headers -#include "mata/afa/afa.hh" - -using std::tie; - -using namespace mata::utils; -using namespace mata::afa; - -const std::string mata::afa::TYPE_AFA = "AFA"; - -std::ostream& std::operator<<(std::ostream& os, const mata::afa::Trans& trans) { - std::string result = "(" + std::to_string(trans.src) + ", " - + std::to_string(trans.symb) + ", " - + std::to_string(trans.dst) + ")"; - return os << result; -} // operator<<(ostream, Trans) }}} - -/** This function adds a new transition to the automaton. It changes a transition -* relation. The transition is added to the transition relation it its current form. -* @brief adds a new transition -* @param trans a given transition -*/ -void Afa::add_trans(const Trans& trans) -{ // {{{ - assert(trans.src < this->transitionrelation.size() && "It is not possible to perform a transition " && - "from non-existing state."); - - // If the corresponding transition already exists, given 'dst' will be added to - // the transition - for(auto & transVec : transitionrelation[trans.src]) - { - if(transVec.symb == trans.symb) - { - // Before the dst nodes are added to the transition, we want to get rid - // of redundant clauses. For example, in context of the formula - // (1 || (1 && 2)), the clause (1 && 2) could be deleted - auto cl = StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1, transVec.dst); - cl.insert(trans.dst); - transVec.dst = cl.antichain(); - return; - } - } - - // If there is no result, a new transition will be created - transitionrelation[trans.src].push_back(trans); - -} // add_trans }}} - -/** This function gets a vector of all transitions which are possible to -* be performed from the given state. -* @brief gets all the transitions from the given state -* @param state a state of the automaton -* @return a vector of transitions -*/ -std::vector Afa::get_trans_from_state(State state) const -{ - assert(state < transitionrelation.size() && - "It is not possible to perform transitions from an non-existing state."); - std::vector result = std::vector(); - for(const auto& transition : transitionrelation[state]) - { - result.push_back(transition); - } - return result; -} - -/** This function gets a vector of all transitions which are possible to -* be performed from the given state using the given symbol. -* If there is no such transition, the result will be an empty transition. -* @brief gets all the transitions from the given state -* @param state a state of the automaton -* @param symbol a symbol which could be used to perform a transition -* @return a corresponding transition -*/ -Trans Afa::get_trans_from_state(State state, Symbol symbol) const -{ - assert(state < transitionrelation.size() && - "It is not possible to perform transitions from an non-existing state."); - for(auto transition : transitionrelation[state]) - { - if(transition.symb == symbol) - { - return transition; - } - } - return { state, symbol, Nodes{} }; -} - - -/** This function adds a new inverse transition to the automaton -* It changes an inverse transition relation. -* @brief adds a new inverse transition -* @param trans a given TRANSITION (it will be inverted within this function) -*/ -void Afa::add_inverse_trans(const Trans& trans) -{// {{{ - - // Iterating through all the nodes which were given as a destination of the current transition - for(auto node : trans.dst) - { - - // If there is already a memory cell which corresponds to the current dst node and a - // transition symbol, we have to find it and add the 'src' state to the corresponding - // result_node vector. Let us recall that the inverse transition datatype is a vector - // of vectors of tuples (symbol, vector_of_inverse_results). Each InverseResult is - // a tuple (result_node, precondition). If there exists such a tuple, where - // the precondition corresponds to the current dst node, we can simply add the current - // 'src' state to the result_node. Since the corresponding tuple (result_node, - // precondition) would be identical for all states of the current node, we can store it - // to the memory only once. For this purpose, we choose the minimal element from - // the current node. Then, it is sufficient to choose the minimal element of the dst - // node and look if there exists such a tuple (result_node, precondition), where - // precondition == dst node in context of the current symbol. - // - // Example: We have transitions (0, a, {0, 1}), (0, b, {1}). - // The inverse transition data structure looks like this: - // - // 0 -> {('a', {(result_node:{0}, precondition:{0, 1})})} - // 1 -> {('a', {}), - // ('b', {(result_node:{0}, precondition:{1})})} - // - // Now, we want to add the transition (1, a, {0, 1}), so we choose the minimal element - // of the dst node {0, 1}, access the corresponding element of the inverse transition - // relation and look if there exists a tuple (result_node, precondition), - // where precondition == {0, 1}. If so, we add 1 to the result_node. The result: - // - // 0 -> {('a', {(result_node:{0, 1}, precondition:{0, 1})})} - // 1 -> {('a', {}), - // ('b', {(result_node:{0}, precondition:{1})})} - bool found = false; - - State storeTo = *(node.begin()); - - auto inverseTransResults = perform_inverse_trans(storeTo, trans.symb); - for(auto & result : inverseTransResults) - { - if(result.precondition == node) - { - result.result_node.insert(trans.src); - found = true; - break; - } - } - - if(found) - { - continue; - } - - // Otherwise, we need to create a new tuple (result_node, precondition) - // == ({src state}, node) and store it to the vector given by the minimal - // state of the current node and the current symbol - - // If there is no tuple (symbol, vector_of_pointers) in context of the current - // state and symbol because the symbol has not been used yet, we need to create it - if(perform_inverse_trans(storeTo, trans.symb).empty()) { - inverseTransRelation[storeTo].emplace_back(trans.src, trans.symb, InverseResults(trans.src, node)); - continue; - } - - // Otherwise, we need to find the appropriate tuple (symbol, inverse_results) - // and store the inverse result to the vector of inverse results - for(auto & transVec : inverseTransRelation[storeTo]) - { - if(transVec.symb == trans.symb) - { - transVec.inverseResults.emplace_back(trans.src, node); - break; - } - } - } - -} // add_inverse_trans }}} - - -/** This function adds new state to the automaton. -* @brief adds new state -* @return id of the created state -*/ -State Afa::add_new_state() { - transitionrelation.emplace_back(); - inverseTransRelation.emplace_back(); - return transitionrelation.size() - 1; -} - -//*************************************************** -// -// POST -// -// Inspection of the automaton in the forward fashion -// -//*************************************************** - -/** This function takes a single state and a symbol and returns all the nodes -* which are accessible from the node {state} in one step using the given symbol. -* The output will be represented as a ClosedSet to omit the neccessity -* to explicitly return all the proper nodes. The result is always an upward closed set! -* @param state a source state -* @param symb a symbol used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const State state, const Symbol symb) const { - return { ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1, get_trans_from_state(state, symb).dst }; -} - -/** This function takes a single node and a symbol and returns all the nodes -* which are accessible from the node in one step using the given symbol. -* The output will be represented as a ClosedSet to omit the neccessity -* to explicitly return all the proper nodes. We will perform a transition -* for each state of the given node and then, we perform an intersection -* over these subresults. The result is always an upward closed set! -* @param node a source set of states -* @param symb a symbol used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const Node& node, const Symbol symb) const -{ - // initially, the result is empty - StateClosedSet result = StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1); - if(node.empty()) - { - result.insert(node); - return result; - } - - // we get the first result without any changes and then, we will - // perform several intersections over it - bool used = false; - for(auto state : node) - { - if(!used) - { - result.insert(post(state, symb).antichain()); - used = true; - continue; - } - result = result.intersection(post(state, symb)); - } - return result; -} // post }}} - -/** This function takes a whole set of nodes and a symbol and returns all the nodes -* which are accessible from the given nodes in one step using the given symbol. -* The output will be represented as a ClosedSet to omit the neccessity -* to explicitly return all the proper nodes. We will perform a transition for each node -* of the given set of nodes and then, we perform an union over these subresults. -* The result is always an upward closed set! -* @param nodes a source set of sets of states -* @param symb a symbol used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const Nodes& nodes, const Symbol symb) const -{ - // initially, the result is empty - StateClosedSet result = StateClosedSet{ ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1 }; - for(const auto& node : nodes) - { - result.insert(post(node, symb).antichain()); - } - return result; -} // post }}} - -/** This function allows us to perform post directly over the closed set. -* The output will be represented as a ClosedSet to omit the neccessity to -* explicitly return all the proper nodes. We will perform a transition for -* each node of the antichain of the given set of nodes and then we perform -* an union over these subresults. The result is always an upward closed set! -* @param closed_set an upward closed set which will be used to perform a transition -* @param symb a symbol used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const StateClosedSet& closed_set, const Symbol symb) const -{ - assert(closed_set.type() == mata::ClosedSetType::upward_closed_set && "The predicate transformer " && - " post can be computed only over upward-closed sets."); - return post(closed_set.antichain(), symb); -} // post }}} - - -/** This function takes a single node and and returns all the nodes which are -* accessible from the node in one step using any symbol. The output will be -* represented as a ClosedSet to omit the neccessity to explicitly return all -* the proper nodes. We will perform a transition for each state of the given -* node and then, we perform an intersection over these subresults. -* The result is always an upward closed set! -* @param node a source set of states -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const Node& node) const -{ - if(node.empty()) - { - return StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1, Nodes{Node{}}); - } - StateClosedSet result = StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1); - - // It is sufficient to access the first element of the node - // to collect all required symbols of the alphabet. If there is another symbol used - // in context of another state of the node, it won't affect the result. The result for - // such symbol will be empty since it is not used in context of all states - // stored in the node - for(const auto& transVec : transitionrelation[*(node.begin())]) - { - result.insert(post(node, transVec.symb).antichain()); - } - return result; -} // post }}} - -/** This function allows us to perfom "post" and use the whole alphabet -* to perform individual transitions. The output will be represented as -* a ClosedSet to omit the neccessity to explicitly return all the proper nodes. -* We will perform a transition for each node of the antichain of the given set -* of nodes and then we perform an union over these subresults. -* The result is always an upward closed set! -* @param nodes a set of sets of nodes used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const Nodes& nodes) const -{ - StateClosedSet result(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1); - for(const auto& node : nodes) - { - result.insert(post(node).antichain()); - } - return result; -} // post }}} - - -/** This function allows us to perfom "post" and use the whole alphabet -* to perform individual transitions directly over the closed set. -* The output will be represented as a ClosedSet to omit the neccessity to -* explicitly return all the proper nodes. We will perform a transition -* for each node of the antichain of the given set -* of nodes and then we perform an union over these subresults. -* The result is always an upward closed set! -* @param nodes a set of sets of nodes used to perform a transition -* @return closed set of nodes -*/ -StateClosedSet Afa::post(const StateClosedSet& closed_set) const -{ - assert(closed_set.type() == mata::ClosedSetType::upward_closed_set && "The predicate transformer " && - " post can be computed only over upward-closed sets."); - return post(closed_set.antichain()); -}; - -// The end of the definitions of the "post" functions - -//*************************************************** -// -// PRE -// -// Inspection of the automaton in the backward fashion -// -//*************************************************** - -/** This function inspects an inverse transition relation and returns a vector -* of inverse results according to the given source state and symbol. -* Otherwise, it gives us an empty vector which means that the result does not exist. -* @brief performs an inverse transition using a single state and symbol -* @param src a source state -* @param symb a symbol used to perform an inverse transition -* @return a vector of the inverse results -*/ -std::vector Afa::perform_inverse_trans(const State src, const Symbol symb) const -{ - for(const auto& element : this->inverseTransRelation[src]) - { - if(element.symb == symb) - { - return element.inverseResults; - } - } - return {}; -} // perform_inverse_trans }}} - -/** This function inspects an inverse transition relation and returns a vector -* of inverse results according to the given source states and symbol. -* Otherwise, it gives us an empty vector which means that the result does not exist. -* @brief performs an inverse transition using a single state and symbol -* @param node source states -* @param symb a symbol used to perform an inverse transition -* @return a vector of the inverse results -*/ -std::vector Afa::perform_inverse_trans(const Node& node, Symbol symb) const -{ - std::vector result{}; - for(auto state : node) - { - auto subresult = perform_inverse_trans(state, symb); - result.insert(result.end(), subresult.begin(), subresult.end()); - } - return result; -} // perform_inverse_trans }}} - -/** This function takes a single node and a symbol and returns all the nodes -* which are able to access the given node in one step using the given symbol. -* The output will be represented as ClosedSet to omit the neccessity -* to explicitly return all the proper nodes. -* The result is always a downward closed set! -* @param node source nodes -* @param symb a symbol used to perform an inverse transition -* @return closed set of nodes -*/ -StateClosedSet Afa::pre(const Node& node, Symbol symb) const -{ - std::vector candidates = perform_inverse_trans(node, symb); - Node result{}; - for(const auto& candidate : candidates) - { - if(candidate.precondition.IsSubsetOf(node)) - { - for(auto el : candidate.result_node) - { - result.insert(el); - } - } - } - return { ClosedSetType::downward_closed_set, 0, transitionrelation.size()-1, result }; -} // pre }}} - -/** This function takes a set of nodes and a symbol and returns all the nodes -* which are able to access the given nodes in one step using the given symbol. -* The output will be represented as ClosedSet to omit the neccessity -* to explicitly return all the proper nodes. The result is always a downward closed set! -* @param nodes source nodes -* @param symb a symbol used to perform an inverse transition -* @return closed set of nodes -*/ -StateClosedSet Afa::pre(const Nodes& nodes, Symbol symb) const -{ - StateClosedSet result(ClosedSetType::downward_closed_set, 0, transitionrelation.size()-1); - for(const auto& node : nodes) - { - result = result.Union(pre(node, symb)); - } - return result; -} // pre }}} - -/** This function performs 'pre' directly over the given closed set -* and the given symbol. The result is always a downward closed set! -* @param closed_set a closed set -* @param symb a symbol used to perform an inverse transition -* @return closed set of nodes -*/ -StateClosedSet Afa::pre(const StateClosedSet& closed_set, const Symbol symb) const -{ - assert(closed_set.type() == ClosedSetType::downward_closed_set && "The predicate transformer " && - "pre can be computed only over downward-closed sets."); - return pre(closed_set.antichain(), symb); -} // pre }}} - -/** This function allows us to perfom pre over a node and use the whole -* alphabet to perform individual transitions. The result is always -* a downward closed set! -* @param node a set of states -* @return closed set of nodes -*/ -StateClosedSet Afa::pre(const Node& node) const -{ - if(node.empty()) - { - return StateClosedSet(ClosedSetType::downward_closed_set, 0, transitionrelation.size()-1, Nodes{Node{}}); - } - StateClosedSet result(ClosedSetType::downward_closed_set, 0, transitionrelation.size()-1); - - // It is sufficient to access the first element of the node - // to collect all required symbols of the alphabet. If there is another symbol used - // in context of another state of the node, it won't affect the result. The result for - // such symbol will be empty since it is not used in context of all states - // stored in the node - for(const auto& transVec : inverseTransRelation[*(node.begin())]) - { - result.insert(pre(node, transVec.symb).antichain()); - } - return result; -} // pre }}} - -/** This function allows us to perfom pre over a set of nodes and use -* the whole alphabet to perform individual transitions -* The result is always a downward closed set! -* @param nodes a set of sets of states -* @return closed set of nodes -*/ -StateClosedSet Afa::pre(const Nodes& nodes) const { - StateClosedSet result{ ClosedSetType::downward_closed_set, 0, transitionrelation.size() - 1 }; - for(const auto& node : nodes) { result.insert(pre(node).antichain()); } - return result; -} // pre }}} - -// The end of the definitions of the "pre" functions -//////////////////////////////////////////////////// - -bool Afa::has_trans(const Trans& trans) const -{ // {{{ - Nodes res = get_trans_from_state(trans.src, trans.symb).dst; - if(!res.empty() && res.IsSubsetOf(trans.dst)) - { - return true; - } - return false; -} // has_trans }}} - - -size_t Afa::trans_size() const -{ // {{{ - size_t result = 0; - for(const auto& state : transitionrelation) - { - result += state.size(); - } - return result; -} // trans_size() }}} - -StateClosedSet Afa::get_non_final_nodes() const { - StateClosedSet result(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1); - auto transSize = transitionrelation.size(); - for(State state = 0; state < transSize; ++state) - { - if(!has_final(state)) - { - result.insert(state); - } - } - return result; -} - -StateClosedSet Afa::get_initial_nodes() const { - StateClosedSet result = StateClosedSet(ClosedSetType::upward_closed_set, 0, transitionrelation.size()-1); - for(const auto& node : initialstates) - { - result.insert(node); - } - return result; -} - - -std::ostream& mata::afa::operator<<(std::ostream& os, const Afa& afa) -{ // {{{ - return os << std::to_string(serialize(afa)); -} // Nfa::operator<<(ostream) }}} - - -bool mata::afa::are_state_disjoint(const Afa& lhs, const Afa& rhs) -{ // {{{ - assert(&lhs); - assert(&rhs); - - // TODO - assert(false); - return {}; -} // are_disjoint }}} - - -void mata::afa::union_norename( - Afa* result, - const Afa& lhs, - const Afa& rhs) -{ // {{{ - assert(nullptr != result); - - assert(&lhs); - assert(&rhs); - - // TODO - assert(false); -} // union_norename }}} - - -Afa mata::afa::union_rename( - const Afa& lhs, - const Afa& rhs) -{ // {{{ - assert(&lhs); - assert(&rhs); - - // TODO - assert(false); - return {}; -} // union_rename }}} - - -bool mata::afa::is_lang_empty(const Afa& aut, Path* cex) -{ // {{{ - assert(&aut); - assert(&cex); - - // TODO - assert(false); - return {}; -} // is_lang_empty }}} - - -bool mata::afa::is_lang_empty_cex(const Afa& aut, Word* cex) -{ // {{{ - assert(nullptr != cex); - - assert(&aut); - assert(&cex); - - // TODO - assert(false); - return {}; -} // is_lang_empty_cex }}} - -/** This function decides whether the given automaton is empty using -* an antichain-based emptiness test working in the concrete domain -* in the forward fashion -* @param aut a given automaton -* @return true iff the automaton is empty -*/ -bool mata::afa::antichain_concrete_forward_emptiness_test_old(const Afa& aut) -{ - // We will iteratively build a set of reachable nodes (next) until - // we reach a fixed point or until we find out that there exists - // a final node which is reachable (is not part of goal). - // We will perform each operation directly over antichains. - // Note that the fixed point always exists so the while loop always terminates. - StateClosedSet goal = aut.get_non_final_nodes(); - StateClosedSet current = StateClosedSet(ClosedSetType::upward_closed_set, 0, aut.get_num_of_states()-1); - StateClosedSet next = aut.get_initial_nodes(); - - while(current != next) - { - current = next; - next = current.Union(aut.post(current)); - if(!(next <= goal)) // inclusion test - { - return false; - } - } - return true; -} - -/** This function decides whether the given automaton is empty using -* an antichain-based emptiness test working in the concrete domain -* in the forward fashion -* @param aut a given automaton -* @return true iff the automaton is empty -*/ -bool mata::afa::antichain_concrete_forward_emptiness_test_new(const Afa& aut) -{ - StateClosedSet goal = aut.get_non_final_nodes(); - StateClosedSet result = aut.get_initial_nodes(); - std::set processed = std::set(); - std::vector worklist = std::vector(); - for(const Node& node : aut.get_initial_nodes().antichain()) - { - worklist.push_back(node); - } - - if(!(result <= goal)) - { - return false; - } - - while(!worklist.empty()) - { - Node current = worklist.back(); - worklist.pop_back(); - auto post_current = aut.post(current); - result = result.Union(post_current); - for(const Node& node : post_current.antichain()) - { - if(!goal.contains(node)) - { - return false; - } - if(!processed.count(node)) - { - worklist.push_back(node); - } - } - processed.insert(current); - } - return true; -} - -/** This function decides whether the given automaton is empty using -* an antichain-based emptiness test working in the concrete domain -* in the backward fashion -* @param aut a given automaton -* @return true iff the automaton is empty -*/ -bool mata::afa::antichain_concrete_backward_emptiness_test_old(const Afa& aut) -{ - // We will iteratively build a set of terminating nodes (next) - // until we reach a fixed point or until we find out that there exists - // an initial node which is terminating (is not part of goal). - // We will perform each operation directly over antichains - // Note that the fixed point always exists so the while loop always terminates - StateClosedSet goal = aut.get_non_initial_nodes(); - StateClosedSet current = StateClosedSet(ClosedSetType::downward_closed_set, 0, aut.get_num_of_states()-1); - StateClosedSet next = aut.get_final_nodes(); - - while(current != next) - { - current = next; - next = current.Union(aut.pre(current)); - if(!(next <= goal)) - { - return false; - } - } - return true; -} - - -/** This function decides whether the given automaton is empty using -* an antichain-based emptiness test working in the concrete domain -* in the backward fashion -* @param aut a given automaton -* @return true iff the automaton is empty -*/ -bool mata::afa::antichain_concrete_backward_emptiness_test_new(const Afa& aut) -{ - StateClosedSet goal = aut.get_non_initial_nodes(); - StateClosedSet result = aut.get_final_nodes(); - std::set processed = std::set(); - std::vector worklist = std::vector(); - for(const Node& node : aut.get_final_nodes().antichain()) - { - worklist.push_back(node); - } - - if(!(result <= goal)) - { - return false; - } - - while(!worklist.empty()) - { - Node current = worklist.back(); - worklist.pop_back(); - auto pre_current = aut.pre(current); - result = result.Union(pre_current); - for(const Node& node : pre_current.antichain()) - { - if(!goal.contains(node)) - { - return false; - } - if(!processed.count(node)) - { - worklist.push_back(node); - } - } - processed.insert(current); - } - return true; -} - - -void mata::afa::make_complete( - Afa* aut, - const Alphabet& alphabet, - State sink_state) -{ // {{{ - assert(nullptr != aut); - - assert(&alphabet); - assert(&sink_state); - - // TODO - assert(false); -} // make_complete }}} - - -mata::parser::ParsedSection mata::afa::serialize( - const Afa& aut, - const SymbolToStringMap* symbol_map, - const StateNameMap* state_map) -{ // {{{ - mata::parser::ParsedSection parsec; - parsec.type = mata::afa::TYPE_AFA; - - using bool_str_pair = std::pair; - - std::function state_namer = nullptr; - if (nullptr == state_map) - { - state_namer = [](State st) -> auto { - return bool_str_pair(true, "q" + std::to_string(st)); - }; - } - else - { - state_namer = [&state_map](State st) -> auto { - auto it = state_map->find(st); - if (it != state_map->end()) { return bool_str_pair(true, it->second); } - else { return bool_str_pair(false, ""); } - }; - } - - std::function symbol_namer = nullptr; - if (nullptr == symbol_map) { - symbol_namer = [](Symbol sym) -> auto { - return bool_str_pair(true, "a" + std::to_string(sym)); - }; - } else { - symbol_namer = [&symbol_map](Symbol sym) -> auto { - auto it = symbol_map->find(sym); - if (it != symbol_map->end()) { return bool_str_pair(true, it->second); } - else { return bool_str_pair(false, ""); } - }; - } - - // construct initial states - std::vector init_states; - for (const Node& node : aut.initialstates) { - std::string init_res = "( "; - bool first = true; - for (State s : node) { - bool_str_pair bsp = state_namer(s); - if (!bsp.first) { throw std::runtime_error("cannot translate state " + std::to_string(s)); } - if(!first) {init_res += " & ";} - init_res += bsp.second; - first = false; - } - init_res += " )"; - init_states.push_back(init_res); - } - parsec.dict["Initial"] = init_states; - - // construct final states - std::vector fin_states; - for (State s : aut.finalstates) { - bool_str_pair bsp = state_namer(s); - if (!bsp.first) { throw std::runtime_error("cannot translate state " + std::to_string(s)); } - fin_states.push_back(bsp.second); - } - parsec.dict["Final"] = fin_states; - - // TODO: transitions serialization - - return parsec; -} // serialize }}} - - -void mata::afa::revert(Afa* result, const Afa& aut) -{ // {{{ - assert(nullptr != result); - - assert(&aut); - - // TODO - assert(false); -} // revert }}} - - -void mata::afa::remove_epsilon(Afa* result, const Afa& aut, Symbol epsilon) -{ // {{{ - assert(nullptr != result); - - assert(&aut); - assert(&epsilon); - - // TODO - assert(false); -} // remove_epsilon }}} - - -void mata::afa::minimize( - Afa* result, - const Afa& aut, - const StringDict& params) -{ // {{{ - assert(nullptr != result); - - assert(&aut); - assert(¶ms); - - // TODO - assert(false); -} // minimize }}} - -// TODO this function should the same thing as the one taking IntermediateAut or be deleted -Afa mata::afa::construct( - const mata::parser::ParsedSection& parsec, - Alphabet* alphabet, - NameStateMap* state_map) -{ // {{{ - assert(nullptr != alphabet); - Afa aut; - - if (parsec.type != mata::afa::TYPE_AFA) { - throw std::runtime_error(std::string(__FUNCTION__) + ": expecting type \"" + - mata::afa::TYPE_AFA + "\""); - } - - bool remove_state_map = false; - if (nullptr == state_map) { - state_map = new NameStateMap(); - remove_state_map = true; - } - - State cnt_state = 0; - - // a lambda for translating state names to identifiers - auto get_state_name = [state_map, &cnt_state](const std::string& str) { - auto it_insert_pair = state_map->insert({str, cnt_state}); - if (it_insert_pair.second) { return cnt_state++; } - else { return it_insert_pair.first->second; } - }; - - // a lambda for cleanup - auto clean_up = [&]() { - if (remove_state_map) { delete state_map; } - }; - - - auto it = parsec.dict.find("Initial"); - if (parsec.dict.end() != it) { - for (const auto& str : it->second) { - State state = get_state_name(str); - aut.initialstates.insert(Node{state}); - } - } - - - it = parsec.dict.find("Final"); - if (parsec.dict.end() != it) { - for (const auto& str : it->second) { - State state = get_state_name(str); - aut.finalstates.insert(state); - } - } - - for (const auto& body_line : parsec.body) { - if (body_line.size() < 2) { - clean_up(); - - throw std::runtime_error("Invalid transition: " + std::to_string(body_line)); - } - - std::string formula; - for (size_t i = 1; i < body_line.size(); ++i) { - formula += body_line[i] + " "; - } - - // TODO: Transform a positive Boolean formula from the string format - // to the inner representation (src state, symbol on transition, ordered - // vector of ordered vectors of states which corresponds to the formula in DNF) - // Call the "add_trans" and "add_inverse_trans" functions over the - // parsed formula to add it do the automaton - - } - - // do the dishes and take out garbage - clean_up(); - - return aut; -} // construct }}} - -Afa mata::afa::construct( - const mata::IntermediateAut& inter_aut, - Alphabet* alphabet, - NameStateMap* state_map) -{ // {{{ - Afa aut; - assert(nullptr != alphabet); - - if (!inter_aut.is_afa()) { - throw std::runtime_error(std::string(__FUNCTION__) + ": expecting type \"" + - mata::afa::TYPE_AFA + "\""); - } - - NameStateMap tmp_state_map; - if (nullptr == state_map) { - state_map = &tmp_state_map; - } - - // a lambda for translating state names to identifiers - auto get_state_name = [&state_map, &aut](const std::string& str) { - if (!state_map->count(str)) { - State state = aut.add_new_state(); - state_map->insert({str, state}); - return state; - } else { - return (*state_map)[str]; - } - }; - - // lambda returning true if node is operator of given type - auto is_node_operator = - [](const FormulaNode& node, FormulaNode::OperatorType type) -> bool { - return node.is_operator() && node.operator_type == type; - }; - - // lambda creates Node from set of strings which are state names - auto create_node = [get_state_name]( - const std::unordered_set& states_names) -> Node { - Node tgt_node; - for (const std::string& s : states_names) - { - tgt_node.insert(get_state_name(s)); - } - - return tgt_node; - }; - - - const FormulaGraph* init_graph = &inter_aut.initial_formula; - if (is_node_operator(init_graph->node, FormulaNode::OperatorType::AND)) { // initial formula is just conjunction - Node initial_node; - for (const auto& str : init_graph->collect_node_names()) - { - State state = get_state_name(str); - initial_node.insert(state); - } - aut.add_initial(initial_node); - } else { // initial formula is dnf - while (is_node_operator(init_graph->node, FormulaNode::OperatorType::OR)) - { // Processes each clause separately - assert(init_graph->children[1].node.is_operand() || - is_node_operator(init_graph->children[1].node, FormulaNode::OperatorType::AND) || - "Clause should be conjunction or single state"); - // Conjunction is the right son of initent node - Node initial_node; - for (const auto& s : init_graph->children[1].collect_node_names()) - initial_node.insert(get_state_name(s)); - aut.add_initial(initial_node); - - // jump to another clause which is the left son of initent node - init_graph = &init_graph->children.front(); - } - assert(init_graph->node.is_operand() || - is_node_operator(init_graph->node, FormulaNode::OperatorType::AND) || - "Remaining clause should be conjunction or single element"); - Node initial_node; - for (const auto& s : init_graph->collect_node_names()) - initial_node.insert(get_state_name(s)); - aut.add_initial(initial_node); - } - - for (const auto& trans : inter_aut.transitions) - { - State src_state = get_state_name(trans.first.name); - if (trans.second.node.is_operand() && trans.second.node.operand_type == FormulaNode::OperandType::SYMBOL) - { - Symbol symbol = alphabet->translate_symb(trans.second.node.name); - aut.add_trans(src_state, symbol, Node()); - continue; - } - else if (trans.second.children.size() != 2) - { - if (trans.second.children.size() == 1) - { - throw std::runtime_error("Epsilon transitions not supported"); - } - else - { - throw std::runtime_error("Invalid transition"); - } - } - - assert(is_node_operator(trans.second.node, FormulaNode::OperatorType::AND) || - "Clause of DNF should be conjunction"); - assert(trans.second.children.front().node.is_operand() || "Node in conjunction should be operand"); - Symbol symbol = alphabet->translate_symb(trans.second.children.front().node.name); - - const FormulaGraph* curr_graph = &trans.second.children[1]; - - while (is_node_operator(curr_graph->node, FormulaNode::OperatorType::OR)) - { // Processes each clause separately - assert(curr_graph->children[1].node.is_operand() || - is_node_operator(curr_graph->children[1].node, FormulaNode::OperatorType::AND) || - "Clause should be conjunction"); - // Conjunction is the right son of current node - aut.add_trans(src_state, symbol, - create_node(curr_graph->children[1].collect_node_names())); - - // jump to another clause which is the left son of current node - curr_graph = &curr_graph->children.front(); - } - - // process remaining conjunction - assert(curr_graph->node.is_operand() || - is_node_operator(curr_graph->node, FormulaNode::OperatorType::AND) || - "Remaining clause should be conjunction"); - aut.add_trans(src_state, symbol, - create_node(curr_graph->collect_node_names())); - } - - // TODO final states can be also given as true/false - if (inter_aut.are_final_states_conjunction_of_negation()) { - // final states are given as a conjunction of non-final states - auto non_final_states = inter_aut.final_formula.collect_node_names(); - for (const auto &state_name_and_number : *state_map) { - if (!non_final_states.count(state_name_and_number.first)) { - aut.finalstates.insert(state_name_and_number.second); - } - } - } else { - // final states are given normally - for (const auto& str : inter_aut.final_formula.collect_node_names()) - { - State state = get_state_name(str); - aut.finalstates.insert(state); - } - } - return aut; -} // construct }}} - -bool mata::afa::is_in_lang(const Afa& aut, const Word& word) -{ // {{{ - assert(&aut); - assert(&word); - - // TODO - assert(false); -} // is_in_lang }}} - - -bool mata::afa::is_prfx_in_lang(const Afa& aut, const Word& word) -{ // {{{ - assert(&aut); - assert(&word); - - // TODO - assert(false); -} // is_prfx_in_lang }}} - - -bool mata::afa::is_deterministic(const Afa& aut) -{ // {{{ - assert(&aut); - - // TODO - assert(false); -} // is_deterministic }}} - - -bool mata::afa::is_complete(const Afa& aut, const Alphabet& alphabet) -{ // {{{ - assert(&aut); - assert(&alphabet); - - // TODO - assert(false); - return {}; -} // is_complete }}} - -bool mata::afa::accepts_epsilon(const Afa& aut) { - return std::any_of(aut.initialstates.cbegin(), aut.initialstates.cend(), - [&aut](const Node& node) { return node.IsSubsetOf(aut.finalstates); }); -} - -Word encode_word(const mata::Alphabet& alphabet, const std::vector &input) { - return alphabet.translate_word(input); -} - -std::ostream& std::operator<<(std::ostream& os, const mata::afa::AfaWrapper& afa_wrap) -{ // {{{ - os << "{AFA wrapper|AFA: " << afa_wrap.afa << "|alphabet: " << afa_wrap.alphabet << - "|state_dict: " << std::to_string(afa_wrap.state_dict) << "}"; - return os; -} // operator<<(AfaWrapper) }}} - -namespace std { - inline size_t hash::operator()(const mata::afa::Trans& trans) const { - size_t accum = std::hash{}(trans.src); - accum = mata::utils::hash_combine(accum, trans.symb); - accum = mata::utils::hash_combine(accum, trans.dst); - return accum; - } -} - -#pragma GCC diagnostic pop diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index f6b820374..c7a0a17e6 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -7,7 +7,6 @@ add_executable(tests parser.cc re2parser.cc mintermization.cc - afa/afa.cc nfa/delta.cc nfa/nfa.cc nfa/builder.cc diff --git a/tests/afa/afa.cc b/tests/afa/afa.cc deleted file mode 100644 index 4af153e19..000000000 --- a/tests/afa/afa.cc +++ /dev/null @@ -1,741 +0,0 @@ -// TODO: some header - -#include - -#include - -#include "mata/afa/afa.hh" - -using namespace mata::afa; -using namespace mata::utils; -using namespace mata::parser; - -TEST_CASE("mata::afa::Trans::operator<<") -{ // {{{ - Trans trans(1, 0, {{0, 1}, {0, 2}}); - - REQUIRE(std::to_string(trans) == "(1, 0, { { 0, 1}, { 0, 2}})"); -} // }}} - -TEST_CASE("mata::afa::ClosedSet creating closed sets") -{ // {{{ - StateClosedSet c1 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 2, Nodes()); - StateClosedSet c2 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 10, 20, Nodes()); - - REQUIRE(c1.type() == mata::ClosedSetType::upward_closed_set); - REQUIRE(c2.type() == mata::ClosedSetType::downward_closed_set); - REQUIRE(c1.type() != c2.type()); - REQUIRE(c1.antichain().size() == 0); - REQUIRE(c2.antichain().size() == 0); - -} // }}} - -TEST_CASE("mata::afa::ClosedSet operation over closed sets") -{ // {{{ - StateClosedSet c1 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes()); - StateClosedSet c2 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes()); - - REQUIRE(!c1.contains(Node{0})); - REQUIRE(!c2.contains(Node{0})); - - c1.insert(Node{0, 1}); - c2.insert(Node{0, 1}); - - REQUIRE(!c1.contains(Node{0})); - REQUIRE(c2.contains(Node{0})); - - c1.insert(Node{0, 2}); - c2.insert(Node{0, 2}); - - REQUIRE(c1.contains(Node{0, 1, 2})); - REQUIRE(!c2.contains(Node{0, 1, 2})); - REQUIRE(!c1.contains(Node{})); - REQUIRE(c2.contains(Node{})); - - StateClosedSet c3 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes{ Node{ 0, 1}}); - StateClosedSet c4 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes{ Node{ 0, 3}}); - - REQUIRE(c3.Union(c4).contains(Node{0, 1})); - REQUIRE(c3.Union(c4).contains(Node{0, 3})); - REQUIRE(!c3.intersection(c4).contains(Node{0, 1})); - REQUIRE(!c3.intersection(c4).contains(Node{0, 3})); - - REQUIRE(c3.Union(c4).contains(Node{0, 1, 3})); - REQUIRE(c3.intersection(c4).contains(Node{0, 1, 3})); - REQUIRE(!c3.Union(c4).contains(Node{})); - REQUIRE(!c3.intersection(c4).contains(Node{})); - - StateClosedSet c5 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes{ Node{ 0, 1}}); - StateClosedSet c6 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes{ Node{ 0, 3}}); - - REQUIRE(c5.Union(c6).contains(Node{0, 1})); - REQUIRE(c5.Union(c6).contains(Node{0, 3})); - REQUIRE(!c5.intersection(c6).contains(Node{0, 1})); - REQUIRE(!c5.intersection(c6).contains(Node{0, 3})); - - REQUIRE(!c5.Union(c6).contains(Node{0, 1, 3})); - REQUIRE(!c5.intersection(c6).contains(Node{0, 1, 3})); - REQUIRE(c5.Union(c6).contains(Node{})); - REQUIRE(c5.intersection(c6).contains(Node{})); - - REQUIRE(std::to_string(c5.Union(c6).antichain()) == "{ { 0, 1}, { 0, 3}}"); - REQUIRE(std::to_string(c5.intersection(c6).antichain()) == "{ { 0}}"); - - StateClosedSet c7 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes{ Node{ 0, 3}}); - c7.insert(Node{0}); - REQUIRE(std::to_string(c7.antichain()) == "{ { 0, 3}}"); - c7.insert(Node{0, 2}); - REQUIRE(std::to_string(c7.antichain()) == "{ { 0, 2}, { 0, 3}}"); - c7.insert(Node{0, 2, 3}); - REQUIRE(std::to_string(c7.antichain()) == "{ { 0, 2, 3}}"); - - StateClosedSet c8 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes{ Node{ 0, 3}}); - c8.insert(Node{0, 1, 3}); - REQUIRE(std::to_string(c8.antichain()) == "{ { 0, 3}}"); - c8.insert(Node{0, 2}); - REQUIRE(std::to_string(c8.antichain()) == "{ { 0, 2}, { 0, 3}}"); - c8.insert(Node{0}); - REQUIRE(std::to_string(c8.antichain()) == "{ { 0}}"); - - StateClosedSet c9 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 4, Nodes()); - - c9.insert(Node{1, 4}); - c9.insert(Node{1, 2, 3}); - - REQUIRE(c9.complement().antichain() == Nodes{{0, 1, 2}, {0, 1, 3}, {0, 2, 3, 4}}); - REQUIRE(!(c9.complement().antichain() == Nodes{{0, 2}, {0, 1, 3}, {0, 2, 3, 4}})); - - REQUIRE(c9.complement().complement().antichain() == Nodes{{1, 4}, {1, 2, 3}}); - REQUIRE(!(c9.complement().complement().antichain() == Nodes{{0, 1, 4}, {1, 2, 3}})); - - StateClosedSet c10 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes()); - - c10.insert(Node{1, 2}); - c10.insert(Node{2, 3}); - - REQUIRE(c10.complement().antichain() == Nodes{{0}, {1, 3}}); - - REQUIRE(c10.type() == mata::ClosedSetType::downward_closed_set); - c10 = c10.complement(); - REQUIRE(c10.type() == mata::ClosedSetType::upward_closed_set); - - StateClosedSet c11 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes()); - REQUIRE(c11.complement().antichain() == Nodes{{}}); - - StateClosedSet c12 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes()); - REQUIRE(c12.complement().antichain() == Nodes{{0, 1, 2, 3}}); - - StateClosedSet c13 = StateClosedSet(mata::ClosedSetType::downward_closed_set, 0, 3, Nodes()); - c13.insert(Node{0, 1, 2, 3}); - REQUIRE(c13.complement().antichain() == Nodes{}); - - StateClosedSet c14 = StateClosedSet(mata::ClosedSetType::upward_closed_set, 0, 3, Nodes()); - c14.insert(Node{0, 1, 2, 3}); - REQUIRE(c14.complement().antichain() == Nodes{{0, 1, 2}, {0, 1, 3}, {0, 2, 3}, {1, 2, 3}}); - -} // }}} - - -TEST_CASE("mata::afa creating an AFA, basic properties") -{ // {{{ - - Afa aut(4); - - aut.initialstates = {{0}}; - aut.finalstates = {3}; - aut.add_trans(0, 0, Node{1, 2}); - aut.add_trans(1, 0, Node{2}); - aut.add_trans(1, 1, Node{2, 3}); - aut.add_trans(2, 1, Node{3}); - aut.add_trans(3, 1, Node{3}); - aut.add_trans(3, 0, Node{0}); - - REQUIRE(aut.trans_size() == 6); - REQUIRE(aut.has_final(3)); - REQUIRE(!aut.has_final(2)); - REQUIRE(aut.has_initial(0)); - REQUIRE(!aut.has_initial(1)); - - - - REQUIRE(aut.get_num_of_states() == 4); - REQUIRE(aut.add_new_state() == 4); - REQUIRE(aut.add_new_state() == 5); - REQUIRE(aut.add_new_state() == 6); - REQUIRE(aut.add_new_state() == 7); - REQUIRE(aut.get_num_of_states() == 8); - - auto transitions1 = aut.get_trans_from_state(0); - auto transitions2 = aut.get_trans_from_state(1); - - REQUIRE(transitions1.size() == 1); - REQUIRE(transitions2.size() == 2); - - REQUIRE(transitions1[0].src == 0); - REQUIRE(transitions1[0].symb == 0); - REQUIRE(transitions1[0].dst == Nodes{Node{1, 2}}); - - REQUIRE(transitions2[0].src == 1); - REQUIRE(transitions2[0].symb == 0); - REQUIRE(transitions2[0].dst == Nodes{Node{2}}); - - REQUIRE(transitions2[1].src == 1); - REQUIRE(transitions2[1].symb == 1); - REQUIRE(transitions2[1].dst == Nodes{Node{2, 3}}); - - aut.add_trans(7, 0, Node{0}); - - REQUIRE(aut.trans_size() == 7); - - aut.add_trans(7, 0, Node{1}); - aut.add_trans(7, 0, Node{2, 3}); - - auto transitions3 = aut.get_trans_from_state(7); - - REQUIRE(transitions3.size() == 1); - REQUIRE(transitions3[0].src == 7); - REQUIRE(transitions3[0].symb == 0); - REQUIRE(transitions3[0].dst == Nodes{Node{0}, Node{1}, Node{2, 3}}); - -} // }}} - -TEST_CASE("mata::afa transition test") -{ // {{{ - - Afa aut(3); - - aut.initialstates = {{0}}; - aut.finalstates = {2}; - aut.add_trans(0, 0, Nodes{Node{0}}); - aut.add_trans(0, 1, Nodes{Node{1}}); - aut.add_trans(1, 1, Nodes{Node{0}, Node{1, 2}}); - aut.add_trans(2, 0, Nodes{Node{2}, Node{0, 1}}); - - REQUIRE(std::to_string(aut.post(Nodes{}).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{}}).antichain()) == "{ {}}"); - - REQUIRE(std::to_string(aut.post(0, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.post(Node{0}, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{0}}, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 0}}), 0).antichain()) == "{ { 0}}"); - - REQUIRE(std::to_string(aut.post(0, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.post(Node{0}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{0}}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 0}}), 1).antichain()) == "{ { 1}}"); - - REQUIRE(std::to_string(aut.post(1, 0).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{1}, 0).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{1}}, 0).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 1}}), 0).antichain()) == "{}"); - - REQUIRE(std::to_string(aut.post(1, 1).antichain()) == "{ { 0}, { 1, 2}}"); - REQUIRE(std::to_string(aut.post(Node{1}, 1).antichain()) == "{ { 0}, { 1, 2}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{1}}, 1).antichain()) == "{ { 0}, { 1, 2}}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 1}}), 1).antichain()) == "{ { 0}, { 1, 2}}"); - - REQUIRE(std::to_string(aut.post(2, 0).antichain()) == "{ { 0, 1}, { 2}}"); - REQUIRE(std::to_string(aut.post(Node{2}, 0).antichain()) == "{ { 0, 1}, { 2}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{2}}, 0).antichain()) == "{ { 0, 1}, { 2}}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 2}}), 0).antichain()) == "{ { 0, 1}, { 2}}"); - - REQUIRE(std::to_string(aut.post(2, 1).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{2}, 1).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{2}}, 1).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(StateClosedSet - (mata::ClosedSetType::upward_closed_set, 0, 2, Nodes{ Node{ 2}}), 1).antichain()) == "{}"); - - REQUIRE(std::to_string(aut.post(Node{0, 1}, 0).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{0, 2}, 0).antichain()) == "{ { 0, 1}, { 0, 2}}"); - REQUIRE(std::to_string(aut.post(Node{1, 2}, 0).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{0, 1, 2}, 0).antichain()) == "{}"); - - REQUIRE(std::to_string(aut.post(Node{0, 1}, 1).antichain()) == "{ { 0, 1}, { 1, 2}}"); - REQUIRE(std::to_string(aut.post(Node{0, 2}, 1).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{1, 2}, 1).antichain()) == "{}"); - REQUIRE(std::to_string(aut.post(Node{0, 1, 2}, 1).antichain()) == "{}"); - - REQUIRE(std::to_string(aut.post(Nodes{Node{0}, Node{1}}, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{0}, Node{1}}, 1).antichain()) == "{ { 0}, { 1}}"); - REQUIRE(std::to_string(aut.post(Nodes{Node{0}, Node{1}}).antichain()) == "{ { 0}, { 1}}"); - -} // }}} - -TEST_CASE("mata::afa inverse transition test") -{ // {{{ - - Afa aut(3); - - aut.initialstates = {{0}}; - aut.finalstates = {2}; - aut.add_inverse_trans(0, 0, Nodes{Node{0}}); - aut.add_inverse_trans(0, 1, Nodes{Node{1}}); - aut.add_inverse_trans(1, 1, Nodes{Node{0}, Node{1, 2}}); - aut.add_inverse_trans(2, 0, Nodes{Node{2}, Node{0, 1}}); - - REQUIRE(std::to_string(aut.pre(Node{}, 0).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(Node{}, 1).antichain()) == "{ {}}"); - - REQUIRE(std::to_string(aut.pre(0, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(Node{0}, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{0}}, 0).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 0}}), 0).antichain()) == "{ { 0}}"); - - REQUIRE(std::to_string(aut.pre(1, 0).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(Node{1}, 0).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{1}}, 0).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 1}}), 0).antichain()) == "{ {}}"); - - REQUIRE(std::to_string(aut.pre(2, 0).antichain()) == "{ { 2}}"); - REQUIRE(std::to_string(aut.pre(Node{2}, 0).antichain()) == "{ { 2}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{2}}, 0).antichain()) == "{ { 2}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 2}}), 0).antichain()) == "{ { 2}}"); - - - REQUIRE(std::to_string(aut.pre(0, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.pre(Node{0}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{0}}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 0}}), 1).antichain()) == "{ { 1}}"); - - REQUIRE(std::to_string(aut.pre(1, 1).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(Node{1}, 1).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{1}}, 1).antichain()) == "{ { 0}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 1}}), 1).antichain()) == "{ { 0}}"); - - REQUIRE(std::to_string(aut.pre(2, 1).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(Node{2}, 1).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{2}}, 1).antichain()) == "{ {}}"); - REQUIRE(std::to_string(aut.pre(StateClosedSet - (mata::ClosedSetType::downward_closed_set, 0, 2, Nodes{ Node{ 2}}), 1).antichain()) == "{ {}}"); - - - REQUIRE(std::to_string(aut.pre(Node{0, 1}, 0).antichain()) == "{ { 0, 2}}"); - REQUIRE(std::to_string(aut.pre(Node{0, 2}, 0).antichain()) == "{ { 0, 2}}"); - REQUIRE(std::to_string(aut.pre(Node{1, 2}, 0).antichain()) == "{ { 2}}"); - REQUIRE(std::to_string(aut.pre(Node{0, 1, 2}, 0).antichain()) == "{ { 0, 2}}"); - - REQUIRE(std::to_string(aut.pre(Node{0, 1}, 1).antichain()) == "{ { 0, 1}}"); - REQUIRE(std::to_string(aut.pre(Node{0, 2}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.pre(Node{1, 2}, 1).antichain()) == "{ { 0, 1}}"); - REQUIRE(std::to_string(aut.pre(Node{0, 1, 2}, 1).antichain()) == "{ { 0, 1}}"); - - REQUIRE(std::to_string(aut.pre(Nodes{Node{0}, Node{2}}, 0).antichain()) == "{ { 0}, { 2}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{0}, Node{2}}, 1).antichain()) == "{ { 1}}"); - REQUIRE(std::to_string(aut.pre(Nodes{Node{0}, Node{2}}).antichain()) == "{ { 0}, { 1}, { 2}}"); - -} // }}} - -TEST_CASE("mata::afa antichain emptiness test") -{ - ///////////////////////////////// - // Example of an automaton - ///////////////////////////////// - - Afa aut(3); - - aut.initialstates = {{0}}; - aut.finalstates = {2}; - - // TODO: Add transition and inverse transition simultaneously??? - // Do we always care about inverse transitions (in context of other - // operations than backward emptiness test etc.?) Is it better - // to add inverse transitions on demand or always? - - aut.add_trans(0, 0, Nodes{Node{0}}); - aut.add_trans(0, 1, Nodes{Node{1}}); - aut.add_trans(1, 1, Nodes{Node{0}, Node{1, 2}}); - aut.add_trans(2, 0, Nodes{Node{2}, Node{0, 1}}); - - aut.add_inverse_trans(0, 0, Nodes{Node{0}}); - aut.add_inverse_trans(0, 1, Nodes{Node{1}}); - aut.add_inverse_trans(1, 1, Nodes{Node{0}, Node{1, 2}}); - aut.add_inverse_trans(2, 0, Nodes{Node{2}, Node{0, 1}}); - - REQUIRE(antichain_concrete_forward_emptiness_test_old(aut)); - REQUIRE(antichain_concrete_backward_emptiness_test_old(aut)); - - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut)); - REQUIRE(antichain_concrete_backward_emptiness_test_new(aut)); - - aut.finalstates = {0}; - REQUIRE(!antichain_concrete_forward_emptiness_test_old(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_old(aut)); - - REQUIRE(!antichain_concrete_forward_emptiness_test_new(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_new(aut)); - - aut.finalstates = {1}; - - REQUIRE(!antichain_concrete_forward_emptiness_test_old(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_old(aut)); - - REQUIRE(!antichain_concrete_forward_emptiness_test_new(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_new(aut)); - - ///////////////////////////////// - // Example of an automaton - ///////////////////////////////// - - Afa aut1(10); - - aut1.initialstates = {{0}}; - aut1.finalstates = {9}; - - aut1.add_trans(0, 0, Nodes{Node{1}}); - aut1.add_trans(1, 0, Nodes{Node{2}}); - aut1.add_trans(2, 0, Nodes{Node{3}}); - aut1.add_trans(3, 0, Nodes{Node{4}}); - aut1.add_trans(4, 0, Nodes{Node{5}}); - aut1.add_trans(5, 0, Nodes{Node{6}}); - aut1.add_trans(6, 0, Nodes{Node{7}}); - aut1.add_trans(7, 0, Nodes{Node{8}}); - aut1.add_trans(8, 0, Nodes{Node{8, 9}}); - - aut1.add_inverse_trans(0, 0, Nodes{Node{1}}); - aut1.add_inverse_trans(1, 0, Nodes{Node{2}}); - aut1.add_inverse_trans(2, 0, Nodes{Node{3}}); - aut1.add_inverse_trans(3, 0, Nodes{Node{4}}); - aut1.add_inverse_trans(4, 0, Nodes{Node{5}}); - aut1.add_inverse_trans(5, 0, Nodes{Node{6}}); - aut1.add_inverse_trans(6, 0, Nodes{Node{7}}); - aut1.add_inverse_trans(7, 0, Nodes{Node{8}}); - aut1.add_inverse_trans(8, 0, Nodes{Node{8, 9}}); - - REQUIRE(antichain_concrete_forward_emptiness_test_old(aut1)); - REQUIRE(antichain_concrete_backward_emptiness_test_old(aut1)); - - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut1)); - REQUIRE(antichain_concrete_backward_emptiness_test_new(aut1)); - - aut1.add_trans(8, 0, Nodes{Node{9}}); - aut1.add_trans(8, 0, Nodes{Node{9}}); - - aut1.add_inverse_trans(8, 0, Nodes{Node{9}}); - aut1.add_inverse_trans(8, 0, Nodes{Node{9}}); - - REQUIRE(!antichain_concrete_forward_emptiness_test_old(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_old(aut)); - - REQUIRE(!antichain_concrete_forward_emptiness_test_new(aut)); - REQUIRE(!antichain_concrete_backward_emptiness_test_new(aut)); - - ///////////////////////////////// - // Automaton with no transitions - ///////////////////////////////// - - Afa aut2(3); - - REQUIRE(antichain_concrete_forward_emptiness_test_old(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_old(aut2)); - - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_new(aut2)); - - aut2.initialstates = {{0}}; - - REQUIRE(antichain_concrete_forward_emptiness_test_old(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_old(aut2)); - - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_new(aut2)); - - aut2.finalstates = {1}; - - REQUIRE(antichain_concrete_forward_emptiness_test_old(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_old(aut2)); - - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut2)); - REQUIRE(antichain_concrete_backward_emptiness_test_new(aut2)); - - aut2.finalstates = {0}; - - REQUIRE(!antichain_concrete_forward_emptiness_test_old(aut2)); - REQUIRE(!antichain_concrete_backward_emptiness_test_old(aut2)); - - REQUIRE(!antichain_concrete_forward_emptiness_test_new(aut2)); - REQUIRE(!antichain_concrete_backward_emptiness_test_new(aut2)); -} - -TEST_CASE("mata::afa::construct() from IntermediateAut correct calls") -{ // {{{ - Afa aut; - mata::IntermediateAut inter_aut; - mata::OnTheFlyAlphabet alphabet; - - SECTION("construct an empty automaton") - { - inter_aut.automaton_type = mata::IntermediateAut::AutomatonType::AFA; - aut = mata::afa::construct(inter_aut, &alphabet); - REQUIRE(true); - } - - SECTION("construct a simple non-empty automaton accepting the empty word from intermediate automaton") - { - std::string file = - "@AFA-explicit\n" - "%States-enum p q r\n" - "%Alphabet-auto\n" - "%Initial p | q\n" - "%Final p | q\n"; - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - aut = construct(inter_aut); - - REQUIRE(aut.initialstates.size() == 2); - REQUIRE(aut.finalstates.size() == 2); - } - - SECTION("construct an automaton with more than one initial/final states from intermediate automaton") { - std::string file = - "@AFA-explicit\n" - "%States-enum p q 3\n" - "%Alphabet-auto\n" - "%Initial p | q\n" - "%Final p & q & r\n"; - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - construct(&aut, inter_aut); - - REQUIRE(aut.initialstates.size() == 2); - REQUIRE(aut.finalstates.size() == 3); - } - - SECTION("construct an automaton with implicit operator completion one initial/final states from intermediate automaton") - { - std::string file = - "@AFA-explicit\n" - "%States-enum p q r\n" - "%Alphabet-auto\n" - "%Initial p q\n" - "%Final p q r\n"; - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - construct(&aut, inter_aut); - - REQUIRE(aut.initialstates.size() == 2); - REQUIRE(aut.finalstates.size() == 3); - } - - SECTION("construct an automaton with implicit operator completion one initial/final states from intermediate automaton") - { - std::string file = - "@AFA-explicit\n" - "%States-enum p q r m n\n" - "%Alphabet-auto\n" - "%Initial p q r\n" - "%Final p q m n\n"; - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - construct(&aut, inter_aut); - - REQUIRE(aut.initialstates.size() == 3); - REQUIRE(aut.finalstates.size() == 4); - } - - SECTION("construct a simple non-empty automaton accepting only the word 'a' from intermediate automaton") - { - std::string file = - "@AFA-explicit\n" - "%States-enum p q 3\n" - "%Alphabet-auto\n" - "%Initial q1\n" - "%Final q2\n" - "q1 a & q2\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - construct(&aut, inter_aut, &alphabet); - } - - SECTION("construct a more complicated non-empty automaton from intermediate automaton") - { - std::string file = - "@AFA-explicit\n" - "%States-enum p q 3\n" - "%Alphabet-auto\n" - "%Initial q1 | q3\n" - "%Final q5\n" - "q1 a & ((q2 & q3) | (q4 & q5))\n" - "q1 a & q1 & q3\n" - "q1 b & q3 & q4\n" - "q2 a & ((q3 & q4) | (q4 & q5) | (q3 & q6))\n" - "q3 a & ((q3 & q4) | (q4 & q5) | (q3 & q6 & q4) & q5)\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - NameStateMap state_map; - construct(&aut, inter_aut, &alphabet, &state_map); - - REQUIRE(aut.trans_size() == 4); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["a"]).dst.size() == 3); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["a"]).dst.begin()->count( - state_map["q1"])); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["a"]).dst.begin()->count( - state_map["q3"])); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["b"]).dst.size() == 1); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["b"]).dst.begin()->count( - state_map["q3"])); - REQUIRE(aut.get_trans_from_state(state_map["q1"], alphabet["b"]).dst.begin()->count( - state_map["q4"])); - REQUIRE(aut.get_trans_from_state(state_map["q2"], alphabet["a"]).dst.size() == 3); - REQUIRE(aut.get_trans_from_state(state_map["q3"], alphabet["a"]).dst.size() == 2); - } - - SECTION("Initial formula in DNF") - { - std::string file = - "@AFA-explicit\n" - "%Initial qQC0_0 | (qQC0_1 & qQC1_1 & qQC1_0) \n" - "%Final !qQC0_2 & !qQC0_1 & !qQC1_1 & !qQC1_0 & !qQC0_0\n" - "qQC0_1 a & (qQC0_1 | qQC0_2)\n" - "qQC1_1 a & qQC1_1\n" - "qQC0_2 a\n" - "qQC1_0 a & qQC1_1\n" - "qQC0_0 a & (qQC0_2 | qQC0_1)\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - NameStateMap state_map; - construct(&aut, inter_aut, &alphabet, &state_map); - - REQUIRE(aut.initialstates.size() == 2); - auto it = aut.initialstates.begin(); - REQUIRE(it->count(state_map["QC0_1"])); - REQUIRE(it->count(state_map["QC1_1"])); - REQUIRE(it->count(state_map["QC1_0"])); - ++it; - REQUIRE(it->count(state_map["QC0_0"])); - } - - SECTION("AFA with a simple initial formula, just disjunction") - { - std::string file = - "@AFA-explicit\n" - "%Initial q1 | q2\n" - "%Final !q0 & !q1 & !q2 & !q3\n" - "q0 a1\n" - "q1 a2 & (q2 & q3)\n" - "q2 a2 & (q0 & q3)\n" - "q3 a1 & (q0 | q2)\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - NameStateMap state_map; - construct(&aut, inter_aut, &alphabet, &state_map); - - // Two initial nodes {q1} and {q2} - REQUIRE(aut.initialstates.size() == 2); - REQUIRE(!antichain_concrete_forward_emptiness_test_new(aut)); - } - - SECTION("AFA with a simple initial formula, just conjunction") - { - std::string file = - "@AFA-explicit\n" - "%Initial q1 & q2\n" - "%Final !q0 & !q1 & !q2 & !q3\n" - "q0 a1\n" - "q1 a2 & (q2 & q3)\n" - "q2 a2 & (q0 & q3)\n" - "q3 a1 & (q0 | q2)\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - NameStateMap state_map; - construct(&aut, inter_aut, &alphabet, &state_map); - - // One initial node {q1, q2} - REQUIRE(aut.initialstates.size() == 1); - REQUIRE(antichain_concrete_forward_emptiness_test_new(aut)); - } - - SECTION("AFA final states from multiple negations") - { - std::string file = - "@AFA-explicit\n" - "%Initial q1\n" - "%Final !q0 & !q1 & !q3\n" - "q0 a1 & q1\n" - "q1 a2 & q2\n" - "q2 a1 & (q3 | q2)\n" - "q2 a2 & (q4 & q1)\n"; - - const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); - inter_aut = auts[0]; - - NameStateMap state_map; - construct(&aut, inter_aut, &alphabet, &state_map); - - CHECK(aut.finalstates.size() == 2); - CHECK(aut.finalstates.count(state_map.at("2"))); - CHECK(aut.finalstates.count(state_map.at("4"))); - - } - -} // }}} - -TEST_CASE("mata::afa::construct() correct calls") -{ // {{{ - Afa aut; - mata::parser::ParsedSection parsec; - - SECTION("construct an empty automaton") - { - parsec.type = mata::afa::TYPE_AFA; - - construct(&aut, parsec); - - // REQUIRE(is_lang_empty(aut)); - } - - SECTION("construct a simple non-empty automaton accepting the empty word") - { - parsec.type = mata::afa::TYPE_AFA; - parsec.dict.insert({"Initial", {"q1"}}); - parsec.dict.insert({"Final", {"q1"}}); - - construct(&aut, parsec); - - // REQUIRE(!is_lang_empty(aut)); - } - - SECTION("construct an automaton with more than one initial/final states") - { - parsec.type = mata::afa::TYPE_AFA; - parsec.dict.insert({"Initial", {"q1", "q2"}}); - parsec.dict.insert({"Final", {"q1", "q2", "q3"}}); - - construct(&aut, parsec); - - // REQUIRE(aut.initial.size() == 2); - // REQUIRE(aut.final.size() == 3); - } - - SECTION("construct a simple non-empty automaton accepting only the word 'a'") - { - parsec.type = mata::afa::TYPE_AFA; - parsec.dict.insert({"Initial", {"q1"}}); - parsec.dict.insert({"Final", {"q2"}}); - parsec.body = { {"q1", "a AND q2"} }; - - construct(&aut, parsec); - } -} diff --git a/tests/mintermization.cc b/tests/mintermization.cc index c0bec44b5..c8dee29c8 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -141,13 +141,11 @@ TEST_CASE("mata::Mintermization::compute_minterms") } } // compute_minterms -TEST_CASE("mata::Mintermization::mintermization") -{ +TEST_CASE("mata::Mintermization::mintermization") { Parsed parsed; mata::Mintermization mintermization{}; - SECTION("Mintermization small") - { + SECTION("Mintermization small") { std::string file = "@NFA-bits\n" "%States-enum q r s t \"(r,s)\"\n" @@ -175,213 +173,7 @@ TEST_CASE("mata::Mintermization::mintermization") REQUIRE(res.transitions[3].second.children[1].node.name == "t"); } - SECTION("Mintermization AFA small") - { - Parsed parsed; - mata::Mintermization mintermization{}; - std::string file = - "@AFA-bits\n" - "%Initial (q0) & ((q1 & q1' & q3 & q3'))\n" - "%Final \\true & (!q3' | (!q1))\n" - "q1 (!a0 & !a1 & (q2))\n" - "q1 (a1 & !a2 & (q3))\n" - "q1' q1'\n" - "q3' q3'\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 8); - REQUIRE(res.transitions[0].first.name == "1"); - REQUIRE(res.transitions[1].first.name == "1"); - REQUIRE(res.transitions[2].first.name == "1'"); - REQUIRE(res.transitions[3].first.name == "1'"); - REQUIRE(res.transitions[4].first.name == "1'"); - REQUIRE(res.transitions[5].first.name == "3'"); - REQUIRE(res.transitions[6].first.name == "3'"); - REQUIRE(res.transitions[7].first.name == "3'"); - REQUIRE(((res.transitions[0].second.children[1].node.name == "2" && res.transitions[1].second.children[1].node.name == "3") || (res.transitions[0].second.children[1].node.name == "3" && res.transitions[1].second.children[1].node.name == "2"))); - REQUIRE(res.transitions[2].second.children[1].node.name == "1'"); - REQUIRE(res.transitions[3].second.children[1].node.name == "1'"); - REQUIRE(res.transitions[4].second.children[1].node.name == "1'"); - REQUIRE(res.transitions[5].second.children[1].node.name == "3'"); - REQUIRE(res.transitions[6].second.children[1].node.name == "3'"); - REQUIRE(res.transitions[7].second.children[1].node.name == "3'"); - } - - SECTION("Mintermization AFA small 2") - { - Parsed parsed; - mata::Mintermization mintermization{}; - std::string file = - "@AFA-bits\n" - "%Initial q1\n" - "%Final q2\n" - "q1 a2 | q2\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 3); - REQUIRE(res.transitions[0].first.name == "1"); - REQUIRE(res.transitions[1].first.name == "1"); - REQUIRE(res.transitions[2].first.name == "1"); - REQUIRE(res.transitions[2].second.children.empty()); - REQUIRE(res.transitions[0].second.children[1].node.name == "2"); - REQUIRE(res.transitions[1].second.children[1].node.name == "2"); - } - - SECTION("Mintermization AFA normal") - { - Parsed parsed; - mata::Mintermization mintermization{}; - - std::string file = - "@AFA-bits\n" - "%Initial (q0) & ((q1 & q1' & q3 & q3'))\n" - "%Final \\true & (!q3' | (!q1))\n" - "q1 (!a0 & !a1 & !a2 & !a3 & (q2))\n" - "q0 (a4 & !a5 & !a6 & !a7 & (q0)) | (!a4 & a5 & !a6 & !a7 & (q1)) | (a4 & a5 & !a6 & !a7 & (q2))\n" - "q1' q1'\n" - "q3' q3'\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 26); - REQUIRE(res.transitions[0].first.name == "1"); - REQUIRE(res.transitions[1].first.name == "1"); - REQUIRE(res.transitions[2].first.name == "1"); - REQUIRE(res.transitions[3].first.name == "1"); - REQUIRE(res.transitions[4].first.name == "0"); - REQUIRE(res.transitions[5].first.name == "0"); - REQUIRE(res.transitions[6].first.name == "0"); - REQUIRE(res.transitions[7].first.name == "0"); - REQUIRE(res.transitions[8].first.name == "0"); - REQUIRE(res.transitions[9].first.name == "0"); - std::unordered_set symbols_from1 = {res.transitions[0].second.children[0].node.name, - res.transitions[1].second.children[0].node.name, - res.transitions[2].second.children[0].node.name, - res.transitions[3].second.children[0].node.name}; - REQUIRE(symbols_from1.size() == 4); - REQUIRE(res.transitions[0].second.children[1].node.name == "2"); - REQUIRE(res.transitions[1].second.children[1].node.name == "2"); - REQUIRE(res.transitions[2].second.children[1].node.name == "2"); - REQUIRE(res.transitions[3].second.children[1].node.name == "2"); - } - - SECTION("Mintermization AFA complex") - { - Parsed parsed; - mata::Mintermization mintermization{}; - - std::string file = - "@AFA-bits\n" - "%Initial (q0) & ((q1 & q1' & q3 & q3'))\n" - "%Final \\true & (!q3' | (!q1))\n" - "q1 (!a0 & !a1 & !a2 & !a3 & (q2))\n" - "q0 (a4 & !a5 & !a6 & !a7 & (q0)) | (!a4 & a5 & !a6 & !a7 & (q0)) | (a4 & a5 & !a6 & !a7 & (q0)) | (!a4 & !a5 & a6 & !a7 & (q0)) | (a4 & !a5 & a6 & !a7 & (q0)) | (!a4 & a5 & a6 & !a7 & (q0)) | (a4 & a5 & a6 & !a7 & (q0)) | (!a4 & !a5 & !a6 & a7 & (q0)) | (a4 & !a5 & !a6 & a7 & (q0)) | (!a4 & a5 & !a6 & a7 & (q0)) | (a4 & a5 & !a6 & a7 & (q0)) | (!a4 & !a5 & a6 & a7 & (q0)) | (!a4 & !a5 & !a6 & !a7 & (q0)) | (a4 & !a5 & a6 & a7 & (q0))\n" - "q3 (a8 & !a9 & !a10 & !a11 & (q3)) | (!a8 & a9 & !a10 & !a11 & (q3)) | (a8 & a9 & !a10 & !a11 & (q3)) | (!a8 & !a9 & a10 & !a11 & (q3)) | (a8 & !a9 & a10 & !a11 & (q3)) | (!a8 & a9 & a10 & !a11 & (q3)) | (a8 & a9 & a10 & !a11 & (q3)) | (!a8 & !a9 & !a10 & a11 & (q3)) | (a8 & !a9 & !a10 & a11 & (q3)) | (!a8 & a9 & !a10 & a11 & (q3)) | (a8 & a9 & !a10 & a11 & (q3)) | (!a8 & !a9 & a10 & a11 & (q3)) | (!a8 & !a9 & !a10 & !a11 & (q3)) | (a8 & !a9 & a10 & a11 & (q3))\n" - "q1' q1'\n" - "q3' q3'\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 1965); - } - - SECTION("Mintermization AFA state conjunction") - { - Parsed parsed; - mata::Mintermization mintermization{}; - - std::string file = - "@AFA-bits\n" - "%Initial (q0) & ((q1 & q1' & q3 & q3'))\n" - "%Final \\true & (!q3' | (!q1))\n" - "q1 (!a0 & !a1 & !a2 & !a3 & (q2 & q3 & q0))\n" - "q0 (a4 & !a5 & !a6 & !a7 & (q0 & q1 & q1')) | (!a4 & a5 & !a6 & !a7 & (q1)) | (a4 & a5 & !a6 & !a7 & q2 & q1')\n" - "q1' q1'\n" - "q3' q3'\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 26); - REQUIRE(res.transitions[0].first.name == "1"); - REQUIRE(res.transitions[1].first.name == "1"); - REQUIRE(res.transitions[2].first.name == "1"); - REQUIRE(res.transitions[3].first.name == "1"); - REQUIRE(res.transitions[4].first.name == "0"); - REQUIRE(res.transitions[5].first.name == "0"); - REQUIRE(res.transitions[6].first.name == "0"); - REQUIRE(res.transitions[7].first.name == "0"); - REQUIRE(res.transitions[8].first.name == "0"); - REQUIRE(res.transitions[9].first.name == "0"); - std::unordered_set symbols_from1 = {res.transitions[0].second.children[0].node.name, - res.transitions[1].second.children[0].node.name, - res.transitions[2].second.children[0].node.name, - res.transitions[3].second.children[0].node.name}; - REQUIRE(symbols_from1.size() == 4); - REQUIRE(res.transitions[0].second.children[1].node.name == "&"); - REQUIRE(res.transitions[1].second.children[1].node.name == "&"); - REQUIRE(res.transitions[2].second.children[1].node.name == "&"); - REQUIRE(res.transitions[3].second.children[1].node.name == "&"); - REQUIRE(res.transitions[4].second.children[1].node.name == "&"); - REQUIRE(res.transitions[5].second.children[1].node.name == "&"); - } - - SECTION("Mintermization AFA difficult") - { - Parsed parsed; - mata::Mintermization mintermization{}; - - std::string file = - "@AFA-bits\n" - "%Initial q11\n" - "%Final !q0 & !q1 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11\n" - "q10 (a1 & !a0 & a0 & q9) | (a1 & !a0 & q9 & q10)\n" - "q6 a3\n" - "q8 !a2 | (a3 & !a0 & q8)\n" - "q4 !a0 & q3\n" - "q3 !a0 & q2\n" - "q1 (!a1 & a0) | (!a1 & q1) | (!a0 & a0 & q0) | (!a0 & q0 & q1)\n" - "q11 (!a1 & a0 & a4 & !a0 & !a0 & !a0 & a0 & q2 & q3 & q4) | (!a1 & a0 & a4 & !a0 & !a0 & !a0 & q2 & q3 & q4 & q5) | (!a1 & a0 & a3 & !a0 & a0 & q6) | (!a1 & a0 & a3 & !a0 & q6 & q7) | (!a1 & a0 & a1 & !a0 & a0 & q9) | (!a1 & a0 & a1 & !a0 & q9 & q10) | (!a1 & a4 & !a0 & !a0 & !a0 & a0 & q1 & q2 & q3 & q4) | (!a1 & a4 & !a0 & !a0 & !a0 & q1 & q2 & q3 & q4 & q5) | (!a1 & a3 & !a0 & a0 & q1 & q6) | (!a1 & a3 & !a0 & q1 & q6 & q7) | (!a1 & a1 & !a0 & a0 & q1 & q9) | (!a1 & a1 & !a0 & q1 & q9 & q10) | (!a0 & a0 & a4 & !a0 & !a0 & !a0 & a0 & q0 & q2 & q3 & q4) | (!a0 & a0 & a4 & !a0 & !a0 & !a0 & q0 & q2 & q3 & q4 & q5) | (!a0 & a0 & a3 & !a0 & a0 & q0 & q6) | (!a0 & a0 & a3 & !a0 & q0 & q6 & q7) | (!a0 & a0 & a1 & !a0 & a0 & q0 & q9) | (!a0 & a0 & a1 & !a0 & q0 & q9 & q10) | (!a0 & a4 & !a0 & !a0 & !a0 & a0 & q0 & q1 & q2 & q3 & q4) | (!a0 & a4 & !a0 & !a0 & !a0 & q0 & q1 & q2 & q3 & q4 & q5) | (!a0 & a3 & !a0 & a0 & q0 & q1 & q6) | (!a0 & a3 & !a0 & q0 & q1 & q6 & q7) | (!a0 & a1 & !a0 & a0 & q0 & q1 & q9) | (!a0 & a1 & !a0 & q0 & q1 & q9 & q10)\n" - "q7 (a3 & !a0 & a0 & q6) | (a3 & !a0 & q6 & q7)\n" - "q2 !a3\n" - "q9 q8\n" - "q5 (a4 & !a0 & !a0 & !a0 & a0 & q2 & q3 & q4) | (a4 & !a0 & !a0 & !a0 & q2 & q3 & q4 & q5)\n" - "q0 a2\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - - const auto res = mintermization.mintermize(aut); - } - - SECTION("Mintermization NFA true and false") - { + SECTION("Mintermization NFA true and false") { std::string file = "@NFA-bits\n" "%States-enum q r s\n" @@ -407,38 +199,7 @@ TEST_CASE("mata::Mintermization::mintermization") REQUIRE(res.transitions[2].first.name == "r"); } - SECTION("Mintermization AFA true and false") - { - std::string file = - "@AFA-bits\n" - "%Initial q0\n" - "%Final q3\n" - "q0 (\\true & q2 & q3 & q0) | (a4 & !a5 & !a6 & !a7 & q0 & q1 & q2)\n" - "q1 \\false\n" - "q2 q1\n" - "q3 \\true\n"; - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.node.is_operator()); - REQUIRE(aut.transitions[0].second.node.raw == "|"); - REQUIRE(aut.transitions[0].second.children[1].node.is_operator()); - REQUIRE(aut.transitions[0].second.children[1].node.raw == "&"); - - const auto res = mintermization.mintermize(aut); - REQUIRE(res.transitions.size() == 7); - REQUIRE(res.transitions[0].first.raw == "q0"); - REQUIRE(res.transitions[1].first.raw == "q0"); - REQUIRE(res.transitions[2].first.raw == "q0"); - REQUIRE(res.transitions[3].first.raw == "q2"); - REQUIRE(res.transitions[4].first.raw == "q2"); - REQUIRE(res.transitions[5].first.raw == "q3"); - REQUIRE(res.transitions[6].first.raw == "q3"); - } - - SECTION("Mintermization NFA multiple") - { + SECTION("Mintermization NFA multiple") { Parsed parsed; mata::Mintermization mintermization{}; @@ -483,134 +244,4 @@ TEST_CASE("mata::Mintermization::mintermization") REQUIRE(res[1].transitions[0].second.children[1].node.name == "r"); REQUIRE(res[1].transitions[1].second.children[1].node.name == "r"); } -} - -TEST_CASE("mata::Mintermization::trans_to_bdd_nfa with big AFA","[.expensive]") -{ - - Parsed parsed; - mata::Mintermization mintermization{}; - - SECTION("AFA big") - { - std::string file = - "@AFA-bits\n" - "%Initial qQC0_0 & qQC1_0\n" - "%Final !qQC0_39 & !qQC0_5 & !qQC1_12 & !qQC0_20 & !qQC1_22 & !qQC0_10 & !qQC1_36 & !qQC0_40 & !qQC1_2 & !qQC1_31 & !qQC0_47 & !qQC1_5 & !qQC1_28 & !qQC0_35 & !qQC1_43 & !qQC0_9 & !qQC1_51 & !qQC1_48 & !qQC0_2 & !qQC1_15 & !qQC0_27 & !qQC0_7 & !qQC1_10 & !qQC0_22 & !qQC1_24 & !qQC0_52 & !qQC0_16 & !qQC1_9 & !qQC0_13 & !qQC1_38 & !qQC1_21 & !qQC0_18 & !qQC1_33 & !qQC0_45 & !qQC1_7 & !qQC0_37 & !qQC1_41 & !qQC0_30 & !qQC1_46 & !qQC0_29 & !qQC1_52 & !qQC0_1 & !qQC1_16 & !qQC0_24 & !qQC0_14 & !qQC0_49 & !qQC1_26 & !qQC0_50 & !qQC0_11 & !qQC1_23 & !qQC1_35 & !qQC0_43 & !qQC1_1 & !qQC1_4 & !qQC1_29 & !qQC1_30 & !qQC0_46 & !qQC0_32 & !qQC1_44 & !qQC1_19 & !qQC1_50 & !qQC1_49 & !qQC0_3 & !qQC1_14 & !qQC0_26 & !qQC0_4 & !qQC1_13 & !qQC0_21 & !qQC0_38 & !qQC1_8 & !qQC1_25 & !qQC0_53 & !qQC0_17 & !qQC1_3 & !qQC1_37 & !qQC0_41 & !qQC1_6 & !qQC0_19 & !qQC1_32 & !qQC0_44 & !qQC0_34 & !qQC1_42 & !qQC0_8 & !qQC0_28 & !qQC0_31 & !qQC1_47 & !qQC1_11 & !qQC0_23 & !qQC0_6 & !qQC1_27 & !qQC0_51 & !qQC0_15 & !qQC0_48 & !qQC1_20 & !qQC0_12 & !qQC1_39 & !qQC1_0 & !qQC1_34 & !qQC0_42 & !qQC0_36 & !qQC1_40 & !qQC1_18 & !qQC0_33 & !qQC1_45 & !qQC0_25 & !qQC1_53 & !qQC0_0 & !qQC1_17\n" - "qQC1_34 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_35\n" - "qQC1_1 aF | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & (aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0))) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & qQC1_1) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & qQC1_2) | (qQC1_2 & qQC1_1)\n" - "qQC0_42 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_43\n"; // I cut it here to make test time feasible. - /* - "qQC0_3 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_4\n" - "qQC1_40 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_41\n" - "qQC0_36 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_37\n" - "qQC1_9 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_10\n" - "qQC1_10 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_11\n" - "qQC1_4 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_5\n" - "qQC0_22 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_23\n" - "qQC1_3 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_4\n" - "qQC0_25 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_26\n" - "qQC1_53 !aF\n" - "qQC1_17 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_18\n" - "qQC1_38 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_39\n" - "qQC1_21 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_22\n" - "qQC0_13 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_14\n" - "qQC1_33 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_34\n" - "qQC0_18 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_19\n" - "qQC0_45 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_46\n" - "qQC0_4 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_5\n" - "qQC1_36 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_37\n" - "qQC0_40 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_41\n" - "qQC0_1 (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_2) | (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_1)\n" - "qQC0_30 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_31\n" - "qQC0_29 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_30\n" - "qQC1_46 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_47\n" - "qQC0_35 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_36\n" - "qQC1_43 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_44\n" - "qQC0_27 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_28\n" - "qQC1_51 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_52\n" - "qQC1_48 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_49\n" - "qQC1_15 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_16\n" - "qQC1_23 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_24\n" - "qQC0_11 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_12\n" - "qQC1_24 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_25\n" - "qQC0_16 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_17\n" - "qQC0_52 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_53\n" - "qQC0_46 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_47\n" - "qQC0_7 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_8\n" - "qQC1_30 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_31\n" - "qQC1_29 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_30\n" - "qQC0_32 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_33\n" - "qQC1_44 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_45\n" - "qQC1_19 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_20\n" - "qQC1_8 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_9\n" - "qQC1_41 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_42\n" - "qQC0_37 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_38\n" - "qQC0_21 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_22\n" - "qQC1_13 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_14\n" - "qQC0_38 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_39\n" - "qQC1_7 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_8\n" - "qQC0_24 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_25\n" - "qQC1_52 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_53\n" - "qQC1_16 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_17\n" - "qQC1_2 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_3\n" - "qQC0_14 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_15\n" - "qQC0_49 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_50\n" - "qQC0_50 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_51\n" - "qQC0_8 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_9\n" - "qQC1_26 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_27\n" - "qQC0_19 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_20\n" - "qQC0_44 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_45\n" - "qQC0_5 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_6\n" - "qQC1_32 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_33\n" - "qQC0_43 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_44\n" - "qQC0_2 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_3\n" - "qQC1_35 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_36\n" - "qQC0_28 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_29\n" - "qQC1_47 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_48\n" - "qQC0_31 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_32\n" - "qQC1_11 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_12\n" - "qQC1_5 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_6\n" - "qQC0_23 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_24\n" - "qQC1_50 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_51\n" - "qQC1_49 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_50\n" - "qQC1_14 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_15\n" - "qQC1_0 aF | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & (aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0)) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & qQC1_2) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & qQC1_1) | (qQC1_1 & qQC1_2)\n" - "qQC0_26 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_27\n" - "qQC0_12 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_13\n" - "qQC1_39 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_40\n" - "qQC1_20 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_21\n" - "qQC0_53 aF\n" - "qQC1_25 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_26\n" - "qQC0_17 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_18\n" - "qQC0_41 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_42\n" - "qQC0_0 (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_1) | (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_2)\n" - "qQC1_37 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_38\n" - "qQC1_45 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_46\n" - "qQC1_18 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_19\n" - "qQC0_33 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_34\n" - "qQC1_42 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_43\n" - "qQC0_34 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_35\n" - "qQC1_12 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_13\n" - "qQC0_39 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_40\n" - "qQC1_6 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_7\n" - "qQC0_20 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_21\n" - "qQC1_22 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_23\n" - "qQC0_10 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_11\n" - "qQC0_51 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_52\n" - "qQC0_9 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_10\n" - "qQC1_27 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_28\n" - "qQC0_15 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_16\n" - "qQC0_48 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_49\n" - "qQC1_31 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_32\n" - "qQC1_28 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_29\n" - "qQC0_47 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_48\n" - "qQC0_6 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_7\n"; - */ - - parsed = parse_mf(file); - std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); - const auto& aut= auts[0]; - const auto res = mintermization.mintermize(aut); - } -} // mintermization +} // TEST_CASE("mata::Mintermization::mintermization")