Adding simulation reduction rules

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_

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

src/nfa/operations.cc

@@ -3,10 +3,12 @@
 
 #include <algorithm>
 #include <list>
+#include <string>
 #include <unordered_set>
 
 // 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"
@@ -21,111 +23,6 @@ using mata::Symbol;
 using StateBoolArray = std::vector<bool>; ///< Bool array for states in the automaton.
 
 namespace {
-    Simlib::Util::BinaryRelation compute_fw_direct_simulation(const Nfa& aut) {
-        OrdVector<mata::Symbol> 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();
-    }
-
-    Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming) {
-        Nfa result;
-        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();
-
-        // for State q, quot_proj[q] should be the representative state representing the symmetric class of states in simulation
-        std::vector<size_t> 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_to
-                    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 (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;
-    }
-
     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();
@@ -1128,7 +1025,11 @@ 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 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__) +
@@ -1147,7 +1048,8 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param
     std::unordered_map<State,State> 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 = 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