Move gamebased-ar to own lib (#434)

moves-rwth · Nov 21, 2023 · 3b9d8bf · 3b9d8bf
2 parents c710f65 + cc6162e
commit 3b9d8bf
Show file tree

Hide file tree

Showing 105 changed files with 842 additions and 743 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -7,6 +7,7 @@ add_custom_target(binaries)
 add_subdirectory(storm)
 add_subdirectory(storm-counterexamples)
 add_subdirectory(storm-permissive)
+add_subdirectory(storm-gamebased-ar)
 add_subdirectory(storm-parsers)
 add_subdirectory(storm-version-info)
 add_subdirectory(storm-cli-utilities)

diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt
@@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-cli-utilities)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-parsers storm-version-info)
+target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info)
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_CLI_UTIL_HEADERS})

diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
@@ -3,6 +3,7 @@
 #include "storm/api/storm.h"
 
 #include "storm-counterexamples/api/counterexamples.h"
+#include "storm-gamebased-ar/api/verification.h"
 #include "storm-parsers/api/storm-parsers.h"
 
 #include "storm/io/file.h"

diff --git a/src/storm-gamebased-ar/CMakeLists.txt b/src/storm-gamebased-ar/CMakeLists.txt
@@ -0,0 +1,36 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.h ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-gamebased-ar)
+
+file(GLOB_RECURSE STORM_GBAR_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.cpp)
+file(GLOB_RECURSE STORM_GBAR_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.h)
+
+# Create storm-gamebased-ar.
+add_library(storm-gamebased-ar SHARED ${STORM_GBAR_SOURCES} ${STORM_GBAR_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-gamebased-ar PROPERTIES DEFINE_SYMBOL "")
+list(APPEND STORM_TARGETS storm-gamebased-ar)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-gamebased-ar PUBLIC storm)
+
+# Install storm headers to include directory.
+foreach (HEADER ${STORM_GBAR_HEADERS})
+    string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
+    string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
+    string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
+    add_custom_command(
+            OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+            COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
+            COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+            DEPENDS ${HEADER}
+    )
+    list(APPEND STORM_GBAR_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach ()
+add_custom_target(copy_storm_gbar_headers DEPENDS ${STORM_GBAR_OUTPUT_HEADERS} ${STORM_GBAR_HEADERS})
+add_dependencies(storm-gamebased-ar copy_storm_gbar_headers)
+
+# installation
+install(TARGETS storm-gamebased-ar EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+
diff --git a/...rm/abstraction/AbstractionInformation.cpp → ...ar/abstraction/AbstractionInformation.cpp b/...rm/abstraction/AbstractionInformation.cpp → ...ar/abstraction/AbstractionInformation.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
 
 #include "storm/storage/BitVector.h"
 

diff --git a/...torm/abstraction/AbstractionInformation.h → ...d-ar/abstraction/AbstractionInformation.h b/...torm/abstraction/AbstractionInformation.h → ...d-ar/abstraction/AbstractionInformation.h
diff --git a/src/storm/abstraction/BottomStateResult.cpp → ...ased-ar/abstraction/BottomStateResult.cpp b/src/storm/abstraction/BottomStateResult.cpp → ...ased-ar/abstraction/BottomStateResult.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/BottomStateResult.h"
+#include "storm-gamebased-ar/abstraction/BottomStateResult.h"
 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
 namespace storm {

diff --git a/src/storm/abstraction/BottomStateResult.h → ...ebased-ar/abstraction/BottomStateResult.h b/src/storm/abstraction/BottomStateResult.h → ...ebased-ar/abstraction/BottomStateResult.h
diff --git a/...raction/ExplicitQualitativeGameResult.cpp → ...raction/ExplicitQualitativeGameResult.cpp b/...raction/ExplicitQualitativeGameResult.cpp → ...raction/ExplicitQualitativeGameResult.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/ExplicitQualitativeGameResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...straction/ExplicitQualitativeGameResult.h → ...straction/ExplicitQualitativeGameResult.h b/...straction/ExplicitQualitativeGameResult.h → ...straction/ExplicitQualitativeGameResult.h
@@ -1,6 +1,6 @@
 #pragma once
 
-#include "storm/abstraction/ExplicitQualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeResult.h"
 #include "storm/utility/graph.h"
 
 namespace storm {

diff --git a/...n/ExplicitQualitativeGameResultMinMax.cpp → ...n/ExplicitQualitativeGameResultMinMax.cpp b/...n/ExplicitQualitativeGameResultMinMax.cpp → ...n/ExplicitQualitativeGameResultMinMax.cpp
@@ -1,5 +1,4 @@
-#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
-#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...ion/ExplicitQualitativeGameResultMinMax.h → ...ion/ExplicitQualitativeGameResultMinMax.h b/...ion/ExplicitQualitativeGameResultMinMax.h → ...ion/ExplicitQualitativeGameResultMinMax.h
@@ -1,7 +1,7 @@
 #pragma once
 
-#include "storm/abstraction/ExplicitQualitativeGameResult.h"
-#include "storm/abstraction/ExplicitQualitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...abstraction/ExplicitQualitativeResult.cpp → ...abstraction/ExplicitQualitativeResult.cpp b/...abstraction/ExplicitQualitativeResult.cpp → ...abstraction/ExplicitQualitativeResult.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/ExplicitQualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeResult.h"
 
-#include "storm/abstraction/ExplicitQualitativeGameResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...m/abstraction/ExplicitQualitativeResult.h → ...r/abstraction/ExplicitQualitativeResult.h b/...m/abstraction/ExplicitQualitativeResult.h → ...r/abstraction/ExplicitQualitativeResult.h
@@ -2,7 +2,7 @@
 
 #include "storm/storage/dd/DdType.h"
 
-#include "storm/abstraction/QualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/QualitativeResult.h"
 
 namespace storm {
 namespace storage {

diff --git a/...ction/ExplicitQualitativeResultMinMax.cpp → ...ction/ExplicitQualitativeResultMinMax.cpp b/...ction/ExplicitQualitativeResultMinMax.cpp → ...ction/ExplicitQualitativeResultMinMax.cpp
@@ -1,6 +1,4 @@
-#include "storm/abstraction/ExplicitQualitativeResultMinMax.h"
-
-#include "storm/abstraction/ExplicitQualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...raction/ExplicitQualitativeResultMinMax.h → ...raction/ExplicitQualitativeResultMinMax.h b/...raction/ExplicitQualitativeResultMinMax.h → ...raction/ExplicitQualitativeResultMinMax.h
@@ -2,7 +2,7 @@
 
 #include "storm/solver/OptimizationDirection.h"
 
-#include "storm/abstraction/QualitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/QualitativeResultMinMax.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...bstraction/ExplicitQuantitativeResult.cpp → ...bstraction/ExplicitQuantitativeResult.cpp b/...bstraction/ExplicitQuantitativeResult.cpp → ...bstraction/ExplicitQuantitativeResult.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/ExplicitQuantitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.h"
 
 #include "storm/storage/BitVector.h"
 

diff --git a/.../abstraction/ExplicitQuantitativeResult.h → .../abstraction/ExplicitQuantitativeResult.h b/.../abstraction/ExplicitQuantitativeResult.h → .../abstraction/ExplicitQuantitativeResult.h
diff --git a/...tion/ExplicitQuantitativeResultMinMax.cpp → ...tion/ExplicitQuantitativeResultMinMax.cpp b/...tion/ExplicitQuantitativeResultMinMax.cpp → ...tion/ExplicitQuantitativeResultMinMax.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h"
 
 #include "storm/adapters/RationalNumberAdapter.h"
 

diff --git a/...action/ExplicitQuantitativeResultMinMax.h → ...action/ExplicitQuantitativeResultMinMax.h b/...action/ExplicitQuantitativeResultMinMax.h → ...action/ExplicitQuantitativeResultMinMax.h
@@ -1,6 +1,6 @@
 #pragma once
 
-#include "storm/abstraction/ExplicitQuantitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.h"
 
 #include "storm/solver/OptimizationDirection.h"
 

diff --git a/...torm/abstraction/ExpressionTranslator.cpp → ...d-ar/abstraction/ExpressionTranslator.cpp b/...torm/abstraction/ExpressionTranslator.cpp → ...d-ar/abstraction/ExpressionTranslator.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/ExpressionTranslator.h"
+#include "storm-gamebased-ar/abstraction/ExpressionTranslator.h"
 
-#include "storm/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
 
 #include "storm/storage/dd/Bdd.h"
 #include "storm/storage/dd/DdManager.h"

diff --git a/src/storm/abstraction/ExpressionTranslator.h → ...sed-ar/abstraction/ExpressionTranslator.h b/src/storm/abstraction/ExpressionTranslator.h → ...sed-ar/abstraction/ExpressionTranslator.h
diff --git a/src/storm/abstraction/GameBddResult.cpp → ...amebased-ar/abstraction/GameBddResult.cpp b/src/storm/abstraction/GameBddResult.cpp → ...amebased-ar/abstraction/GameBddResult.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/GameBddResult.h"
+#include "storm-gamebased-ar/abstraction/GameBddResult.h"
 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
 namespace storm {

diff --git a/src/storm/abstraction/GameBddResult.h → ...-gamebased-ar/abstraction/GameBddResult.h b/src/storm/abstraction/GameBddResult.h → ...-gamebased-ar/abstraction/GameBddResult.h
diff --git a/...bstraction/LocalExpressionInformation.cpp → ...bstraction/LocalExpressionInformation.cpp b/...bstraction/LocalExpressionInformation.cpp → ...bstraction/LocalExpressionInformation.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/LocalExpressionInformation.h"
+#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h"
 
-#include "storm/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
 
 #include <boost/algorithm/string/join.hpp>
 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h"

diff --git a/.../abstraction/LocalExpressionInformation.h → .../abstraction/LocalExpressionInformation.h b/.../abstraction/LocalExpressionInformation.h → .../abstraction/LocalExpressionInformation.h
diff --git a/src/storm/abstraction/MenuGame.cpp → ...orm-gamebased-ar/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp → ...orm-gamebased-ar/abstraction/MenuGame.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/MenuGame.h"
+#include "storm-gamebased-ar/abstraction/MenuGame.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidOperationException.h"

diff --git a/src/storm/abstraction/MenuGame.h → ...storm-gamebased-ar/abstraction/MenuGame.h b/src/storm/abstraction/MenuGame.h → ...storm-gamebased-ar/abstraction/MenuGame.h
diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp → ...sed-ar/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp → ...sed-ar/abstraction/MenuGameAbstractor.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/MenuGameAbstractor.h"
+#include "storm-gamebased-ar/abstraction/MenuGameAbstractor.h"
 
-#include "storm/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 

diff --git a/src/storm/abstraction/MenuGameAbstractor.h → ...based-ar/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h → ...based-ar/abstraction/MenuGameAbstractor.h
@@ -5,8 +5,8 @@
 
 #include "storm/storage/dd/DdType.h"
 
-#include "storm/abstraction/MenuGame.h"
-#include "storm/abstraction/RefinementCommand.h"
+#include "storm-gamebased-ar/abstraction/MenuGame.h"
+#include "storm-gamebased-ar/abstraction/RefinementCommand.h"
 
 #include "storm/storage/expressions/Expression.h"
 

diff --git a/src/storm/abstraction/MenuGameRefiner.cpp → ...ebased-ar/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp → ...ebased-ar/abstraction/MenuGameRefiner.cpp
@@ -1,12 +1,12 @@
-#include "storm/abstraction/MenuGameRefiner.h"
+#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h"
 
-#include "storm/abstraction/AbstractionInformation.h"
-#include "storm/abstraction/MenuGameAbstractor.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/MenuGameAbstractor.h"
 
-#include "storm/abstraction/ExplicitGameStrategyPair.h"
-#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
-#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h"
 #include "storm/storage/BitVector.h"
+#include "storm/storage/ExplicitGameStrategyPair.h"
 
 #include "storm/storage/dd/DdManager.h"
 #include "storm/storage/dd/Odd.h"
@@ -1187,7 +1187,7 @@ template<typename ValueType>
 void performDijkstraStep(std::set<ExplicitDijkstraQueueElement<ValueType>, ExplicitDijkstraQueueElementLess<ValueType>>& dijkstraQueue,
                          bool probabilityDistances, std::vector<ValueType>& distances, std::vector<std::pair<uint64_t, uint64_t>>& predecessors,
                          bool generatePredecessors, bool lower, uint64_t currentState, ValueType const& currentDistance, bool isPivotState,
-                         ExplicitGameStrategyPair const& strategyPair, ExplicitGameStrategyPair const& otherStrategyPair,
+                         storm::storage::ExplicitGameStrategyPair const& strategyPair, storm::storage::ExplicitGameStrategyPair const& otherStrategyPair,
                          std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Grouping,
                          storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& targetStates,
                          storm::storage::BitVector const& relevantStates) {
@@ -1230,8 +1230,8 @@ boost::optional<ExplicitPivotStateResult<ValueType>> pickPivotState(
     bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic,
     storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling,
     storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates,
-    ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector<ValueType> const* lowerValues = nullptr,
-    std::vector<ValueType> const* upperValues = nullptr) {
+    storage::ExplicitGameStrategyPair const& minStrategyPair, storage::ExplicitGameStrategyPair const& maxStrategyPair,
+    std::vector<ValueType> const* lowerValues = nullptr, std::vector<ValueType> const* upperValues = nullptr) {
     STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results.");
     STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results.");
 
@@ -1395,7 +1395,7 @@ boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePr
     storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
     std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
     storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability,
-    ExplicitGameStrategyPair const& maxStrategyPair) const {
+    storage::ExplicitGameStrategyPair const& maxStrategyPair) const {
     // Extract the underlying DTMC of the max strategy pair.
 
     // Start by determining which states are reachable.
@@ -1490,7 +1490,8 @@ bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type,
                                               std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling,
                                               storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates,
                                               storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult,
-                                              ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const {
+                                              storage::ExplicitGameStrategyPair const& minStrategyPair,
+                                              storage::ExplicitGameStrategyPair const& maxStrategyPair) const {
     //            boost::optional<RefinementPredicates> kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix,
     //            player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, storm::utility::zero<ValueType>(),
     //            storm::utility::one<ValueType>(), maxStrategyPair);
@@ -1579,7 +1580,8 @@ bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type,
                                               storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates,
                                               storm::storage::BitVector const& targetStates,
                                               ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult,
-                                              ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const {
+                                              storage::ExplicitGameStrategyPair const& minStrategyPair,
+                                              storage::ExplicitGameStrategyPair const& maxStrategyPair) const {
     //            ValueType lower = quantitativeResult.getMin().getRange(initialStates).first;
     //            ValueType upper = quantitativeResult.getMax().getRange(initialStates).second;
 

diff --git a/src/storm/abstraction/MenuGameRefiner.h → ...amebased-ar/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h → ...amebased-ar/abstraction/MenuGameRefiner.h
@@ -6,9 +6,9 @@
 
 #include <boost/optional.hpp>
 
-#include "storm/abstraction/RefinementCommand.h"
-#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h"
-#include "storm/abstraction/SymbolicQuantitativeGameResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/RefinementCommand.h"
+#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.h"
 
 #include "storm/storage/expressions/EquivalenceChecker.h"
 #include "storm/storage/expressions/Expression.h"
@@ -27,7 +27,8 @@ class Odd;
 
 namespace storage {
 class BitVector;
-}
+class ExplicitGameStrategyPair;
+}  // namespace storage
 
 namespace abstraction {
 
@@ -93,7 +94,6 @@ struct ExplicitPivotStateResult {
 };
 
 class ExplicitQualitativeGameResultMinMax;
-class ExplicitGameStrategyPair;
 
 template<typename ValueType>
 class ExplicitQuantitativeResultMinMax;
@@ -144,8 +144,8 @@ class MenuGameRefiner {
                 storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
                 std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
                 storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
-                ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair,
-                ExplicitGameStrategyPair const& maxStrategyPair) const;
+                ExplicitQualitativeGameResultMinMax const& qualitativeResult, storage::ExplicitGameStrategyPair const& minStrategyPair,
+                storage::ExplicitGameStrategyPair const& maxStrategyPair) const;
 
     /*!
      * Refines the abstractor based on the qualitative result by trying to derive suitable predicates.
@@ -156,8 +156,8 @@ class MenuGameRefiner {
                 storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
                 std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
                 storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
-                ExplicitQuantitativeResultMinMax<ValueType> const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair,
-                ExplicitGameStrategyPair const& maxStrategyPair) const;
+                ExplicitQuantitativeResultMinMax<ValueType> const& qualitativeResult, storage::ExplicitGameStrategyPair const& minStrategyPair,
+                storage::ExplicitGameStrategyPair const& maxStrategyPair) const;
 
     /*!
      * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
@@ -220,7 +220,7 @@ class MenuGameRefiner {
         storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
         std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
         storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability,
-        ExplicitGameStrategyPair const& maxStrategyPair) const;
+        storage::ExplicitGameStrategyPair const& maxStrategyPair) const;
     boost::optional<RefinementPredicates> derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd,
                                                                                         storm::expressions::ExpressionManager& interpolationManager,
                                                                                         std::vector<uint64_t> const& reversedPath,

diff --git a/src/storm/abstraction/QualitativeResult.cpp → ...ased-ar/abstraction/QualitativeResult.cpp b/src/storm/abstraction/QualitativeResult.cpp → ...ased-ar/abstraction/QualitativeResult.cpp
@@ -1,7 +1,7 @@
-#include "storm/abstraction/QualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/QualitativeResult.h"
 
-#include "storm/abstraction/ExplicitQualitativeResult.h"
-#include "storm/abstraction/SymbolicQualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeResult.h"
+#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/src/storm/abstraction/QualitativeResult.h → ...ebased-ar/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h → ...ebased-ar/abstraction/QualitativeResult.h
diff --git a/...m/abstraction/QualitativeResultMinMax.cpp → ...r/abstraction/QualitativeResultMinMax.cpp b/...m/abstraction/QualitativeResultMinMax.cpp → ...r/abstraction/QualitativeResultMinMax.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/QualitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/QualitativeResultMinMax.h"
 
-#include "storm/abstraction/SymbolicQualitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/...orm/abstraction/QualitativeResultMinMax.h → ...-ar/abstraction/QualitativeResultMinMax.h b/...orm/abstraction/QualitativeResultMinMax.h → ...-ar/abstraction/QualitativeResultMinMax.h
diff --git a/src/storm/abstraction/RefinementCommand.cpp → ...ased-ar/abstraction/RefinementCommand.cpp b/src/storm/abstraction/RefinementCommand.cpp → ...ased-ar/abstraction/RefinementCommand.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/RefinementCommand.h"
+#include "storm-gamebased-ar/abstraction/RefinementCommand.h"
 
 namespace storm {
 namespace abstraction {

diff --git a/src/storm/abstraction/RefinementCommand.h → ...ebased-ar/abstraction/RefinementCommand.h b/src/storm/abstraction/RefinementCommand.h → ...ebased-ar/abstraction/RefinementCommand.h
diff --git a/src/storm/abstraction/StateSet.cpp → ...orm-gamebased-ar/abstraction/StateSet.cpp b/src/storm/abstraction/StateSet.cpp → ...orm-gamebased-ar/abstraction/StateSet.cpp
@@ -1,5 +1,5 @@
-#include "storm/abstraction/StateSet.h"
-#include "storm/abstraction/SymbolicStateSet.h"
+#include "storm-gamebased-ar/abstraction/StateSet.h"
+#include "storm-gamebased-ar/abstraction/SymbolicStateSet.h"
 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
 namespace storm {

diff --git a/src/storm/abstraction/StateSet.h → ...storm-gamebased-ar/abstraction/StateSet.h b/src/storm/abstraction/StateSet.h → ...storm-gamebased-ar/abstraction/StateSet.h
diff --git a/src/storm/abstraction/StateSetAbstractor.cpp → ...sed-ar/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp → ...sed-ar/abstraction/StateSetAbstractor.cpp
@@ -1,6 +1,6 @@
-#include "storm/abstraction/StateSetAbstractor.h"
+#include "storm-gamebased-ar/abstraction/StateSetAbstractor.h"
 
-#include "storm/abstraction/AbstractionInformation.h"
+#include "storm-gamebased-ar/abstraction/AbstractionInformation.h"
 
 #include "storm/storage/dd/DdManager.h"
 

diff --git a/src/storm/abstraction/StateSetAbstractor.h → ...based-ar/abstraction/StateSetAbstractor.h b/src/storm/abstraction/StateSetAbstractor.h → ...based-ar/abstraction/StateSetAbstractor.h
@@ -11,7 +11,7 @@
 #include "storm/solver/SmtSolver.h"
 #include "storm/utility/solver.h"
 
-#include "storm/abstraction/LocalExpressionInformation.h"
+#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h"
 
 namespace storm {
 namespace utility {

diff --git a/...raction/SymbolicQualitativeGameResult.cpp → ...raction/SymbolicQualitativeGameResult.cpp b/...raction/SymbolicQualitativeGameResult.cpp → ...raction/SymbolicQualitativeGameResult.cpp
@@ -1,4 +1,4 @@
-#include "storm/abstraction/SymbolicQualitativeGameResult.h"
+#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h"
 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
 namespace storm {