diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 26ade1d9c..12527223a 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -18,6 +18,7 @@ #include #include #include +#include #include "mata/alphabet.hh" #include "mata/parser/parser.hh" @@ -535,11 +536,14 @@ Nfa determinize(const Nfa& aut, std::unordered_map *subset_map * @param[in] aut Automaton to reduce. * @param[out] state_renaming Mapping of original states to reduced states. * @param[in] params Optional parameters to control the reduction algorithm: - * - "algorithm": "simulation". + * - "algorithm": "simulation", "residual", + * and options to parametrize residual reduction, not utilized in simulation + * - "type": "after", "with", + * - "direction": "forward", "backward". * @return Reduced automaton. */ Nfa reduce(const Nfa &aut, StateRenaming *state_renaming = nullptr, - const ParameterMap& params = {{ "algorithm", "simulation" } }); + const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" } }); /** * @brief Checks inclusion of languages of two NFAs: @p smaller and @p bigger (smaller <= bigger). diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index f3aea2af1..3de3dad65 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -114,6 +114,363 @@ namespace { } } +namespace { + void remove_covered_state(const StateSet& covering_set, const State remove, Nfa& nfa) { + StateSet tmp_targets; // help set to store elements to remove + for (auto move_it = nfa.delta[remove].begin(); move_it != nfa.delta[remove].end();) { // remove trans from covered state + tmp_targets = move_it->targets; + for (State target: tmp_targets) { + nfa.delta.remove(remove, move_it->symbol, target); + } + } + + auto remove_transitions = nfa.delta.get_transitions_to(remove); + for (auto move: remove_transitions) { // transfer transitions from covered state to covering set + for (State switch_target: covering_set) { + nfa.delta.add(move.source, move.symbol, switch_target); + } + nfa.delta.remove(move); + } + + // check final and initial states + nfa.final.erase(remove); + if (nfa.initial.contains(remove)) { + nfa.initial.erase(remove); + for (State new_init: covering_set) { + nfa.initial.insert(new_init); + } + } + } + + void check_covered_and_covering(std::vector& covering_states, // covering sets for each state + std::vector& covering_indexes, // indexes of covering states + std::unordered_map& covered, // map of covered states + std::unordered_map* subset_map, // map of non-covered states + const State Tid, const StateSet T, // current state to check + Nfa& result) { + + std::unordered_map::iterator it = subset_map->begin(); + + // initiate with empty StateSets + covering_states.push_back(mata::utils::OrdVector()); + covering_indexes.push_back(mata::utils::OrdVector()); + + while (it != subset_map->end()) { // goes through all found states + if (it->first.IsSubsetOf(T)) { + // check if T is covered + // if so add covering state to its covering StateSet + + covering_states[Tid].insert(it->first); + covering_indexes[Tid].insert(it->second); + } + else if (T.IsSubsetOf(it->first)) { + // check if state in map is covered + // if so add covering state to its covering StateSet + + covering_states[it->second].insert(T); + covering_indexes[it->second].insert(Tid); + + // check is some already existing state that had a new covering state added turned fully covered + if (it->first == covering_states[it->second]) { + // if any covered state is in the covering set of newly turned covered state, + // then it has to be replaced by its covering set + // + // same applies for any covered state, if it contains newly turned state in theirs + // covering set, then it has to be updated + for (auto covered_pair: covered) { + if (covering_indexes[covered_pair.second].contains(it->second)) { + covering_indexes[covered_pair.second].erase(it->second); + covering_indexes[covered_pair.second].insert(covering_indexes[it->second]); + } + if (covering_indexes[it->second].contains(covered_pair.second)) { + covering_indexes[it->second].erase(covered_pair.second); + covering_indexes[it->second].insert(covering_indexes[covered_pair.second]); + } + } + + // remove covered state from the automaton, replace with covering set + remove_covered_state(covering_indexes[it->second], it->second, result); + + std::unordered_map::iterator temp = it++; + // move state from subset_map to covered + auto transfer = subset_map->extract(temp); + covered.insert(std::move(transfer)); + continue; // skip increasing map pointer + } + } + it++; + } + } + + Nfa residual_with(const Nfa& aut) { // modified algorithm of determinization + + Nfa result; + + //assuming all sets targets are non-empty + std::vector> worklist; + std::unordered_map * subset_map = new std::unordered_map(); + + std::vector covering_states; // check covering set + std::vector covering_indexes; // indexes of covering macrostates + std::unordered_map covered; // map of covered states for transfering new transitions + + result.clear(); + const StateSet S0 = StateSet(aut.initial); + const State S0id = result.add_state(); + result.initial.insert(S0id); + + if (aut.final.intersects_with(S0)) { + result.final.insert(S0id); + } + worklist.emplace_back(S0id, S0); + + (*subset_map)[mata::utils::OrdVector(S0)] = S0id; + covering_states.push_back(mata::utils::OrdVector()); + covering_indexes.push_back(mata::utils::OrdVector()); + + if (aut.delta.empty()) + return result; + + using Iterator = mata::utils::OrdVector::const_iterator; + SynchronizedExistentialSymbolPostIterator synchronized_iterator; + + while (!worklist.empty()) { + const auto Spair = worklist.back(); + worklist.pop_back(); + const StateSet S = Spair.second; + const State Sid = Spair.first; + if (S.empty()) { + // This should not happen assuming all sets targets are non-empty. + break; + } + + // add moves of S to the sync ex iterator + // TODO: shouldn't we also reset first? + for (State q: S) { + mata::utils::push_back(synchronized_iterator, aut.delta[q]); + } + + bool add; // check whether to add transitions + while (synchronized_iterator.advance()) { + add = false; + + // extract post from the sychronized_iterator iterator + const std::vector& moves = synchronized_iterator.get_current(); + Symbol currentSymbol = (*moves.begin())->symbol; + StateSet T = synchronized_iterator.unify_targets(); // new state unify + + auto existingTitr = subset_map->find(T); // check if state was alredy discovered + State Tid; + if (existingTitr != subset_map->end()) { // already visited state + Tid = existingTitr->second; + add = true; + } + else if((existingTitr = covered.find(T)) != covered.end()) { + Tid = existingTitr->second; + } else { // add new state + Tid = result.add_state(); + check_covered_and_covering(covering_states, covering_indexes, covered, subset_map, Tid, T, result); + + if (T != covering_states[Tid]){ // new state is not covered, replace transitions + (*subset_map)[mata::utils::OrdVector(T)] = Tid; // add to map + + if (aut.final.intersects_with(T)) // add to final + result.final.insert(Tid); + + worklist.emplace_back(Tid, T); + add = true; + + } else { // new state is covered + covered[mata::utils::OrdVector(T)] = Tid; + } + } + + if (covered.find(S) != covered.end()) { + continue; // skip generationg any transitions as the source state was covered right now + } + + if (add) { + result.delta.mutable_state_post(Sid).insert(SymbolPost(currentSymbol, Tid)); + } else { + for (State switch_target: covering_indexes[Tid]){ + result.delta.add(Sid, currentSymbol, switch_target); + } + } + } + } + + delete subset_map; + return result; + } + + void residual_recurse_coverable(const std::vector & macrostate_vec, // vector of nfa macrostates + const std::vector & covering_indexes, // sub-vector of macrostates indexes + std::vector & covered, // flags of covered states + std::vector & visited, // flags fo visited states + unsigned long start_index, // starting index for covering_indexes vec + std::unordered_map *subset_map, // mapping of indexes to macrostates + Nfa& nfa) { + + StateSet check_state = macrostate_vec[covering_indexes[start_index]]; + StateSet covering_set; // doesn't contain duplicates + std::vector sub_covering_indexes; // // indexes of covering states + + for (auto i = covering_indexes.begin() + static_cast(start_index+1), e = covering_indexes.end(); i != e; i++) { + if (covered[*i]) // was aready processed + continue; + + if (macrostate_vec[*i].IsSubsetOf(check_state)) { + covering_set.insert(macrostate_vec[*i]); // is never covered + sub_covering_indexes.push_back(*i); + } + } + + if (covering_set == check_state) { // can recurse even without covered :thinking: + + for (unsigned long k = 0; k < sub_covering_indexes.size()-1; k++) { + if (macrostate_vec[sub_covering_indexes[k]].size() == 1) // end on single-sized states + break; + + if (visited[sub_covering_indexes[k]]) // already processed + continue; + + visited[sub_covering_indexes[k]] = true; + + residual_recurse_coverable(macrostate_vec, sub_covering_indexes, covered, visited, k, subset_map, nfa); + } + + covering_set.clear(); // clear variable to store only needed macrostates + for (auto index : sub_covering_indexes) { + if (covered[index] == 0) { + auto macrostate_ptr = subset_map->find(macrostate_vec[index]); + if (macrostate_ptr == subset_map->end()) // should never happen + throw std::runtime_error(std::to_string(__func__) + " couldn't find expected element in a map."); + + covering_set.insert(macrostate_ptr->second); //todo check for null but should be impossible + } + } + + remove_covered_state(covering_set, subset_map->find(check_state)->second, nfa); + covered[covering_indexes[start_index]] = true; + } + + + } + + Nfa residual_after(const Nfa& aut) { + std::unordered_map *subset_map = new std::unordered_map(); + Nfa result; + result = determinize(aut, subset_map); + + std::vector macrostate_vec; // ordered vector of macrostates + macrostate_vec.reserve(subset_map->size()); + for (auto pair: *subset_map) { // order by size from largest to smallest + macrostate_vec.insert(std::upper_bound(macrostate_vec.begin(), macrostate_vec.end(), pair.first, + [](const StateSet & a, const StateSet & b){ return a.size() > b.size(); }), pair.first); + } + + std::vector covered(subset_map->size(), false); // flag of covered states, removed from nfa + std::vector visited(subset_map->size(), false); // flag of processed state + + StateSet covering_set; // doesn't contain duplicates + std::vector covering_indexes; // indexes of covering states + for (unsigned long i = 0; i < macrostate_vec.size()-1; i++) { + if (macrostate_vec[i].size() == 1) // end searching on single-sized macrostates + break; + + if (visited[i]) // was already processed + continue; + + covering_set.clear(); + covering_indexes.clear(); + visited[i] = true; + + for (unsigned long j = i+1; j < macrostate_vec.size(); j++) { // find covering macrostates + if (covered[j]) // if covered there are smaller macrostates, skip + continue; + + if (macrostate_vec[j].IsSubsetOf(macrostate_vec[i])) { // found covering state + covering_set.insert(macrostate_vec[j]); // is not covered + covering_indexes.push_back(j); + } + } + + if (covering_set == macrostate_vec[i]) { + for (unsigned long k = 0; k < covering_indexes.size()-1; k++) { // check resurse coverability + if (macrostate_vec[covering_indexes[k]].size() == 1) // end on single-sized + break; + + if (visited[covering_indexes[k]]) // already processed + continue; + + visited[covering_indexes[k]] = true; + + residual_recurse_coverable(macrostate_vec, covering_indexes, covered, visited, k, subset_map, result); + } + + covering_set.clear(); // clear variable to store only needed macrostates + for (auto index : covering_indexes) { + if (covered[index] == 0) { + auto macrostate_ptr = subset_map->find(macrostate_vec[index]); + if (macrostate_ptr == subset_map->end()) // should never happen + throw std::runtime_error(std::to_string(__func__) + " couldn't find expected element in a map."); + + covering_set.insert(macrostate_ptr->second); + } + } + + remove_covered_state(covering_set, subset_map->find(macrostate_vec[i])->second, result); + covered[i] = true; + } + } + + delete subset_map; // clean up + return result; + } + + Nfa reduce_size_by_residual(const Nfa& aut, StateRenaming &state_renaming, const std::string& type, const std::string& direction){ + Nfa back_determinized = aut; + Nfa result; + + if (direction != "forward" && direction != "backward"){ + throw std::runtime_error(std::to_string(__func__) + + " received an unknown value of the \"direction\" key: " + direction); + } + + // forward canonical residual automaton is firstly backward determinized and + // then the residual construction is done forward, for backward residual automaton + // is it the opposite, so the automaton is reverted once more before and after + // construction, however the first two reversion negate each other out + if (direction == "forward") + back_determinized = revert(back_determinized); + back_determinized = revert(determinize(back_determinized)); // backward deteminization + + // not relly sure how to handle state_renaming + state_renaming; + + // two different implementations of the same algorithm, for type "after" the + // residual automaton and removal of covering states is done after the final + // determinization if finished, for type "with" this residual construction is + // done during the last determinization, both types had similar results in + // effectivity, their output is almost the same expect the transitions, those + // may slightly differ, but number of states is the same for both types + if (type == "with") { + result = residual_with(back_determinized); + } + else if (type == "after") { + result = residual_after(back_determinized); + } else { + throw std::runtime_error(std::to_string(__func__) + + " received an unknown value of the \"type\" key: " + type); + } + + if (direction == "backward") + result = revert(result); + + return result.trim(); + } +} + std::ostream &std::operator<<(std::ostream &os, const mata::nfa::Transition &trans) { // {{{ std::string result = "(" + std::to_string(trans.source) + ", " + std::to_string(trans.symbol) + ", " + std::to_string(trans.target) + ")"; @@ -650,6 +1007,25 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param const std::string& algorithm = params.at("algorithm"); if ("simulation" == algorithm) { result = reduce_size_by_simulation(aut, reduced_state_map); + } + else if ("residual" == algorithm) { + // reduce type either 'after' or 'with' creation of residual automaton + if (!haskey(params, "type")) { + throw std::runtime_error(std::to_string(__func__) + + " requires setting the \"type\" key in the \"params\" argument; " + "received: " + std::to_string(params)); + } + // forward or backward canonical residual automaton + if (!haskey(params, "direction")) { + throw std::runtime_error(std::to_string(__func__) + + " requires setting the \"direction\" key in the \"params\" argument; " + "received: " + std::to_string(params)); + } + + const std::string& residual_type = params.at("type"); + const std::string& residual_direction = params.at("direction"); + + result = reduce_size_by_residual(aut, reduced_state_map, residual_type, residual_direction); } else { throw std::runtime_error(std::to_string(__func__) + " received an unknown value of the \"algorithm\" key: " + algorithm); diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 6598bc3a9..275d7f30e 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -2163,6 +2163,309 @@ TEST_CASE("mata::nfa::reduce_size_by_simulation()") } } +TEST_CASE("mata::nfa::reduce_size_by_residual()") { + Nfa aut; + StateRenaming state_renaming; + ParameterMap params_after, params_with; + params_after["algorithm"] = "residual"; + params_with["algorithm"] = "residual"; + + SECTION("empty automaton") + { + params_after["type"] = "after"; + params_after["direction"] = "forward"; + params_with["type"] = "with"; + params_with["direction"] = "forward"; + + Nfa result_after = reduce(aut, &state_renaming, params_after); + Nfa result_with = reduce(aut, &state_renaming, params_with); + + REQUIRE(result_after.delta.empty()); + REQUIRE(result_after.initial.empty()); + REQUIRE(result_after.final.empty()); + REQUIRE(result_after.is_identical(result_with)); + REQUIRE(are_equivalent(aut, result_after)); + } + + SECTION("simple automaton") + { + params_after["type"] = "after"; + params_after["direction"] = "forward"; + params_with["type"] = "with"; + params_with["direction"] = "forward"; + aut.add_state(2); + aut.initial.insert(1); + + aut.final.insert(2); + Nfa result_after = reduce(aut, &state_renaming, params_after); + Nfa result_with = reduce(aut, &state_renaming, params_with); + + REQUIRE(result_after.num_of_states() == 0); + REQUIRE(result_after.initial.empty()); + REQUIRE(result_after.final.empty()); + REQUIRE(result_after.delta.empty()); + REQUIRE(result_after.is_identical(result_with)); + REQUIRE(are_equivalent(aut, result_after)); + + aut.delta.add(1, 'a', 2); + result_after = reduce(aut, &state_renaming, params_after); + result_with = reduce(aut, &state_renaming, params_with); + + REQUIRE(result_after.num_of_states() == 2); + REQUIRE(result_after.initial[0]); + REQUIRE(result_after.final[1]); + REQUIRE(result_after.delta.contains(0, 'a', 1)); + REQUIRE(result_after.is_identical(result_with)); + REQUIRE(are_equivalent(aut, result_after)); + } + + SECTION("medium automaton") + { + params_after["type"] = "after"; + params_after["direction"] = "forward"; + params_with["type"] = "with"; + params_with["direction"] = "forward"; + aut.add_state(4); + + aut.initial = { 1 }; + aut.final = { 2,3 }; + aut.delta.add(1, 'b', 4); + aut.delta.add(1, 'a', 3); + aut.delta.add(4, 'a', 2); + aut.delta.add(4, 'a', 3); + aut.delta.add(3, 'a', 2); + aut.delta.add(3, 'a', 3); + aut.delta.add(2, 'a', 1); + + Nfa result_after = reduce(aut, &state_renaming, params_after); + Nfa result_with = reduce(aut, &state_renaming, params_with); + + REQUIRE(result_after.num_of_states() == 4); + REQUIRE(result_after.initial[0]); + REQUIRE(result_after.delta.contains(0, 'a', 1)); + REQUIRE(result_after.delta.contains(0, 'b', 2)); + REQUIRE(result_after.delta.contains(1, 'a', 3)); + REQUIRE(!result_after.delta.contains(1, 'b', 3)); + REQUIRE(result_after.delta.contains(2, 'a', 3)); + REQUIRE(!result_after.delta.contains(2, 'a', 2)); + REQUIRE(result_after.delta.contains(3, 'a', 3)); + REQUIRE(result_after.delta.contains(3, 'a', 0)); + REQUIRE(!result_after.delta.contains(3, 'b', 2)); + REQUIRE(result_after.final[1]); + REQUIRE(result_after.final[3]); + REQUIRE(result_after.is_identical(result_with)); + } + + SECTION("big automaton") + { + params_after["type"] = "after"; + params_after["direction"] = "forward"; + params_with["type"] = "with"; + params_with["direction"] = "forward"; + aut.add_state(7); + + aut.initial = { 0 }; + aut.final = { 0,1,2,4,5,6 }; + aut.delta.add(0, 'a', 1); + aut.delta.add(0, 'b', 1); + aut.delta.add(0, 'c', 1); + aut.delta.add(0, 'd', 2); + + aut.delta.add(1, 'a', 1); + aut.delta.add(1, 'b', 1); + aut.delta.add(1, 'c', 1); + aut.delta.add(1, 'd', 1); + + aut.delta.add(2, 'a', 3); + aut.delta.add(2, 'b', 1); + aut.delta.add(2, 'c', 4); + aut.delta.add(2, 'd', 1); + + aut.delta.add(3, 'a', 1); + aut.delta.add(3, 'b', 1); + aut.delta.add(3, 'c', 1); + aut.delta.add(3, 'd', 1); + + aut.delta.add(4, 'a', 1); + aut.delta.add(4, 'b', 1); + aut.delta.add(4, 'c', 1); + aut.delta.add(4, 'd', 5); + + aut.delta.add(5, 'a', 3); + aut.delta.add(5, 'b', 1); + aut.delta.add(5, 'c', 1); + aut.delta.add(5, 'd', 6); + + aut.delta.add(6, 'a', 3); + aut.delta.add(6, 'b', 1); + aut.delta.add(6, 'c', 1); + aut.delta.add(6, 'd', 1); + + Nfa result_after = reduce(aut, &state_renaming, params_after); + Nfa result_with = reduce(aut, &state_renaming, params_with); + + REQUIRE(result_after.num_of_states() == 5); + REQUIRE(result_after.initial[0]); + REQUIRE(result_after.delta.contains(0, 'd', 1)); + REQUIRE(!result_after.delta.contains(0, 'd', 0)); + REQUIRE(!result_after.delta.contains(0, 'd', 2)); + REQUIRE(result_after.delta.contains(0, 'a', 0)); + REQUIRE(result_after.delta.contains(0, 'a', 1)); + REQUIRE(result_after.delta.contains(0, 'b', 0)); + REQUIRE(result_after.delta.contains(0, 'b', 1)); + REQUIRE(result_after.delta.contains(0, 'c', 0)); + REQUIRE(result_after.delta.contains(0, 'c', 1)); + + REQUIRE(result_after.delta.contains(1, 'a', 2)); + REQUIRE(!result_after.delta.contains(1, 'a', 3)); + REQUIRE(result_after.delta.contains(1, 'b', 0)); + REQUIRE(result_after.delta.contains(1, 'b', 1)); + REQUIRE(result_after.delta.contains(1, 'c', 3)); + REQUIRE(!result_after.delta.contains(1, 'c', 2)); + REQUIRE(result_after.delta.contains(1, 'd', 0)); + REQUIRE(result_after.delta.contains(1, 'd', 1)); + + REQUIRE(result_after.delta.contains(2, 'a', 0)); + REQUIRE(result_after.delta.contains(2, 'a', 1)); + REQUIRE(result_after.delta.contains(2, 'b', 0)); + REQUIRE(result_after.delta.contains(2, 'b', 1)); + REQUIRE(result_after.delta.contains(2, 'c', 0)); + REQUIRE(result_after.delta.contains(2, 'c', 1)); + REQUIRE(result_after.delta.contains(2, 'd', 0)); + REQUIRE(result_after.delta.contains(2, 'd', 1)); + + REQUIRE(result_after.delta.contains(3, 'a', 0)); + REQUIRE(result_after.delta.contains(3, 'a', 1)); + REQUIRE(result_after.delta.contains(3, 'b', 0)); + REQUIRE(result_after.delta.contains(3, 'b', 1)); + REQUIRE(result_after.delta.contains(3, 'c', 0)); + REQUIRE(result_after.delta.contains(3, 'c', 1)); + REQUIRE(result_after.delta.contains(3, 'd', 4)); + REQUIRE(!result_after.delta.contains(3, 'd', 2)); + REQUIRE(!result_after.delta.contains(3, 'd', 3)); + + REQUIRE(result_after.delta.contains(4, 'a', 2)); + REQUIRE(result_after.delta.contains(4, 'b', 0)); + REQUIRE(result_after.delta.contains(4, 'b', 1)); + REQUIRE(result_after.delta.contains(4, 'c', 0)); + REQUIRE(result_after.delta.contains(4, 'c', 1)); + REQUIRE(result_after.delta.contains(4, 'd', 1)); + REQUIRE(result_after.delta.contains(4, 'd', 4)); + REQUIRE(!result_after.delta.contains(4, 'd', 0)); + REQUIRE(!result_after.delta.contains(4, 'd', 3)); + REQUIRE(result_after.final[0]); + REQUIRE(result_after.final[1]); + REQUIRE(result_after.final[3]); + REQUIRE(result_after.final[4]); + REQUIRE(are_equivalent(result_after, result_with)); + REQUIRE(are_equivalent(aut, result_after)); + } + + SECTION("backward residual big automaton") + { + params_after["type"] = "after"; + params_after["direction"] = "backward"; + params_with["type"] = "with"; + params_with["direction"] = "backward"; + + aut.add_state(7); + + aut.initial = { 0 }; + aut.final = { 0,1,2,4,5,6 }; + aut.delta.add(0, 'a', 1); + aut.delta.add(0, 'b', 1); + aut.delta.add(0, 'c', 1); + aut.delta.add(0, 'd', 2); + + aut.delta.add(1, 'a', 1); + aut.delta.add(1, 'b', 1); + aut.delta.add(1, 'c', 1); + aut.delta.add(1, 'd', 1); + + aut.delta.add(2, 'a', 3); + aut.delta.add(2, 'b', 1); + aut.delta.add(2, 'c', 4); + aut.delta.add(2, 'd', 1); + + aut.delta.add(3, 'a', 1); + aut.delta.add(3, 'b', 1); + aut.delta.add(3, 'c', 1); + aut.delta.add(3, 'd', 1); + + aut.delta.add(4, 'a', 1); + aut.delta.add(4, 'b', 1); + aut.delta.add(4, 'c', 1); + aut.delta.add(4, 'd', 5); + + aut.delta.add(5, 'a', 3); + aut.delta.add(5, 'b', 1); + aut.delta.add(5, 'c', 1); + aut.delta.add(5, 'd', 6); + + aut.delta.add(6, 'a', 3); + aut.delta.add(6, 'b', 1); + aut.delta.add(6, 'c', 1); + aut.delta.add(6, 'd', 1); + + Nfa result_after = reduce(aut, &state_renaming, params_after); + Nfa result_with = reduce(aut, &state_renaming, params_with); + + result_after.print_to_DOT(std::cout); + + REQUIRE(result_after.num_of_states() == 6); + REQUIRE(result_after.initial[0]); + REQUIRE(result_after.initial[1]); + REQUIRE(result_after.initial[3]); + REQUIRE(result_after.initial[4]); + + REQUIRE(!result_after.delta.contains(0, 'a', 0)); + REQUIRE(!result_after.delta.contains(0, 'c', 2)); + + REQUIRE(result_after.delta.contains(1, 'a', 0)); + REQUIRE(!result_after.delta.contains(1, 'd', 2)); + REQUIRE(!result_after.delta.contains(1, 'd', 3)); + + REQUIRE(result_after.delta.contains(2, 'd', 1)); + REQUIRE(!result_after.delta.contains(2, 'c', 4)); + + REQUIRE(result_after.delta.contains(3, 'c', 2)); + REQUIRE(result_after.delta.contains(3, 'c', 4)); + + REQUIRE(result_after.delta.contains(4, 'd', 2)); + REQUIRE(!result_after.delta.contains(4, 'd', 3)); + + REQUIRE(result_after.delta.contains(5, 'd', 3)); + + REQUIRE(result_after.final[0]); + + REQUIRE(are_equivalent(result_after, result_with)); + REQUIRE(are_equivalent(aut, result_after)); + + } + + SECTION("error checking") + { + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after), + Catch::Contains("requires setting the \"type\" key in the \"params\" argument;")); + + params_after["type"] = "bad_type"; + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after), + Catch::Contains("requires setting the \"direction\" key in the \"params\" argument;")); + + params_after["direction"] = "unknown_direction"; + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after), + Catch::Contains("received an unknown value of the \"direction\" key")); + + params_after["direction"] = "forward"; + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after), + Catch::Contains("received an unknown value of the \"type\" key")); + + params_after["type"] = "after"; + CHECK_NOTHROW(reduce(aut, &state_renaming, params_after)); + + } +} + TEST_CASE("mata::nfa::union_norename()") { Run one{{1},{}}; Run zero{{0}, {}};