diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 24b7175b9..34167b587 100644 --- 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 index bf98385bf..12ca21b6b 100644 --- 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 index e4b5c9913..b88a083db 100644 --- 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 new file mode 100644 index 000000000..7f7e2dc74 --- /dev/null +++ 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/src/storm/abstraction/AbstractionInformation.cpp b/src/storm-gamebased-ar/abstraction/AbstractionInformation.cpp similarity index 99% rename from src/storm/abstraction/AbstractionInformation.cpp rename to src/storm-gamebased-ar/abstraction/AbstractionInformation.cpp index 92a50475f..d96387409 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm-gamebased-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/src/storm/abstraction/AbstractionInformation.h b/src/storm-gamebased-ar/abstraction/AbstractionInformation.h similarity index 100% rename from src/storm/abstraction/AbstractionInformation.h rename to src/storm-gamebased-ar/abstraction/AbstractionInformation.h diff --git a/src/storm/abstraction/BottomStateResult.cpp b/src/storm-gamebased-ar/abstraction/BottomStateResult.cpp similarity index 89% rename from src/storm/abstraction/BottomStateResult.cpp rename to src/storm-gamebased-ar/abstraction/BottomStateResult.cpp index 115fc08cf..665d91f35 100644 --- a/src/storm/abstraction/BottomStateResult.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/BottomStateResult.h similarity index 100% rename from src/storm/abstraction/BottomStateResult.h rename to src/storm-gamebased-ar/abstraction/BottomStateResult.h diff --git a/src/storm/abstraction/ExplicitQualitativeGameResult.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.cpp similarity index 85% rename from src/storm/abstraction/ExplicitQualitativeGameResult.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.cpp index 109201197..ee792a989 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResult.cpp +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQualitativeGameResult.h b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.h similarity index 87% rename from src/storm/abstraction/ExplicitQualitativeGameResult.h rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResult.h index 33cc2a7e2..2c706fc6b 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResult.h +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.cpp similarity index 90% rename from src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.cpp index af7ec9b4e..b9cf8962e 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h similarity index 85% rename from src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h index a62488c76..3fb7941bb 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQualitativeResult.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeResult.cpp similarity index 75% rename from src/storm/abstraction/ExplicitQualitativeResult.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeResult.cpp index 3cae12b88..bc7147374 100644 --- a/src/storm/abstraction/ExplicitQualitativeResult.cpp +++ b/src/storm-gamebased-ar/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/src/storm/abstraction/ExplicitQualitativeResult.h b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeResult.h similarity index 90% rename from src/storm/abstraction/ExplicitQualitativeResult.h rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeResult.h index 146acd165..225cbb5f6 100644 --- a/src/storm/abstraction/ExplicitQualitativeResult.h +++ b/src/storm-gamebased-ar/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/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.cpp similarity index 91% rename from src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.cpp index e2d1d11bf..40db2421e 100644 --- a/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQualitativeResultMinMax.h b/src/storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.h similarity index 94% rename from src/storm/abstraction/ExplicitQualitativeResultMinMax.h rename to src/storm-gamebased-ar/abstraction/ExplicitQualitativeResultMinMax.h index 8132a701c..69b3b08bd 100644 --- a/src/storm/abstraction/ExplicitQualitativeResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQuantitativeResult.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.cpp similarity index 96% rename from src/storm/abstraction/ExplicitQuantitativeResult.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.cpp index 0bdc4c5ed..012362c8a 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResult.cpp +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQuantitativeResult.h b/src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.h similarity index 100% rename from src/storm/abstraction/ExplicitQuantitativeResult.h rename to src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.h diff --git a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.cpp similarity index 96% rename from src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.cpp index af18eecaf..c52188d00 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExplicitQuantitativeResultMinMax.h b/src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h similarity index 93% rename from src/storm/abstraction/ExplicitQuantitativeResultMinMax.h rename to src/storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h index c6edb9105..7f4b848b9 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/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/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm-gamebased-ar/abstraction/ExpressionTranslator.cpp similarity index 99% rename from src/storm/abstraction/ExpressionTranslator.cpp rename to src/storm-gamebased-ar/abstraction/ExpressionTranslator.cpp index db50c0115..4fc4029d8 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/ExpressionTranslator.h similarity index 100% rename from src/storm/abstraction/ExpressionTranslator.h rename to src/storm-gamebased-ar/abstraction/ExpressionTranslator.h diff --git a/src/storm/abstraction/GameBddResult.cpp b/src/storm-gamebased-ar/abstraction/GameBddResult.cpp similarity index 92% rename from src/storm/abstraction/GameBddResult.cpp rename to src/storm-gamebased-ar/abstraction/GameBddResult.cpp index fcc83906c..6196195e4 100644 --- a/src/storm/abstraction/GameBddResult.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/GameBddResult.h similarity index 100% rename from src/storm/abstraction/GameBddResult.h rename to src/storm-gamebased-ar/abstraction/GameBddResult.h diff --git a/src/storm/abstraction/LocalExpressionInformation.cpp b/src/storm-gamebased-ar/abstraction/LocalExpressionInformation.cpp similarity index 98% rename from src/storm/abstraction/LocalExpressionInformation.cpp rename to src/storm-gamebased-ar/abstraction/LocalExpressionInformation.cpp index 8ec5b8958..b0efd756c 100644 --- a/src/storm/abstraction/LocalExpressionInformation.cpp +++ b/src/storm-gamebased-ar/abstraction/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 #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" diff --git a/src/storm/abstraction/LocalExpressionInformation.h b/src/storm-gamebased-ar/abstraction/LocalExpressionInformation.h similarity index 100% rename from src/storm/abstraction/LocalExpressionInformation.h rename to src/storm-gamebased-ar/abstraction/LocalExpressionInformation.h diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm-gamebased-ar/abstraction/MenuGame.cpp similarity index 98% rename from src/storm/abstraction/MenuGame.cpp rename to src/storm-gamebased-ar/abstraction/MenuGame.cpp index 7b7381a1d..562270223 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/src/storm-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 b/src/storm-gamebased-ar/abstraction/MenuGame.h similarity index 100% rename from src/storm/abstraction/MenuGame.h rename to src/storm-gamebased-ar/abstraction/MenuGame.h diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp similarity index 98% rename from src/storm/abstraction/MenuGameAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp index 3c8b03933..a397503f2 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.h similarity index 97% rename from src/storm/abstraction/MenuGameAbstractor.h rename to src/storm-gamebased-ar/abstraction/MenuGameAbstractor.h index 7f9318703..34ccb369f 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/MenuGameRefiner.cpp similarity index 98% rename from src/storm/abstraction/MenuGameRefiner.cpp rename to src/storm-gamebased-ar/abstraction/MenuGameRefiner.cpp index bba7c0ccc..f495c868a 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm-gamebased-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 void performDijkstraStep(std::set, ExplicitDijkstraQueueElementLess>& dijkstraQueue, bool probabilityDistances, std::vector& distances, std::vector>& 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 const& player1Labeling, std::vector const& player2Grouping, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& relevantStates) { @@ -1230,8 +1230,8 @@ boost::optional> pickPivotState( bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector 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 const* lowerValues = nullptr, - std::vector const* upperValues = nullptr) { + storage::ExplicitGameStrategyPair const& minStrategyPair, storage::ExplicitGameStrategyPair const& maxStrategyPair, + std::vector const* lowerValues = nullptr, std::vector 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 MenuGameRefiner::derivePr storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector 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::refine(storm::abstraction::MenuGame const& player1Labeling, std::vector 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 kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix, // player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, storm::utility::zero(), // storm::utility::one(), maxStrategyPair); @@ -1579,7 +1580,8 @@ bool MenuGameRefiner::refine(storm::abstraction::MenuGame 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 b/src/storm-gamebased-ar/abstraction/MenuGameRefiner.h similarity index 95% rename from src/storm/abstraction/MenuGameRefiner.h rename to src/storm-gamebased-ar/abstraction/MenuGameRefiner.h index 196c31c1c..b980b601b 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm-gamebased-ar/abstraction/MenuGameRefiner.h @@ -6,9 +6,9 @@ #include -#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 class ExplicitQuantitativeResultMinMax; @@ -144,8 +144,8 @@ class MenuGameRefiner { storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector 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 const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, - ExplicitQuantitativeResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, - ExplicitGameStrategyPair const& maxStrategyPair) const; + ExplicitQuantitativeResultMinMax 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 const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector 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 derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd, storm::expressions::ExpressionManager& interpolationManager, std::vector const& reversedPath, diff --git a/src/storm/abstraction/QualitativeResult.cpp b/src/storm-gamebased-ar/abstraction/QualitativeResult.cpp similarity index 81% rename from src/storm/abstraction/QualitativeResult.cpp rename to src/storm-gamebased-ar/abstraction/QualitativeResult.cpp index 9ff82eefa..34c25c101 100644 --- a/src/storm/abstraction/QualitativeResult.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/QualitativeResult.h similarity index 100% rename from src/storm/abstraction/QualitativeResult.h rename to src/storm-gamebased-ar/abstraction/QualitativeResult.h diff --git a/src/storm/abstraction/QualitativeResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/QualitativeResultMinMax.cpp similarity index 89% rename from src/storm/abstraction/QualitativeResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/QualitativeResultMinMax.cpp index 86ea9e242..e7d80dc1f 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.cpp +++ b/src/storm-gamebased-ar/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/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm-gamebased-ar/abstraction/QualitativeResultMinMax.h similarity index 100% rename from src/storm/abstraction/QualitativeResultMinMax.h rename to src/storm-gamebased-ar/abstraction/QualitativeResultMinMax.h diff --git a/src/storm/abstraction/RefinementCommand.cpp b/src/storm-gamebased-ar/abstraction/RefinementCommand.cpp similarity index 93% rename from src/storm/abstraction/RefinementCommand.cpp rename to src/storm-gamebased-ar/abstraction/RefinementCommand.cpp index 18b70b8f7..d97e96069 100644 --- a/src/storm/abstraction/RefinementCommand.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/RefinementCommand.h similarity index 100% rename from src/storm/abstraction/RefinementCommand.h rename to src/storm-gamebased-ar/abstraction/RefinementCommand.h diff --git a/src/storm/abstraction/StateSet.cpp b/src/storm-gamebased-ar/abstraction/StateSet.cpp similarity index 88% rename from src/storm/abstraction/StateSet.cpp rename to src/storm-gamebased-ar/abstraction/StateSet.cpp index ec43a0ab2..237b766ef 100644 --- a/src/storm/abstraction/StateSet.cpp +++ b/src/storm-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 b/src/storm-gamebased-ar/abstraction/StateSet.h similarity index 100% rename from src/storm/abstraction/StateSet.h rename to src/storm-gamebased-ar/abstraction/StateSet.h diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm-gamebased-ar/abstraction/StateSetAbstractor.cpp similarity index 98% rename from src/storm/abstraction/StateSetAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/StateSetAbstractor.cpp index 29e0f0e85..a90e15fa1 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm-gamebased-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 b/src/storm-gamebased-ar/abstraction/StateSetAbstractor.h similarity index 98% rename from src/storm/abstraction/StateSetAbstractor.h rename to src/storm-gamebased-ar/abstraction/StateSetAbstractor.h index 4af20848b..74aabe7cd 100644 --- a/src/storm/abstraction/StateSetAbstractor.h +++ b/src/storm-gamebased-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/src/storm/abstraction/SymbolicQualitativeGameResult.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.cpp similarity index 90% rename from src/storm/abstraction/SymbolicQualitativeGameResult.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.cpp index 9bf0c4a8a..c2737d5a4 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResult.cpp +++ b/src/storm-gamebased-ar/abstraction/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 { diff --git a/src/storm/abstraction/SymbolicQualitativeGameResult.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h similarity index 88% rename from src/storm/abstraction/SymbolicQualitativeGameResult.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h index a209c8b2d..0cd23eb5e 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResult.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/abstraction/SymbolicQualitativeResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h" #include "storm/utility/graph.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.cpp similarity index 91% rename from src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.cpp index 85917b5bd..85cc87301 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h similarity index 83% rename from src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h index 06dfec4a5..31a93c395 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h @@ -2,8 +2,8 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/SymbolicQualitativeGameResult.h" -#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResult.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.cpp similarity index 89% rename from src/storm/abstraction/SymbolicQualitativeMdpResult.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.cpp index 6034c77b5..9969d5aeb 100644 --- a/src/storm/abstraction/SymbolicQualitativeMdpResult.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicQualitativeMdpResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResult.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h similarity index 87% rename from src/storm/abstraction/SymbolicQualitativeMdpResult.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h index a84c1cec9..9bbc1be1a 100644 --- a/src/storm/abstraction/SymbolicQualitativeMdpResult.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/abstraction/SymbolicQualitativeResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h" #include "storm/storage/dd/Bdd.h" diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.cpp similarity index 91% rename from src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.cpp index 7c4b2f4c7..c97f1909d 100644 --- a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicQualitativeMdpResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.h similarity index 83% rename from src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.h index 0266da256..44feca195 100644 --- a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.h @@ -2,8 +2,8 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/SymbolicQualitativeMdpResult.h" -#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/SymbolicQualitativeResult.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h similarity index 88% rename from src/storm/abstraction/SymbolicQualitativeResult.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h index 4428980e9..95efaea33 100644 --- a/src/storm/abstraction/SymbolicQualitativeResult.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResult.h @@ -2,7 +2,7 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/QualitativeResult.h" +#include "storm-gamebased-ar/abstraction/QualitativeResult.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.cpp similarity index 89% rename from src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.cpp index 44cc04479..2309f4408 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.cpp @@ -1,7 +1,7 @@ -#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" -#include "storm/abstraction/QualitativeResult.h" +#include "storm-gamebased-ar/abstraction/QualitativeResult.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h similarity index 93% rename from src/storm/abstraction/SymbolicQualitativeResultMinMax.h rename to src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h index 2ece2da63..78f35652b 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQualitativeResultMinMax.h @@ -4,7 +4,7 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/QualitativeResultMinMax.h" +#include "storm-gamebased-ar/abstraction/QualitativeResultMinMax.h" namespace storm { namespace dd { diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.cpp similarity index 97% rename from src/storm/abstraction/SymbolicQuantitativeGameResult.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.cpp index 018a69c0f..079a1d1ba 100644 --- a/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicQuantitativeGameResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResult.h b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.h similarity index 100% rename from src/storm/abstraction/SymbolicQuantitativeGameResult.h rename to src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.h diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.cpp similarity index 87% rename from src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.cpp index 2fa8a0f75..5028601d3 100644 --- a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicQuantitativeGameResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.h similarity index 88% rename from src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h rename to src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.h index 0f5605114..120d7f1b4 100644 --- a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResultMinMax.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/abstraction/SymbolicQuantitativeGameResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQuantitativeGameResult.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/SymbolicStateSet.cpp b/src/storm-gamebased-ar/abstraction/SymbolicStateSet.cpp similarity index 91% rename from src/storm/abstraction/SymbolicStateSet.cpp rename to src/storm-gamebased-ar/abstraction/SymbolicStateSet.cpp index 8f5b4daf8..42af52fd3 100644 --- a/src/storm/abstraction/SymbolicStateSet.cpp +++ b/src/storm-gamebased-ar/abstraction/SymbolicStateSet.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/SymbolicStateSet.h" +#include "storm-gamebased-ar/abstraction/SymbolicStateSet.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { diff --git a/src/storm/abstraction/SymbolicStateSet.h b/src/storm-gamebased-ar/abstraction/SymbolicStateSet.h similarity index 89% rename from src/storm/abstraction/SymbolicStateSet.h rename to src/storm-gamebased-ar/abstraction/SymbolicStateSet.h index 4effcc7fe..3e8080c11 100644 --- a/src/storm/abstraction/SymbolicStateSet.h +++ b/src/storm-gamebased-ar/abstraction/SymbolicStateSet.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/abstraction/StateSet.h" +#include "storm-gamebased-ar/abstraction/StateSet.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdType.h" diff --git a/src/storm/abstraction/ValidBlockAbstractor.cpp b/src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.cpp similarity index 98% rename from src/storm/abstraction/ValidBlockAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.cpp index 66564a2a8..382de9dc8 100644 --- a/src/storm/abstraction/ValidBlockAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.cpp @@ -1,6 +1,6 @@ -#include "storm/abstraction/ValidBlockAbstractor.h" +#include "storm-gamebased-ar/abstraction/ValidBlockAbstractor.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/ValidBlockAbstractor.h b/src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.h similarity index 97% rename from src/storm/abstraction/ValidBlockAbstractor.h rename to src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.h index 1ce760e10..5b693113b 100644 --- a/src/storm/abstraction/ValidBlockAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/ValidBlockAbstractor.h @@ -8,7 +8,7 @@ #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/LocalExpressionInformation.h" +#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h" #include "storm/solver/SmtSolver.h" diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.cpp similarity index 96% rename from src/storm/abstraction/jani/AutomatonAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.cpp index 0ca8a34b3..f4bc2b4f4 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.cpp @@ -1,8 +1,8 @@ -#include "storm/abstraction/jani/AutomatonAbstractor.h" +#include "storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.h" -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.h similarity index 98% rename from src/storm/abstraction/jani/AutomatonAbstractor.h rename to src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.h index 04b49802b..37252495d 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.h @@ -2,7 +2,7 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/jani/EdgeAbstractor.h" +#include "storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h" #include "storm/settings/modules/AbstractionSettings.h" diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.cpp similarity index 99% rename from src/storm/abstraction/jani/EdgeAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.cpp index 8727e0e87..bf801ce34 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.cpp @@ -1,11 +1,11 @@ -#include "storm/abstraction/jani/EdgeAbstractor.h" +#include "storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h" #include #include -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h similarity index 98% rename from src/storm/abstraction/jani/EdgeAbstractor.h rename to src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h index 3fb4ee599..ce2f19c37 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h @@ -5,9 +5,9 @@ #include #include -#include "storm/abstraction/GameBddResult.h" -#include "storm/abstraction/LocalExpressionInformation.h" -#include "storm/abstraction/StateSetAbstractor.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h" +#include "storm-gamebased-ar/abstraction/StateSetAbstractor.h" #include "storm/storage/expressions/ExpressionEvaluator.h" diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.cpp similarity index 98% rename from src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.cpp index 7f99bd953..908727abd 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -1,8 +1,8 @@ -#include "storm/abstraction/jani/JaniMenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h" -#include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/ExpressionTranslator.h" -#include "storm/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/ExpressionTranslator.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" #include "storm/storage/BitVector.h" diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h similarity index 94% rename from src/storm/abstraction/jani/JaniMenuGameAbstractor.h rename to src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h index 228cef986..077522d25 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h @@ -2,12 +2,12 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/MenuGame.h" -#include "storm/abstraction/MenuGameAbstractor.h" -#include "storm/abstraction/RefinementCommand.h" -#include "storm/abstraction/ValidBlockAbstractor.h" -#include "storm/abstraction/jani/AutomatonAbstractor.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/MenuGame.h" +#include "storm-gamebased-ar/abstraction/MenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/RefinementCommand.h" +#include "storm-gamebased-ar/abstraction/ValidBlockAbstractor.h" +#include "storm-gamebased-ar/abstraction/jani/AutomatonAbstractor.h" #include "storm/storage/dd/Add.h" diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.cpp similarity index 99% rename from src/storm/abstraction/prism/CommandAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.cpp index 2dbd03322..0de8440c9 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.cpp @@ -1,11 +1,11 @@ -#include "storm/abstraction/prism/CommandAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/CommandAbstractor.h" #include #include -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.h similarity index 98% rename from src/storm/abstraction/prism/CommandAbstractor.h rename to src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.h index 1072f041e..505639fbc 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/prism/CommandAbstractor.h @@ -5,9 +5,9 @@ #include #include -#include "storm/abstraction/GameBddResult.h" -#include "storm/abstraction/LocalExpressionInformation.h" -#include "storm/abstraction/StateSetAbstractor.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h" +#include "storm-gamebased-ar/abstraction/StateSetAbstractor.h" #include "storm/storage/expressions/ExpressionEvaluator.h" diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.cpp similarity index 96% rename from src/storm/abstraction/prism/ModuleAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.cpp index 7cb59c4bb..201cd8261 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.cpp @@ -1,8 +1,8 @@ -#include "storm/abstraction/prism/ModuleAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/ModuleAbstractor.h" -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.h similarity index 98% rename from src/storm/abstraction/prism/ModuleAbstractor.h rename to src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.h index 11151cc19..637933e18 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/prism/ModuleAbstractor.h @@ -2,7 +2,7 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/prism/CommandAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/CommandAbstractor.h" #include "storm/settings/modules/AbstractionSettings.h" diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.cpp similarity index 98% rename from src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp rename to src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.cpp index c46b9eec4..697e8d654 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -1,8 +1,8 @@ -#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h" -#include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/ExpressionTranslator.h" -#include "storm/abstraction/GameBddResult.h" +#include "storm-gamebased-ar/abstraction/BottomStateResult.h" +#include "storm-gamebased-ar/abstraction/ExpressionTranslator.h" +#include "storm-gamebased-ar/abstraction/GameBddResult.h" #include "storm/storage/BitVector.h" diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h similarity index 94% rename from src/storm/abstraction/prism/PrismMenuGameAbstractor.h rename to src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h index 2bf1ea368..443b5feee 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h @@ -2,12 +2,12 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/AbstractionInformation.h" -#include "storm/abstraction/MenuGame.h" -#include "storm/abstraction/MenuGameAbstractor.h" -#include "storm/abstraction/RefinementCommand.h" -#include "storm/abstraction/ValidBlockAbstractor.h" -#include "storm/abstraction/prism/ModuleAbstractor.h" +#include "storm-gamebased-ar/abstraction/AbstractionInformation.h" +#include "storm-gamebased-ar/abstraction/MenuGame.h" +#include "storm-gamebased-ar/abstraction/MenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/RefinementCommand.h" +#include "storm-gamebased-ar/abstraction/ValidBlockAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/ModuleAbstractor.h" #include "storm/storage/dd/Add.h" diff --git a/src/storm-gamebased-ar/api/verification.h b/src/storm-gamebased-ar/api/verification.h new file mode 100644 index 000000000..c761293c1 --- /dev/null +++ b/src/storm-gamebased-ar/api/verification.h @@ -0,0 +1,106 @@ +#pragma once + +#include "storm/environment/Environment.h" + +#include "storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" +#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h" + +namespace storm::api { +// +// Verifying with Abstraction Refinement engine +// +struct AbstractionRefinementOptions { + AbstractionRefinementOptions() = default; + AbstractionRefinementOptions(std::vector&& constraints, + std::vector>&& injectedRefinementPredicates) + : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { + // Intentionally left empty. + } + + std::vector constraints; + std::vector> injectedRefinementPredicates; +}; + +template +typename std::enable_if::value, std::unique_ptr>::type +verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const& model, + storm::modelchecker::CheckTask const& task, + AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { + storm::modelchecker::GameBasedMdpModelCheckerOptions modelCheckerOptions(options.constraints, options.injectedRefinementPredicates); + + std::unique_ptr result; + if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + } else if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP) { + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "The model type " << model.getModelType() << " is not supported by the abstraction refinement engine."); + } + return result; +} + +template +typename std::enable_if::value, std::unique_ptr>::type +verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const&, + storm::modelchecker::CheckTask const&, + AbstractionRefinementOptions const& = AbstractionRefinementOptions()) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); +} + +template +std::unique_ptr verifyWithAbstractionRefinementEngine( + storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, + AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { + Environment env; + return verifyWithAbstractionRefinementEngine(env, model, task, options); +} + +template +typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine( + storm::Environment const& env, std::shared_ptr> const& model, + storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + model->getManager().execute([&]() { + if (model->getType() == storm::models::ModelType::Dtmc) { + storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker( + *model->template as>()); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker( + *model->template as>()); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "The model type " << model->getType() << " is not supported by the abstraction refinement engine."); + } + }); + return result; +} + +template +typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine( + storm::Environment const&, std::shared_ptr> const&, + storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); +} + +template +std::unique_ptr verifyWithAbstractionRefinementEngine( + std::shared_ptr> const& model, + storm::modelchecker::CheckTask const& task) { + Environment env; + return verifyWithAbstractionRefinementEngine(env, model, task); +} + +} // namespace storm::api \ No newline at end of file diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp similarity index 99% rename from src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp rename to src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index d271cd3f2..919fb32df 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" +#include "storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" @@ -22,12 +22,12 @@ #include "storm/solver/SymbolicGameSolver.h" -#include "storm/abstraction/QualitativeResultMinMax.h" -#include "storm/abstraction/StateSet.h" -#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" -#include "storm/abstraction/SymbolicQualitativeMdpResult.h" -#include "storm/abstraction/SymbolicQualitativeMdpResultMinMax.h" -#include "storm/abstraction/SymbolicStateSet.h" +#include "storm-gamebased-ar/abstraction/QualitativeResultMinMax.h" +#include "storm-gamebased-ar/abstraction/StateSet.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeMdpResultMinMax.h" +#include "storm-gamebased-ar/abstraction/SymbolicStateSet.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/AbstractionSettings.h" diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h similarity index 100% rename from src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h rename to src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp similarity index 97% rename from src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp rename to src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp index 9c438298b..5180046ab 100644 --- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp +++ b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp @@ -1,11 +1,11 @@ -#include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" +#include "storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" -#include "storm/abstraction/SymbolicStateSet.h" +#include "storm-gamebased-ar/abstraction/SymbolicStateSet.h" #include "storm/storage/dd/BisimulationDecomposition.h" diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h similarity index 95% rename from src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h rename to src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h index 140e89012..b8ce12a99 100644 --- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h +++ b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h @@ -2,7 +2,7 @@ #include -#include "storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" +#include "storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" namespace storm { namespace models { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp similarity index 98% rename from src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp rename to src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 18dd0c1f2..6fc8874d7 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -11,6 +11,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/VariableSetPredicateSplitter.h" +#include "storm/storage/ExplicitGameStrategyPair.h" #include "storm/storage/jani/Automaton.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/Edge.h" @@ -22,13 +23,12 @@ #include "storm/storage/dd/DdManager.h" -#include "storm/abstraction/ExplicitGameStrategyPair.h" -#include "storm/abstraction/MenuGameRefiner.h" -#include "storm/abstraction/jani/JaniMenuGameAbstractor.h" -#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h" +#include "storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.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/logic/FragmentSpecification.h" @@ -55,11 +55,11 @@ namespace storm { namespace modelchecker { using detail::PreviousExplicitResult; -using storm::abstraction::ExplicitGameStrategyPair; using storm::abstraction::ExplicitQuantitativeResult; using storm::abstraction::ExplicitQuantitativeResultMinMax; using storm::abstraction::SymbolicQuantitativeGameResult; using storm::abstraction::SymbolicQuantitativeGameResultMinMax; +using storm::storage::ExplicitGameStrategyPair; template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, @@ -482,9 +482,10 @@ template ExplicitQuantitativeResult computeQuantitativeResult( Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, - ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair, + ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, storage::ExplicitGameStrategyPair& strategyPair, storm::dd::Odd const& odd, ExplicitQuantitativeResult const* startingQuantitativeResult = nullptr, - ExplicitGameStrategyPair const* startingStrategyPair = nullptr, boost::optional> const& previousResult = boost::none) { + storage::ExplicitGameStrategyPair const* startingStrategyPair = nullptr, + boost::optional> const& previousResult = boost::none) { bool player2Min = player2Direction == storm::OptimizationDirection::Minimize; auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States(); @@ -879,8 +880,8 @@ std::unique_ptr GameBasedMdpModelChecker::performS } template -void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, - abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, +void postProcessStrategies(storm::OptimizationDirection const& player1Direction, storage::ExplicitGameStrategyPair& minStrategyPair, + storage::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) { @@ -982,8 +983,8 @@ class ExplicitGameExporter { void exportToJson(std::string const& filename, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, - ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, - ExplicitGameStrategyPair const* maxStrategyPair) { + ExplicitQuantitativeResultMinMax const& quantitativeResult, storage::ExplicitGameStrategyPair const* minStrategyPair, + storage::ExplicitGameStrategyPair const* maxStrategyPair) { // Export game as json. std::ofstream outfile(filename); exportGame(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, @@ -1089,8 +1090,8 @@ class ExplicitGameExporter { void exportGame(std::ofstream& out, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, - ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, - ExplicitGameStrategyPair const* maxStrategyPair) { + ExplicitQuantitativeResultMinMax const& quantitativeResult, storage::ExplicitGameStrategyPair const* minStrategyPair, + storage::ExplicitGameStrategyPair const* maxStrategyPair) { // To export the game as JSON, we build some data structures through a traversal and then emit them. std::vector nodes; std::vector edges; @@ -1188,8 +1189,8 @@ class ExplicitGameExporter { }; template -void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, - abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, +void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection const& player1Direction, storage::ExplicitGameStrategyPair& minStrategyPair, + storage::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, @@ -1419,8 +1420,8 @@ std::unique_ptr GameBasedMdpModelChecker::performE STORM_LOG_INFO("Translation to explicit representation completed in " << translationWatch.getTimeInMilliseconds() << "ms."); // Prepare the two strategies. - abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); - abstraction::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); + storage::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); + storage::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). storm::utility::Stopwatch qualitativeWatch(true); @@ -1637,8 +1638,8 @@ ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::c boost::optional> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, - storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, - abstraction::ExplicitGameStrategyPair& maxStrategyPair) { + storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, storage::ExplicitGameStrategyPair& minStrategyPair, + storage::ExplicitGameStrategyPair& maxStrategyPair) { ExplicitQualitativeGameResultMinMax result; // ExplicitQualitativeGameResult problematicStates = storm::utility::graph::performProb0(transitionMatrix, player1Groups, diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h similarity index 88% rename from src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h rename to src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h index 057e2b1cb..433334c49 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -12,9 +12,9 @@ #include "storm/storage/SymbolicModelDescription.h" -#include "storm/abstraction/ExplicitQuantitativeResult.h" -#include "storm/abstraction/SymbolicQualitativeGameResult.h" -#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" +#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResult.h" +#include "storm-gamebased-ar/abstraction/SymbolicQualitativeGameResultMinMax.h" #include "storm/logic/Bound.h" @@ -157,15 +157,12 @@ class GameBasedMdpModelChecker : public AbstractModelChecker { storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousResult, - storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, - storm::storage::SparseMatrix const& transitionMatrix, - std::vector const& player1RowGrouping, - storm::storage::SparseMatrix const& player1BackwardTransitions, - std::vector const& player2BackwardTransitions, - storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, - abstraction::ExplicitGameStrategyPair& minStrategyPair, - abstraction::ExplicitGameStrategyPair& maxStrategyPair); + ExplicitQualitativeGameResultMinMax computeProb01States( + boost::optional> const& previousResult, storm::dd::Odd const& odd, + storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, + std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, + std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, + storm::storage::BitVector const& targetStates, storage::ExplicitGameStrategyPair& minStrategyPair, storage::ExplicitGameStrategyPair& maxStrategyPair); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const; diff --git a/src/storm-pars/analysis/MonotonicityHelper.cpp b/src/storm-pars/analysis/MonotonicityHelper.cpp index 4fc8292c4..c9524a674 100644 --- a/src/storm-pars/analysis/MonotonicityHelper.cpp +++ b/src/storm-pars/analysis/MonotonicityHelper.cpp @@ -11,6 +11,7 @@ #include "storm/exceptions/NotImplementedException.h" #include "storm-pars/analysis/AssumptionChecker.h" +#include "storm/utility/Stopwatch.h" namespace storm { diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index 8ac469018..f1e79badb 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -6,11 +6,13 @@ #include "storm/adapters/RationalFunctionAdapter.h" + #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Dtmc.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/Stopwatch.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 52210f69b..5b68f5649 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -9,10 +9,12 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" + #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm-pomdp/builder/BeliefMdpExplorer.cpp b/src/storm-pomdp/builder/BeliefMdpExplorer.cpp index 150bae5eb..851bc77c5 100644 --- a/src/storm-pomdp/builder/BeliefMdpExplorer.cpp +++ b/src/storm-pomdp/builder/BeliefMdpExplorer.cpp @@ -12,6 +12,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/utility/SignalHandler.h" #include "storm/utility/constants.h" +#include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 3123b2485..d12b63f57 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -4,8 +4,6 @@ #include "storm/environment/Environment.h" -#include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" -#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" @@ -46,103 +44,6 @@ storm::modelchecker::CheckTask createTask(std: return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); } -// -// Verifying with Abstraction Refinement engine -// -struct AbstractionRefinementOptions { - AbstractionRefinementOptions() = default; - AbstractionRefinementOptions(std::vector&& constraints, - std::vector>&& injectedRefinementPredicates) - : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { - // Intentionally left empty. - } - - std::vector constraints; - std::vector> injectedRefinementPredicates; -}; - -template -typename std::enable_if::value, std::unique_ptr>::type -verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const& model, - storm::modelchecker::CheckTask const& task, - AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { - storm::modelchecker::GameBasedMdpModelCheckerOptions modelCheckerOptions(options.constraints, options.injectedRefinementPredicates); - - std::unique_ptr result; - if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } - } else if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "The model type " << model.getModelType() << " is not supported by the abstraction refinement engine."); - } - return result; -} - -template -typename std::enable_if::value, std::unique_ptr>::type -verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const&, - storm::modelchecker::CheckTask const&, - AbstractionRefinementOptions const& = AbstractionRefinementOptions()) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); -} - -template -std::unique_ptr verifyWithAbstractionRefinementEngine( - storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, - AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { - Environment env; - return verifyWithAbstractionRefinementEngine(env, model, task, options); -} - -template -typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine( - storm::Environment const& env, std::shared_ptr> const& model, - storm::modelchecker::CheckTask const& task) { - std::unique_ptr result; - model->getManager().execute([&]() { - if (model->getType() == storm::models::ModelType::Dtmc) { - storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker( - *model->template as>()); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker( - *model->template as>()); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(env, task); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "The model type " << model->getType() << " is not supported by the abstraction refinement engine."); - } - }); - return result; -} - -template -typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine( - storm::Environment const&, std::shared_ptr> const&, - storm::modelchecker::CheckTask const&) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); -} - -template -std::unique_ptr verifyWithAbstractionRefinementEngine( - std::shared_ptr> const& model, - storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithAbstractionRefinementEngine(env, model, task); -} - // // Verifying with Exploration engine // diff --git a/src/storm/abstraction/ExplicitGameStrategy.cpp b/src/storm/storage/ExplicitGameStrategy.cpp similarity index 94% rename from src/storm/abstraction/ExplicitGameStrategy.cpp rename to src/storm/storage/ExplicitGameStrategy.cpp index 012f4e89a..1a811eba8 100644 --- a/src/storm/abstraction/ExplicitGameStrategy.cpp +++ b/src/storm/storage/ExplicitGameStrategy.cpp @@ -1,10 +1,10 @@ -#include "storm/abstraction/ExplicitGameStrategy.h" +#include "storm/storage/ExplicitGameStrategy.h" #include #include namespace storm { -namespace abstraction { +namespace storage { const uint64_t ExplicitGameStrategy::UNDEFINED = std::numeric_limits::max(); @@ -61,5 +61,5 @@ std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy return out; } -} // namespace abstraction +} // namespace storage } // namespace storm diff --git a/src/storm/abstraction/ExplicitGameStrategy.h b/src/storm/storage/ExplicitGameStrategy.h similarity index 93% rename from src/storm/abstraction/ExplicitGameStrategy.h rename to src/storm/storage/ExplicitGameStrategy.h index 1b7e68207..7a2f57a53 100644 --- a/src/storm/abstraction/ExplicitGameStrategy.h +++ b/src/storm/storage/ExplicitGameStrategy.h @@ -5,7 +5,7 @@ #include namespace storm { -namespace abstraction { +namespace storage { class ExplicitGameStrategy { public: @@ -28,5 +28,5 @@ class ExplicitGameStrategy { std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy); -} // namespace abstraction +} // namespace storage } // namespace storm diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.cpp b/src/storm/storage/ExplicitGameStrategyPair.cpp similarity index 93% rename from src/storm/abstraction/ExplicitGameStrategyPair.cpp rename to src/storm/storage/ExplicitGameStrategyPair.cpp index c4adc9e10..eedce77c1 100644 --- a/src/storm/abstraction/ExplicitGameStrategyPair.cpp +++ b/src/storm/storage/ExplicitGameStrategyPair.cpp @@ -1,7 +1,7 @@ -#include "storm/abstraction/ExplicitGameStrategyPair.h" +#include "storm/storage/ExplicitGameStrategyPair.h" namespace storm { -namespace abstraction { +namespace storage { ExplicitGameStrategyPair::ExplicitGameStrategyPair(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States) : player1Strategy(numberOfPlayer1States), player2Strategy(numberOfPlayer2States) { @@ -43,5 +43,5 @@ std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& stra return out; } -} // namespace abstraction +} // namespace storage } // namespace storm diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.h b/src/storm/storage/ExplicitGameStrategyPair.h similarity index 89% rename from src/storm/abstraction/ExplicitGameStrategyPair.h rename to src/storm/storage/ExplicitGameStrategyPair.h index 201499311..b9012cab4 100644 --- a/src/storm/abstraction/ExplicitGameStrategyPair.h +++ b/src/storm/storage/ExplicitGameStrategyPair.h @@ -3,10 +3,10 @@ #include #include -#include "storm/abstraction/ExplicitGameStrategy.h" +#include "storm/storage/ExplicitGameStrategy.h" namespace storm { -namespace abstraction { +namespace storage { class ExplicitGameStrategyPair { public: @@ -28,5 +28,5 @@ class ExplicitGameStrategyPair { std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& strategyPair); -} // namespace abstraction +} // namespace storage } // namespace storm diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index c6f2cea1f..eab80b0cb 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -11,7 +11,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/storage/sparse/StateType.h" -#include "storm/abstraction/ExplicitGameStrategyPair.h" +#include "storm/storage/ExplicitGameStrategyPair.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/DeterministicModel.h" @@ -1309,7 +1309,7 @@ ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix co storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair) { + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair) { ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); // Initialize the stack used for the DFS with the states @@ -1519,7 +1519,7 @@ ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix co storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates) { // During the execution, the two state sets in the result hold the potential player 1/2 states. ExplicitGameProb01Result result; @@ -2025,14 +2025,13 @@ template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, - storm::abstraction::ExplicitGameStrategyPair* strategyPair); + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair); template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); @@ -2154,15 +2153,14 @@ template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, - storm::abstraction::ExplicitGameStrategyPair* strategyPair); + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair); template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 0221ebd96..8572110c3 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -51,7 +51,7 @@ class Add; } // namespace dd -namespace abstraction { +namespace storage { class ExplicitGameStrategyPair; } @@ -779,8 +779,7 @@ ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix co storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, - storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr); + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -802,8 +801,7 @@ ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix co storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, - storm::OptimizationDirection const& player2Direction, - storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr, + storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr, boost::optional const& player1Candidates = boost::none); /*! diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 48d02a7c8..1389a9d53 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -1,5 +1,6 @@ add_subdirectory(storm) -add_subdirectory(storm-pars) add_subdirectory(storm-dft) -add_subdirectory(storm-pomdp) +add_subdirectory(storm-gamebased-ar) +add_subdirectory(storm-pars) add_subdirectory(storm-permissive) +add_subdirectory(storm-pomdp) \ No newline at end of file diff --git a/src/test/storm-gamebased-ar/CMakeLists.txt b/src/test/storm-gamebased-ar/CMakeLists.txt new file mode 100644 index 000000000..5fd63554d --- /dev/null +++ b/src/test/storm-gamebased-ar/CMakeLists.txt @@ -0,0 +1,22 @@ +# Base path for test files +set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-gamebased-ar") + +# Test Sources +file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" test) + +# Note that the tests also need the source files, except for the main file +include_directories(${GTEST_INCLUDE_DIR}) + +foreach (testsuite modelchecker abstraction) + file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) + add_executable(test-gamebased-ar-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) + target_link_libraries(test-gamebased-ar-${testsuite} storm-gamebased-ar storm-parsers) + target_link_libraries(test-gamebased-ar-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) + + add_dependencies(test-gamebased-ar-${testsuite} test-resources) + add_test(NAME run-test-gamebased-ar-${testsuite} COMMAND $) + add_dependencies(tests test-gamebased-ar-${testsuite}) + +endforeach () diff --git a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp new file mode 100644 index 000000000..48f006fd6 --- /dev/null +++ b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp @@ -0,0 +1,460 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/PrismParser.h" +#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/dd/DdManager.h" +#include "storm/utility/graph.h" + +#ifdef STORM_HAVE_MSAT + +#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h" +#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h" + +#include "storm/storage/expressions/Expression.h" + +#include "storm/utility/solver.h" + +TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); + + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); + + storm::abstraction::MenuGame game = abstractor.abstract(); + + // The target states are those states where !(s < 3). + storm::dd::Bdd targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); + + storm::utility::graph::SymbolicGameProb01Result result = + storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + refiner.refine({manager.getVariableExpression("s") < manager.integer(2)}); + game = abstractor.abstract(); + + // We need to create a new BDD for the target states since the reachable states might have changed. + targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. + storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one action in each state. + storm::dd::Add stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + EXPECT_EQ(0ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). + storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(0.0, stateDistributionCount.getMax()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); + EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. + storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one action in each state. + stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + EXPECT_EQ(8ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). + stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); +} + +TEST(GraphTestAR, SymbolicProb01StochasticGameTwoDice) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); + program = program.substituteConstantsFormulas(); + program = program.flattenModules(std::make_unique()); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6)); + + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); + + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); + + storm::abstraction::MenuGame game = abstractor.abstract(); + + // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2. + storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && + abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && + game.getReachableStates(); + + storm::utility::graph::SymbolicGameProb01Result result = + storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. + storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one exaction in each state. + storm::dd::Add stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + EXPECT_EQ(153ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. + storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one action in each state. + stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + EXPECT_EQ(1ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). + stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); +} + +TEST(GraphTestAR, SymbolicProb01StochasticGameWlan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); + program = program.substituteConstantsFormulas(); + program = program.flattenModules(std::make_unique()); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2)); + + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12)); + + initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14)); + initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15)); + + initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12)); + + initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1)); + + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14)); + initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15)); + + initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); + + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); + + storm::abstraction::MenuGame game = abstractor.abstract(); + + // The target states are those states where col == 2. + storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates(); + + storm::utility::graph::SymbolicGameProb01Result result = + storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. + storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one action in each state. + storm::dd::Add stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + ; + EXPECT_EQ(2831ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). + storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); + + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, + storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); + EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); + + // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. + storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); + EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); + + // Proceed by checking whether they select exactly one action in each state. + stateDistributionsUnderStrategies = + (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) + .sumAbstract(game.getColumnVariables()); + EXPECT_EQ(2884ull, stateDistributionsUnderStrategies.getNonZeroCount()); + + // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). + stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); +} + +#endif \ No newline at end of file diff --git a/src/test/storm/abstraction/PrismMenuGameTest.cpp b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp similarity index 99% rename from src/test/storm/abstraction/PrismMenuGameTest.cpp rename to src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp index c4f32286c..855b838d4 100644 --- a/src/test/storm/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp @@ -5,8 +5,8 @@ #include "storm-parsers/parser/PrismParser.h" -#include "storm/abstraction/MenuGameRefiner.h" -#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h" +#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/test/storm/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp similarity index 98% rename from src/test/storm/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp rename to src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp index 50f46be75..01b8046c4 100644 --- a/src/test/storm/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp @@ -1,11 +1,11 @@ #include "storm-config.h" #include "test/storm_gtest.h" +#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/logic/Formulas.h" -#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp similarity index 99% rename from src/test/storm/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp rename to src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp index f0b7d26bc..8d7247220 100644 --- a/src/test/storm/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp @@ -1,9 +1,9 @@ #include "storm-config.h" #include "test/storm_gtest.h" +#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" -#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/models/sparse/Model.h" #include "storm/models/symbolic/StandardRewardModel.h" diff --git a/src/test/storm-gamebased-ar/storm-test.cpp b/src/test/storm-gamebased-ar/storm-test.cpp new file mode 100644 index 000000000..2c189b7c9 --- /dev/null +++ b/src/test/storm-gamebased-ar/storm-test.cpp @@ -0,0 +1,9 @@ +#include "storm/settings/SettingsManager.h" +#include "test/storm_gtest.h" + +int main(int argc, char **argv) { + storm::settings::initializeAll("Storm-gamebased-ar (Functional) Testing Suite", "test-gamebased-ar"); + storm::test::initialize(); + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +} diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index 1f76f9374..87f04a5ed 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -15,6 +15,7 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/graph.h" #include "test/storm_gtest.h" diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index b59c99e23..ed117a430 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -14,6 +14,7 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/graph.h" TEST(AssumptionMakerTest, Brp_without_bisimulation) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index 6fda1867b..514e38694 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -14,6 +14,7 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" #include "test/storm_gtest.h" diff --git a/src/test/storm-pars/analysis/OrderExtenderTest.cpp b/src/test/storm-pars/analysis/OrderExtenderTest.cpp index b638173bc..5f72d274b 100644 --- a/src/test/storm-pars/analysis/OrderExtenderTest.cpp +++ b/src/test/storm-pars/analysis/OrderExtenderTest.cpp @@ -13,6 +13,7 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/graph.h" #include "test/storm_gtest.h" diff --git a/src/test/storm-pars/analysis/OrderTest.cpp b/src/test/storm-pars/analysis/OrderTest.cpp index 31b1e7b9d..afcf4678e 100644 --- a/src/test/storm-pars/analysis/OrderTest.cpp +++ b/src/test/storm-pars/analysis/OrderTest.cpp @@ -3,6 +3,7 @@ #include "storm-config.h" #include "storm-pars/api/analysis.h" #include "storm/storage/BitVector.h" +#include "storm/utility/graph.h" TEST(OrderTest, Simple) { auto numberOfStates = 7; diff --git a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp index 734e32d57..df2d2c4c7 100644 --- a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp +++ b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp @@ -5,6 +5,7 @@ #include "mathsat.h" #include "storm/adapters/MathsatExpressionAdapter.h" #include "storm/settings/SettingsManager.h" +#include "storm/storage/expressions/OperatorType.h" TEST(MathsatExpressionAdapter, StormToMathsatBasic) { msat_config config = msat_create_config(); diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp index 99b5671b7..024855855 100644 --- a/src/test/storm/utility/GraphTest.cpp +++ b/src/test/storm/utility/GraphTest.cpp @@ -230,449 +230,6 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } } -#ifdef STORM_HAVE_MSAT - -#include "storm/abstraction/MenuGameRefiner.h" -#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" - -#include "storm/storage/expressions/Expression.h" - -#include "storm/utility/solver.h" - -TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - - std::vector initialPredicates; - storm::expressions::ExpressionManager& manager = program.getManager(); - - initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - - auto smtSolverFactory = std::make_shared(); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); - storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); - refiner.refine(initialPredicates); - - storm::abstraction::MenuGame game = abstractor.abstract(); - - // The target states are those states where !(s < 3). - storm::dd::Bdd targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); - - storm::utility::graph::SymbolicGameProb01Result result = - storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - refiner.refine({manager.getVariableExpression("s") < manager.integer(2)}); - game = abstractor.abstract(); - - // We need to create a new BDD for the target states since the reachable states might have changed. - targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - ASSERT_TRUE(result.hasPlayer1Strategy()); - ASSERT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. - storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one action in each state. - storm::dd::Add stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - EXPECT_EQ(0ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). - storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(0.0, stateDistributionCount.getMax()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. - storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one action in each state. - stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - EXPECT_EQ(8ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). - stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1.0, stateDistributionCount.getMax()); -} - -TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - program = program.substituteConstantsFormulas(); - program = program.flattenModules(std::make_unique()); - - std::vector initialPredicates; - storm::expressions::ExpressionManager& manager = program.getManager(); - - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7)); - - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6)); - - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7)); - - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - - auto smtSolverFactory = std::make_shared(); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); - storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); - refiner.refine(initialPredicates); - - storm::abstraction::MenuGame game = abstractor.abstract(); - - // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2. - storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && - abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && - game.getReachableStates(); - - storm::utility::graph::SymbolicGameProb01Result result = - storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); - ASSERT_TRUE(result.hasPlayer1Strategy()); - ASSERT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. - storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one exaction in each state. - storm::dd::Add stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - EXPECT_EQ(153ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1.0, stateDistributionCount.getMax()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. - storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one action in each state. - stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - EXPECT_EQ(1ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). - stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1.0, stateDistributionCount.getMax()); -} - -TEST(GraphTest, SymbolicProb01StochasticGameWlan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); - program = program.substituteConstantsFormulas(); - program = program.flattenModules(std::make_unique()); - - std::vector initialPredicates; - storm::expressions::ExpressionManager& manager = program.getManager(); - - initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2)); - - initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2)); - - initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2)); - - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7)); - - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11)); - initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12)); - - initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1)); - - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14)); - initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15)); - - initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1)); - - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7)); - - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11)); - initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12)); - - initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1)); - - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14)); - initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15)); - - initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); - initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - - auto smtSolverFactory = std::make_shared(); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); - storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); - refiner.refine(initialPredicates); - - storm::abstraction::MenuGame game = abstractor.abstract(); - - // The target states are those states where col == 2. - storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates(); - - storm::utility::graph::SymbolicGameProb01Result result = - storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. - storm::dd::Bdd nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one action in each state. - storm::dd::Add stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - ; - EXPECT_EQ(2831ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). - storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1.0, stateDistributionCount.getMax()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); - - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, - storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); - EXPECT_TRUE(result.hasPlayer1Strategy()); - EXPECT_TRUE(result.hasPlayer2Strategy()); - - // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. - storm::dd::Bdd nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get(); - EXPECT_TRUE(nonProb1StatesWithStrategy.isZero()); - - // Proceed by checking whether they select exactly one action in each state. - stateDistributionsUnderStrategies = - (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) - .sumAbstract(game.getColumnVariables()); - EXPECT_EQ(2884ull, stateDistributionsUnderStrategies.getNonZeroCount()); - - // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). - stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1.0, stateDistributionCount.getMax()); -} - -#endif - TEST(GraphTest, ExplicitProb01) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram();