default level set to 1; levels size synchronized with delta

include/mata/nft/nft.hh

@@ -51,7 +51,7 @@ struct Nft : public mata::nfa::Nfa {
 public:
     /// @brief For state q, levels[q] gives the state a level.
     std::vector<Level> levels{};
-    Level levels_cnt = 0;
+    Level levels_cnt = 1;
     /// Key value store for additional attributes for the NFT. Keys are attribute names as strings and the value types
     ///  are up to the user.
     /// For example, we can set up attributes such as "state_dict" for state dictionary attribute mapping states to their
@@ -62,22 +62,24 @@ public:
 
 public:
     explicit Nft(Delta delta = {}, utils::SparseSet<State> initial_states = {},
-                 utils::SparseSet<State> final_states = {}, std::vector<Level> levels = {}, const Level levels_cnt = 0,
+                 utils::SparseSet<State> final_states = {}, std::vector<Level> levels = {}, const Level levels_cnt = 1,
                  Alphabet* alphabet = nullptr)
-        : mata::nfa::Nfa(std::move(delta), std::move(initial_states), std::move(final_states), alphabet), levels(levels), levels_cnt(levels_cnt) {}
+        : mata::nfa::Nfa(std::move(delta), std::move(initial_states), std::move(final_states), alphabet),
+          levels(levels.size() ? std::move(levels) : std::vector<Level>(delta.num_of_states(), 0)), levels_cnt(levels_cnt) {}
     /**
      * @brief Construct a new explicit NFT with num_of_states states and optionally set initial and final states.
      *
      * @param[in] num_of_states Number of states for which to preallocate Delta.
      */
     explicit Nft(const unsigned long num_of_states, StateSet initial_states = {},
-                 StateSet final_states = {}, std::vector<Level> levels = {}, const Level levels_cnt = 0, Alphabet*
+                 StateSet final_states = {}, std::vector<Level> levels = {}, const Level levels_cnt = 1, Alphabet*
                  alphabet = nullptr)
-        : mata::nfa::Nfa(num_of_states, std::move(initial_states), std::move(final_states), alphabet), levels(levels), levels_cnt(levels_cnt) {}
+        : mata::nfa::Nfa(num_of_states, std::move(initial_states), std::move(final_states), alphabet),
+        levels(levels.size() ? std::move(levels) : std::vector<Level>(num_of_states, 0)), levels_cnt(levels_cnt) {}
 
     explicit Nft(const mata::nfa::Nfa& other)
         : mata::nfa::Nfa(other.delta, other.initial, other.final, other.alphabet),
-          levels(std::vector<Level>()), levels_cnt(0) {}
+          levels(std::vector<Level>(other.delta.num_of_states(), 0)), levels_cnt(1) {}
 
     /**
      * @brief Construct a new explicit NFT from other NFT.

src/nft/builder.cc

@@ -340,5 +340,9 @@ Nft builder::create_from_nfa(const mata::nfa::Nfa& nfa, Level level_cnt, const s
     std::ranges::for_each(nfa.initial, [&](const State nfa_state){ nft.initial.insert(state_mapping[nfa_state]); });
     nft.final.reserve(nfa.final.size());
     std::ranges::for_each(nfa.final, [&](const State nfa_state){ nft.final.insert(state_mapping[nfa_state]); });
+
+    // TODO(nft): HACK. Levels do not work if the size of delta differs from the size of the vector level.
+    nft.levels.resize(nft.delta.num_of_states());
+
     return nft;
 }

src/nft/inclusion.cc

@@ -37,7 +37,6 @@ bool mata::nft::algorithms::is_included_antichains(
     Run*                   cex)
 { // {{{
     if (smaller.levels_cnt != bigger.levels_cnt) { return false; }
-    if (smaller.levels_cnt == 0) { return nfa::algorithms::is_included_antichains(smaller, bigger, alphabet, cex); }
 
     OrdVector<mata::Symbol> symbols;
     if (alphabet == nullptr) {
@@ -58,17 +57,6 @@ bool mata::nft::algorithms::is_included_antichains(
 namespace {
     using AlgoType = decltype(algorithms::is_included_naive)*;
 
-    bool compute_equivalence(const Nft &lhs, const Nft &rhs, const mata::Alphabet *const alphabet, const AlgoType &algo) {
-        //alphabet should not be needed as input parameter
-        if (algo(lhs, rhs, alphabet, nullptr)) {
-            if (algo(rhs, lhs, alphabet, nullptr)) {
-                return true;
-            }
-        }
-
-        return false;
-    }
-
     AlgoType set_algorithm(const std::string &function_name, const ParameterMap &params) {
         if (!haskey(params, "algorithm")) {
             throw std::runtime_error(function_name +
@@ -106,7 +94,6 @@ bool mata::nft::is_included(
 bool mata::nft::are_equivalent(const Nft& lhs, const Nft& rhs, const Alphabet *alphabet, const ParameterMap& params)
 {
     if (lhs.levels_cnt != rhs.levels_cnt) { return false; }
-    if (lhs.levels_cnt == 0) { return nfa::are_equivalent(lhs, rhs, alphabet, params); }
 
     OrdVector<mata::Symbol> symbols;
     if (alphabet == nullptr) {

src/nft/nft.cc

@@ -240,6 +240,13 @@ void Nft::make_one_level_aut(const utils::OrdVector<Symbol> &dcare_replacements)
 
 Nft Nft::get_one_level_aut(const utils::OrdVector<Symbol> &dcare_replacements) const {
     Nft result{ *this };
+
+    // TODO(nft): Create a class for LEVELS with overloaded getter and setter.
+    // HACK. Works only for automata without levels.
+    if (result.levels.size() != result.num_of_states()) {
+        return result;
+    }
+
     result.make_one_level_aut(dcare_replacements);
     return result;
 }
@@ -263,7 +270,12 @@ State Nft::add_state() {
 }
 
 State Nft::add_state(State state) {
-    levels.push_back(0);
+    const size_t levels_size = levels.size();
+    if (state >= levels_size) {
+        levels.resize(state + 1);
+        const size_t begin_idx = (levels_size == 0) ? 0 : levels_size - 1;
+        std::fill(levels.begin() + static_cast<long int>(begin_idx), levels.end(), 0);
+    }
     return mata::nfa::Nfa::add_state(state);
 }
 

tests/nft/nft.cc

@@ -3008,7 +3008,7 @@ TEST_CASE("mata::nft::Nft::get_one_level_aut") {
                 REPLACE_DONT_CARE(delta, inter, trg);\
 
     SECTION("level_cnt == 1") {
-        Nft aut(5, {0}, {3, 4}, {0, 0, 0, 0, 0}, 1);
+        Nft aut(5, {0}, {3, 4});
         aut.delta.add(0, 0, 1);
         aut.delta.add(0, 1, 2);
         aut.delta.add(1, 0, 1);
@@ -3020,7 +3020,7 @@ TEST_CASE("mata::nft::Nft::get_one_level_aut") {
         aut.delta.add(4, 1, 2);
         aut.delta.add(4, DONT_CARE, 4);
 
-        Nft expected(5, {0}, {3, 4}, {0, 0, 0, 0, 0}, 1);
+        Nft expected(5, {0}, {3, 4});
         expected.delta.add(0, 0, 1);
         expected.delta.add(0, 1, 2);
         expected.delta.add(1, 0, 1);