From 112fb8f61eec05e2cf09a7441b28f6f9d25111c2 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 25 Nov 2016 00:35:25 +0100 Subject: [PATCH] moving dfts to their own lib and cli --- src/CMakeLists.txt | 2 + src/storm-dft-cli/CMakeLists.txt | 4 + .../settings/modules/DFTSettings.cpp | 0 .../settings/modules/DFTSettings.h | 0 src/{storm => storm-dft-cli}/storm-dyftee.cpp | 8 +- src/storm-dft/CMakeLists.txt | 13 ++ .../builder/DftExplorationHeuristic.cpp | 3 +- .../builder/DftExplorationHeuristic.h | 6 +- .../builder/ExplicitDFTModelBuilder.cpp | 10 +- .../builder/ExplicitDFTModelBuilder.h | 24 ++-- .../builder/ExplicitDFTModelBuilderApprox.cpp | 10 +- .../builder/ExplicitDFTModelBuilderApprox.h | 27 ++-- .../generator/DftNextStateGenerator.cpp | 2 +- .../generator/DftNextStateGenerator.h | 10 +- .../modelchecker/dft/DFTASFChecker.cpp | 0 .../modelchecker/dft/DFTASFChecker.h | 3 +- .../modelchecker/dft/DFTModelChecker.cpp | 9 +- .../modelchecker/dft/DFTModelChecker.h | 10 +- .../parser/DFTGalileoParser.cpp | 0 .../parser/DFTGalileoParser.h | 14 +- .../storage/BucketPriorityQueue.cpp | 2 +- .../storage/BucketPriorityQueue.h | 8 +- src/{storm => storm-dft}/storage/dft/DFT.cpp | 14 +- src/{storm => storm-dft}/storage/dft/DFT.h | 21 ++- .../storage/dft/DFTBuilder.cpp | 9 +- .../storage/dft/DFTBuilder.h | 17 +-- .../storage/dft/DFTElementState.h | 7 +- .../storage/dft/DFTElementType.h | 5 +- src/storm-dft/storage/dft/DFTElements.h | 12 ++ .../storage/dft/DFTIsomorphism.h | 7 +- .../storage/dft/DFTState.cpp | 4 +- .../storage/dft/DFTState.h | 14 +- .../storage/dft/DFTStateGenerationInfo.h | 0 .../dft/DFTStateSpaceGenerationQueues.h | 10 +- .../storage/dft/DFTUnit.h | 5 +- .../storage/dft/OrderDFTElementsById.cpp | 2 +- .../storage/dft/OrderDFTElementsById.h | 7 +- .../storage/dft/SymmetricUnits.h | 0 .../storage/dft/elements/DFTAnd.h | 0 .../storage/dft/elements/DFTBE.h | 0 .../storage/dft/elements/DFTConst.h | 0 .../storage/dft/elements/DFTDependency.h | 0 .../storage/dft/elements/DFTElement.cpp | 0 .../storage/dft/elements/DFTElement.h | 0 .../storage/dft/elements/DFTGate.h | 0 .../storage/dft/elements/DFTOr.h | 0 .../storage/dft/elements/DFTPand.h | 0 .../storage/dft/elements/DFTPor.h | 0 .../storage/dft/elements/DFTRestriction.h | 0 .../storage/dft/elements/DFTSpare.h | 0 .../storage/dft/elements/DFTVot.h | 0 src/storm/CMakeLists.txt | 6 - src/storm/builder/DftSmtBuilder.cpp | 120 ------------------ src/storm/builder/DftSmtBuilder.h | 49 ------- src/storm/storage/dft/DFTElements.h | 12 -- src/storm/utility/math.h | 1 + 56 files changed, 154 insertions(+), 333 deletions(-) create mode 100644 src/storm-dft-cli/CMakeLists.txt rename src/{storm => storm-dft-cli}/settings/modules/DFTSettings.cpp (100%) rename src/{storm => storm-dft-cli}/settings/modules/DFTSettings.h (100%) rename src/{storm => storm-dft-cli}/storm-dyftee.cpp (98%) create mode 100644 src/storm-dft/CMakeLists.txt rename src/{storm => storm-dft}/builder/DftExplorationHeuristic.cpp (98%) rename src/{storm => storm-dft}/builder/DftExplorationHeuristic.h (97%) rename src/{storm => storm-dft}/builder/ExplicitDFTModelBuilder.cpp (99%) rename src/{storm => storm-dft}/builder/ExplicitDFTModelBuilder.h (95%) rename src/{storm => storm-dft}/builder/ExplicitDFTModelBuilderApprox.cpp (99%) rename src/{storm => storm-dft}/builder/ExplicitDFTModelBuilderApprox.h (97%) rename src/{storm => storm-dft}/generator/DftNextStateGenerator.cpp (99%) rename src/{storm => storm-dft}/generator/DftNextStateGenerator.h (93%) rename src/{storm => storm-dft}/modelchecker/dft/DFTASFChecker.cpp (100%) rename src/{storm => storm-dft}/modelchecker/dft/DFTASFChecker.h (97%) rename src/{storm => storm-dft}/modelchecker/dft/DFTModelChecker.cpp (99%) rename src/{storm => storm-dft}/modelchecker/dft/DFTModelChecker.h (97%) rename src/{storm => storm-dft}/parser/DFTGalileoParser.cpp (100%) rename src/{storm => storm-dft}/parser/DFTGalileoParser.h (87%) rename src/{storm => storm-dft}/storage/BucketPriorityQueue.cpp (99%) rename src/{storm => storm-dft}/storage/BucketPriorityQueue.h (89%) rename src/{storm => storm-dft}/storage/dft/DFT.cpp (99%) rename src/{storm => storm-dft}/storage/dft/DFT.h (97%) rename src/{storm => storm-dft}/storage/dft/DFTBuilder.cpp (98%) rename src/{storm => storm-dft}/storage/dft/DFTBuilder.h (98%) rename src/{storm => storm-dft}/storage/dft/DFTElementState.h (96%) rename src/{storm => storm-dft}/storage/dft/DFTElementType.h (97%) create mode 100644 src/storm-dft/storage/dft/DFTElements.h rename src/{storm => storm-dft}/storage/dft/DFTIsomorphism.h (99%) rename src/{storm => storm-dft}/storage/dft/DFTState.cpp (99%) rename src/{storm => storm-dft}/storage/dft/DFTState.h (98%) rename src/{storm => storm-dft}/storage/dft/DFTStateGenerationInfo.h (100%) rename src/{storm => storm-dft}/storage/dft/DFTStateSpaceGenerationQueues.h (95%) rename src/{storm => storm-dft}/storage/dft/DFTUnit.h (83%) rename src/{storm => storm-dft}/storage/dft/OrderDFTElementsById.cpp (95%) rename src/{storm => storm-dft}/storage/dft/OrderDFTElementsById.h (89%) rename src/{storm => storm-dft}/storage/dft/SymmetricUnits.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTAnd.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTBE.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTConst.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTDependency.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTElement.cpp (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTElement.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTGate.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTOr.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTPand.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTPor.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTRestriction.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTSpare.h (100%) rename src/{storm => storm-dft}/storage/dft/elements/DFTVot.h (100%) delete mode 100644 src/storm/builder/DftSmtBuilder.cpp delete mode 100644 src/storm/builder/DftSmtBuilder.h delete mode 100644 src/storm/storage/dft/DFTElements.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 665c16847..80f7bd9b7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -3,4 +3,6 @@ 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/settings/modules/DFTSettings.cpp b/src/storm-dft-cli/settings/modules/DFTSettings.cpp similarity index 100% rename from src/storm/settings/modules/DFTSettings.cpp rename to src/storm-dft-cli/settings/modules/DFTSettings.cpp diff --git a/src/storm/settings/modules/DFTSettings.h b/src/storm-dft-cli/settings/modules/DFTSettings.h similarity index 100% rename from src/storm/settings/modules/DFTSettings.h rename to src/storm-dft-cli/settings/modules/DFTSettings.h diff --git a/src/storm/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp similarity index 98% rename from src/storm/storm-dyftee.cpp rename to src/storm-dft-cli/storm-dyftee.cpp index e7e3002aa..03aa1cab8 100644 --- a/src/storm/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -1,14 +1,14 @@ #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-dft/builder/DftSmtBuilder.h" #include "storm/settings/modules/GeneralSettings.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 99% rename from src/storm/modelchecker/dft/DFTModelChecker.cpp rename to src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 39a3966c8..584d1edca 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" + namespace storm { namespace modelchecker { 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/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/CMakeLists.txt b/src/storm/CMakeLists.txt index 91b2abd53..f0d64ab0c 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -10,7 +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) # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) @@ -18,7 +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}) # Add custom additional include or link directories if (ADDITIONAL_INCLUDE_DIRS) @@ -48,10 +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") # Install storm headers to include directory. foreach(HEADER ${STORM_LIB_HEADERS}) 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/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 {