Merge pull request #483 from VeriFIT/reduce_residual_public #patch

feat(reduce): Move reduce residual algorithms into the public interface

bindings/python/libmata/nfa/nfa.pxd

@@ -206,6 +206,8 @@ cdef extern from "mata/nfa/plumbing.hh" namespace "mata::nfa::plumbing":
     cdef void c_remove_epsilon "mata::nfa::plumbing::remove_epsilon" (CNfa*, CNfa&, Symbol) except +
     cdef void c_minimize "mata::nfa::plumbing::minimize" (CNfa*, CNfa&, ParameterMap&)
     cdef void c_reduce "mata::nfa::plumbing::reduce" (CNfa*, CNfa&, StateRenaming*, ParameterMap&)
+    cdef void c_reduce_residual_with "mata::nfa::plumbing::reduce_residual_with" (CNfa*, CNfa&)
+    cdef void c_reduce_residual_after "mata::nfa::plumbing::reduce_residual_after" (CNfa*, CNfa&)
 
 
 

bindings/python/libmata/nfa/nfa.pyx

@@ -994,7 +994,8 @@ def reduce_with_state_map(Nfa aut, params = None):
 
     :param Nfa aut: Original automaton to reduce.
     :param Dict params: Additional parameters for the reduction algorithm:
-        - "algorithm": "simulation"
+        - "algorithm":
+          - "simulation": Reduce size by simulation.
     :return: (Reduced automaton, state map of original to new states)
     """
     params = params or {"algorithm": "simulation"}
@@ -1013,8 +1014,16 @@ def reduce(Nfa aut, params = None):
 
     :param Nfa aut: Original automaton to reduce.
     :param Dict params: Additional parameters for the reduction algorithm:
-        - "algorithm": "simulation"
-    :return: Reduced automaton
+        - "algorithm":
+          - "simulation": Reduce size by simulation.
+          - "residual": Reduce size by residual construction.
+        - "type":
+          - "after": (Only for "algorithm": "residual") Residual construction after the last determinization.
+          - "with": (Only for "algorithm": "residual") Residual construction during the last determinization.
+        - "direction":
+          - "forward": (Only for "algorithm": "residual") Forward residual construction.
+          - "backward": (Only for "algorithm": "residual") Backward residual construction.
+    :return: Reduced automaton.
     """
     params = params or {"algorithm": "simulation"}
     result = Nfa()
@@ -1025,6 +1034,26 @@ def reduce(Nfa aut, params = None):
                     )
     return result
 
+def reduce_residual_after(Nfa aut):
+    """Reduce the automaton by residual construction after the last determinization.
+
+    :param Nfa aut: Original automaton to reduce.
+    :return: Reduced automaton.
+    """
+    result = Nfa()
+    mata_nfa.c_reduce_residual_after(result.thisptr.get(), dereference(aut.thisptr.get()))
+    return result
+
+def reduce_residual_with(Nfa aut):
+    """Reduce the automaton by residual construction during the last determinization.
+
+    :param Nfa aut: Original automaton to reduce.
+    :return: Reduced automaton.
+    """
+    result = Nfa()
+    mata_nfa.c_reduce_residual_with(result.thisptr.get(), dereference(aut.thisptr.get()))
+    return result
+
 def compute_relation(Nfa lhs, params = None):
     """Computes the relation for the automaton
 

bindings/python/tests/test_nfa.py

@@ -953,6 +953,18 @@ def test_reduce():
     nfa.add_transition(9, ord('c'), 0)
     nfa.add_transition(0, ord('a'), 4)
 
+    result = mata_nfa.reduce(nfa, params={"algorithm": "residual", "type": "after", "direction": "forward"})
+    assert result.num_of_states() < nfa.num_of_states()
+
+    result = mata_nfa.reduce(nfa, params={"algorithm": "residual", "type": "after", "direction": "backward"})
+    assert result.num_of_states() < nfa.num_of_states()
+
+    result = mata_nfa.reduce_residual_after(mata_nfa.determinize(nfa))
+    assert result.num_of_states() < nfa.num_of_states()
+
+    result = mata_nfa.reduce_residual_with(mata_nfa.determinize(nfa))
+    assert result.num_of_states() < nfa.num_of_states()
+
     result, state_map = mata_nfa.reduce_with_state_map(nfa)
     assert result.num_of_states() == 6
     assert result.has_initial_state(state_map[1])

include/mata/nfa/algorithms.hh

@@ -15,13 +15,6 @@
  * these function according to parameters provided by a user.
  * E.g. we can call the following function: `is_universal(aut, alph, {{'algorithm', 'antichains'}})`
  * to check for universality based on antichain-based algorithm.
- *
- * In particular, this includes algorithms for:
- *   1. Complementation,
- *   2. Inclusion,
- *   3. Universality checking,
- *   4. Intersection/concatenation with epsilon transitions, or,
- *   5. Computing relation.
  */
 namespace mata::nfa::algorithms {
 
@@ -138,6 +131,43 @@ Nfa product(const Nfa& lhs, const Nfa& rhs, const std::function<bool(State,State
 Nfa concatenate_eps(const Nfa& lhs, const Nfa& rhs, const Symbol& epsilon, bool use_epsilon = false,
                     StateRenaming* lhs_state_renaming = nullptr, StateRenaming* rhs_state_renaming = nullptr);
 
+/**
+ * @brief Reduce NFA using residual construction.
+ *
+ * @param[in] nfa NFA to reduce.
+ * @param[in] state_renaming Map mapping original states to the reduced states.
+ * @param[in] type Type of the residual construction (values: "after", "with").
+ * @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);
+
+/**
+ * @brief Reduce NFA using residual construction.
+ *
+ * The residual construction of the residual automaton and the removal of the
+ *  covering states is done during the last determinization.
+ *
+ * Similar performance to `reduce_residual_after()`.
+ * The output is almost the same except the transitions: transitions may
+ *  slightly differ, but the number of states is the same for both algorithm
+ *  types.
+ */
+Nfa reduce_residual_with(const Nfa& nfa);
+
+/**
+ * @brief Reduce NFA using residual construction.
+ *
+ * The residual construction of the residual automaton and the removal of the
+ *  covering states is done after the final determinization.
+ *
+ * Similar performance to `reduce_residual_with()`.
+ * The output is almost the same except the transitions: transitions may
+ *  slightly differ, but the number of states is the same for both algorithm
+ *  types.
+ */
+Nfa reduce_residual_after(const Nfa& nfa);
+
 } // Namespace mata::nfa::algorithms.
 
 #endif // MATA_NFA_INTERNALS_HH_

include/mata/nfa/plumbing.hh

@@ -93,6 +93,36 @@ inline void concatenate(Nfa* res, const Nfa& lhs, const Nfa& rhs, bool use_epsil
     *res = concatenate(lhs, rhs, use_epsilon, lhs_result_state_renaming, rhs_result_state_renaming);
 }
 
-} // namespace mata::nfa::Plumbing.
+/**
+ * @brief Reduce NFA using residual construction.
+ *
+ * The residual construction of the residual automaton and the removal of the
+ *  covering states is done during the last determinization.
+ *
+ * Similar performance to `reduce_residual_after()`.
+ * The output is almost the same except the transitions: transitions may
+ *  slightly differ, but the number of states is the same for both algorithm
+ *  types.
+ */
+inline void reduce_residual_with(Nfa* res, const Nfa& nfa) {
+  *res = algorithms::reduce_residual_with(nfa);
+}
+
+/**
+ * @brief Reduce NFA using residual construction.
+ *
+ * The residual construction of the residual automaton and the removal of the
+ *  covering states is done after the final determinization.
+ *
+ * Similar performance to `reduce_residual_with()`.
+ * The output is almost the same except the transitions: transitions may
+ *  slightly differ, but the number of states is the same for both algorithm
+ *  types.
+ */
+inline void reduce_residual_after(Nfa* res, const Nfa& nfa) {
+  *res = algorithms::reduce_residual_after(nfa);
+}
+
+} // namespace mata::nfa::plumbing.
 
 #endif // MATA_NFA_PLUMBING_HH_