diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index c771052a5..59402ec69 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -669,12 +669,23 @@ Nfa complement(const Nfa& aut, const utils::OrdVector& symbols, /** * @brief Compute minimal deterministic automaton. * - * @param[in] aut Automaton whose minimal version to compute. + * @param[in] aut NFA whose minimal version to compute. * @param[in] params Optional parameters to control the minimization algorithm: - * - "algorithm": "brzozowski" + * - "algorithm": "brzozowski" (Default: "brzozowski") * @return Minimal deterministic automaton. */ -Nfa minimize(const Nfa &aut, const ParameterMap& params = { { "algorithm", "brzozowski" } }); +Nfa make_minimal_dfa(const Nfa &nfa, const ParameterMap& params = { { "algorithm", "brzozowski" } }); + +/** + * @brief Compute minimal deterministic automaton. + * + * @param[in] aut DFA whose minimal version to compute. Trimming on the copy of the automaton + * will be performed if the automaton is not already trimmed. + * @param[in] params Optional parameters to control the minimization algorithm: + * - "algorithm": "hopcroft", "brzozowski" (Default: "hopcroft") + * @return Minimal deterministic automaton. + */ +Nfa minimize(const Nfa &dfa, const ParameterMap& params = { { "algorithm", "hopcroft" } }); /** * @brief Determinize automaton. diff --git a/include/mata/nfa/plumbing.hh b/include/mata/nfa/plumbing.hh index 9d1c08f0f..775affd6b 100644 --- a/include/mata/nfa/plumbing.hh +++ b/include/mata/nfa/plumbing.hh @@ -35,7 +35,9 @@ inline void complement( { "minimize", "false"}}) { *result = complement(aut, alphabet, params); } -inline void minimize(Nfa* res, const Nfa &aut) { *res = minimize(aut); } +inline void minimize(Nfa* res, const Nfa &dfa, const ParameterMap& params = {{ "algorithm", "hopcroft" }}) { *res = minimize(dfa, params); } + +inline void make_minimal_dfa(Nfa* res, const Nfa &nfa, const ParameterMap& params = {{ "algorithm", "brzozowski" }}) { *res = make_minimal_dfa(nfa, params); } inline void determinize(Nfa* result, const Nfa& aut, std::unordered_map *subset_map = nullptr) { *result = determinize(aut, subset_map); diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 21fe0caf7..ac6996a38 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -927,27 +927,54 @@ Nfa mata::nfa::algorithms::minimize_brzozowski(const Nfa& aut) { return determinize(revert(determinize(revert(aut)))); } -Nfa mata::nfa::minimize( - const Nfa& aut, - const ParameterMap& params) -{ - Nfa result; - // setting the default algorithm - decltype(algorithms::minimize_brzozowski)* algo = algorithms::minimize_brzozowski; +Nfa mata::nfa::make_minimal_dfa(const Nfa& nfa, const ParameterMap& params) { if (!haskey(params, "algorithm")) { throw std::runtime_error(std::to_string(__func__) + " requires setting the \"algorithm\" key in the \"params\" argument; " "received: " + std::to_string(params)); } + // Setting the algorithm. Default is Brzozowski. const std::string& str_algo = params.at("algorithm"); - if ("brzozowski" == str_algo) { /* default */ } + decltype(algorithms::minimize_brzozowski)* algo = algorithms::minimize_brzozowski; + if (str_algo == "brzozowski") { /* default */ } else { + throw std::runtime_error(std::string(__func__) + + " received an unknown value for the \"algorithm\" key: " + str_algo); + } + + return algo(nfa); +} + +Nfa mata::nfa::minimize(const Nfa &dfa, const ParameterMap& params) +{ + if (!haskey(params, "algorithm")) { throw std::runtime_error(std::to_string(__func__) + - " received an unknown value of the \"algorithm\" key: " + str_algo); + " requires setting the \"algorithm\" key in the \"params\" argument; " + "received: " + std::to_string(params)); } - return algo(aut); + // Setting the algorithm. Default is Hopcroft. + const std::string& str_algo = params.at("algorithm"); + decltype(algorithms::minimize_hopcroft)* algo = algorithms::minimize_hopcroft; + if (str_algo == "hopcroft") { + /* default */; + } else if (str_algo == "brzozowski") { + algo = algorithms::minimize_brzozowski; + } else { + throw std::runtime_error(std::string(__func__) + + " received an unknown value for the \"algorithm\" key: " + str_algo); + } + + // Hopcroft algorithm does not work with non-trimmed automata. + if (str_algo == "hopcroft") { + const BoolVector is_used = dfa.get_useful_states(); + bool is_trimmed = std::all_of(is_used.begin(), is_used.end(), [](bool b) { return b; }); + if (!is_trimmed) { + return algo(Nfa(dfa).trim()); + } + } + return algo(dfa); } // Anonymous namespace for the Hopcroft minimization algorithm. @@ -1295,7 +1322,7 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) { for (const SymbolPost &symbol_post : dfa_trimmed.delta[q]) { assert(symbol_post.targets.size() == 1); const State target = brp.set_idx[*symbol_post.targets.begin()]; - mut_state_post.push_back(SymbolPost{ symbol_post.symbol, StateSet{ target } }); + mut_state_post.emplace_back(SymbolPost{ symbol_post.symbol, StateSet{ target } }); } } diff --git a/tests-integration/src/test-unary-op.cc b/tests-integration/src/test-unary-op.cc index 770610d86..ece07a789 100644 --- a/tests-integration/src/test-unary-op.cc +++ b/tests-integration/src/test-unary-op.cc @@ -36,7 +36,7 @@ int main(int argc, char *argv[]) { // minimization test Nfa aut_min(aut); - aut_min = mata::nfa::minimize(aut_min); + aut_min = mata::nfa::make_minimal_dfa(aut_min); std::cout << "minimize:" << (mata::nfa::are_equivalent(aut, aut_min) ? "ok" : "fail") << std::endl; return EXIT_SUCCESS; diff --git a/tests-integration/src/unary-operations.cc b/tests-integration/src/unary-operations.cc index 9b2cb175f..f1c6a91e1 100644 --- a/tests-integration/src/unary-operations.cc +++ b/tests-integration/src/unary-operations.cc @@ -64,12 +64,12 @@ int main(int argc, char *argv[]) { TIME_END(reduce); Nfa minimized_aut; - TIME_BEGIN(minimize); + TIME_BEGIN(make_minimal_dfa); // > START OF PROFILED CODE // Only minimize and its callees will be measured - mata::nfa::plumbing::minimize(&minimized_aut, aut); + mata::nfa::plumbing::make_minimal_dfa(&minimized_aut, aut); // > END OF PROFILED CODE - TIME_END(minimize); + TIME_END(make_minimal_dfa); Nfa det_aut; TIME_BEGIN(determinize); diff --git a/tests/nfa/nfa-plumbing.cc b/tests/nfa/nfa-plumbing.cc index c85dc81cc..5d9c13a99 100644 --- a/tests/nfa/nfa-plumbing.cc +++ b/tests/nfa/nfa-plumbing.cc @@ -109,7 +109,7 @@ TEST_CASE("Mata::nfa::Plumbing") { SECTION("Mata::nfa::Plumbing::minimize") { FILL_WITH_AUT_A(lhs); - mata::nfa::plumbing::minimize(&result, lhs); + mata::nfa::plumbing::make_minimal_dfa(&result, lhs); CHECK(!result.is_lang_empty()); } diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 2213f4edb..0b13d8114 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -1017,7 +1017,7 @@ TEST_CASE("mata::nfa::minimize() for profiling", "[.profiling],[minimize]") { aut.delta.add(3, 110, 3); aut.delta.add(3, 111, 3); aut.delta.add(3, 114, 3); - minimize(&result, aut); + make_minimal_dfa(&result, aut); } TEST_CASE("mata::nfa::construct() correct calls")