From b98885df3d8cc7e22805890ef05c536649d51ebb Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Sun, 23 Feb 2025 11:41:09 +0100 Subject: [PATCH 1/8] Added backwards simulation --- src/nfa/operations.cc | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index dcdb3fc77..6f23850df 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -3,6 +3,7 @@ #include #include +#include #include // MATA headers @@ -54,10 +55,17 @@ namespace { return lts_for_simulation.compute_simulation(); } - Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming) { + Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { Nfa result; + Nfa aut_m; + + if (simulation_direction == "backward") + aut_m = revert(aut); + else + aut_m = aut; + const auto sim_relation = algorithms::compute_relation( - aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + aut_m, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); auto sim_relation_symmetric = sim_relation; sim_relation_symmetric.restrict_to_symmetric(); @@ -66,7 +74,7 @@ namespace { std::vector quot_proj; sim_relation_symmetric.get_quotient_projection(quot_proj); - const size_t num_of_states = aut.num_of_states(); + const size_t num_of_states = aut_m.num_of_states(); // map each state q of aut to the state of the reduced automaton representing the simulation class of q for (State q = 0; q < num_of_states; ++q) { @@ -83,12 +91,12 @@ namespace { for (State q = 0; q < num_of_states; ++q) { const State q_class_state = state_renaming.at(q); - if (aut.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial + if (aut_m.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial result.initial.insert(q_class_state); } if (quot_proj[q] == q) { // we process only transitions starting from the representative state, this is enough for simulation - for (const auto &q_trans : aut.delta.state_post(q)) { + for (const auto &q_trans : aut_m.delta.state_post(q)) { const StateSet representatives_of_states_to = [&]{ StateSet state_set; for (auto s : q_trans.targets) { @@ -117,12 +125,15 @@ namespace { result.delta.mutable_state_post(q_class_state).insert(SymbolPost(q_trans.symbol, representatives_class_states)); } - if (aut.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final + if (aut_m.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final result.final.insert(q_class_state); } } } + if (simulation_direction == "backward") + result = revert(result); + return result; } @@ -1147,7 +1158,8 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param std::unordered_map reduced_state_map; const std::string& algorithm = params.at("algorithm"); if ("simulation" == algorithm) { - result = reduce_size_by_simulation(aut, reduced_state_map); + const std::string& simulation_direction = params.at("direction"); + result = reduce_size_by_simulation(aut, reduced_state_map, simulation_direction); } else if ("residual" == algorithm) { // reduce type either 'after' or 'with' creation of residual automaton From 5f574fa72f3feecaf244207a6bfc4d7ce6f89b7c Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Sun, 16 Mar 2025 11:07:28 +0100 Subject: [PATCH 2/8] Modified simulation functions --- src/nfa/operations.cc | 74 ++++++++++++++++++++++++++++++++----------- 1 file changed, 55 insertions(+), 19 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 6f23850df..149ad67fd 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -22,7 +22,7 @@ using mata::Symbol; using StateBoolArray = std::vector; ///< Bool array for states in the automaton. namespace { - Simlib::Util::BinaryRelation compute_fw_direct_simulation(const Nfa& aut) { + Simlib::Util::BinaryRelation compute_direct_simulation(const Nfa& aut) { OrdVector used_symbols = aut.delta.get_used_symbols(); mata::Symbol unused_symbol = 0; if (!used_symbols.empty() && *used_symbols.begin() == 0) { @@ -54,18 +54,10 @@ namespace { lts_for_simulation.init(); return lts_for_simulation.compute_simulation(); } - - Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { + + // Merging based on the first and second rule (From the paper 'On NFA Reduction') + Nfa merge_in_one_direction(const Nfa& aut, StateRenaming& state_renaming, const Simlib::Util::BinaryRelation& sim_relation){ Nfa result; - Nfa aut_m; - - if (simulation_direction == "backward") - aut_m = revert(aut); - else - aut_m = aut; - - const auto sim_relation = algorithms::compute_relation( - aut_m, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); auto sim_relation_symmetric = sim_relation; sim_relation_symmetric.restrict_to_symmetric(); @@ -74,7 +66,7 @@ namespace { std::vector quot_proj; sim_relation_symmetric.get_quotient_projection(quot_proj); - const size_t num_of_states = aut_m.num_of_states(); + const size_t num_of_states = aut.num_of_states(); // map each state q of aut to the state of the reduced automaton representing the simulation class of q for (State q = 0; q < num_of_states; ++q) { @@ -91,12 +83,12 @@ namespace { for (State q = 0; q < num_of_states; ++q) { const State q_class_state = state_renaming.at(q); - if (aut_m.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial + if (aut.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial result.initial.insert(q_class_state); } if (quot_proj[q] == q) { // we process only transitions starting from the representative state, this is enough for simulation - for (const auto &q_trans : aut_m.delta.state_post(q)) { + for (const auto &q_trans : aut.delta.state_post(q)) { const StateSet representatives_of_states_to = [&]{ StateSet state_set; for (auto s : q_trans.targets) { @@ -125,14 +117,53 @@ namespace { result.delta.mutable_state_post(q_class_state).insert(SymbolPost(q_trans.symbol, representatives_class_states)); } - if (aut_m.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final + if (aut.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final result.final.insert(q_class_state); } } } + return result; + } + + // Merging based on the third rule (From the paper 'On NFA Reduction') + Nfa merge_in_both_directions(const Nfa& aut, + StateRenaming& state_renaming, + const Simlib::Util::BinaryRelation& fw_relation, + const Simlib::Util::BinaryRelation& bw_relation) + { + Nfa result; - if (simulation_direction == "backward") - result = revert(result); + + return result; + } + + Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { + Nfa result; + + if (simulation_direction == "forward" || simulation_direction == "backward"){ + // Compute the simulation based on simulation_direction + const auto sim_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", simulation_direction}}); + + // Merge states based on the selected rule + result = merge_in_one_direction(aut, state_renaming, sim_relation); + } + else if (simulation_direction == "bidirect"){ + // Compute the forward simulation + const auto sim_fw_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + // Compute the backward simulation + const auto sim_bw_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "backward"}}); + + // Merge states based on the third rule + result = merge_in_both_directions(aut, state_renaming, sim_fw_relation, sim_bw_relation); + } + else { + // TODO throw some error + std::cerr << "TODO error" << std::endl; + } return result; } @@ -1139,7 +1170,12 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& const std::string& relation = params.at("relation"); const std::string& direction = params.at("direction"); if ("simulation" == relation && direction == "forward") { - return compute_fw_direct_simulation(aut); + return compute_direct_simulation(aut); + } + else if ("simulation" == relation && direction == "backward") { + // When computing the reverse simulation, we simply revert the automaton + Nfa tmp_aut = revert(aut); + return compute_direct_simulation(tmp_aut); } else { throw std::runtime_error(std::to_string(__func__) + From 9736dc3307831b424d506598f1b455f190a0e13f Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Sun, 16 Mar 2025 12:44:11 +0100 Subject: [PATCH 3/8] Forward and backward simulation --- src/nfa/operations.cc | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 149ad67fd..11ea369d5 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -140,13 +140,25 @@ namespace { Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { Nfa result; - if (simulation_direction == "forward" || simulation_direction == "backward"){ + if (simulation_direction == "forward"){ // Compute the simulation based on simulation_direction const auto sim_relation = algorithms::compute_relation( - aut, ParameterMap{{ "relation", "simulation"}, { "direction", simulation_direction}}); + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); // Merge states based on the selected rule result = merge_in_one_direction(aut, state_renaming, sim_relation); + return result; + } + else if (simulation_direction == "backward"){ + Nfa aut_r = revert(aut); + + // Compute the simulation based on simulation_direction + const auto sim_relation = algorithms::compute_relation( + aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + // Merge states based on the selected rule + result = merge_in_one_direction(aut_r, state_renaming, sim_relation); + return revert(result); } else if (simulation_direction == "bidirect"){ // Compute the forward simulation @@ -1172,11 +1184,6 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& if ("simulation" == relation && direction == "forward") { return compute_direct_simulation(aut); } - else if ("simulation" == relation && direction == "backward") { - // When computing the reverse simulation, we simply revert the automaton - Nfa tmp_aut = revert(aut); - return compute_direct_simulation(tmp_aut); - } else { throw std::runtime_error(std::to_string(__func__) + " received an unknown value of the \"relation\" key: " + relation); From 19c3543f53082d0cc1d53ba7e95d82e341cfcfb7 Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Wed, 26 Mar 2025 18:44:31 +0100 Subject: [PATCH 4/8] Simulation fixpoint --- src/nfa/operations.cc | 83 ++++++++++++++++++++++++++++++++++++++----- 1 file changed, 75 insertions(+), 8 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 11ea369d5..0343a50bf 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -8,6 +8,7 @@ // MATA headers #include "mata/nfa/delta.hh" +#include "mata/nfa/types.hh" #include "mata/utils/sparse-set.hh" #include "mata/nfa/nfa.hh" #include "mata/nfa/algorithms.hh" @@ -54,9 +55,12 @@ namespace { lts_for_simulation.init(); return lts_for_simulation.compute_simulation(); } + // Merging based on the first and second rule (From the paper 'On NFA Reduction') - Nfa merge_in_one_direction(const Nfa& aut, StateRenaming& state_renaming, const Simlib::Util::BinaryRelation& sim_relation){ + Nfa merge_in_one_direction(const Nfa& aut, StateRenaming& state_renaming, + const Simlib::Util::BinaryRelation& sim_relation, + const bool little_brother){ Nfa result; auto sim_relation_symmetric = sim_relation; @@ -97,14 +101,18 @@ namespace { return state_set; }(); - // get the class states of those representatives that are not simulated by another representative in representatives_of_states_to + // get the class states of those representatives that are not simulated by another representative in representatives_of_states_toA + // this technique is known as little brother elimination. It can pose problems to simulation fixpoint StateSet representatives_class_states; for (const State s : representatives_of_states_to) { bool is_state_important = true; // if true, we need to keep the transition from q to s - for (const State p : representatives_of_states_to) { - if (s != p && sim_relation.get(s, p)) { // if p (different from s) simulates s - is_state_important = false; // as p simulates s, the transition from q to s is not important to keep, as it is subsumed in transition from q to p - break; + + if (little_brother){ + for (const State p : representatives_of_states_to) { + if (s != p && sim_relation.get(s, p)) { // if p (different from s) simulates s + is_state_important = false; // as p simulates s, the transition from q to s is not important to keep, as it is subsumed in transition from q to p + break; + } } } if (is_state_important) { @@ -137,6 +145,57 @@ namespace { return result; } + Nfa simulation_fixpoint(const Nfa& aut){ + Nfa result; + Nfa tmp = aut; + + std::unordered_map state_map_dummy; + + bool forward_eq = false; + bool backward_eq = false; + + while (!(forward_eq && backward_eq)){ + + state_map_dummy.clear(); + + // Compute the forward simulation TODO take out into a function + const auto sim_relation_fw = algorithms::compute_relation( + tmp, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + result = merge_in_one_direction(tmp, state_map_dummy, sim_relation_fw, false); + + if (tmp.num_of_states() == result.num_of_states()){ + forward_eq = true; + } + else { + forward_eq = false; + } + + tmp = result; + + state_map_dummy.clear(); + + // Compute the backward simulation TODO take out into a function + Nfa aut_r = revert(tmp); + const auto sim_relation_bw = algorithms::compute_relation( + aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + result = merge_in_one_direction(aut_r, state_map_dummy, sim_relation_bw, false); + result = revert(result); + + if (tmp.num_of_states() == result.num_of_states()){ + backward_eq = true; + } + else { + backward_eq = false; + } + + tmp = result; + } + + result = tmp; + return result; + } + Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { Nfa result; @@ -146,7 +205,7 @@ namespace { aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); // Merge states based on the selected rule - result = merge_in_one_direction(aut, state_renaming, sim_relation); + result = merge_in_one_direction(aut, state_renaming, sim_relation, true); return result; } else if (simulation_direction == "backward"){ @@ -157,7 +216,7 @@ namespace { aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); // Merge states based on the selected rule - result = merge_in_one_direction(aut_r, state_renaming, sim_relation); + result = merge_in_one_direction(aut_r, state_renaming, sim_relation, true); return revert(result); } else if (simulation_direction == "bidirect"){ @@ -171,6 +230,14 @@ namespace { // Merge states based on the third rule result = merge_in_both_directions(aut, state_renaming, sim_fw_relation, sim_bw_relation); + std::cerr << "ERROR: bidirect not implemented yet"; + + return result; + } + else if (simulation_direction == "fixpoint"){ + // TODO this does not support state renaming + result = simulation_fixpoint(aut); + return result; } else { // TODO throw some error From 4b5f4f2b1b487ee8c6c813ca38b75dd506ced2f6 Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Wed, 2 Apr 2025 19:22:39 +0200 Subject: [PATCH 5/8] Created a separate file for simulations --- include/mata/nfa/algorithms.hh | 11 ++ src/CMakeLists.txt | 1 + src/nfa/operations.cc | 228 +------------------------------ src/nfa/reductionSimulation.cc | 240 +++++++++++++++++++++++++++++++++ 4 files changed, 254 insertions(+), 226 deletions(-) create mode 100644 src/nfa/reductionSimulation.cc diff --git a/include/mata/nfa/algorithms.hh b/include/mata/nfa/algorithms.hh index 18e381bc0..8943a7c49 100644 --- a/include/mata/nfa/algorithms.hh +++ b/include/mata/nfa/algorithms.hh @@ -168,6 +168,17 @@ Nfa reduce_residual_with(const Nfa& nfa); */ Nfa reduce_residual_after(const Nfa& nfa); + +/** + * @brief TODO + */ +Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction); + +/** + * @brief TODO + */ +Simlib::Util::BinaryRelation compute_direct_simulation(const Nfa& aut); + } // Namespace mata::nfa::algorithms. #endif // MATA_NFA_INTERNALS_HH_ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0bfc68a4b..38bacd751 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -23,6 +23,7 @@ add_library(libmata STATIC nfa/delta.cc nfa/operations.cc nfa/builder.cc + nfa/reductionSimulation.cc nft/nft.cc nft/inclusion.cc diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 0343a50bf..66906a88c 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -23,230 +23,6 @@ using mata::Symbol; using StateBoolArray = std::vector; ///< Bool array for states in the automaton. namespace { - Simlib::Util::BinaryRelation compute_direct_simulation(const Nfa& aut) { - OrdVector used_symbols = aut.delta.get_used_symbols(); - mata::Symbol unused_symbol = 0; - if (!used_symbols.empty() && *used_symbols.begin() == 0) { - auto it = used_symbols.begin(); - unused_symbol = *it + 1; - ++it; - const auto used_symbols_end = used_symbols.end(); - while (it != used_symbols_end && unused_symbol == *it) { - unused_symbol = *it + 1; - ++it; - } - if (unused_symbol == 0) { // sanity check to see if we did not use the full range of mata::Symbol - throw std::runtime_error("all symbols are used, we cannot compute simulation reduction"); - } - } - - const size_t state_num{ aut.num_of_states() }; - Simlib::ExplicitLTS lts_for_simulation(state_num); - - for (const Transition& transition : aut.delta.transitions()) { - lts_for_simulation.add_transition(transition.source, transition.symbol, transition.target); - } - - // final states cannot be simulated by nonfinal -> we add new selfloops over final states with new symbol in LTS - for (State final_state : aut.final) { - lts_for_simulation.add_transition(final_state, unused_symbol, final_state); - } - - lts_for_simulation.init(); - return lts_for_simulation.compute_simulation(); - } - - - // Merging based on the first and second rule (From the paper 'On NFA Reduction') - Nfa merge_in_one_direction(const Nfa& aut, StateRenaming& state_renaming, - const Simlib::Util::BinaryRelation& sim_relation, - const bool little_brother){ - Nfa result; - - auto sim_relation_symmetric = sim_relation; - sim_relation_symmetric.restrict_to_symmetric(); - - // for State q, quot_proj[q] should be the representative state representing the symmetric class of states in simulation - std::vector quot_proj; - sim_relation_symmetric.get_quotient_projection(quot_proj); - - const size_t num_of_states = aut.num_of_states(); - - // map each state q of aut to the state of the reduced automaton representing the simulation class of q - for (State q = 0; q < num_of_states; ++q) { - const State qReprState = quot_proj[q]; - if (state_renaming.count(qReprState) == 0) { // we need to map q's class to a new state in reducedAut - const State qClass = result.add_state(); - state_renaming[qReprState] = qClass; - state_renaming[q] = qClass; - } else { - state_renaming[q] = state_renaming[qReprState]; - } - } - - for (State q = 0; q < num_of_states; ++q) { - const State q_class_state = state_renaming.at(q); - - if (aut.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial - result.initial.insert(q_class_state); - } - - if (quot_proj[q] == q) { // we process only transitions starting from the representative state, this is enough for simulation - for (const auto &q_trans : aut.delta.state_post(q)) { - const StateSet representatives_of_states_to = [&]{ - StateSet state_set; - for (auto s : q_trans.targets) { - state_set.insert(quot_proj[s]); - } - return state_set; - }(); - - // get the class states of those representatives that are not simulated by another representative in representatives_of_states_toA - // this technique is known as little brother elimination. It can pose problems to simulation fixpoint - StateSet representatives_class_states; - for (const State s : representatives_of_states_to) { - bool is_state_important = true; // if true, we need to keep the transition from q to s - - if (little_brother){ - for (const State p : representatives_of_states_to) { - if (s != p && sim_relation.get(s, p)) { // if p (different from s) simulates s - is_state_important = false; // as p simulates s, the transition from q to s is not important to keep, as it is subsumed in transition from q to p - break; - } - } - } - if (is_state_important) { - representatives_class_states.insert(state_renaming.at(s)); - } - } - - // add the transition 'q_class_state-q_trans.symbol->representatives_class_states' at the end of transition list of transitions starting from q_class_state - // as the q_trans.symbol should be the largest symbol we saw (as we iterate trough getTransitionsFromState(q) which is ordered) - result.delta.mutable_state_post(q_class_state).insert(SymbolPost(q_trans.symbol, representatives_class_states)); - } - - if (aut.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final - result.final.insert(q_class_state); - } - } - } - return result; - } - - // Merging based on the third rule (From the paper 'On NFA Reduction') - Nfa merge_in_both_directions(const Nfa& aut, - StateRenaming& state_renaming, - const Simlib::Util::BinaryRelation& fw_relation, - const Simlib::Util::BinaryRelation& bw_relation) - { - Nfa result; - - - return result; - } - - Nfa simulation_fixpoint(const Nfa& aut){ - Nfa result; - Nfa tmp = aut; - - std::unordered_map state_map_dummy; - - bool forward_eq = false; - bool backward_eq = false; - - while (!(forward_eq && backward_eq)){ - - state_map_dummy.clear(); - - // Compute the forward simulation TODO take out into a function - const auto sim_relation_fw = algorithms::compute_relation( - tmp, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); - result = merge_in_one_direction(tmp, state_map_dummy, sim_relation_fw, false); - - if (tmp.num_of_states() == result.num_of_states()){ - forward_eq = true; - } - else { - forward_eq = false; - } - - tmp = result; - - state_map_dummy.clear(); - - // Compute the backward simulation TODO take out into a function - Nfa aut_r = revert(tmp); - const auto sim_relation_bw = algorithms::compute_relation( - aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); - - result = merge_in_one_direction(aut_r, state_map_dummy, sim_relation_bw, false); - result = revert(result); - - if (tmp.num_of_states() == result.num_of_states()){ - backward_eq = true; - } - else { - backward_eq = false; - } - - tmp = result; - } - - result = tmp; - return result; - } - - Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { - Nfa result; - - if (simulation_direction == "forward"){ - // Compute the simulation based on simulation_direction - const auto sim_relation = algorithms::compute_relation( - aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); - - // Merge states based on the selected rule - result = merge_in_one_direction(aut, state_renaming, sim_relation, true); - return result; - } - else if (simulation_direction == "backward"){ - Nfa aut_r = revert(aut); - - // Compute the simulation based on simulation_direction - const auto sim_relation = algorithms::compute_relation( - aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); - - // Merge states based on the selected rule - result = merge_in_one_direction(aut_r, state_renaming, sim_relation, true); - return revert(result); - } - else if (simulation_direction == "bidirect"){ - // Compute the forward simulation - const auto sim_fw_relation = algorithms::compute_relation( - aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); - - // Compute the backward simulation - const auto sim_bw_relation = algorithms::compute_relation( - aut, ParameterMap{{ "relation", "simulation"}, { "direction", "backward"}}); - - // Merge states based on the third rule - result = merge_in_both_directions(aut, state_renaming, sim_fw_relation, sim_bw_relation); - std::cerr << "ERROR: bidirect not implemented yet"; - - return result; - } - else if (simulation_direction == "fixpoint"){ - // TODO this does not support state renaming - result = simulation_fixpoint(aut); - return result; - } - else { - // TODO throw some error - std::cerr << "TODO error" << std::endl; - } - - return result; - } - void remove_covered_state(const StateSet& covering_set, const State remove, Nfa& nfa) { StateSet tmp_targets; // help set to store elements to remove auto delta_begin = nfa.delta[remove].begin(); @@ -1249,7 +1025,7 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& const std::string& relation = params.at("relation"); const std::string& direction = params.at("direction"); if ("simulation" == relation && direction == "forward") { - return compute_direct_simulation(aut); + return mata::nfa::algorithms::compute_direct_simulation(aut); } else { throw std::runtime_error(std::to_string(__func__) + @@ -1269,7 +1045,7 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param const std::string& algorithm = params.at("algorithm"); if ("simulation" == algorithm) { const std::string& simulation_direction = params.at("direction"); - result = reduce_size_by_simulation(aut, reduced_state_map, simulation_direction); + result = mata::nfa::algorithms::reduce_size_by_simulation(aut, reduced_state_map, simulation_direction); } else if ("residual" == algorithm) { // reduce type either 'after' or 'with' creation of residual automaton diff --git a/src/nfa/reductionSimulation.cc b/src/nfa/reductionSimulation.cc new file mode 100644 index 000000000..bb296e375 --- /dev/null +++ b/src/nfa/reductionSimulation.cc @@ -0,0 +1,240 @@ +/* nfa.cc -- reduction on NFA + */ + +#include + +// MATA headers +#include "mata/nfa/types.hh" +#include "mata/nfa/delta.hh" +#include "mata/nfa/nfa.hh" +#include "mata/nfa/algorithms.hh" +#include + +using namespace mata::utils; +using namespace mata::nfa; + +namespace { + // Merging based on the first and second rule (From the paper 'On NFA Reduction') + Nfa merge_in_one_direction(const Nfa& aut, StateRenaming& state_renaming, + const Simlib::Util::BinaryRelation& sim_relation, + const bool little_brother){ + Nfa result; + + auto sim_relation_symmetric = sim_relation; + sim_relation_symmetric.restrict_to_symmetric(); + + // for State q, quot_proj[q] should be the representative state representing the symmetric class of states in simulation + std::vector quot_proj; + sim_relation_symmetric.get_quotient_projection(quot_proj); + + const size_t num_of_states = aut.num_of_states(); + + // map each state q of aut to the state of the reduced automaton representing the simulation class of q + for (State q = 0; q < num_of_states; ++q) { + const State qReprState = quot_proj[q]; + if (state_renaming.count(qReprState) == 0) { // we need to map q's class to a new state in reducedAut + const State qClass = result.add_state(); + state_renaming[qReprState] = qClass; + state_renaming[q] = qClass; + } else { + state_renaming[q] = state_renaming[qReprState]; + } + } + + for (State q = 0; q < num_of_states; ++q) { + const State q_class_state = state_renaming.at(q); + + if (aut.initial[q]) { // if a symmetric class contains initial state, then the whole class should be initial + result.initial.insert(q_class_state); + } + + if (quot_proj[q] == q) { // we process only transitions starting from the representative state, this is enough for simulation + for (const auto &q_trans : aut.delta.state_post(q)) { + const StateSet representatives_of_states_to = [&]{ + StateSet state_set; + for (auto s : q_trans.targets) { + state_set.insert(quot_proj[s]); + } + return state_set; + }(); + + // get the class states of those representatives that are not simulated by another representative in representatives_of_states_toA + // this technique is known as little brother elimination. It can pose problems to simulation fixpoint + StateSet representatives_class_states; + for (const State s : representatives_of_states_to) { + bool is_state_important = true; // if true, we need to keep the transition from q to s + + if (little_brother){ + for (const State p : representatives_of_states_to) { + if (s != p && sim_relation.get(s, p)) { // if p (different from s) simulates s + is_state_important = false; // as p simulates s, the transition from q to s is not important to keep, as it is subsumed in transition from q to p + break; + } + } + } + if (is_state_important) { + representatives_class_states.insert(state_renaming.at(s)); + } + } + + // add the transition 'q_class_state-q_trans.symbol->representatives_class_states' at the end of transition list of transitions starting from q_class_state + // as the q_trans.symbol should be the largest symbol we saw (as we iterate trough getTransitionsFromState(q) which is ordered) + result.delta.mutable_state_post(q_class_state).insert(SymbolPost(q_trans.symbol, representatives_class_states)); + } + + if (aut.final[q]) { // if q is final, then all states in its class are final => we make q_class_state final + result.final.insert(q_class_state); + } + } + } + return result; + } + + // Merging based on the third rule (From the paper 'On NFA Reduction') + Nfa merge_in_both_directions(const Nfa& aut, + StateRenaming& state_renaming, + const Simlib::Util::BinaryRelation& fw_relation, + const Simlib::Util::BinaryRelation& bw_relation) + { + Nfa result; + + // TODO TODAY!!! + + return result; + } + + Nfa simulation_fixpoint(const Nfa& aut){ + Nfa result; + Nfa tmp = aut; + + std::unordered_map state_map_dummy; + + bool forward_eq = false; + bool backward_eq = false; + + while (!(forward_eq && backward_eq)){ + + state_map_dummy.clear(); + + // Compute the forward simulation TODO take out into a function + const auto sim_relation_fw = algorithms::compute_relation( + tmp, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + result = merge_in_one_direction(tmp, state_map_dummy, sim_relation_fw, false); + + if (tmp.num_of_states() == result.num_of_states()){ + forward_eq = true; + } + else { + forward_eq = false; + } + + tmp = result; + + state_map_dummy.clear(); + + // Compute the backward simulation TODO take out into a function + Nfa aut_r = revert(tmp); + const auto sim_relation_bw = algorithms::compute_relation( + aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + result = merge_in_one_direction(aut_r, state_map_dummy, sim_relation_bw, false); + result = revert(result); + + if (tmp.num_of_states() == result.num_of_states()){ + backward_eq = true; + } + else { + backward_eq = false; + } + + tmp = result; + } + + result = tmp; + return result; + } +} + +Nfa mata::nfa::algorithms::reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming, const std::string& simulation_direction) { + Nfa result; + + if (simulation_direction == "forward"){ + // Compute the simulation based on simulation_direction + const auto sim_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + // Merge states based on the selected rule + result = merge_in_one_direction(aut, state_renaming, sim_relation, true); + return result; + } + else if (simulation_direction == "backward"){ + Nfa aut_r = revert(aut); + + // Compute the simulation based on simulation_direction + const auto sim_relation = algorithms::compute_relation( + aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + // Merge states based on the selected rule + result = merge_in_one_direction(aut_r, state_renaming, sim_relation, true); + return revert(result); + } + else if (simulation_direction == "bidirect"){ + // Compute the forward simulation + const auto sim_fw_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + // Compute the backward simulation + const auto sim_bw_relation = algorithms::compute_relation( + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "backward"}}); + + // Merge states based on the third rule + result = merge_in_both_directions(aut, state_renaming, sim_fw_relation, sim_bw_relation); + std::cerr << "ERROR: bidirect not implemented yet"; + + return result; + } + else if (simulation_direction == "fixpoint"){ + // TODO this does not support state renaming + result = simulation_fixpoint(aut); + return result; + } + else { + // TODO throw some error + std::cerr << "TODO error" << std::endl; + } + + return result; +} + +Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_direct_simulation(const Nfa& aut) { + OrdVector used_symbols = aut.delta.get_used_symbols(); + mata::Symbol unused_symbol = 0; + if (!used_symbols.empty() && *used_symbols.begin() == 0) { + auto it = used_symbols.begin(); + unused_symbol = *it + 1; + ++it; + const auto used_symbols_end = used_symbols.end(); + while (it != used_symbols_end && unused_symbol == *it) { + unused_symbol = *it + 1; + ++it; + } + if (unused_symbol == 0) { // sanity check to see if we did not use the full range of mata::Symbol + throw std::runtime_error("all symbols are used, we cannot compute simulation reduction"); + } + } + + const size_t state_num{ aut.num_of_states() }; + Simlib::ExplicitLTS lts_for_simulation(state_num); + + for (const Transition& transition : aut.delta.transitions()) { + lts_for_simulation.add_transition(transition.source, transition.symbol, transition.target); + } + + // final states cannot be simulated by nonfinal -> we add new selfloops over final states with new symbol in LTS + for (State final_state : aut.final) { + lts_for_simulation.add_transition(final_state, unused_symbol, final_state); + } + + lts_for_simulation.init(); + return lts_for_simulation.compute_simulation(); +} From e624707be8a09b8b2fc405c7e6171f4c900c8ba3 Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Wed, 16 Apr 2025 18:50:29 +0200 Subject: [PATCH 6/8] Rule 3 implemented --- src/nfa/operations.cc | 4 ++ src/nfa/reductionSimulation.cc | 127 +++++++++++++++++++++++++++++++-- 2 files changed, 127 insertions(+), 4 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 66906a88c..0376521e5 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1027,6 +1027,10 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& if ("simulation" == relation && direction == "forward") { return mata::nfa::algorithms::compute_direct_simulation(aut); } + if ("simulation" == relation && direction == "backward") { + Nfa aut_r = revert(aut); + return mata::nfa::algorithms::compute_direct_simulation(aut_r); + } else { throw std::runtime_error(std::to_string(__func__) + " received an unknown value of the \"relation\" key: " + relation); diff --git a/src/nfa/reductionSimulation.cc b/src/nfa/reductionSimulation.cc index bb296e375..303e99f5b 100644 --- a/src/nfa/reductionSimulation.cc +++ b/src/nfa/reductionSimulation.cc @@ -1,14 +1,20 @@ /* nfa.cc -- reduction on NFA */ +#include +#include #include // MATA headers +#include "mata/alphabet.hh" #include "mata/nfa/types.hh" #include "mata/nfa/delta.hh" #include "mata/nfa/nfa.hh" #include "mata/nfa/algorithms.hh" +#include "mata/simlib/util/binary_relation.hh" #include +#include +#include using namespace mata::utils; using namespace mata::nfa; @@ -90,6 +96,28 @@ namespace { return result; } + void rename_states(StateRenaming& state_renaming, + State p, + State q) + { + // States p and q are in relation such that "p is simulated by q" + state_renaming[p] = q; + + // Now the state renaming must be updated, firstly in the forward direction + // If (q is simulated by x) and (p is simulated by q) -> (p is simulated by x) + if (state_renaming.count(q) != 0) { + state_renaming[p] = state_renaming[q]; + } + + // Now the backwards direction + // if (x is simulated by p) and (p is simulated as q) -> (x is simulated as q) + for (auto& pair: state_renaming) { + if (pair.second == p) { + state_renaming[pair.first] = state_renaming[p]; + } + } + } + // Merging based on the third rule (From the paper 'On NFA Reduction') Nfa merge_in_both_directions(const Nfa& aut, StateRenaming& state_renaming, @@ -98,7 +126,98 @@ namespace { { Nfa result; - // TODO TODAY!!! + const size_t num_of_states = aut.num_of_states(); + + Simlib::Util::BinaryRelation work_relation; + work_relation.resize(num_of_states, 0); + + // Fill the work relation + for (size_t i = 0; i < num_of_states; i++){ + for (size_t j = 0; j < num_of_states; j++){ + work_relation.set(i, j, bw_relation.get(i, j) & fw_relation.get(i, j)); + //std::cerr << work_relation.get(i, j) << " "; + } + //std::cerr << std::endl; + } + + // Set the state renaming + std::vector simulated_states {}; + for (State p = 0; p < num_of_states; p++) { + // Find the first occurence of one (ignore diagonal) + for (State q = 0; q < num_of_states; q++){ + // If the one is before diagonal (symmetric pairs must NOT merge one into another) + if (work_relation.get(p, q) == 1 && p != q && p > q) { + // p is simulated by q, rename p + rename_states(state_renaming, p, q); + simulated_states.push_back(p); + break; + } + // If the one is after diagonal + if (work_relation.get(p, q) == 1 && p != q && p < q) { + // Check for symmetry + if (work_relation.get(q, p) == 1){ + continue; // Do nothing + } + rename_states(state_renaming, p, q); + simulated_states.push_back(p); + break; + } + } + } + + // Rename the states the will not be deleted + size_t renamed = 0; + for (State p = 0; p < num_of_states; p++) { + // The state is not simulated + if (state_renaming.count(p) == 0) { + // Rename the state + state_renaming[p] = renamed; + + // Rename every occurence of p in state_renaming are replace it with its new name + for (auto& pair : state_renaming) { + if (pair.second == p) { + state_renaming[pair.first] = renamed; + } + } + + // Increment for the next state + renamed++; + } + + } + + // Add the new states + result.add_state(num_of_states - simulated_states.size() - 1); + + // Build the resulting automaton based on the simulated_states and state_renaming + for (State p = 0; p < num_of_states; ++p) { + // If the state is simulated, its not added to the resulting automaton + if (std::find(simulated_states.begin(), simulated_states.end(), p) != simulated_states.end()) { + continue; + } + + // The current state + State renamed_state = state_renaming[p]; + + // Check for Initial + if (aut.initial[p]){ + result.initial.insert(renamed_state); + } + + // Copy transitions + for (const auto &p_trans_symbol : aut.delta.state_post(p)) { + for (const auto &target_state :p_trans_symbol.targets){ + // The transition is translated + result.delta.add(renamed_state, p_trans_symbol.symbol, state_renaming[target_state]); + } + } + + // Check for Final + if (aut.final[p]){ + result.final.insert(renamed_state); + } + + } return result; } @@ -168,17 +287,18 @@ Nfa mata::nfa::algorithms::reduce_size_by_simulation(const Nfa& aut, StateRenami return result; } else if (simulation_direction == "backward"){ - Nfa aut_r = revert(aut); // Compute the simulation based on simulation_direction const auto sim_relation = algorithms::compute_relation( - aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + aut, ParameterMap{{ "relation", "simulation"}, { "direction", "backward"}}); // Merge states based on the selected rule + Nfa aut_r = revert(aut); result = merge_in_one_direction(aut_r, state_renaming, sim_relation, true); return revert(result); } else if (simulation_direction == "bidirect"){ + // TODO this does not support state renaming // Compute the forward simulation const auto sim_fw_relation = algorithms::compute_relation( aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); @@ -189,7 +309,6 @@ Nfa mata::nfa::algorithms::reduce_size_by_simulation(const Nfa& aut, StateRenami // Merge states based on the third rule result = merge_in_both_directions(aut, state_renaming, sim_fw_relation, sim_bw_relation); - std::cerr << "ERROR: bidirect not implemented yet"; return result; } From 58af2e9ff474184140e42b3bf1dc9a23fed4434a Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Wed, 23 Apr 2025 21:58:26 +0200 Subject: [PATCH 7/8] Fixpoint with 3. rule --- src/nfa/reductionSimulation.cc | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/src/nfa/reductionSimulation.cc b/src/nfa/reductionSimulation.cc index 303e99f5b..88e6a8fe3 100644 --- a/src/nfa/reductionSimulation.cc +++ b/src/nfa/reductionSimulation.cc @@ -230,9 +230,32 @@ namespace { bool forward_eq = false; bool backward_eq = false; + bool bidirect_eq = false; - while (!(forward_eq && backward_eq)){ - + while (!(forward_eq && backward_eq && bidirect_eq)){ + + // MERGE IN BOTH DIRECTIONS + state_map_dummy.clear(); + + const auto sim_birelation_fw = algorithms::compute_relation( + tmp, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + Nfa aut_bir = revert(tmp); + const auto sim_birelation_bw = algorithms::compute_relation( + aut_bir, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); + + result = merge_in_both_directions(tmp, state_map_dummy, sim_birelation_fw, sim_birelation_bw); + + if (tmp.num_of_states() == result.num_of_states()){ + bidirect_eq = true; + } + else { + bidirect_eq = false; + } + + tmp = result; + + // MERGE IN FORWARD DIRECTION state_map_dummy.clear(); // Compute the forward simulation TODO take out into a function @@ -249,6 +272,7 @@ namespace { tmp = result; + // MERGE IN BACKWARD DIRECTION state_map_dummy.clear(); // Compute the backward simulation TODO take out into a function From 0be5eae54a4a51af3b8d77f6efdca0f4cb0bd06b Mon Sep 17 00:00:00 2001 From: Samuel Luptak Date: Thu, 5 Jun 2025 09:37:45 +0200 Subject: [PATCH 8/8] Final touches --- src/nfa/reductionSimulation.cc | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/nfa/reductionSimulation.cc b/src/nfa/reductionSimulation.cc index 88e6a8fe3..60302bdb6 100644 --- a/src/nfa/reductionSimulation.cc +++ b/src/nfa/reductionSimulation.cc @@ -2,7 +2,6 @@ */ #include -#include #include // MATA headers @@ -135,9 +134,7 @@ namespace { for (size_t i = 0; i < num_of_states; i++){ for (size_t j = 0; j < num_of_states; j++){ work_relation.set(i, j, bw_relation.get(i, j) & fw_relation.get(i, j)); - //std::cerr << work_relation.get(i, j) << " "; } - //std::cerr << std::endl; } // Set the state renaming @@ -258,7 +255,6 @@ namespace { // MERGE IN FORWARD DIRECTION state_map_dummy.clear(); - // Compute the forward simulation TODO take out into a function const auto sim_relation_fw = algorithms::compute_relation( tmp, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); result = merge_in_one_direction(tmp, state_map_dummy, sim_relation_fw, false); @@ -275,7 +271,6 @@ namespace { // MERGE IN BACKWARD DIRECTION state_map_dummy.clear(); - // Compute the backward simulation TODO take out into a function Nfa aut_r = revert(tmp); const auto sim_relation_bw = algorithms::compute_relation( aut_r, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); @@ -322,7 +317,6 @@ Nfa mata::nfa::algorithms::reduce_size_by_simulation(const Nfa& aut, StateRenami return revert(result); } else if (simulation_direction == "bidirect"){ - // TODO this does not support state renaming // Compute the forward simulation const auto sim_fw_relation = algorithms::compute_relation( aut, ParameterMap{{ "relation", "simulation"}, { "direction", "forward"}}); @@ -337,13 +331,11 @@ Nfa mata::nfa::algorithms::reduce_size_by_simulation(const Nfa& aut, StateRenami return result; } else if (simulation_direction == "fixpoint"){ - // TODO this does not support state renaming result = simulation_fixpoint(aut); return result; } else { - // TODO throw some error - std::cerr << "TODO error" << std::endl; + throw std::runtime_error("invalid reduction algorithm selected"); } return result;