added more basic dfa manipulations

src/synthesis/header/ExplicitStateDfaMona.h

@@ -65,9 +65,68 @@ namespace Syft {
          */
         static ExplicitStateDfaMona dfa_of_formula(const whitemech::lydia::LTLfFormula& formula);
 
+        /**
+         * \brief Take the product AND of a vector of DFAs.
+         *
+         * \param dfa_vector The DFAs to be processed.
+         * \return The product DFA.
+         */
+        static ExplicitStateDfaMona dfa_product_and(const std::vector<ExplicitStateDfaMona>& dfa_vector);
+
+        /**
+         * \brief Take the product AND of a vector of DFAs.
+         *
+         * \param dfa_vector The DFAs to be processed.
+         * \return The product DFA.
+         */
+        static ExplicitStateDfaMona dfa_product_or(const std::vector<ExplicitStateDfaMona>& dfa_vector);
+
+        /**
+         * \brief Minimize a given DFA.
+         *
+         * \param d The DFA to be minimized.
+         * \return The minimal DFA.
+         */
+        static ExplicitStateDfaMona dfa_minimize(const ExplicitStateDfaMona& d);
+
+
+        /**
+         * \brief Construct DFA from a given formula
+         *
+         *
+         * \param formula An LTLf formula.
+         * \return The corresponding explicit-state DFA.
+         */
+        static ExplicitStateDfaMona dfa_of_formula(const std::string& formula);
+
+        /**
+      * \brief Prune a DFA with given set of states.
+      *
+      * Basically remove a set of states from the DFA, and return a minimized one.
+      *
+      * \param d The DFA to be pruned.
+      * \param states The set of states to be removed.
+      * \return The pruned DFA.
+      */
+        static ExplicitStateDfaMona prune_dfa_with_states(ExplicitStateDfaMona& d, std::vector<size_t> states);
 
+        /**
+         * \brief Prune a DFA with given transitions.
+         *
+         * Basically remove a set of transitions from the DFA, and return a minimized one.
+         *
+         * \param d The DFA to be pruned.
+         * \param transitions The set of transitions to be removed.
+         * \return The pruned DFA.
+         */
+        static ExplicitStateDfaMona prune_dfa_with_transitions(ExplicitStateDfaMona& d, std::unordered_map<size_t, CUDD::BDD> transitions, std::shared_ptr<VarMgr> var_mgr);
 
+        /**
+         * \brief Complement a DFA.
+         */
+        static ExplicitStateDfaMona dfa_complement(ExplicitStateDfaMona& d);
 
+        static std::vector<std::string> traverse_bdd(CUDD::BDD dd, std::shared_ptr<VarMgr> var_mgr, std::vector<std::string>& names, std::string guard_str);
     };
 
 }

src/synthesis/header/SymbolicStateDfa.h

@@ -108,23 +108,23 @@ class SymbolicStateDfa {
   std::vector<CUDD::BDD> transition_function() const;
 
   /**
-   * \brief Turns the set of invalid states into a sink.
+   * \brief Turns the set of invalid states into a sink (assuming that the initial state is a valid state).
    *
    * All transitions out of the invalid states are redirected to the sink state
    * 0, and the invalid states are removed from the set of final states.
    *
    * \param invalid_states A BDD representing the set of invalid states.
    */
-  void prune_invalid_states(const CUDD::BDD& invalid_states);
+  void prune_dfa_with_states(const CUDD::BDD& invalid_states);
 
   /**
-   * \brief Restricts the DFA to a set of feasible moves, by turning the set of infeasible ones into a sink.
+   * \brief Prune the DFA removing a set of infeasible moves, by turning them into a sink.
    *
-   * All transitions out of the set of feasible moves are redirected to the sink state 0.
+   * All transitions out of the set of infeasible moves are redirected to the sink state 0.
    *
-   * \param feasible_moves A BDD representing the set of feasible moves.
+   * \param infeasible_moves A BDD representing the set of infeasible moves.
    */
-    void restrict_transitions(const CUDD::BDD& feasible_moves);
+    void prune_dfa_with_transitions(const CUDD::BDD& infeasible_moves);
 
   /**
    * \brief Saves the symbolic representation of the DFA in a .dot file.
@@ -137,19 +137,33 @@ class SymbolicStateDfa {
   void dump_dot(const std::string& filename) const;
 
     /**
-     * \brief Returns a product of two symbolic DFAs.
+     * \brief Returns a product AND of two symbolic DFAs.
      *
      * \param first_dfa The first DFA.
      * \param second_dfa The second DFA.
-     * \return A symbolic DFA of the product.
+     * \return A symbolic DFA of the product AND.
      */
-  static SymbolicStateDfa product(const std::vector<SymbolicStateDfa>& dfa_vector);
+  static SymbolicStateDfa product_AND(const std::vector<SymbolicStateDfa>& dfa_vector);
 
 
   static std::vector<int> state_to_binary(std::size_t state,
                                             std::size_t bit_count);
 
     void new_sink_states(const CUDD::BDD& sink_states);
+
+    /**
+* \brief Returns a product AND of two symbolic DFAs.
+*
+* \param first_dfa The first DFA.
+* \param second_dfa The second DFA.
+* \return A symbolic DFA of the product OR.
+*/
+    static SymbolicStateDfa product_OR(const std::vector<SymbolicStateDfa>& dfa_vector);
+
+
+//  void complement();
+
+        static SymbolicStateDfa complement(const SymbolicStateDfa dfa);
 };
 
 }

src/synthesis/header/VarMgr.h

@@ -66,6 +66,9 @@ class VarMgr {
   std::size_t create_product_state_space(
       const std::vector<std::size_t>& automaton_ids);
 
+    std::size_t create_complement_state_space(
+            const std::size_t automaton_id);
+
   /**
    * \brief Returns the i-th state variable for a given automaton.
    */

src/synthesis/source/DfaGameSynthesizer.cpp

@@ -112,7 +112,6 @@ std::unordered_map<int, CUDD::BDD> DfaGameSynthesizer::synthesize_strategy(
 
       output_function[output_index] = parameterized_output_function[i];
 
-      // TODO(Lucas): Replace inner loop with CUDD::BDD::VectorCompose
       for (int j = output_count - 1; j >= i; --j) {
           int parameter_index = index_copy[j];