Remove unused import

include/mata/alphabet.hh

@@ -82,8 +82,13 @@ public:
 
     bool operator==(const Alphabet &) const = delete;
 
+    /**
+     * Checks whether the alphabet has any symbols.
+     */
+    virtual bool empty() const = 0;
+
 protected:
-    virtual const void *address() const { return this; }
+    virtual const void* address() const { return this; }
 }; // class Alphabet.
 
 /**
@@ -115,6 +120,8 @@ public:
 
     IntAlphabet& operator=(const IntAlphabet& int_alphabet) = delete;
 
+    bool empty() const override { return false; }
+
 protected:
     const void* address() const override { return &alphabet_instance; }
 
@@ -234,6 +241,8 @@ public:
      */
     size_t get_number_of_symbols() const { return symbols_.size(); }
 
+    bool empty() const override { return symbols_.empty(); }
+
 private:
     mata::utils::OrdVector<Symbol> symbols_{}; ///< Map of string transition symbols to symbol values.
     Symbol next_symbol_value_{ 0 }; ///< Next value to be used for a newly added symbol.
@@ -362,6 +371,8 @@ public:
      */
     const StringToSymbolMap& get_symbol_map() const { return symbol_map_; }
 
+    bool empty() const override { return symbol_map_.empty(); }
+
 private:
     StringToSymbolMap symbol_map_{}; ///< Map of string transition symbols to symbol values.
     Symbol next_symbol_value_{}; ///< Next value to be used for a newly added symbol.

include/mata/nfa/delta.hh

@@ -113,6 +113,7 @@ public:
     // dangerous, breaks the sortedness invariant
     using super::push_back;
     // is adding non-const version as well ok?
+    using super::front;
     using super::back;
     using super::filter;
 

include/mata/nfa/nfa.hh

@@ -166,7 +166,7 @@ public:
     BoolVector get_useful_states() const;
 
     /**
-     * @brief Structure for storing callback functions (event handlers) utilizing 
+     * @brief Structure for storing callback functions (event handlers) utilizing
      * Tarjan's SCC discover algorithm.
      */
     struct TarjanDiscoverCallback {
@@ -182,7 +182,7 @@ public:
 
     /**
      * @brief Tarjan's SCC discover algorihm.
-     * 
+     *
      * @param callback Callbacks class to instantiate callbacks for the Tarjan's algorithm.
      */
     void tarjan_scc_discover(const TarjanDiscoverCallback& callback) const;
@@ -275,16 +275,16 @@ public:
     StateSet post(const StateSet& states, const Symbol& symbol) const;
 
     /**
-     * Check whether the language of NFA is empty. 
-     * Currently calls is_lang_empty_scc if cex is null 
+     * Check whether the language of NFA is empty.
+     * Currently calls is_lang_empty_scc if cex is null
      * @param[out] cex Counter-example path for a case the language is not empty.
      * @return True if the language is empty, false otherwise.
      */
     bool is_lang_empty(Run* cex = nullptr) const;
 
     /**
      * @brief Check if the language is empty using Tarjan's SCC discover algorithm.
-     * 
+     *
      * @return Language empty <-> True
      */
     bool is_lang_empty_scc() const;
@@ -307,7 +307,7 @@ public:
 
     /**
      * @brief Is the automaton graph acyclic? Used for checking language finiteness.
-     * 
+     *
      * @return true <-> Automaton graph is acyclic.
      */
     bool is_acyclic() const;
@@ -337,7 +337,7 @@ public:
 
     /**
      * @brief Get the set of all words in the language of the automaton whose length is <= @p max_length
-     * 
+     *
      * If you have an automaton with finite language (can be checked using @ref is_acyclic),
      * you can get all words by calling
      *      get_words(aut.num_of_states())

include/mata/nft/algorithms.hh

@@ -0,0 +1,125 @@
+/* algorithms.hh -- Wrapping up algorithms for Nft manipulation which would be otherwise in anonymous namespaces.
+ */
+
+#ifndef MATA_NFT_INTERNALS_HH_
+#define MATA_NFT_INTERNALS_HH_
+
+#include "nft.hh"
+#include "mata/simlib/util/binary_relation.hh"
+
+/**
+ * Concrete NFT implementations of algorithms, such as complement, inclusion, or universality checking.
+ *
+ * This is a separation of the implementation from the interface defined in mata::nft.
+ * Note, that in mata::nft interface, there are particular dispatch functions calling
+ * these function according to parameters provided by a user.
+ * E.g. we can call the following function: `is_universal(aut, alph, {{'algorithm', 'antichains'}})`
+ * to check for universality based on antichain-based algorithm.
+ *
+ * In particular, this includes algorithms for:
+ *   1. Complementation,
+ *   2. Inclusion,
+ *   3. Universality checking,
+ *   4. Intersection/concatenation with epsilon transitions, or,
+ *   5. Computing relation.
+ */
+namespace mata::nft::algorithms {
+
+/**
+ * Brzozowski minimization of automata (revert -> determinize -> revert -> determinize).
+ * @param[in] aut Automaton to be minimized.
+ * @return Minimized automaton.
+ */
+Nft minimize_brzozowski(const Nft& aut);
+
+/**
+ * Complement implemented by determization, adding sink state and making automaton complete. Then it adds final states
+ *  which were non final in the original automaton.
+ * @param[in] aut Automaton to be complemented.
+ * @param[in] symbols Symbols needed to make the automaton complete.
+ * @param[in] minimize_during_determinization Whether the determinized automaton is computed by (brzozowski)
+ *  minimization.
+ * @return Complemented automaton.
+ */
+Nft complement_classical(const Nft& aut, const mata::utils::OrdVector<Symbol>& symbols,
+                         bool minimize_during_determinization = false);
+
+/**
+ * Inclusion implemented by complementation of bigger automaton, intersecting it with smaller and then it checks
+ *  emptiness of intersection.
+ * @param[in] smaller Automaton which language should be included in the bigger one.
+ * @param[in] bigger Automaton which language should include the smaller one.
+ * @param[in] alphabet Alphabet of both automata (it is computed automatically, but it is more efficient to set it if
+ *  you have it).
+ * @param[out] cex A potential counterexample word which breaks inclusion
+ * @return True if smaller language is included,
+ * i.e., if the final intersection of smaller complement of bigger is empty.
+ */
+bool is_included_naive(const Nft& smaller, const Nft& bigger, const Alphabet* alphabet = nullptr, Run* cex = nullptr);
+
+/**
+ * Inclusion implemented by antichain algorithms.
+ * @param[in] smaller Automaton which language should be included in the bigger one
+ * @param[in] bigger Automaton which language should include the smaller one
+ * @param[in] alphabet Alphabet of both automata (not needed for antichain algorithm)
+ * @param[out] cex A potential counterexample word which breaks inclusion
+ * @return True if smaller language is included,
+ * i.e., if the final intersection of smaller complement of bigger is empty.
+ */
+bool is_included_antichains(const Nft& smaller, const Nft& bigger, const Alphabet*  alphabet = nullptr, Run* cex = nullptr);
+
+/**
+ * Universality check implemented by checking emptiness of complemented automaton
+ * @param[in] aut Automaton which universality is checked
+ * @param[in] alphabet Alphabet of the automaton
+ * @param[out] cex Counterexample word which eventually breaks the universality
+ * @return True if the complemented automaton has non empty language, i.e., the original one is not universal
+ */
+bool is_universal_naive(const Nft& aut, const Alphabet& alphabet, Run* cex);
+
+/**
+ * Universality checking based on subset construction with antichain.
+ * @param[in] aut Automaton which universality is checked
+ * @param[in] alphabet Alphabet of the automaton
+ * @param[out] cex Counterexample word which eventually breaks the universality
+ * @return True if the automaton is universal, otherwise false.
+ */
+bool is_universal_antichains(const Nft& aut, const Alphabet& alphabet, Run* cex);
+
+Simlib::Util::BinaryRelation compute_relation(
+        const Nft& aut,
+        const ParameterMap&  params = {{ "relation", "simulation"}, { "direction", "forward"}});
+
+/**
+ * @brief Compute product of two NFTs, final condition is to be specified, with a possibility of using multiple epsilons.
+ *
+ * @param[in] lhs First NFT to compute intersection for.
+ * @param[in] rhs Second NFT to compute intersection for.
+ * @param[in] first_epsilons The smallest epsilon.
+ * @param[in] final_condition The predicate that tells whether a pair of states is final (conjunction for intersection).
+ * @param[out] prod_map Can be used to get the mapping of the pairs of the original states to product states.
+ *   Mostly useless, it is only filled in and returned if !=nullptr, but the algorithm internally uses another data structures,
+ *   because this one is too slow.
+ * @return NFT as a product of NFTs @p lhs and @p rhs with ε-transitions preserved.
+ */
+Nft product(const Nft& lhs, const Nft& rhs, const std::function<bool(State,State)> && final_condition,
+            const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
+
+/**
+ * @brief Concatenate two NFTs.
+ *
+ * Supports epsilon symbols when @p use_epsilon is set to true.
+ * @param[in] lhs First automaton to concatenate.
+ * @param[in] rhs Second automaton to concatenate.
+ * @param[in] epsilon Epsilon to be used co concatenation (provided @p use_epsilon is true)
+ * @param[in] use_epsilon Whether to concatenate over epsilon symbol.
+ * @param[out] lhs_state_renaming Map mapping lhs states to result states.
+ * @param[out] rhs_state_renaming Map mapping rhs states to result states.
+ * @return Concatenated automaton.
+ */
+Nft concatenate_eps(const Nft& lhs, const Nft& rhs, const Symbol& epsilon, bool use_epsilon = false,
+                    StateRenaming* lhs_state_renaming = nullptr, StateRenaming* rhs_state_renaming = nullptr);
+
+} // Namespace mata::nft::algorithms.
+
+#endif // MATA_NFT_INTERNALS_HH_

include/mata/nft/builder.hh

@@ -0,0 +1,110 @@
+// TODO: Insert file header.
+
+#ifndef LIBMATA_NFT_BUILDER_HH
+#define LIBMATA_NFT_BUILDER_HH
+
+#include "mata/nfa/builder.hh"
+#include "nft.hh"
+
+#include <filesystem>
+
+/**
+ * Namespace providing options to build NFAs.
+ */
+namespace mata::nft::builder {
+
+using namespace mata::nft;
+
+using NameStateMap = std::unordered_map<std::string, State>;
+
+/**
+ * Create an automaton accepting only a single @p word.
+ */
+Nft create_single_word_nft(const std::vector<Symbol>& word);
+
+/**
+ * Create an automaton accepting only a single @p word.
+ *
+ * @param word Word to accept.
+ * @param alphabet Alphabet to use in NFA for translating word into symbols. If specified, the alphabet has to contain
+ *  translations for all of the word symbols. If left empty, a new alphabet with only the symbols of the word will be
+ *  created.
+ */
+Nft create_single_word_nft(const std::vector<std::string>& word, Alphabet* alphabet = nullptr);
+
+/**
+ * Create automaton accepting only epsilon string.
+ */
+Nft create_empty_string_nft();
+
+/**
+ * Create automaton accepting sigma star over the passed alphabet using DONT_CARE symbol.
+ */
+Nft create_sigma_star_nft();
+
+/**
+ * Create automaton accepting sigma star over the passed alphabet.
+ *
+ * @param[in] alphabet Alphabet to construct sigma star automaton with. When alphabet is left empty, the default empty
+ *  alphabet is used, creating an automaton accepting only the empty string.
+ */
+Nft create_sigma_star_nft(Alphabet* alphabet = new OnTheFlyAlphabet{});
+
+/** Loads an automaton from Parsed object */
+// TODO this function should the same thing as the one taking IntermediateAut or be deleted
+Nft construct(const mata::parser::ParsedSection& parsec, Alphabet* alphabet, NameStateMap* state_map = nullptr);
+
+/** Loads an automaton from Parsed object */
+Nft construct(const mata::IntermediateAut& inter_aut, Alphabet* alphabet, NameStateMap* state_map = nullptr);
+/** Loads an automaton from Parsed object; version for python binding */
+void construct(
+    Nft* result, const mata::IntermediateAut& inter_aut, Alphabet* alphabet, NameStateMap* state_map = nullptr
+);
+
+template<class ParsedObject>
+Nft construct(const ParsedObject& parsed, Alphabet* alphabet = nullptr,
+              NameStateMap* state_map = nullptr) {
+    OnTheFlyAlphabet tmp_alphabet{};
+    if (!alphabet) {
+        alphabet = &tmp_alphabet;
+    }
+    return construct(parsed, alphabet, state_map);
+} // construct().
+
+/**
+ * Parse NFA from the mata format in an input stream.
+ *
+ * @param nft_stream Input stream containing NFA in mata format.
+ * @throws std::runtime_error Parsing of NFA fails.
+ */
+Nft parse_from_mata(std::istream& nft_stream);
+
+/**
+ * Parse NFA from the mata format in a string.
+ *
+ * @param nft_stream String containing NFA in mata format.
+ * @throws std::runtime_error Parsing of NFA fails.
+ */
+Nft parse_from_mata(const std::string& nft_in_mata);
+
+/**
+ * Parse NFA from the mata format in a file.
+ *
+ * @param nft_stream Path to the file containing NFA in mata format.
+ * @throws std::runtime_error @p nft_file does not exist.
+ * @throws std::runtime_error Parsing of NFA fails.
+ */
+Nft parse_from_mata(const std::filesystem::path& nft_file);
+
+/**
+ * Create NFT from NFA.
+ * @param nfa_state NFA to create NFT from.
+ * @param level_cnt Number of levels of NFT.
+ * @param epsilons Which symbols handle as epsilons.
+ * @return NFT representing @p nfa_state with @p level_cnt number of levels.
+ */
+Nft create_from_nfa(const mata::nfa::Nfa& nfa_state, Level level_cnt = 2, const std::set<Symbol>& epsilons = { EPSILON });
+
+} // namespace mata::nft::builder.
+
+#endif //LIBMATA_NFT_BUILDER_HH