diff --git a/CMakeLists.txt b/CMakeLists.txt index 766b0dd21..e512bc945 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required (VERSION 2.8.6) +cmake_minimum_required (VERSION 3.2) cmake_policy(VERSION 3.2) # Set project name @@ -168,6 +168,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Intel") elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") message(FATAL_ERROR "Visual Studio compiler is currently not supported.") endif() +set(STORM_COMPILER_VERSION ${CMAKE_CXX_COMPILER_VERSION}) if(CCACHE_FOUND) set(STORM_COMPILER_ID "${STORM_COMPILER_ID} (ccache)") @@ -260,7 +261,7 @@ if ("${CMAKE_GENERATOR}" STREQUAL "Xcode") endif() # Display information about build configuration. -message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID}.") +message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.") if (STORM_DEVELOPER) message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}") message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}") diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 7f9faa2ad..8d414ea64 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -4,10 +4,14 @@ add_custom_target(test-resources) set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty) set(STORM_3RDPARTY_BINARY_DIR ${PROJECT_BINARY_DIR}/resources/3rdparty) -#### -#### Find autoreconf for cudd update step -find_program(AUTORECONF autoreconf) -mark_as_advanced(AUTORECONF) +if (STORM_PYTHON) + find_package(PythonInterp 3 REQUIRED QUIET) + find_package(PythonLibs 3 REQUIRED QUIET) + + message(STATUS "Python executable: ${PYTHON_EXECUTABLE}") + message(STATUS "Python include: ${PYTHON_INCLUDE_DIRS}") + message(STATUS "Python include: ${PYTHON_LIBRARIES}") +endif() ############################################################# ## diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index d4db55653..79edfc071 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -1,7 +1,19 @@ + +#### +#### Find autoreconf for cudd update step +find_program(AUTORECONF autoreconf) +find_program(ACLOCAL aclocal) +mark_as_advanced(AUTORECONF) +mark_as_advanced(ACLOCAL) + if (NOT AUTORECONF) message(FATAL_ERROR "Cannot find autoreconf, cannot compile cudd3.") endif() +if (NOT ACLOCAL) + message(FATAL_ERROR "Cannot find aclocal, cannot compile cudd3.") +endif() + set(CUDD_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib) ExternalProject_Add( diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake index 4db0dff57..834f697d2 100644 --- a/resources/3rdparty/include_xerces.cmake +++ b/resources/3rdparty/include_xerces.cmake @@ -1,7 +1,6 @@ if(USE_XERCESC) - set(XERCESC_FIND_QUIETLY ON) - find_package(Xerces QUIET REQUIRED) - if(XERCESC_FOUND) + find_package(XercesC QUIET) + if(XercesC_FOUND) message(STATUS "Storm - Use system version of xerces.") else() message(STATUS "Storm - Use shipped version of xerces.") @@ -20,13 +19,13 @@ if(USE_XERCESC) ) set(XERCESC_ROOT ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2) - set(XERCESC_INCLUDE ${XERCESC_ROOT}/include) + set(XercesC_INCLUDE_DIRS ${XERCESC_ROOT}/include) set(XERCESC_LIBRARY_PATH ${XERCESC_LIB_DIR}) if(BUILD_STATIC) - set(XERCESC_LIBRARIES ${XERCESC_LIBRARY_PATH}/libxerces-c${STATIC_EXT}) + set(XercesC_LIBRARIES ${XERCESC_LIBRARY_PATH}/libxerces-c${STATIC_EXT}) else() - set(XERCESC_LIBRARIES ${XERCESC_LIBRARY_PATH}/libxerces-c${DYNAMIC_EXT}) + set(XercesC_LIBRARIES ${XERCESC_LIBRARY_PATH}/libxerces-c${DYNAMIC_EXT}) endif() add_dependencies(resources xercesc) @@ -34,7 +33,7 @@ if(USE_XERCESC) message (STATUS "Storm - Linking with xercesc.") set(STORM_HAVE_XERCES ON) - include_directories(${XERCESC_INCLUDE}) + include_directories(${XercesC_INCLUDE_DIRS}) if(APPLE) FIND_LIBRARY(COREFOUNDATION_LIBRARY CoreFoundation ) FIND_LIBRARY(CORESERVICES_LIBRARY CoreServices ) @@ -42,7 +41,7 @@ if(USE_XERCESC) mark_as_advanced(CORESERVICES_LIBRARY) endif() find_package(CURL) - list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES}) + list(APPEND STORM_GSPN_LINK_LIBRARIES ${XercesC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES}) else() message (WARNING "Storm - Building without Xerces disables parsing XML formats (for GSPNs)") endif(USE_XERCESC) diff --git a/resources/cmake/find_modules/FindXerces.cmake b/resources/cmake/find_modules/FindXerces.cmake index aa137b50c..f16483769 100644 --- a/resources/cmake/find_modules/FindXerces.cmake +++ b/resources/cmake/find_modules/FindXerces.cmake @@ -12,14 +12,6 @@ IF (XERCESC_INCLUDE AND XERCESC_LIBRARY) SET(XERCESC_FIND_QUIETLY TRUE) ENDIF (XERCESC_INCLUDE AND XERCESC_LIBRARY) -OPTION(XERCESC_STATIC "Set to ON to link your project with static library (instead of DLL)." ON) - -IF (NOT ${XERCESC_WAS_STATIC} STREQUAL ${XERCESC_STATIC}) - UNSET(XERCESC_LIBRARY CACHE) - UNSET(XERCESC_LIBRARY_DEBUG CACHE) -ENDIF (NOT ${XERCESC_WAS_STATIC} STREQUAL ${XERCESC_STATIC}) - -SET(XERCESC_WAS_STATIC ${XERCESC_STATIC} CACHE INTERNAL "" ) FIND_PATH(XERCESC_INCLUDE NAMES xercesc/util/XercesVersion.hpp PATHS @@ -101,4 +93,4 @@ IF(XERCESC_FOUND) ENDIF(XERCESC_FOUND) -MARK_AS_ADVANCED(XERCESC_INCLUDE XERCESC_LIBRARIES) \ No newline at end of file +MARK_AS_ADVANCED(XERCESC_INCLUDE XERCESC_LIBRARIES) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0fec9497c..80f7bd9b7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,4 +1,8 @@ add_subdirectory(storm) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) +add_subdirectory(storm-gspn) +add_subdirectory(storm-gspn-cli) +add_subdirectory(storm-dft) +add_subdirectory(storm-dft-cli) add_subdirectory(test) diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt new file mode 100644 index 000000000..f44c57103 --- /dev/null +++ b/src/storm-dft-cli/CMakeLists.txt @@ -0,0 +1,4 @@ +# Create storm-dft. +add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) +target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode +set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") \ No newline at end of file diff --git a/src/storm/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp similarity index 97% rename from src/storm/storm-dyftee.cpp rename to src/storm-dft-cli/storm-dyftee.cpp index e7e3002aa..fe5c1ad47 100644 --- a/src/storm/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -1,18 +1,17 @@ #include "storm/logic/Formula.h" #include "storm/utility/initialize.h" #include "storm/utility/storm.h" -#include "storm/parser/DFTGalileoParser.h" -#include "storm/modelchecker/dft/DFTModelChecker.h" +#include "storm-dft/parser/DFTGalileoParser.h" +#include "storm-dft/modelchecker/dft/DFTModelChecker.h" -#include "storm/modelchecker/dft/DFTASFChecker.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm/cli/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" -#include "storm/builder/DftSmtBuilder.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/DFTSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" //#include "storm/settings/modules/CounterexampleGeneratorSettings.h" diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt new file mode 100644 index 000000000..df0c067e0 --- /dev/null +++ b/src/storm-dft/CMakeLists.txt @@ -0,0 +1,13 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-dft/*.h ${PROJECT_SOURCE_DIR}/src/storm-dft/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-dft) + + + +file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp) +file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) + + +# Create storm-pgcl. +add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) +target_link_libraries(storm-dft storm ${STORM_DFT_LINK_LIBRARIES}) diff --git a/src/storm/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp similarity index 98% rename from src/storm/builder/DftExplorationHeuristic.cpp rename to src/storm-dft/builder/DftExplorationHeuristic.cpp index 9662c48ba..0bcbd98ae 100644 --- a/src/storm/builder/DftExplorationHeuristic.cpp +++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp @@ -1,4 +1,5 @@ -#include "storm/builder/DftExplorationHeuristic.h" +#include "DftExplorationHeuristic.h" + #include "storm/adapters/CarlAdapter.h" #include "storm/utility/macros.h" #include "storm/utility/constants.h" diff --git a/src/storm/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h similarity index 97% rename from src/storm/builder/DftExplorationHeuristic.h rename to src/storm-dft/builder/DftExplorationHeuristic.h index af8aef4a1..874cfb586 100644 --- a/src/storm/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -1,6 +1,4 @@ -#ifndef STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ -#define STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ - +#pragma once #include namespace storm { @@ -186,5 +184,3 @@ namespace storm { } } - -#endif /* STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ */ diff --git a/src/storm/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp similarity index 99% rename from src/storm/builder/ExplicitDFTModelBuilder.cpp rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index de261ce2a..bdee4eedc 100644 --- a/src/storm/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -1,12 +1,16 @@ -#include "storm/builder/ExplicitDFTModelBuilder.h" +#include "ExplicitDFTModelBuilder.h" + +#include + #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Ctmc.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" #include "storm/exceptions/UnexpectedException.h" -#include "storm/settings/modules/DFTSettings.h" #include "storm/settings/SettingsManager.h" -#include + +#include "storm-dft/settings/modules/DFTSettings.h" + namespace storm { namespace builder { diff --git a/src/storm/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h similarity index 95% rename from src/storm/builder/ExplicitDFTModelBuilder.h rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h index f79ee5b2f..d3d191a8a 100644 --- a/src/storm/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -1,17 +1,23 @@ -#ifndef EXPLICITDFTMODELBUILDER_H -#define EXPLICITDFTMODELBUILDER_H +#pragma once + +#include +#include +#include +#include + #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Model.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/BitVectorHashMap.h" -#include "storm/storage/dft/DFT.h" -#include "storm/storage/dft/SymmetricUnits.h" -#include -#include -#include -#include + +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/storage/dft/SymmetricUnits.h" + + + + namespace storm { namespace builder { @@ -93,5 +99,3 @@ namespace storm { }; } } - -#endif /* EXPLICITDFTMODELBUILDER_H */ diff --git a/src/storm/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp similarity index 99% rename from src/storm/builder/ExplicitDFTModelBuilderApprox.cpp rename to src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 0581ecc12..194372a30 100644 --- a/src/storm/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -1,13 +1,17 @@ -#include "storm/builder/ExplicitDFTModelBuilderApprox.h" +#include "ExplicitDFTModelBuilderApprox.h" + +#include + #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Ctmc.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" #include "storm/utility/bitoperations.h" #include "storm/exceptions/UnexpectedException.h" -#include "storm/settings/modules/DFTSettings.h" #include "storm/settings/SettingsManager.h" -#include + +#include "storm-dft/settings/modules/DFTSettings.h" + namespace storm { namespace builder { diff --git a/src/storm/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h similarity index 97% rename from src/storm/builder/ExplicitDFTModelBuilderApprox.h rename to src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 3533d077f..52bcbf2c9 100644 --- a/src/storm/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -1,22 +1,23 @@ -#ifndef EXPLICITDFTMODELBUILDERAPPROX_H -#define EXPLICITDFTMODELBUILDERAPPROX_H +#pragma once -#include "storm/builder/DftExplorationHeuristic.h" -#include "storm/models/sparse/StateLabeling.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/sparse/Model.h" -#include "storm/generator/DftNextStateGenerator.h" -#include "storm/storage/SparseMatrix.h" -#include "storm/storage/sparse/StateStorage.h" -#include "storm/storage/dft/DFT.h" -#include "storm/storage/dft/SymmetricUnits.h" -#include "storm/storage/BucketPriorityQueue.h" #include #include #include #include #include +#include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/sparse/StateStorage.h" + +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/storage/dft/SymmetricUnits.h" +#include "storm-dft/storage/BucketPriorityQueue.h" + namespace storm { namespace builder { @@ -331,5 +332,3 @@ namespace storm { } } - -#endif /* EXPLICITDFTMODELBUILDERAPPROX_H */ diff --git a/src/storm/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp similarity index 99% rename from src/storm/generator/DftNextStateGenerator.cpp rename to src/storm-dft/generator/DftNextStateGenerator.cpp index 023bcd85a..3f1361f93 100644 --- a/src/storm/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -1,4 +1,4 @@ -#include "storm/generator/DftNextStateGenerator.h" +#include "DftNextStateGenerator.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" diff --git a/src/storm/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h similarity index 93% rename from src/storm/generator/DftNextStateGenerator.h rename to src/storm-dft/generator/DftNextStateGenerator.h index fa8295a4f..2f614afe6 100644 --- a/src/storm/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -1,11 +1,11 @@ -#ifndef STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ -#define STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ +#pragma once #include "storm/generator/NextStateGenerator.h" -#include "storm/storage/dft/DFT.h" - #include "storm/utility/ConstantsComparator.h" +#include "storm-dft/storage/dft/DFT.h" + + namespace storm { namespace generator { @@ -69,5 +69,3 @@ namespace storm { } } - -#endif /* STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ */ diff --git a/src/storm/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp similarity index 100% rename from src/storm/modelchecker/dft/DFTASFChecker.cpp rename to src/storm-dft/modelchecker/dft/DFTASFChecker.cpp diff --git a/src/storm/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h similarity index 97% rename from src/storm/modelchecker/dft/DFTASFChecker.h rename to src/storm-dft/modelchecker/dft/DFTASFChecker.h index 6e7d31e79..c4a47116d 100644 --- a/src/storm/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -3,7 +3,8 @@ #include #include #include -#include "storm/storage/dft/DFT.h" + +#include "storm-dft/storage/dft/DFT.h" namespace storm { diff --git a/src/storm/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp similarity index 98% rename from src/storm/modelchecker/dft/DFTModelChecker.cpp rename to src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 894b56712..ae4144ee7 100644 --- a/src/storm/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -1,12 +1,13 @@ -#include "storm/modelchecker/dft/DFTModelChecker.h" +#include "DFTModelChecker.h" -#include "storm/builder/ExplicitDFTModelBuilder.h" -#include "storm/builder/ExplicitDFTModelBuilderApprox.h" #include "storm/builder/ParallelCompositionBuilder.h" -#include "storm/storage/dft/DFTIsomorphism.h" -#include "storm/settings/modules/DFTSettings.h" #include "storm/utility/bitoperations.h" +#include "storm-dft/builder/ExplicitDFTModelBuilder.h" +#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" +#include "storm-dft/storage/dft/DFTIsomorphism.h" +#include "storm-dft/settings/modules/DFTSettings.h" + namespace storm { namespace modelchecker { @@ -395,7 +396,7 @@ namespace storm { } template - bool DFTModelChecker::isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative) { + bool DFTModelChecker::isApproximationSufficient(ValueType , ValueType , double , bool ) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); } diff --git a/src/storm/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h similarity index 97% rename from src/storm/modelchecker/dft/DFTModelChecker.h rename to src/storm-dft/modelchecker/dft/DFTModelChecker.h index 1637c50ac..7cee7b0e4 100644 --- a/src/storm/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -1,9 +1,10 @@ -#ifndef STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_ +#pragma once #include "storm/logic/Formula.h" #include "storm/modelchecker/results/CheckResult.h" -#include "storm/storage/dft/DFT.h" -#include "storm/utility/storm.h" +#include "storm/utility/storm.h" // TODO this should not be included here. + +#include "storm-dft/storage/dft/DFT.h" #include @@ -136,5 +137,4 @@ namespace storm { }; } -} -#endif /* STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_ */ +} \ No newline at end of file diff --git a/src/storm/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp similarity index 100% rename from src/storm/parser/DFTGalileoParser.cpp rename to src/storm-dft/parser/DFTGalileoParser.cpp diff --git a/src/storm/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h similarity index 87% rename from src/storm/parser/DFTGalileoParser.h rename to src/storm-dft/parser/DFTGalileoParser.h index 51cb54c0a..3f19683ff 100644 --- a/src/storm/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -1,13 +1,14 @@ -#ifndef DFTGALILEOPARSER_H -#define DFTGALILEOPARSER_H +#pragma once + +#include -#include "storm/storage/dft/DFT.h" -#include "storm/storage/dft/DFTBuilder.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" -#include +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/storage/dft/DFTBuilder.h" + namespace storm { namespace parser { @@ -39,6 +40,3 @@ namespace storm { }; } } - -#endif /* DFTGALILEOPARSER_H */ - diff --git a/src/storm/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp similarity index 99% rename from src/storm/settings/modules/DFTSettings.cpp rename to src/storm-dft/settings/modules/DFTSettings.cpp index 359bab023..5bf705d8a 100644 --- a/src/storm/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/settings/modules/DFTSettings.h" +#include "DFTSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h similarity index 96% rename from src/storm/settings/modules/DFTSettings.h rename to src/storm-dft/settings/modules/DFTSettings.h index e18d626ca..1b1b097f9 100644 --- a/src/storm/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -1,9 +1,9 @@ -#ifndef STORM_SETTINGS_MODULES_DFTSETTINGS_H_ -#define STORM_SETTINGS_MODULES_DFTSETTINGS_H_ +#pragma once #include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" -#include "storm/builder/DftExplorationHeuristic.h" + +#include "storm-dft/builder/DftExplorationHeuristic.h" namespace storm { namespace settings { @@ -167,5 +167,3 @@ namespace storm { } // namespace modules } // namespace settings } // namespace storm - -#endif /* STORM_SETTINGS_MODULES_DFTSETTINGS_H_ */ diff --git a/src/storm/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp similarity index 99% rename from src/storm/storage/BucketPriorityQueue.cpp rename to src/storm-dft/storage/BucketPriorityQueue.cpp index 96a06e74a..89d7c7cce 100644 --- a/src/storm/storage/BucketPriorityQueue.cpp +++ b/src/storm-dft/storage/BucketPriorityQueue.cpp @@ -1,4 +1,4 @@ -#include "storm/storage/BucketPriorityQueue.h" +#include "BucketPriorityQueue.h" #include "storm/utility/macros.h" #include "storm/adapters/CarlAdapter.h" diff --git a/src/storm/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h similarity index 89% rename from src/storm/storage/BucketPriorityQueue.h rename to src/storm-dft/storage/BucketPriorityQueue.h index d11ba150d..a332311a7 100644 --- a/src/storm/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -1,12 +1,12 @@ -#ifndef STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ -#define STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ +#pragma once -#include "storm/builder/DftExplorationHeuristic.h" #include #include #include #include +#include "storm-dft/builder/DftExplorationHeuristic.h" + namespace storm { namespace storage { @@ -69,5 +69,3 @@ namespace storm { } } - -#endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ diff --git a/src/storm/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp similarity index 99% rename from src/storm/storage/dft/DFT.cpp rename to src/storm-dft/storage/dft/DFT.cpp index d118ba75e..8f19119a2 100644 --- a/src/storm/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -1,13 +1,15 @@ -#include +#include "DFT.h" +#include #include -#include "DFT.h" -#include "DFTBuilder.h" + #include "storm/exceptions/NotSupportedException.h" +#include "storm/utility/iota_n.h" +#include "storm/utility/vector.h" + +#include "storm-dft/storage/dft/DFTBuilder.h" +#include "storm-dft/storage/dft/DFTIsomorphism.h" -#include "DFTIsomorphism.h" -#include "utility/iota_n.h" -#include "utility/vector.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h similarity index 97% rename from src/storm/storage/dft/DFT.h rename to src/storm-dft/storage/dft/DFT.h index 4b54391f2..9ef232a65 100644 --- a/src/storm/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -1,6 +1,4 @@ - -#ifndef DFT_H -#define DFT_H +#pragma once #include #include @@ -10,13 +8,14 @@ #include -#include "DFTElements.h" -#include "elements/DFTRestriction.h" -#include "../BitVector.h" -#include "SymmetricUnits.h" -#include "../../utility/math.h" +#include "storm/storage/BitVector.h" +#include "storm/utility/math.h" #include "storm/utility/macros.h" -#include "DFTStateGenerationInfo.h" + +#include "storm-dft/storage/dft/DFTElements.h" +#include "storm-dft/storage/dft/SymmetricUnits.h" +#include "storm-dft/storage/dft/DFTStateGenerationInfo.h" + namespace storm { namespace storage { @@ -38,8 +37,6 @@ namespace storm { template class DFTBuilder; - - /** * Represents a Dynamic Fault Tree @@ -281,5 +278,3 @@ namespace storm { } } -#endif /* DFT_H */ - diff --git a/src/storm/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp similarity index 98% rename from src/storm/storage/dft/DFTBuilder.cpp rename to src/storm-dft/storage/dft/DFTBuilder.cpp index 4e6e53944..612008226 100644 --- a/src/storm/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -1,14 +1,13 @@ - - #include "DFTBuilder.h" #include -#include "DFT.h" -#include "OrderDFTElementsById.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" -#include "../../exceptions/WrongFormatException.h" +#include "storm/exceptions/WrongFormatException.h" + +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/storage/dft/OrderDFTElementsById.h" namespace storm { diff --git a/src/storm/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h similarity index 98% rename from src/storm/storage/dft/DFTBuilder.h rename to src/storm-dft/storage/dft/DFTBuilder.h index 3964079ff..f9a11d52b 100644 --- a/src/storm/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -1,14 +1,14 @@ - -#ifndef DFTBUILDER_H -#define DFTBUILDER_H - -#include "DFTElements.h" -#include "elements/DFTRestriction.h" +#pragma once #include #include #include + #include "storm/utility/macros.h" +#include "storm-dft/storage/dft/DFTElements.h" +#include "storm-dft/storage/dft/elements/DFTRestriction.h" + + namespace storm { namespace storage { template @@ -190,8 +190,3 @@ namespace storm { }; } } - - - -#endif /* DFTBUILDER_H */ - diff --git a/src/storm/storage/dft/DFTElementState.h b/src/storm-dft/storage/dft/DFTElementState.h similarity index 96% rename from src/storm/storage/dft/DFTElementState.h rename to src/storm-dft/storage/dft/DFTElementState.h index 8fc30e32b..4eab014f7 100644 --- a/src/storm/storage/dft/DFTElementState.h +++ b/src/storm-dft/storage/dft/DFTElementState.h @@ -1,6 +1,4 @@ - -#ifndef DFTELEMENTSTATE_H -#define DFTELEMENTSTATE_H +#pragma once #include "storm/utility/macros.h" @@ -77,6 +75,3 @@ namespace storm { } } - -#endif /* DFTELEMENTSTATE_H */ - diff --git a/src/storm/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h similarity index 97% rename from src/storm/storage/dft/DFTElementType.h rename to src/storm-dft/storage/dft/DFTElementType.h index ddd339c0a..800da161f 100644 --- a/src/storm/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -1,5 +1,4 @@ -#ifndef DFTELEMENTTYPE_H -#define DFTELEMENTTYPE_H +#pragma once #include "storm/utility/macros.h" @@ -83,5 +82,3 @@ namespace storm { } } - -#endif /* DFTELEMENTTYPE_H */ diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h new file mode 100644 index 000000000..8cbfec680 --- /dev/null +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -0,0 +1,12 @@ +#pragma once + +#include "storm-dft/storage/dft/elements/DFTAnd.h" +#include "storm-dft/storage/dft/elements/DFTBE.h" +#include "storm-dft/storage/dft/elements/DFTConst.h" +#include "storm-dft/storage/dft/elements/DFTDependency.h" +#include "storm-dft/storage/dft/elements/DFTOr.h" +#include "storm-dft/storage/dft/elements/DFTPand.h" +#include "storm-dft/storage/dft/elements/DFTPor.h" +#include "storm-dft/storage/dft/elements/DFTRestriction.h" +#include "storm-dft/storage/dft/elements/DFTSpare.h" +#include "storm-dft/storage/dft/elements/DFTVot.h" diff --git a/src/storm/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h similarity index 99% rename from src/storm/storage/dft/DFTIsomorphism.h rename to src/storm-dft/storage/dft/DFTIsomorphism.h index 1f66e5449..86625c975 100644 --- a/src/storm/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -3,9 +3,10 @@ #include #include #include -#include "DFTElementType.h" -#include "DFTElements.h" -#include "DFT.h" + +#include "storm-dft/storage/dft/DFTElementType.h" +#include "storm-dft/storage/dft/DFTElements.h" +#include "storm-dft/storage/dft/DFT.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp similarity index 99% rename from src/storm/storage/dft/DFTState.cpp rename to src/storm-dft/storage/dft/DFTState.cpp index cc0eaabec..78c0937d8 100644 --- a/src/storm/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -1,6 +1,6 @@ #include "DFTState.h" -#include "DFTElements.h" -#include "DFT.h" +#include "storm-dft/storage/dft/DFTElements.h" +#include "storm-dft/storage/dft/DFT.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h similarity index 98% rename from src/storm/storage/dft/DFTState.h rename to src/storm-dft/storage/dft/DFTState.h index 7b73d2ce7..4dfcf3a13 100644 --- a/src/storm/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -1,13 +1,13 @@ -#ifndef DFTSTATE_H -#define DFTSTATE_H - -#include "storm/storage/dft/DFTElementState.h" -#include "storm/storage/BitVector.h" -#include "storm/builder/DftExplorationHeuristic.h" +#pragma once #include #include +#include "storm/storage/BitVector.h" + +#include "storm-dft/storage/dft/DFTElementState.h" +#include "storm-dft/builder/DftExplorationHeuristic.h" + namespace storm { namespace storage { @@ -306,5 +306,3 @@ namespace std { }; } -#endif /* DFTSTATE_H */ - diff --git a/src/storm/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h similarity index 100% rename from src/storm/storage/dft/DFTStateGenerationInfo.h rename to src/storm-dft/storage/dft/DFTStateGenerationInfo.h diff --git a/src/storm/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h similarity index 95% rename from src/storm/storage/dft/DFTStateSpaceGenerationQueues.h rename to src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h index bd71b5fbf..a969cc83b 100644 --- a/src/storm/storage/dft/DFTStateSpaceGenerationQueues.h +++ b/src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h @@ -1,12 +1,11 @@ -#ifndef DFTSTATESPACEGENERATIONQUEUES_H -#define DFTSTATESPACEGENERATIONQUEUES_H +#pragma once #include #include #include #include -#include "OrderDFTElementsById.h" +#include "storm-dft/storage/dft/OrderDFTElementsById.h" namespace storm { namespace storage { @@ -99,7 +98,4 @@ namespace storm { }; } -} - -#endif /* DFTSTATESPACEGENERATIONQUEUES_H */ - +} \ No newline at end of file diff --git a/src/storm/storage/dft/DFTUnit.h b/src/storm-dft/storage/dft/DFTUnit.h similarity index 83% rename from src/storm/storage/dft/DFTUnit.h rename to src/storm-dft/storage/dft/DFTUnit.h index 5e179f091..6af505770 100644 --- a/src/storm/storage/dft/DFTUnit.h +++ b/src/storm-dft/storage/dft/DFTUnit.h @@ -1,7 +1,6 @@ -#ifndef DFTUNIT_H -#define DFTUNIT_H +#pragma once -#include "../BitVector.h" +#include "storm/storage/BitVector.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dft/OrderDFTElementsById.cpp b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp similarity index 95% rename from src/storm/storage/dft/OrderDFTElementsById.cpp rename to src/storm-dft/storage/dft/OrderDFTElementsById.cpp index 6c9493bee..8812eb763 100644 --- a/src/storm/storage/dft/OrderDFTElementsById.cpp +++ b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp @@ -1,5 +1,5 @@ #include "OrderDFTElementsById.h" -#include "DFTElements.h" +#include "storm-dft/storage/dft/DFTElements.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dft/OrderDFTElementsById.h b/src/storm-dft/storage/dft/OrderDFTElementsById.h similarity index 89% rename from src/storm/storage/dft/OrderDFTElementsById.h rename to src/storm-dft/storage/dft/OrderDFTElementsById.h index 821a2de45..d73a1ae2e 100644 --- a/src/storm/storage/dft/OrderDFTElementsById.h +++ b/src/storm-dft/storage/dft/OrderDFTElementsById.h @@ -1,6 +1,4 @@ -#ifndef ORDERDFTELEMENTS_H -#define ORDERDFTELEMENTS_H - +#pragma once #include namespace storm { @@ -25,6 +23,3 @@ namespace storm { } } - -#endif /* ORDERDFTELEMENTSBYID_H */ - diff --git a/src/storm/storage/dft/SymmetricUnits.h b/src/storm-dft/storage/dft/SymmetricUnits.h similarity index 100% rename from src/storm/storage/dft/SymmetricUnits.h rename to src/storm-dft/storage/dft/SymmetricUnits.h diff --git a/src/storm/storage/dft/elements/DFTAnd.h b/src/storm-dft/storage/dft/elements/DFTAnd.h similarity index 100% rename from src/storm/storage/dft/elements/DFTAnd.h rename to src/storm-dft/storage/dft/elements/DFTAnd.h diff --git a/src/storm/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h similarity index 100% rename from src/storm/storage/dft/elements/DFTBE.h rename to src/storm-dft/storage/dft/elements/DFTBE.h diff --git a/src/storm/storage/dft/elements/DFTConst.h b/src/storm-dft/storage/dft/elements/DFTConst.h similarity index 100% rename from src/storm/storage/dft/elements/DFTConst.h rename to src/storm-dft/storage/dft/elements/DFTConst.h diff --git a/src/storm/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h similarity index 100% rename from src/storm/storage/dft/elements/DFTDependency.h rename to src/storm-dft/storage/dft/elements/DFTDependency.h diff --git a/src/storm/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp similarity index 100% rename from src/storm/storage/dft/elements/DFTElement.cpp rename to src/storm-dft/storage/dft/elements/DFTElement.cpp diff --git a/src/storm/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h similarity index 100% rename from src/storm/storage/dft/elements/DFTElement.h rename to src/storm-dft/storage/dft/elements/DFTElement.h diff --git a/src/storm/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h similarity index 100% rename from src/storm/storage/dft/elements/DFTGate.h rename to src/storm-dft/storage/dft/elements/DFTGate.h diff --git a/src/storm/storage/dft/elements/DFTOr.h b/src/storm-dft/storage/dft/elements/DFTOr.h similarity index 100% rename from src/storm/storage/dft/elements/DFTOr.h rename to src/storm-dft/storage/dft/elements/DFTOr.h diff --git a/src/storm/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h similarity index 100% rename from src/storm/storage/dft/elements/DFTPand.h rename to src/storm-dft/storage/dft/elements/DFTPand.h diff --git a/src/storm/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h similarity index 100% rename from src/storm/storage/dft/elements/DFTPor.h rename to src/storm-dft/storage/dft/elements/DFTPor.h diff --git a/src/storm/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h similarity index 100% rename from src/storm/storage/dft/elements/DFTRestriction.h rename to src/storm-dft/storage/dft/elements/DFTRestriction.h diff --git a/src/storm/storage/dft/elements/DFTSpare.h b/src/storm-dft/storage/dft/elements/DFTSpare.h similarity index 100% rename from src/storm/storage/dft/elements/DFTSpare.h rename to src/storm-dft/storage/dft/elements/DFTSpare.h diff --git a/src/storm/storage/dft/elements/DFTVot.h b/src/storm-dft/storage/dft/elements/DFTVot.h similarity index 100% rename from src/storm/storage/dft/elements/DFTVot.h rename to src/storm-dft/storage/dft/elements/DFTVot.h diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt new file mode 100644 index 000000000..343b8acc8 --- /dev/null +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gspn.cpp) +target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode +set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") diff --git a/src/storm/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp similarity index 95% rename from src/storm/storm-gspn.cpp rename to src/storm-gspn-cli/storm-gspn.cpp index 87e39084f..b973d046d 100644 --- a/src/storm/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -1,9 +1,12 @@ -#include "storm/builder/ExplicitGspnModelBuilder.h" +#include "storm-gspn/builder/ExplicitGspnModelBuilder.h" +#include "storm-gspn/parser/GspnParser.h" +#include "storm-gspn/storage/gspn/GSPN.h" +#include "storm-gspn/storage/gspn/GspnBuilder.h" +#include "storm-gspn/builder/JaniGSPNBuilder.h" + #include "storm/exceptions/BaseException.h" #include "storm/exceptions/WrongFormatException.h" -#include "storm/parser/GspnParser.h" -#include "storm/storage/gspn/GSPN.h" -#include "storm/storage/gspn/GspnBuilder.h" + #include "storm/utility/macros.h" #include "storm/utility/initialize.h" @@ -13,7 +16,6 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/JSONExporter.h" -#include "storm/builder/JaniGSPNBuilder.h" #include #include #include diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt new file mode 100644 index 000000000..a5478280d --- /dev/null +++ b/src/storm-gspn/CMakeLists.txt @@ -0,0 +1,13 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.h ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-gspn) + + + +file(GLOB_RECURSE STORM_GSPN_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.cpp) +file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) + + +# Create storm-pgcl. +add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS}) +target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) diff --git a/src/storm/adapters/XercesAdapter.h b/src/storm-gspn/adapters/XercesAdapter.h similarity index 100% rename from src/storm/adapters/XercesAdapter.h rename to src/storm-gspn/adapters/XercesAdapter.h diff --git a/src/storm/builder/ExplicitGspnModelBuilder.cpp b/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp similarity index 100% rename from src/storm/builder/ExplicitGspnModelBuilder.cpp rename to src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp diff --git a/src/storm/builder/ExplicitGspnModelBuilder.h b/src/storm-gspn/builder/ExplicitGspnModelBuilder.h similarity index 100% rename from src/storm/builder/ExplicitGspnModelBuilder.h rename to src/storm-gspn/builder/ExplicitGspnModelBuilder.h diff --git a/src/storm/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp similarity index 100% rename from src/storm/builder/JaniGSPNBuilder.cpp rename to src/storm-gspn/builder/JaniGSPNBuilder.cpp diff --git a/src/storm/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h similarity index 99% rename from src/storm/builder/JaniGSPNBuilder.h rename to src/storm-gspn/builder/JaniGSPNBuilder.h index 46c0fb095..4fcb19f16 100644 --- a/src/storm/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/storage/gspn/GSPN.h" +#include "storm-gspn/storage/gspn/GSPN.h" #include "storm/storage/jani/Model.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/storm/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp similarity index 100% rename from src/storm/parser/GreatSpnEditorProjectParser.cpp rename to src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp diff --git a/src/storm/parser/GreatSpnEditorProjectParser.h b/src/storm-gspn/parser/GreatSpnEditorProjectParser.h similarity index 100% rename from src/storm/parser/GreatSpnEditorProjectParser.h rename to src/storm-gspn/parser/GreatSpnEditorProjectParser.h diff --git a/src/storm/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp similarity index 98% rename from src/storm/parser/GspnParser.cpp rename to src/storm-gspn/parser/GspnParser.cpp index 6f5b3c731..dfb3575d3 100644 --- a/src/storm/parser/GspnParser.cpp +++ b/src/storm-gspn/parser/GspnParser.cpp @@ -1,6 +1,6 @@ #include "GspnParser.h" #include "storm-config.h" -#include "storm/adapters/XercesAdapter.h" +#include "storm-gspn/adapters/XercesAdapter.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/GspnParser.h b/src/storm-gspn/parser/GspnParser.h similarity index 80% rename from src/storm/parser/GspnParser.h rename to src/storm-gspn/parser/GspnParser.h index 0b80a1615..862dfc757 100644 --- a/src/storm/parser/GspnParser.h +++ b/src/storm-gspn/parser/GspnParser.h @@ -1,4 +1,4 @@ -#include "storm/storage/gspn/GSPN.h" +#include "storm-gspn/storage/gspn/GSPN.h" namespace storm { namespace parser { diff --git a/src/storm/parser/PnmlParser.cpp b/src/storm-gspn/parser/PnmlParser.cpp similarity index 99% rename from src/storm/parser/PnmlParser.cpp rename to src/storm-gspn/parser/PnmlParser.cpp index bf256ec6c..4869405eb 100644 --- a/src/storm/parser/PnmlParser.cpp +++ b/src/storm-gspn/parser/PnmlParser.cpp @@ -1,5 +1,5 @@ -#include "storm/parser/PnmlParser.h" +#include "storm-gspn/parser/PnmlParser.h" #ifdef USE_XERCES #include diff --git a/src/storm/parser/PnmlParser.h b/src/storm-gspn/parser/PnmlParser.h similarity index 100% rename from src/storm/parser/PnmlParser.h rename to src/storm-gspn/parser/PnmlParser.h diff --git a/src/storm/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp similarity index 98% rename from src/storm/storage/gspn/GSPN.cpp rename to src/storm-gspn/storage/gspn/GSPN.cpp index 87d123619..8377f2f8e 100644 --- a/src/storm/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -1,11 +1,14 @@ -#include "storm/storage/gspn/GSPN.h" -#include "storm/utility/macros.h" -#include "storm/exceptions/InvalidArgumentException.h" +#include "GSPN.h" #include #include +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + + + namespace storm { namespace gspn { uint64_t GSPN::timedTransitionIdToTransitionId(uint64_t ttId) { @@ -169,7 +172,7 @@ namespace storm { if (trans.getInhibitionPlaces().count(outEntry.first) == 1) { outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[arrowtail=\"dot\", label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "") << "\", dir=both];" << std::endl; } else if (trans.getInputPlaces().count(outEntry.first) == 1) { - outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[arrowtail=\"dot\", label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "")<< "\", dir=both];" << std::endl; + outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "")<< "\", dir=both];" << std::endl; } else { outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "") << "\"];" << std::endl; } @@ -193,7 +196,7 @@ namespace storm { if (trans.getInhibitionPlaces().count(outEntry.first) == 1) { outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[arrowtail=\"dot\", label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "") << "\", dir=both];" << std::endl; } else if (trans.getInputPlaces().count(outEntry.first) == 1) { - outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[arrowtail=\"dot\", label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "")<< "\", dir=both];" << std::endl; + outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "")<< "\", dir=both];" << std::endl; } else { outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << (outEntry.second > 1 ? std::to_string(outEntry.second) : "") << "\"];" << std::endl; } diff --git a/src/storm/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h similarity index 96% rename from src/storm/storage/gspn/GSPN.h rename to src/storm-gspn/storage/gspn/GSPN.h index aee3bbd4c..17448bc8b 100644 --- a/src/storm/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -6,10 +6,10 @@ #include #include -#include "storm/storage/gspn/ImmediateTransition.h" -#include "storm/storage/gspn/Marking.h" -#include "storm/storage/gspn/Place.h" -#include "storm/storage/gspn/TimedTransition.h" +#include "storm-gspn/storage/gspn/ImmediateTransition.h" +#include "storm-gspn/storage/gspn/Marking.h" +#include "storm-gspn/storage/gspn/Place.h" +#include "storm-gspn/storage/gspn/TimedTransition.h" namespace storm { namespace gspn { diff --git a/src/storm/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp similarity index 99% rename from src/storm/storage/gspn/GspnBuilder.cpp rename to src/storm-gspn/storage/gspn/GspnBuilder.cpp index 1800f02d5..cbea96b6a 100644 --- a/src/storm/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -1,6 +1,8 @@ -#include "storm/exceptions/IllegalFunctionCallException.h" #include "GspnBuilder.h" + +#include "storm/exceptions/IllegalFunctionCallException.h" + #include "storm/utility/macros.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/exceptions/InvalidArgumentException.h" diff --git a/src/storm/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h similarity index 100% rename from src/storm/storage/gspn/GspnBuilder.h rename to src/storm-gspn/storage/gspn/GspnBuilder.h diff --git a/src/storm/storage/gspn/ImmediateTransition.h b/src/storm-gspn/storage/gspn/ImmediateTransition.h similarity index 84% rename from src/storm/storage/gspn/ImmediateTransition.h rename to src/storm-gspn/storage/gspn/ImmediateTransition.h index 6728db936..4dd107f6c 100644 --- a/src/storm/storage/gspn/ImmediateTransition.h +++ b/src/storm-gspn/storage/gspn/ImmediateTransition.h @@ -1,7 +1,6 @@ -#ifndef STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ -#define STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ +#pragma once -#include "storm/storage/gspn/Transition.h" +#include "storm-gspn/storage/gspn/Transition.h" #include "storm/utility/constants.h" namespace storm { @@ -39,5 +38,3 @@ namespace storm { }; } } - -#endif //STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ diff --git a/src/storm/storage/gspn/Marking.cpp b/src/storm-gspn/storage/gspn/Marking.cpp similarity index 98% rename from src/storm/storage/gspn/Marking.cpp rename to src/storm-gspn/storage/gspn/Marking.cpp index 3e9f680d0..559464c7c 100644 --- a/src/storm/storage/gspn/Marking.cpp +++ b/src/storm-gspn/storage/gspn/Marking.cpp @@ -1,5 +1,8 @@ +#include "Marking.h" + + #include -#include "storm/storage/gspn/Marking.h" + namespace storm { namespace gspn { diff --git a/src/storm/storage/gspn/Marking.h b/src/storm-gspn/storage/gspn/Marking.h similarity index 100% rename from src/storm/storage/gspn/Marking.h rename to src/storm-gspn/storage/gspn/Marking.h diff --git a/src/storm/storage/gspn/Place.cpp b/src/storm-gspn/storage/gspn/Place.cpp similarity index 100% rename from src/storm/storage/gspn/Place.cpp rename to src/storm-gspn/storage/gspn/Place.cpp diff --git a/src/storm/storage/gspn/Place.h b/src/storm-gspn/storage/gspn/Place.h similarity index 100% rename from src/storm/storage/gspn/Place.h rename to src/storm-gspn/storage/gspn/Place.h diff --git a/src/storm/storage/gspn/TimedTransition.h b/src/storm-gspn/storage/gspn/TimedTransition.h similarity index 80% rename from src/storm/storage/gspn/TimedTransition.h rename to src/storm-gspn/storage/gspn/TimedTransition.h index 339a19a0f..d8399319d 100644 --- a/src/storm/storage/gspn/TimedTransition.h +++ b/src/storm-gspn/storage/gspn/TimedTransition.h @@ -1,7 +1,6 @@ -#ifndef STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ -#define STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ +#pragma once -#include "storm/storage/gspn/Transition.h" +#include "storm-gspn/storage/gspn/Transition.h" namespace storm { namespace gspn { @@ -31,6 +30,4 @@ namespace storm { RateType rate; }; } -} - -#endif //STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ +} \ No newline at end of file diff --git a/src/storm/storage/gspn/Transition.cpp b/src/storm-gspn/storage/gspn/Transition.cpp similarity index 99% rename from src/storm/storage/gspn/Transition.cpp rename to src/storm-gspn/storage/gspn/Transition.cpp index adb6b3fdc..ccc24d8c3 100644 --- a/src/storm/storage/gspn/Transition.cpp +++ b/src/storm-gspn/storage/gspn/Transition.cpp @@ -1,4 +1,4 @@ -#include "storm/storage/gspn/Transition.h" +#include "Transition.h" #include "storm/utility/macros.h" diff --git a/src/storm/storage/gspn/Transition.h b/src/storm-gspn/storage/gspn/Transition.h similarity index 98% rename from src/storm/storage/gspn/Transition.h rename to src/storm-gspn/storage/gspn/Transition.h index 460e307b6..d61affaea 100644 --- a/src/storm/storage/gspn/Transition.h +++ b/src/storm-gspn/storage/gspn/Transition.h @@ -3,8 +3,8 @@ #include #include #include -#include "storm/storage/gspn/Marking.h" -#include "storm/storage/gspn/Place.h" +#include "storm-gspn/storage/gspn/Marking.h" +#include "storm-gspn/storage/gspn/Place.h" namespace storm { namespace gspn { diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 27dcb0913..f0d64ab0c 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -10,8 +10,6 @@ register_source_groups_from_filestructure("${ALL_FILES}" storm) file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/storm/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/storm/*/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm/storm.cpp) -file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm/storm-dyftee.cpp) -file(GLOB_RECURSE STORM_GSPN_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm/storm-gspn.cpp) # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) @@ -19,8 +17,6 @@ file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN}) set(STORM_LIB_HEADERS ${STORM_HEADERS}) set(STORM_MAIN_SOURCES ${STORM_MAIN_FILE}) -set(STORM_DFT_MAIN_SOURCES ${STORM_DFT_MAIN_FILE}) -set(STORM_GSPN_MAIN_SOURCES ${STORM_GSPN_MAIN_FILE}) # Add custom additional include or link directories if (ADDITIONAL_INCLUDE_DIRS) @@ -50,14 +46,6 @@ add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) target_link_libraries(storm-main storm) set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") -# Create storm-dft. -add_executable(storm-dft-main ${STORM_DFT_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) -target_link_libraries(storm-dft-main storm) # Adding headers for xcode -set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft") - -add_executable(storm-gspn-main ${STORM_GSPN_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) -target_link_libraries(storm-gspn-main storm) # Adding headers for xcode -set_target_properties(storm-gspn-main PROPERTIES OUTPUT_NAME "storm-gspn") # Install storm headers to include directory. foreach(HEADER ${STORM_LIB_HEADERS}) diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index de9293ab4..7c5b6dce4 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -35,7 +35,7 @@ namespace storm { * @param expression The expression to translate. * @return An equivalent expression for Smt2. */ - std::string translateExpression(storm::expressions::Expression const& expression) { + std::string translateExpression(storm::expressions::Expression const& ) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } @@ -98,7 +98,7 @@ namespace storm { * @param variable The variable to translate. * @return An equivalent expression for smt2. */ - std::string translateExpression(storm::expressions::Variable const& variable) { + std::string translateExpression(storm::expressions::Variable const& ) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } @@ -108,7 +108,7 @@ namespace storm { * @param smt2Declaration The declaration for which to find the equivalent. * @return The equivalent counterpart. */ - storm::expressions::Variable const& getVariable(std::string smt2Declaration) { + storm::expressions::Variable const& getVariable(std::string const&) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } diff --git a/src/storm/builder/DftSmtBuilder.cpp b/src/storm/builder/DftSmtBuilder.cpp deleted file mode 100644 index 198f71ebf..000000000 --- a/src/storm/builder/DftSmtBuilder.cpp +++ /dev/null @@ -1,120 +0,0 @@ -#include "storm/builder/DftSmtBuilder.h" -#include "storm/exceptions/NotImplementedException.h" - -namespace storm { - namespace builder { - - template - DFTSMTBuilder::DFTSMTBuilder() : manager(std::make_shared()) { - solver = storm::utility::solver::SmtSolverFactory().create(*manager); - } - - template - void DFTSMTBuilder::convertToSMT(storm::storage::DFT const& dft) { - std::cout << "Convert DFT to SMT" << std::endl; - timeMax = manager->integer(dft.nrBasicElements()); - timeFailSafe = manager->integer(dft.nrBasicElements() + 1); - timeZero = manager->integer(0); - - // Convert all elements - for (size_t i = 0; i < dft.nrElements(); ++i) { - std::shared_ptr const> element = dft.getElement(i); - std::cout << "Consider " << element->toString() << std::endl; - if (element->isBasicElement()) { - storm::expressions::Variable varBE = convert(std::static_pointer_cast const>(element)); - varsBE.push_back(varBE); - } else if (element->isGate()) { - storm::expressions::Variable varGate = convert(std::static_pointer_cast const>(element)); - if (dft.getTopLevelIndex() == i) { - topLevel = varGate; - } - } else if (element->isDependency()) { - convert(std::static_pointer_cast const>(element)); - } else if (element->isRestriction()) { - convert(std::static_pointer_cast const>(element)); - } - } - - // No simultaneous fails can occur - for (size_t i = 0; i < varsBE.size() - 1; ++i) { - storm::expressions::Expression be = varsBE[i]; - for (size_t j = i + 1; j < varsBE.size(); ++j) { - storm::expressions::Expression assertion = be != varsBE[j]; - solver->add(assertion); - } - } - - // For every time-point one BE must fail - for (size_t time = 1; time <= dft.nrBasicElements(); ++time) { - storm::expressions::Expression exprTime = manager->integer(time); - storm::expressions::Expression assertion = varsBE[0] == exprTime; - for (size_t i = 1; i < varsBE.size(); ++i) { - assertion = assertion || varsBE[i] == exprTime; - } - assertion = assertion || topLevel <= exprTime; - solver->add(assertion); - } - - } - - template - storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& be) { - storm::expressions::Variable var = manager->declareIntegerVariable(be->name()); - storm::expressions::Expression assertion = timeZero < var && var < timeFailSafe; - solver->add(assertion); - return var; - } - - template - storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& gate) { - storm::expressions::Variable var = manager->declareIntegerVariable(gate->name()); - storm::expressions::Expression assertion = timeZero < var && var <= timeFailSafe; - solver->add(assertion); - return var; - } - - template - storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& dependency) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The dependency cannot be converted into SMT."); - } - - template - storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& restriction) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The restriction cannot be converted into SMT."); - } - - template - bool DFTSMTBuilder::check() const { - std::cout << "Check" << std::endl; - storm::solver::SmtSolver::CheckResult result = solver->check(); - switch (result) { - case solver::SmtSolver::CheckResult::Sat: - { - std::cout << "SAT with model:" << std::endl; - std::shared_ptr model = solver->getModel(); - for (auto const& pair : *manager) { - std::cout << pair.first.getName() << "->" << model->getIntegerValue(pair.first) << std::endl; - } - return true; - } - case solver::SmtSolver::CheckResult::Unsat: - return false; - case solver::SmtSolver::CheckResult::Unknown: - default: - STORM_LOG_ASSERT(false, "Result is unknown."); - return false; - } - } - - - // Explicitly instantiate the class. - template class DFTSMTBuilder; - -#ifdef STORM_HAVE_CARL - template class DFTSMTBuilder; -#endif - - } // namespace builder -} // namespace storm - - diff --git a/src/storm/builder/DftSmtBuilder.h b/src/storm/builder/DftSmtBuilder.h deleted file mode 100644 index 158a62f33..000000000 --- a/src/storm/builder/DftSmtBuilder.h +++ /dev/null @@ -1,49 +0,0 @@ -#ifndef DFTSMTBUILDER_H -#define DFTSMTBUILDER_H - -#include "storm/solver/SmtSolver.h" -#include "storm/utility/solver.h" -#include "storm/storage/dft/DFT.h" - -namespace storm { - namespace builder { - - template - class DFTSMTBuilder { - - public: - DFTSMTBuilder(); - - void convertToSMT(storm::storage::DFT const& dft); - - bool check() const; - - private: - - std::shared_ptr solver; - - std::shared_ptr manager; - - storm::expressions::Expression timeMax; - - storm::expressions::Expression timeFailSafe; - - storm::expressions::Expression timeZero; - - storm::expressions::Expression topLevel; - - std::vector varsBE; - - storm::expressions::Variable convert(std::shared_ptr const> const& be); - - storm::expressions::Variable convert(std::shared_ptr const> const& gate); - - storm::expressions::Variable convert(std::shared_ptr const> const& dependency); - - storm::expressions::Variable convert(std::shared_ptr const> const& restriction); - - }; - } -} - -#endif /* DFTSMTBUILDER_H */ diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index a6133da95..f47f4bc10 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -178,7 +178,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& , std::vector const& , bool ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif diff --git a/src/storm/storage/dft/DFTElements.h b/src/storm/storage/dft/DFTElements.h deleted file mode 100644 index d65403403..000000000 --- a/src/storm/storage/dft/DFTElements.h +++ /dev/null @@ -1,12 +0,0 @@ -#pragma once - -#include "elements/DFTAnd.h" -#include "elements/DFTBE.h" -#include "elements/DFTConst.h" -#include "elements/DFTDependency.h" -#include "elements/DFTOr.h" -#include "elements/DFTPand.h" -#include "elements/DFTPor.h" -#include "elements/DFTRestriction.h" -#include "elements/DFTSpare.h" -#include "elements/DFTVot.h" diff --git a/src/storm/utility/math.h b/src/storm/utility/math.h index 850c137a9..499cb2ac8 100644 --- a/src/storm/utility/math.h +++ b/src/storm/utility/math.h @@ -3,6 +3,7 @@ #include +#include "storm/utility/macros.h" #include "storm/utility/OsDetection.h" namespace storm { diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index abac269f6..e13ec574e 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -270,12 +270,12 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr const& formula) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model."); } template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr const& formula) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif diff --git a/src/storm/utility/sylvan.h b/src/storm/utility/sylvan.h index 0abee4c59..f6d4e5ec1 100644 --- a/src/storm/utility/sylvan.h +++ b/src/storm/utility/sylvan.h @@ -10,6 +10,8 @@ #pragma GCC diagnostic push #pragma GCC diagnostic ignored "-Wpedantic" +#pragma GCC system_header // Only way to suppress some warnings atm. + #include "sylvan_obj.hpp" #include "sylvan_storm_rational_function.h" diff --git a/stormpy/CMakeLists.txt b/stormpy/CMakeLists.txt index 349780709..afd91d57e 100644 --- a/stormpy/CMakeLists.txt +++ b/stormpy/CMakeLists.txt @@ -1,6 +1,3 @@ -find_package(PythonInterp REQUIRED) -find_package(PythonLibs REQUIRED) - set(STORMPY_OUTPUT_DIR "${PROJECT_BINARY_DIR}/stormpy") set(STORMPY_SOURCE_DIR "${PROJECT_SOURCE_DIR}/stormpy") diff --git a/stormpy/src/mod_expressions.cpp b/stormpy/src/mod_expressions.cpp index 7ca054be9..ef89106c8 100644 --- a/stormpy/src/mod_expressions.cpp +++ b/stormpy/src/mod_expressions.cpp @@ -9,6 +9,12 @@ PYBIND11_PLUGIN(expressions) { ; py::class_(m, "Expression", "Holds an expression") + .def("__str__", &storm::expressions::Expression::toString) + .def_property_readonly("contains_variables", &storm::expressions::Expression::containsVariables) + .def_property_readonly("has_boolean_type", &storm::expressions::Expression::hasBooleanType) + .def_property_readonly("has_integer_type", &storm::expressions::Expression::hasIntegerType) + .def_property_readonly("has_rational_type", &storm::expressions::Expression::hasRationalType) + ; return m.ptr();