Skip to content

[WIP] Enum arguments for reduce() #519

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: devel
Choose a base branch
from
Draft

[WIP] Enum arguments for reduce() #519

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8d51297
add enum arguments for reduce()
jurajsic Apr 15, 2025
1b37f65
add direction option to reduce_simulation()
jurajsic Apr 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions include/mata/nfa/algorithms.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ Nfa concatenate_eps(const Nfa& lhs, const Nfa& rhs, const Symbol& epsilon, bool
* @param[in] nfa NFA to reduce
* @param[out] state_renaming Map mapping original states to the reduced states.
*/
Nfa reduce_simulation(const Nfa& nfa, StateRenaming &state_renaming);
Nfa reduce_simulation(const Nfa& nfa, StateRenaming &state_renaming, ReductionDirection direction = ReductionDirection::FORWARD);

/**
* @brief Reduce NFA using residual construction.
Expand All @@ -148,7 +148,7 @@ Nfa reduce_simulation(const Nfa& nfa, StateRenaming &state_renaming);
* @param[in] direction Direction of the residual construction (values: "forward", "backward").
*/
Nfa reduce_residual(const Nfa& nfa, StateRenaming &state_renaming,
const std::string& type, const std::string& direction);
const std::string& type, ReductionDirection direction);

/**
* @brief Reduce NFA using residual construction.
Expand Down
6 changes: 5 additions & 1 deletion include/mata/nfa/nfa.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -788,6 +788,9 @@ Nfa determinize(
const Nfa& aut, std::unordered_map<StateSet, State> *subset_map = nullptr,
std::optional<std::function<bool(const Nfa&, const State, const StateSet&)>> macrostate_discover = std::nullopt);

enum class ReductionAlgorithm { SIMULATION, RESIDUAL_AFTER, RESIDUAL_WITH };
enum class ReductionDirection { FORWARD, BACKWARD };

/**
* @brief Reduce the size of the automaton.
*
Expand All @@ -801,7 +804,8 @@ Nfa determinize(
* @return Reduced automaton.
*/
Nfa reduce(const Nfa &aut, StateRenaming *state_renaming = nullptr,
const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" } });
ReductionAlgorithm reduction_algorithm = ReductionAlgorithm::SIMULATION,
ReductionDirection direction = ReductionDirection::FORWARD);

/**
* @brief Checks inclusion of languages of two NFAs: @p smaller and @p bigger (smaller <= bigger).
Expand Down
5 changes: 3 additions & 2 deletions include/mata/nfa/plumbing.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,9 @@ inline void determinize(Nfa* result, const Nfa& aut, std::unordered_map<StateSet
}

inline void reduce(Nfa* result, const Nfa &aut, StateRenaming *state_renaming = nullptr,
const ParameterMap& params = {{ "algorithm", "simulation"}}) {
*result = reduce(aut, state_renaming, params);
ReductionAlgorithm reduction_algorithm = ReductionAlgorithm::SIMULATION,
ReductionDirection direction = ReductionDirection::FORWARD) {
*result = reduce(aut, state_renaming, reduction_algorithm, direction);
}

inline void revert(Nfa* result, const Nfa& aut) { *result = revert(aut); }
Expand Down
65 changes: 23 additions & 42 deletions src/nfa/operations.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1073,40 +1073,23 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa&
}
}

Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, 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));
}

Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, ReductionAlgorithm reduction_algorithm, ReductionDirection direction) {
Nfa result;
std::unordered_map<State,State> reduced_state_map;
const std::string& algorithm = params.at("algorithm");
if ("simulation" == algorithm) {
result = algorithms::reduce_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 = algorithms::reduce_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);
switch(reduction_algorithm) {
case ReductionAlgorithm::SIMULATION:
result = algorithms::reduce_simulation(aut, reduced_state_map, direction);
break;
case ReductionAlgorithm::RESIDUAL_AFTER:
result = algorithms::reduce_residual(aut, reduced_state_map, "after", direction);
break;
case ReductionAlgorithm::RESIDUAL_WITH:
result = algorithms::reduce_residual(aut, reduced_state_map, "with", direction);
break;
default:
throw std::runtime_error(std::to_string(__func__) +
" received an unknown value of the \"reduction_algorithm\" key");
}

if (state_renaming) {
Expand Down Expand Up @@ -1545,10 +1528,13 @@ std::optional<mata::Word> mata::nfa::get_word_from_lang_difference(const Nfa & n
}).get_word();
}

Nfa mata::nfa::algorithms::reduce_simulation(const Nfa& aut, StateRenaming &state_renaming) {
Nfa mata::nfa::algorithms::reduce_simulation(const Nfa& aut, StateRenaming &state_renaming, ReductionDirection direction) {
Nfa result;
const auto sim_relation = algorithms::compute_relation(
aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}});
if (direction != ReductionDirection::FORWARD) {
throw std::runtime_error(std::to_string(__func__) +
" can only reduce simulation by forward direction (for now)");
}
const auto sim_relation = algorithms::compute_relation(aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}});

auto sim_relation_symmetric = sim_relation;
sim_relation_symmetric.restrict_to_symmetric();
Expand Down Expand Up @@ -1617,20 +1603,15 @@ Nfa mata::nfa::algorithms::reduce_simulation(const Nfa& aut, StateRenaming &stat
return result;
}

Nfa mata::nfa::algorithms::reduce_residual(const Nfa& nfa, StateRenaming &state_renaming, const std::string& type, const std::string& direction) {
Nfa mata::nfa::algorithms::reduce_residual(const Nfa& nfa, StateRenaming &state_renaming, const std::string& type, ReductionDirection direction) {
Nfa back_determinized = nfa;
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")
if (direction == ReductionDirection::FORWARD)
back_determinized = revert(back_determinized);
back_determinized = revert(determinize(back_determinized)); // backward deteminization

Expand All @@ -1653,7 +1634,7 @@ Nfa mata::nfa::algorithms::reduce_residual(const Nfa& nfa, StateRenaming &state_
" received an unknown value of the \"type\" key: " + type);
}

if (direction == "backward")
if (direction == ReductionDirection::BACKWARD)
result = revert(result);

return result.trim();
Expand Down
71 changes: 12 additions & 59 deletions tests/nfa/nfa.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3288,19 +3288,11 @@ TEST_CASE("mata::nfa::algorithms::minimize_hopcroft()") {
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);
Nfa result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER);
Nfa result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH);

REQUIRE(result_after.delta.empty());
REQUIRE(result_after.initial.empty());
Expand All @@ -3311,16 +3303,12 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {

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);
Nfa result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER);
Nfa result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH);

REQUIRE(result_after.num_of_states() == 0);
REQUIRE(result_after.initial.empty());
Expand All @@ -3330,8 +3318,8 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {
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);
result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER);
result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH);

REQUIRE(result_after.num_of_states() == 2);
REQUIRE(result_after.initial[0]);
Expand All @@ -3343,10 +3331,6 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {

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 };
Expand All @@ -3359,8 +3343,8 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {
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);
Nfa result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER);
Nfa result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH);

REQUIRE(result_after.num_of_states() == 4);
REQUIRE(result_after.initial[0]);
Expand All @@ -3380,10 +3364,6 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {

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 };
Expand Down Expand Up @@ -3423,8 +3403,8 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {
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);
Nfa result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER);
Nfa result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH);

REQUIRE(result_after.num_of_states() == 5);
REQUIRE(result_after.initial[0]);
Expand Down Expand Up @@ -3485,11 +3465,6 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {

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 };
Expand Down Expand Up @@ -3529,8 +3504,8 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {
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);
Nfa result_after = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_AFTER, ReductionDirection::BACKWARD);
Nfa result_with = reduce(aut, &state_renaming, ReductionAlgorithm::RESIDUAL_WITH, ReductionDirection::BACKWARD);

REQUIRE(result_after.num_of_states() == 6);
REQUIRE(result_after.initial[0]);
Expand Down Expand Up @@ -3562,28 +3537,6 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") {
REQUIRE(are_equivalent(aut, result_after));

}

SECTION("error checking")
{
CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after),
Catch::Matchers::ContainsSubstring("requires setting the \"type\" key in the \"params\" argument;"));

params_after["type"] = "bad_type";
CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after),
Catch::Matchers::ContainsSubstring("requires setting the \"direction\" key in the \"params\" argument;"));

params_after["direction"] = "unknown_direction";
CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after),
Catch::Matchers::ContainsSubstring("received an unknown value of the \"direction\" key"));

params_after["direction"] = "forward";
CHECK_THROWS_WITH(reduce(aut, &state_renaming, params_after),
Catch::Matchers::ContainsSubstring("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()") {
Expand Down
Loading