From f84683eba54f64c4b3b04c761303f09fd1ae8825 Mon Sep 17 00:00:00 2001 From: Veronika Molnarova Date: Wed, 17 Apr 2024 18:35:52 +0200 Subject: [PATCH] Add residual reduction algorithm Two implementations of residual reductions were added to the reduction function. There is possible parametrization using the ParameterMap to select the type of implementation and its direction. The types differ in whether the construction of residual automaton is done after the final determinization or during the determinization. Both implementations had similar results in effectivity and the result automata are mostly the same, but the approaches may provide further inspiration and different optimizations. However, we were not able to find a way to utilize StateRenaming as it is done for simulation, as for residual reduction the automaton is reverted and determinized twice and there is no possible direct connection between the state of the original and tthe result automaton. For this reason, the parameter is not used. Testing of this new functionality is also provided on various-sized automaton, checking the result construction. In every case, the size of both approaches should be the same(applies only for the same direction) and on some automata the results are identical. --- include/mata/nfa/nfa.hh | 8 +- src/nfa/operations.cc | 376 ++++++++++++++++++++++++++++++++++++++++ tests/nfa/nfa.cc | 303 ++++++++++++++++++++++++++++++++ 3 files changed, 685 insertions(+), 2 deletions(-) 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}, {}};