Merge pull request #28 from MortenSchou/longest-trace

All CEGAR things are in specific folder

src/include/pdaaal/PAutomatonProduct.h

@@ -27,6 +27,8 @@
 #ifndef PDAAAL_PAUTOMATONPRODUCT_H
 #define PDAAAL_PAUTOMATONPRODUCT_H
 
+#include "PDA.h"
+#include "PAutomaton.h"
 #include "pdaaal/internal/PAutomatonAlgorithms.h"
 
 namespace pdaaal {

src/include/pdaaal/PDAFactory.h

@@ -75,12 +75,12 @@ namespace pdaaal {
         builder_pda_t _temp_pda;
     };
 
-    template<typename T, typename W = weight<void>>
+    template<typename T, typename W = weight<void>, TraceInfoType trace_info_type = TraceInfoType::Single>
     class PDAFactory : public BasePDAFactory<T, PDA<T,W,fut::type::hash>, PDA<T,W,fut::type::vector>,
-                                       typename PDA<T,W,fut::type::hash>::rule_t, SolverInstance<T,W>> {
+                                       typename PDA<T,W,fut::type::hash>::rule_t, SolverInstance<T,W,size_t,true,trace_info_type>> {
     private:
         using parent_t = BasePDAFactory<T, PDA<T,W,fut::type::hash>, PDA<T,W,fut::type::vector>,
-                                    typename PDA<T,W,fut::type::hash>::rule_t, SolverInstance<T,W>>;
+                                    typename PDA<T,W,fut::type::hash>::rule_t, SolverInstance<T,W,size_t,true,trace_info_type>>;
     public:
         using rule_t = typename parent_t::rule_t;
         explicit PDAFactory(const std::unordered_set<T>& all_labels) : parent_t(all_labels) { };

src/include/pdaaal/SolverInstance.h

@@ -29,8 +29,6 @@
 
 #include "PAutomaton.h"
 #include "PAutomatonProduct.h"
-#include "pdaaal/cegar/AbstractionPDA.h"
-#include "pdaaal/cegar/AbstractionPAutomaton.h"
 #include <limits>
 
 namespace pdaaal {
@@ -84,57 +82,6 @@ namespace pdaaal {
                    PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type> initial,
                    PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type> final) -> SolverInstance<label_t,W,state_t,skip_state_mapping,trace_info_type>;
 
-    template <typename T, typename W>
-    class AbstractionSolverInstance {
-    public:
-        using pda_t = AbstractionPDA<T,W>;
-        using pautomaton_t = AbstractionPAutomaton<T,W>;
-        using product_t = PAutomatonProduct<pda_t, pautomaton_t, W, TraceInfoType::Single>;
-        AbstractionSolverInstance(pda_t&& pda,
-                                  const NFA<T>& initial_nfa, const std::vector<size_t>& initial_states,
-                                  const NFA<T>& final_nfa,   const std::vector<size_t>& final_states)
-        : _pda(std::move(pda)), _product(_pda, initial_nfa, initial_states, final_nfa, final_states) {};
-
-        auto move_pda_refinement_mapping() {
-            return _pda.move_label_map();
-        }
-        auto move_pda_refinement_mapping(const Refinement<T>& refinement) {
-            auto map = _pda.move_label_map();
-            map.refine(refinement);
-            return map;
-        }
-        auto move_pda_refinement_mapping(const HeaderRefinement<T>& header_refinement) {
-            auto map = _pda.move_label_map();
-            for (const auto& refinement : header_refinement.refinements()) {
-                map.refine(refinement);
-            }
-            return map;
-        }
-
-        product_t* operator->() {
-            return &_product;
-        }
-        const product_t* operator->() const {
-            return &_product;
-        }
-        product_t& operator*() {
-            return _product;
-        }
-        const product_t& operator*() const {
-            return _product;
-        }
-        product_t& get() {
-            return _product;
-        }
-        const product_t& get() const {
-            return _product;
-        }
-
-    private:
-        pda_t _pda;
-        product_t _product;
-    };
-
 }
 
 #endif //PDAAAL_SOLVERINSTANCE_H

src/include/pdaaal/cegar/AbstractionSolverInstance.h

@@ -0,0 +1,88 @@
+/* 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+/*
+ *  Copyright Morten K. Schou
+ */
+
+/* 
+ * File:   AbstractionSolverInstance.h
+ * Author: Morten K. Schou <[email protected]>
+ *
+ * Created on 21-02-2022.
+ */
+
+#ifndef PDAAAL_ABSTRACTIONSOLVERINSTANCE_H
+#define PDAAAL_ABSTRACTIONSOLVERINSTANCE_H
+
+#include "AbstractionPDA.h"
+#include "AbstractionPAutomaton.h"
+#include "pdaaal/PAutomatonProduct.h"
+
+namespace pdaaal {
+
+    template <typename T, typename W>
+    class AbstractionSolverInstance {
+    public:
+        using pda_t = AbstractionPDA<T,W>;
+        using pautomaton_t = AbstractionPAutomaton<T,W>;
+        using product_t = PAutomatonProduct<pda_t, pautomaton_t, W, TraceInfoType::Single>;
+        AbstractionSolverInstance(pda_t&& pda,
+                                  const NFA<T>& initial_nfa, const std::vector<size_t>& initial_states,
+                                  const NFA<T>& final_nfa,   const std::vector<size_t>& final_states)
+                : _pda(std::move(pda)), _product(_pda, initial_nfa, initial_states, final_nfa, final_states) {};
+
+        auto move_pda_refinement_mapping() {
+            return _pda.move_label_map();
+        }
+        auto move_pda_refinement_mapping(const Refinement<T>& refinement) {
+            auto map = _pda.move_label_map();
+            map.refine(refinement);
+            return map;
+        }
+        auto move_pda_refinement_mapping(const HeaderRefinement<T>& header_refinement) {
+            auto map = _pda.move_label_map();
+            for (const auto& refinement : header_refinement.refinements()) {
+                map.refine(refinement);
+            }
+            return map;
+        }
+
+        product_t* operator->() {
+            return &_product;
+        }
+        const product_t* operator->() const {
+            return &_product;
+        }
+        product_t& operator*() {
+            return _product;
+        }
+        const product_t& operator*() const {
+            return _product;
+        }
+        product_t& get() {
+            return _product;
+        }
+        const product_t& get() const {
+            return _product;
+        }
+
+    private:
+        pda_t _pda;
+        product_t _product;
+    };
+}
+
+#endif //PDAAAL_ABSTRACTIONSOLVERINSTANCE_H

src/include/pdaaal/cegar/CegarPdaFactory.h

@@ -30,6 +30,7 @@
 #include "AbstractionMapping.h"
 #include "AbstractionPAutomaton.h"
 #include "AbstractionPDA.h"
+#include "AbstractionSolverInstance.h"
 #include "pdaaal/PDAFactory.h"
 #include "pdaaal/Solver.h"
 #include "pdaaal/internal/PDA.h"