From 1a4bc33e5b2b8692c426414bdbc758bb73c1e7a2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Oct 2017 11:14:04 +0200 Subject: [PATCH 01/15] Fixed setting of debug settings in storm-dft-cli --- src/storm-dft-cli/storm-dyftee.cpp | 63 ++++++++++++++++++++---------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 8eef6f0b5..001adabf4 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -28,6 +28,7 @@ #include "storm-gspn/storm-gspn.h" #include "storm/settings/modules/GSPNSettings.h" #include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-cli-utilities/cli.cpp" #include @@ -125,23 +126,12 @@ void initializeSettings() { storm::settings::addModule(); } -/*! - * Entry point for the DyFTeE backend. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return Return code, 0 if successfull, not 0 otherwise. - */ -int main(const int argc, const char** argv) { - try { - storm::utility::setUp(); - storm::cli::printHeader("Storm-DyFTeE", argc, argv); - initializeSettings(); - - bool optionsCorrect = storm::cli::parseOptions(argc, argv); - if (!optionsCorrect) { - return -1; - } + +void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + storm::cli::setUrgentOptions(); + + storm::cli::processOptions(); storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); @@ -157,7 +147,7 @@ int main(const int argc, const char** argv) { // Export to json storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); storm::utility::cleanUp(); - return 0; + return; } @@ -199,7 +189,7 @@ int main(const int argc, const char** argv) { delete model; delete gspn; storm::utility::cleanUp(); - return 0; + return; } bool parametric = false; @@ -216,7 +206,7 @@ int main(const int argc, const char** argv) { analyzeWithSMT(dftSettings.getDftFilename()); } storm::utility::cleanUp(); - return 0; + return; } #endif @@ -272,7 +262,38 @@ int main(const int argc, const char** argv) { } else { analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); } - +} + +/*! + * Entry point for the DyFTeE backend. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return Return code, 0 if successfull, not 0 otherwise. + */ +/*! + * Main entry point of the executable storm-pars. + */ +int main(const int argc, const char** argv) { + try { + storm::utility::setUp(); + storm::cli::printHeader("Storm-DyFTeE", argc, argv); + //storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); + initializeSettings(); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + processOptions(); + //storm::pars::processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); return 0; From 349e276c9b14c39746b4459be354d19f357df24e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Oct 2017 11:30:25 +0200 Subject: [PATCH 02/15] Removed include of cpp file in storm-pars-cli and storm-dft-cli --- src/storm-cli-utilities/cli.cpp | 2 +- src/storm-cli-utilities/cli.h | 5 +++-- src/storm-dft-cli/CMakeLists.txt | 2 +- src/storm-dft-cli/storm-dyftee.cpp | 2 -- src/storm-pars-cli/CMakeLists.txt | 2 +- src/storm-pars-cli/storm-pars.cpp | 3 +-- 6 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index cb33c3205..3ff4d4593 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -64,7 +64,7 @@ namespace storm { } - void printHeader(std::string const& name, const int argc, const char* argv[]) { + void printHeader(std::string const& name, const int argc, const char** argv) { STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl); // "Compute" the command line argument string with which storm was invoked. diff --git a/src/storm-cli-utilities/cli.h b/src/storm-cli-utilities/cli.h index 4decbb02c..e8d8601e9 100644 --- a/src/storm-cli-utilities/cli.h +++ b/src/storm-cli-utilities/cli.h @@ -11,7 +11,7 @@ namespace storm { */ int64_t process(const int argc, const char** argv); - void printHeader(std::string const& name, const int argc, const char* argv[]); + void printHeader(std::string const& name, const int argc, const char** argv); void printVersion(std::string const& name); @@ -27,7 +27,8 @@ namespace storm { bool parseOptions(const int argc, const char* argv[]); void processOptions(); - + + void setUrgentOptions(); } } diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index b8cdbbd27..152fc5fc7 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -6,4 +6,4 @@ set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") add_dependencies(binaries storm-dft-cli) # installation -install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 001adabf4..b6fb0c751 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -28,8 +28,6 @@ #include "storm-gspn/storm-gspn.h" #include "storm/settings/modules/GSPNSettings.h" #include "storm/settings/modules/GSPNExportSettings.h" -#include "storm-cli-utilities/cli.cpp" - #include #include diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index bda5ad6c2..9e2f6f315 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -1,6 +1,6 @@ # Create storm-pars. add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-pars.cpp) -target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode +target_link_libraries(storm-pars-cli storm-pars storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") add_dependencies(binaries storm-pars-cli) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 5fa744c59..907688ef4 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -7,6 +7,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" #include "storm-cli-utilities/cli.h" +#include "storm-cli-utilities/model-handling.h" #include "storm/models/ModelBase.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/file.h" @@ -23,8 +24,6 @@ #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm-cli-utilities/cli.cpp" - namespace storm { namespace pars { From 9350e281c764abe65fd3b6c3656d11e1c61f3e3d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Oct 2017 11:38:44 +0200 Subject: [PATCH 03/15] Renamed storm-dyftee to storm-dft --- src/storm-dft-cli/CMakeLists.txt | 2 +- src/storm-dft-cli/{storm-dyftee.cpp => storm-dft.cpp} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename src/storm-dft-cli/{storm-dyftee.cpp => storm-dft.cpp} (100%) diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 152fc5fc7..4780eef4d 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -1,5 +1,5 @@ # Create storm-dft. -add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) +add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dft.cpp) target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dft.cpp similarity index 100% rename from src/storm-dft-cli/storm-dyftee.cpp rename to src/storm-dft-cli/storm-dft.cpp From 8a74be1b72f429c0959aa351578438792f86d9ed Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 11 Oct 2017 17:57:15 +0200 Subject: [PATCH 04/15] Refactored DFT settings --- src/storm-dft-cli/storm-dft.cpp | 124 ++++-------- .../builder/ExplicitDFTModelBuilder.cpp | 2 - .../builder/ExplicitDFTModelBuilderApprox.cpp | 4 +- .../generator/DftNextStateGenerator.cpp | 4 +- .../modelchecker/dft/DFTModelChecker.cpp | 4 +- src/storm-dft/settings/DftSettings.cpp | 51 +++++ src/storm-dft/settings/DftSettings.h | 11 + .../settings/modules/DFTSettings.cpp | 189 ------------------ .../settings/modules/DftIOSettings.cpp | 123 ++++++++++++ .../{DFTSettings.h => DftIOSettings.h} | 80 +------- .../settings/modules/FaultTreeSettings.cpp | 93 +++++++++ .../settings/modules/FaultTreeSettings.h | 104 ++++++++++ 12 files changed, 432 insertions(+), 357 deletions(-) create mode 100644 src/storm-dft/settings/DftSettings.cpp create mode 100644 src/storm-dft/settings/DftSettings.h delete mode 100644 src/storm-dft/settings/modules/DFTSettings.cpp create mode 100644 src/storm-dft/settings/modules/DftIOSettings.cpp rename src/storm-dft/settings/modules/{DFTSettings.h => DftIOSettings.h} (63%) create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.cpp create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.h diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index b6fb0c751..3e69fb217 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,20 +1,14 @@ -#include "storm/logic/Formula.h" -#include "storm/utility/initialize.h" -#include "storm/api/storm.h" -#include "storm-cli-utilities/cli.h" -#include "storm/exceptions/BaseException.h" - -#include "storm/logic/Formula.h" +#include "storm-dft/settings/DftSettings.h" +#include "storm-dft/settings/modules/DftIOSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/MinMaxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/modules/EliminationSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/utility/initialize.h" +#include "storm/api/storm.h" +#include "storm-cli-utilities/cli.h" + #include "storm-dft/parser/DFTGalileoParser.h" #include "storm-dft/parser/DFTJsonParser.h" #include "storm-dft/modelchecker/dft/DFTModelChecker.h" @@ -22,12 +16,8 @@ #include "storm-dft/transformations/DftToGspnTransformator.h" #include "storm-dft/storage/dft/DftJsonExporter.h" -#include "storm-dft/settings/modules/DFTSettings.h" - #include "storm-gspn/storage/gspn/GSPN.h" #include "storm-gspn/storm-gspn.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" #include #include @@ -44,18 +34,18 @@ */ template void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); std::shared_ptr> dft; // Build DFT from given file. - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl; + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl; + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } // Build properties @@ -91,72 +81,39 @@ void analyzeWithSMT(std::string filename) { //std::cout << "SMT result: " << sat << std::endl; } - -/*! - * Initialize the settings manager. - */ -void initializeSettings() { - storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft"); - - // Register all known settings modules. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - - // For translation into JANI via GSPN. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); -} - - void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); storm::cli::processOptions(); - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); + storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); - if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) { + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } - if (dftSettings.isExportToJson()) { - STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); + if (dftIOSettings.isExportToJson()) { + STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + storm::storage::DFT dft = parser.parseDFT(dftIOSettings.getDftFilename()); // Export to json - storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::storage::DftJsonExporter::toFile(dft, dftIOSettings.getExportJsonFilename()); storm::utility::cleanUp(); return; } - if (dftSettings.isTransformToGspn()) { + if (dftIOSettings.isTransformToGspn()) { std::shared_ptr> dft; - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser(true, false); - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); gspnTransformator.transform(); @@ -196,12 +153,12 @@ void processOptions() { #endif #ifdef STORM_HAVE_Z3 - if (dftSettings.solveWithSMT()) { + if (faultTreeSettings.solveWithSMT()) { // Solve with SMT if (parametric) { // analyzeWithSMT(dftSettings.getDftFilename()); } else { - analyzeWithSMT(dftSettings.getDftFilename()); + analyzeWithSMT(dftIOSettings.getDftFilename()); } storm::utility::cleanUp(); return; @@ -210,8 +167,8 @@ void processOptions() { // Set min or max std::string optimizationDirection = "min"; - if (dftSettings.isComputeMaximalValue()) { - STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); + if (dftIOSettings.isComputeMaximalValue()) { + STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); optimizationDirection = "max"; } @@ -221,19 +178,19 @@ void processOptions() { if (ioSettings.isPropertySet()) { properties.push_back(ioSettings.getProperty()); } - if (dftSettings.usePropExpectedTime()) { + if (dftIOSettings.usePropExpectedTime()) { properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropProbability()) { + if (dftIOSettings.usePropProbability()) { properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropTimebound()) { + if (dftIOSettings.usePropTimebound()) { std::stringstream stream; - stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]"; properties.push_back(stream.str()); } - if (dftSettings.usePropTimepoints()) { - for (double timepoint : dftSettings.getPropTimepoints()) { + if (dftIOSettings.usePropTimepoints()) { + for (double timepoint : dftIOSettings.getPropTimepoints()) { std::stringstream stream; stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; properties.push_back(stream.str()); @@ -246,19 +203,19 @@ void processOptions() { // Set possible approximation error double approximationError = 0.0; - if (dftSettings.isApproximationErrorSet()) { - approximationError = dftSettings.getApproximationError(); + if (faultTreeSettings.isApproximationErrorSet()) { + approximationError = faultTreeSettings.getApproximationError(); } // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); } } @@ -275,9 +232,8 @@ void processOptions() { int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::cli::printHeader("Storm-DyFTeE", argc, argv); - //storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); - initializeSettings(); + storm::cli::printHeader("Storm-dft", argc, argv); + storm::settings::initializeDftSettings("Storm-dft", "storm-dft"); storm::utility::Stopwatch totalTimer(true); if (!storm::cli::parseOptions(argc, argv)) { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 4a29b0652..5ef6bd07e 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -9,8 +9,6 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" -#include "storm-dft/settings/modules/DFTSettings.h" - namespace storm { namespace builder { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 0c7d69628..f035b0a55 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -10,7 +10,7 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" #include "storm/logic/AtomicLabelFormula.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { @@ -55,7 +55,7 @@ namespace storm { dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), - usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), + usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 7b86d1faa..0002cd6a3 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -4,7 +4,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/settings/SettingsManager.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { namespace generator { @@ -71,7 +71,7 @@ namespace storm { // Let BE fail while (currentFailable < failableCount) { - if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { // We discard further exploration as we already chose one dependent event break; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index d6b7e9138..45d97baa6 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -8,7 +8,7 @@ #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" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { @@ -344,7 +344,7 @@ namespace storm { STORM_LOG_INFO("Building Model..."); std::shared_ptr> model; // TODO Matthias: use only one builder if everything works again - if (storm::settings::getModule().isApproximationErrorSet()) { + if (storm::settings::getModule().isApproximationErrorSet()) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp new file mode 100644 index 000000000..ce48c6fd9 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.cpp @@ -0,0 +1,51 @@ +#include "storm-dft/settings/DftSettings.h" + +#include "storm-dft/settings/modules/DftIOSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/GmmxxEquationSolverSettings.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/GSPNSettings.h" +#include "storm/settings/modules/GSPNExportSettings.h" + + +namespace storm { + namespace settings { + void initializeDftSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + // Register relevant settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + // storm::settings::addModule(); + storm::settings::addModule(); + + // For translation into JANI via GSPN. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + } + + } +} diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h new file mode 100644 index 000000000..8f67ec0b7 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + + void initializeDftSettings(std::string const& name, std::string const& executableName); + + } +} diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp deleted file mode 100644 index 1a8d59d70..000000000 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ /dev/null @@ -1,189 +0,0 @@ -#include "DFTSettings.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/SettingMemento.h" -#include "storm/settings/Option.h" -#include "storm/settings/OptionBuilder.h" -#include "storm/settings/ArgumentBuilder.h" -#include "storm/settings/Argument.h" - -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/IllegalArgumentValueException.h" - -namespace storm { - namespace settings { - namespace modules { - - const std::string DFTSettings::moduleName = "dft"; - const std::string DFTSettings::dftFileOptionName = "dftfile"; - const std::string DFTSettings::dftFileOptionShortName = "dft"; - const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json"; - const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson"; - const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction"; - const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; - const std::string DFTSettings::modularisationOptionName = "modularisation"; - const std::string DFTSettings::disableDCOptionName = "disabledc"; - const std::string DFTSettings::approximationErrorOptionName = "approximation"; - const std::string DFTSettings::approximationErrorOptionShortName = "approx"; - const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; - const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; - const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; - const std::string DFTSettings::propProbabilityOptionName = "probability"; - const std::string DFTSettings::propTimeboundOptionName = "timebound"; - const std::string DFTSettings::propTimepointsOptionName = "timepoints"; - const std::string DFTSettings::minValueOptionName = "min"; - const std::string DFTSettings::maxValueOptionName = "max"; - const std::string DFTSettings::firstDependencyOptionName = "firstdep"; - const std::string DFTSettings::transformToGspnOptionName = "gspn"; - const std::string DFTSettings::exportToJsonOptionName = "export-json"; -#ifdef STORM_HAVE_Z3 - const std::string DFTSettings::solveWithSmtOptionName = "smt"; -#endif - - DFTSettings::DFTSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); -#ifdef STORM_HAVE_Z3 - this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); -#endif - this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); - } - - bool DFTSettings::isDftFileSet() const { - return this->getOption(dftFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftFilename() const { - return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::isDftJsonFileSet() const { - return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftJsonFilename() const { - return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::useSymmetryReduction() const { - return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::useModularisation() const { - return this->getOption(modularisationOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isDisableDC() const { - return this->getOption(disableDCOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isApproximationErrorSet() const { - return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getApproximationError() const { - return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); - } - - storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { - if (!isApproximationErrorSet() || getApproximationError() == 0.0) { - // No approximation is done - return storm::builder::ApproximationHeuristic::NONE; - } - std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); - if (heuristicAsString == "depth") { - return storm::builder::ApproximationHeuristic::DEPTH; - } else if (heuristicAsString == "probability") { - return storm::builder::ApproximationHeuristic::PROBABILITY; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); - } - - bool DFTSettings::usePropExpectedTime() const { - return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropProbability() const { - return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropTimebound() const { - return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getPropTimebound() const { - return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); - } - - bool DFTSettings::usePropTimepoints() const { - return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); - } - - std::vector DFTSettings::getPropTimepoints() const { - double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); - double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); - double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); - std::vector timepoints; - for (double time = starttime; time <= endtime; time += inc) { - timepoints.push_back(time); - } - return timepoints; - } - - bool DFTSettings::isComputeMinimalValue() const { - return this->getOption(minValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isComputeMaximalValue() const { - return this->getOption(maxValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isTakeFirstDependency() const { - return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); - } - -#ifdef STORM_HAVE_Z3 - bool DFTSettings::solveWithSMT() const { - return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); - } -#endif - - bool DFTSettings::isTransformToGspn() const { - return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isExportToJson() const { - return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getExportJsonFilename() const { - return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); - } - - void DFTSettings::finalize() { - } - - bool DFTSettings::check() const { - // Ensure that at most one of min or max is set - STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); - return true; - } - - } // namespace modules - } // namespace settings -} // namespace storm diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp new file mode 100644 index 000000000..cf656333d --- /dev/null +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -0,0 +1,123 @@ +#include "DftIOSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string DftIOSettings::moduleName = "dftIO"; + const std::string DftIOSettings::dftFileOptionName = "dftfile"; + const std::string DftIOSettings::dftFileOptionShortName = "dft"; + const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json"; + const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson"; + const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime"; + const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf"; + const std::string DftIOSettings::propProbabilityOptionName = "probability"; + const std::string DftIOSettings::propTimeboundOptionName = "timebound"; + const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; + const std::string DftIOSettings::minValueOptionName = "min"; + const std::string DftIOSettings::maxValueOptionName = "max"; + const std::string DftIOSettings::transformToGspnOptionName = "gspn"; + const std::string DftIOSettings::exportToJsonOptionName = "export-json"; + + DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); + } + + bool DftIOSettings::isDftFileSet() const { + return this->getOption(dftFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftFilename() const { + return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::isDftJsonFileSet() const { + return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftJsonFilename() const { + return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::usePropExpectedTime() const { + return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropProbability() const { + return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropTimebound() const { + return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); + } + + double DftIOSettings::getPropTimebound() const { + return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); + } + + bool DftIOSettings::usePropTimepoints() const { + return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); + } + + std::vector DftIOSettings::getPropTimepoints() const { + double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); + double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); + double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); + std::vector timepoints; + for (double time = starttime; time <= endtime; time += inc) { + timepoints.push_back(time); + } + return timepoints; + } + + bool DftIOSettings::isComputeMinimalValue() const { + return this->getOption(minValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isComputeMaximalValue() const { + return this->getOption(maxValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isTransformToGspn() const { + return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isExportToJson() const { + return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getExportJsonFilename() const { + return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); + } + + void DftIOSettings::finalize() { + } + + bool DftIOSettings::check() const { + // Ensure that at most one of min or max is set + STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h similarity index 63% rename from src/storm-dft/settings/modules/DFTSettings.h rename to src/storm-dft/settings/modules/DftIOSettings.h index c04ef1a23..8a8fbcdd1 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -1,24 +1,21 @@ #pragma once -#include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" -#include "storm-dft/builder/DftExplorationHeuristic.h" - namespace storm { namespace settings { namespace modules { /*! - * This class represents the settings for DFT model checking. + * This class represents the settings for IO operations concerning DFTs. */ - class DFTSettings : public ModuleSettings { + class DftIOSettings : public ModuleSettings { public: /*! - * Creates a new set of DFT settings. + * Creates a new set of IO settings for DFTs. */ - DFTSettings(); + DftIOSettings(); /*! * Retrieves whether the dft file option was set. @@ -48,48 +45,6 @@ namespace storm { */ std::string getDftJsonFilename() const; - /*! - * Retrieves whether the option to use symmetry reduction is set. - * - * @return True iff the option was set. - */ - bool useSymmetryReduction() const; - - /*! - * Retrieves whether the option to use modularisation is set. - * - * @return True iff the option was set. - */ - bool useModularisation() const; - - /*! - * Retrieves whether the option to disable Dont Care propagation is set. - * - * @return True iff the option was set. - */ - bool isDisableDC() const; - - /*! - * Retrieves whether the option to compute an approximation is set. - * - * @return True iff the option was set. - */ - bool isApproximationErrorSet() const; - - /*! - * Retrieves the relative error allowed for approximating the model checking result. - * - * @return The allowed errorbound. - */ - double getApproximationError() const; - - /*! - * Retrieves the heuristic used for approximation. - * - * @return The heuristic to use. - */ - storm::builder::ApproximationHeuristic getApproximationHeuristic() const; - /*! * Retrieves whether the property expected time should be used. * @@ -146,13 +101,6 @@ namespace storm { */ bool isComputeMaximalValue() const; - /*! - * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. - * - * @return True iff the option was set. - */ - bool isTakeFirstDependency() const; - /*! * Retrieves whether the DFT should be transformed into a GSPN. * @@ -174,15 +122,6 @@ namespace storm { */ std::string getExportJsonFilename() const; -#ifdef STORM_HAVE_Z3 - /*! - * Retrieves whether the DFT should be checked via SMT. - * - * @return True iff the option was set. - */ - bool solveWithSMT() const; -#endif - bool check() const override; void finalize() override; @@ -195,13 +134,6 @@ namespace storm { static const std::string dftFileOptionShortName; static const std::string dftJsonFileOptionName; static const std::string dftJsonFileOptionShortName; - static const std::string symmetryReductionOptionName; - static const std::string symmetryReductionOptionShortName; - static const std::string modularisationOptionName; - static const std::string disableDCOptionName; - static const std::string approximationErrorOptionName; - static const std::string approximationErrorOptionShortName; - static const std::string approximationHeuristicOptionName; static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; @@ -209,10 +141,6 @@ namespace storm { static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; - static const std::string firstDependencyOptionName; -#ifdef STORM_HAVE_Z3 - static const std::string solveWithSmtOptionName; -#endif static const std::string transformToGspnOptionName; static const std::string exportToJsonOptionName; diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp new file mode 100644 index 000000000..7c9ef14af --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -0,0 +1,93 @@ +#include "FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string FaultTreeSettings::moduleName = "dft"; + const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction"; + const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; + const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; + const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; + const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; + const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; + const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; + const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; +#ifdef STORM_HAVE_Z3 + const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; +#endif + + FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); +#ifdef STORM_HAVE_Z3 + this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); +#endif + } + + bool FaultTreeSettings::useSymmetryReduction() const { + return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::useModularisation() const { + return this->getOption(modularisationOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isDisableDC() const { + return this->getOption(disableDCOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isApproximationErrorSet() const { + return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); + } + + double FaultTreeSettings::getApproximationError() const { + return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); + } + + storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const { + if (!isApproximationErrorSet() || getApproximationError() == 0.0) { + // No approximation is done + return storm::builder::ApproximationHeuristic::NONE; + } + std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); + if (heuristicAsString == "depth") { + return storm::builder::ApproximationHeuristic::DEPTH; + } else if (heuristicAsString == "probability") { + return storm::builder::ApproximationHeuristic::PROBABILITY; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); + } + + bool FaultTreeSettings::isTakeFirstDependency() const { + return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); + } + +#ifdef STORM_HAVE_Z3 + bool FaultTreeSettings::solveWithSMT() const { + return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); + } +#endif + + void FaultTreeSettings::finalize() { + } + + bool FaultTreeSettings::check() const { + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h new file mode 100644 index 000000000..171d5c38e --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -0,0 +1,104 @@ +#pragma once + +#include "storm/settings/modules/ModuleSettings.h" +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-config.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for DFT model checking. + */ + class FaultTreeSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of DFT settings. + */ + FaultTreeSettings(); + + /*! + * Retrieves whether the option to use symmetry reduction is set. + * + * @return True iff the option was set. + */ + bool useSymmetryReduction() const; + + /*! + * Retrieves whether the option to use modularisation is set. + * + * @return True iff the option was set. + */ + bool useModularisation() const; + + /*! + * Retrieves whether the option to disable Dont Care propagation is set. + * + * @return True iff the option was set. + */ + bool isDisableDC() const; + + /*! + * Retrieves whether the option to compute an approximation is set. + * + * @return True iff the option was set. + */ + bool isApproximationErrorSet() const; + + /*! + * Retrieves the relative error allowed for approximating the model checking result. + * + * @return The allowed errorbound. + */ + double getApproximationError() const; + + /*! + * Retrieves the heuristic used for approximation. + * + * @return The heuristic to use. + */ + storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + + /*! + * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. + * + * @return True iff the option was set. + */ + bool isTakeFirstDependency() const; + +#ifdef STORM_HAVE_Z3 + /*! + * Retrieves whether the DFT should be checked via SMT. + * + * @return True iff the option was set. + */ + bool solveWithSMT() const; +#endif + + bool check() const override; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string symmetryReductionOptionName; + static const std::string symmetryReductionOptionShortName; + static const std::string modularisationOptionName; + static const std::string disableDCOptionName; + static const std::string approximationErrorOptionName; + static const std::string approximationErrorOptionShortName; + static const std::string approximationHeuristicOptionName; + static const std::string firstDependencyOptionName; +#ifdef STORM_HAVE_Z3 + static const std::string solveWithSmtOptionName; +#endif + + }; + + } // namespace modules + } // namespace settings +} // namespace storm From 5ad60051c32c13eeeabaa0cb30853a16f0f33b83 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 11 Oct 2017 18:50:53 +0200 Subject: [PATCH 05/15] Region model checker can now also return a (quantitative) upper/lower bound for a given region --- .../modelchecker/region/RegionModelChecker.cpp | 7 +++++++ .../modelchecker/region/RegionModelChecker.h | 2 ++ .../region/SparseParameterLiftingModelChecker.cpp | 13 +++++++++++++ .../region/SparseParameterLiftingModelChecker.h | 3 +++ 4 files changed, 25 insertions(+) diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index 23ba29489..ab0142d0b 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -17,6 +17,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/exceptions/NotImplementedException.h" namespace storm { @@ -43,6 +44,12 @@ namespace storm { return std::make_unique>(std::move(result)); } + template + ParametricType RegionModelChecker::getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected region model checker does not support this functionality."); + return storm::utility::zero(); + } + template std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold, RegionResultHypothesis const& hypothesis) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index c1a558800..595d1e8f0 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -42,6 +42,8 @@ namespace storm { */ std::unique_ptr> analyzeRegions(std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion = false) ; + virtual ParametricType getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + /*! * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated). * @param region the considered region diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index d0b2af22b..1accd68cc 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/utility/vector.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -130,6 +131,18 @@ namespace storm { } } + template + std::unique_ptr> SparseParameterLiftingModelChecker::getBound(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula..."); + return std::make_unique>(std::move(computeQuantitativeValues(region, dirForParameters)->template asExplicitQuantitativeCheckResult())); + } + + template + typename SparseModelType::ValueType SparseParameterLiftingModelChecker::getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state."); + return storm::utility::convertNumber(getBound(region, dirForParameters)->template asExplicitQuantitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]); + } + template SparseModelType const& SparseParameterLiftingModelChecker::getConsideredParametricModel() const { return *parametricModel; diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h index e0cabd5f0..cb993ad4f 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h @@ -45,6 +45,9 @@ namespace storm { */ std::unique_ptr check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + std::unique_ptr> getBound(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + virtual typename SparseModelType::ValueType getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; + SparseModelType const& getConsideredParametricModel() const; CheckTask const& getCurrentCheckTask() const; From 91bd638c1876120132994acbb3200eaa4c815d33 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 12 Oct 2017 10:46:53 +0200 Subject: [PATCH 06/15] Fixed segfault --- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index f035b0a55..c7d6605f5 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -581,13 +581,13 @@ namespace storm { maComponents.rateTransitions = true; maComponents.markovianStates = modelComponents.markovianStates; maComponents.exitRates = modelComponents.exitRates; - std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); + ma = std::make_shared>(std::move(maComponents)); } else { storm::storage::sparse::ModelComponents maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); maComponents.rateTransitions = true; maComponents.markovianStates = std::move(modelComponents.markovianStates); maComponents.exitRates = std::move(modelComponents.exitRates); - std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); + ma = std::make_shared>(std::move(maComponents)); } if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC From 983e09fd635b1911821e88b7373a1dd58e8bbc1b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 12 Oct 2017 18:18:36 +0200 Subject: [PATCH 07/15] Fixed possible problem with rates and exit rates in MA --- src/storm/models/sparse/MarkovAutomaton.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 485aa8a64..8bc00fa99 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -50,7 +50,9 @@ namespace storm { if (components.exitRates) { exitRates = std::move(components.exitRates.get()); - } else { + } + + if (components.rateTransitions) { this->turnRatesToProbabilities(); } closed = this->checkIsClosed(); From 88544a9ec79bf7a4613eaf05fba64895701951d3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 12 Oct 2017 18:19:36 +0200 Subject: [PATCH 08/15] Added assertion for turnRatesToProbabilities in MA --- src/storm/models/sparse/MarkovAutomaton.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 8bc00fa99..ca79ccfac 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -152,7 +152,7 @@ namespace storm { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; if (this->markovianStates.get(state)) { if (assertRates) { - STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << "."); + STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << "."); } else { this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row)); } @@ -161,7 +161,11 @@ namespace storm { } ++row; } else { - this->exitRates.push_back(storm::utility::zero()); + if (assertRates) { + STORM_LOG_THROW(storm::utility::isZero(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0."); + } else { + this->exitRates.push_back(storm::utility::zero()); + } } for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); From 4456069e81e995d844bb7e447832f5f258488da5 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 12 Oct 2017 18:19:52 +0200 Subject: [PATCH 09/15] Fixed typo --- src/storm/models/sparse/MarkovAutomaton.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 249766b62..89c73f83c 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -22,7 +22,7 @@ namespace storm { * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. @@ -38,7 +38,7 @@ namespace storm { * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. From 87778a677526a11651a912601b35b45a9896edcf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 12 Oct 2017 20:33:24 +0200 Subject: [PATCH 10/15] Finally removed old DFTModelBuilder --- .../builder/ExplicitDFTModelBuilder.cpp | 471 ------------------ .../builder/ExplicitDFTModelBuilder.h | 102 ---- .../modelchecker/dft/DFTModelChecker.cpp | 17 +- 3 files changed, 4 insertions(+), 586 deletions(-) delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.cpp delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.h diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp deleted file mode 100644 index 5ef6bd07e..000000000 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ /dev/null @@ -1,471 +0,0 @@ -#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/SettingsManager.h" - - -namespace storm { - namespace builder { - - template - ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { - // Intentionally left empty. - } - - template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) { - // stateVectorSize is bound for size of bitvector - - mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(symmetries)); - } - - - template - std::shared_ptr> ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts) { - // Initialize - bool deterministicModel = false; - size_t rowOffset = 0; - ModelComponents modelComponents; - std::vector tmpMarkovianStates; - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - - if(mergeFailedStates) { - // Introduce explicit fail state - failedIndex = newIndex; - newIndex++; - transitionMatrixBuilder.newRowGroup(failedIndex); - transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one()); - STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex); - modelComponents.exitRates.push_back(storm::utility::one()); - tmpMarkovianStates.push_back(failedIndex); - } - - // Explore state space - DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex); - auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); - initialStateIndex = exploreResult.first; - bool deterministic = exploreResult.second; - - // Before ending the exploration check for pseudo states which are not initialized yet - for (auto & pseudoStatePair : mPseudoStatesMapping) { - if (pseudoStatePair.first == 0) { - // Create state from pseudo state and explore - STORM_LOG_ASSERT(mStates.contains(pseudoStatePair.second), "Pseudo state not contained."); - STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state."); - STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second); - DFTStatePointer pseudoState = std::make_shared>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex); - pseudoState->construct(); - STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide."); - STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId()); - auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); - deterministic &= exploreResult.second; - STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide"); - STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide."); - } - } - - // Replace pseudo states in matrix - std::vector pseudoStatesVector; - for (auto const& pseudoStatePair : mPseudoStatesMapping) { - pseudoStatesVector.push_back(pseudoStatePair.first); - } - STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained."); - transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE); - - STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states"); - STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic")); - - size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0); - // Build Markov Automaton - modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates); - // Build transition matrix - modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize); - if (stateSize <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } - STORM_LOG_TRACE("Exit rates: " << storm::utility::vector::toString(modelComponents.exitRates)); - STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); - - // Build state labeling - modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0)); - // Initial state is always first state without any failure - modelComponents.stateLabeling.addLabel("init"); - modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); - // Label all states corresponding to their status (failed, failsafe, failed BE) - if(labelOpts.buildFailLabel) { - modelComponents.stateLabeling.addLabel("failed"); - } - if(labelOpts.buildFailSafeLabel) { - modelComponents.stateLabeling.addLabel("failsafe"); - } - - // Collect labels for all BE - std::vector>> basicElements = mDft.getBasicElements(); - for (std::shared_ptr> elem : basicElements) { - if(labelOpts.beLabels.count(elem->name()) > 0) { - modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); - } - } - - if(mergeFailedStates) { - modelComponents.stateLabeling.addLabelToState("failed", failedIndex); - } - for (auto const& stateIdPair : mStates) { - storm::storage::BitVector state = stateIdPair.first; - size_t stateId = stateIdPair.second; - if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) { - modelComponents.stateLabeling.addLabelToState("failed", stateId); - } - if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) { - modelComponents.stateLabeling.addLabelToState("failsafe", stateId); - }; - // Set fail status for each BE - for (std::shared_ptr> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) { - modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId); - } - } - } - - std::shared_ptr> model; - storm::storage::sparse::ModelComponents components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); - components.exitRates = std::move(modelComponents.exitRates); - if (deterministic) { - components.transitionMatrix.makeRowGroupingTrivial(); - model = std::make_shared>(std::move(components)); - } else { - components.markovianStates = std::move(modelComponents.markovianStates); - std::shared_ptr> ma = std::make_shared>(std::move(components)); - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - model = ma->convertToCTMC(); - } else { - model = ma; - } - } - - return model; - } - - template - std::pair ExplicitDFTModelBuilder::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { - STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state)); - - auto explorePair = checkForExploration(state); - if (!explorePair.first) { - // State does not need any exploration - return std::make_pair(explorePair.second, true); - } - - - // Initialization - // TODO Matthias: set Markovian states directly as bitvector? - std::map outgoingRates; - std::vector> outgoingProbabilities; - bool hasDependencies = state->nrFailableDependencies() > 0; - size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); - size_t smallest = 0; - ValueType exitRate = storm::utility::zero(); - bool deterministic = !hasDependencies; - - // Absorbing state - if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) { - uint_fast64_t stateId = addState(state); - STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide."); - - // Add self loop - transitionMatrixBuilder.newRowGroup(stateId + rowOffset); - transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one()); - STORM_LOG_TRACE("Added self loop for " << stateId); - exitRates.push_back(storm::utility::one()); - STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id."); - markovianStates.push_back(stateId); - // No further exploration required - return std::make_pair(stateId, true); - } - - // Let BE fail - while (smallest < failableCount) { - STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); - - // Construct new state as copy from original one - DFTStatePointer newState = std::make_shared>(*state); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(smallest++); - std::shared_ptr const>& nextBE = nextBEPair.first; - STORM_LOG_ASSERT(nextBE, "NextBE is null."); - STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match."); - STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state)); - - // Propagate failures - storm::storage::DFTStateSpaceGenerationQueues queues; - - for (DFTGatePointer parent : nextBE->parents()) { - if (newState->isOperational(parent->id())) { - queues.propagateFailure(parent); - } - } - for (DFTRestrictionPointer restr : nextBE->restrictions()) { - queues.checkRestrictionLater(restr); - } - - while (!queues.failurePropagationDone()) { - DFTGatePointer next = queues.nextFailurePropagation(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - } - - while(!queues.restrictionChecksDone()) { - DFTRestrictionPointer next = queues.nextRestrictionCheck(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - } - - if(newState->isInvalid()) { - continue; - } - bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex()); - - while (!dftFailed && !queues.failsafePropagationDone()) { - DFTGatePointer next = queues.nextFailsafePropagation(); - next->checkFailsafe(*newState, queues); - } - - while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) { - DFTElementPointer next = queues.nextDontCarePropagation(); - next->checkDontCareAnymore(*newState, queues); - } - - // Update failable dependencies - if (!dftFailed) { - newState->updateFailableDependencies(nextBE->id()); - newState->updateDontCareDependencies(nextBE->id()); - } - - uint_fast64_t newStateId; - if(dftFailed && mergeFailedStates) { - newStateId = failedIndex; - } else { - // Explore new state recursively - auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates); - newStateId = explorePair.first; - deterministic &= explorePair.second; - } - - // Set transitions - if (hasDependencies) { - // Failure is due to dependency -> add non-deterministic choice - std::map choiceProbabilities; - std::shared_ptr const> dependency = mDft.getDependency(state->getDependencyId(smallest-1)); - choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability())); - STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability()); - - if (!storm::utility::isOne(dependency->probability())) { - // Add transition to state where dependency was unsuccessful - DFTStatePointer unsuccessfulState = std::make_shared>(*state); - unsuccessfulState->letDependencyBeUnsuccessful(smallest-1); - auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates); - uint_fast64_t unsuccessfulStateId = explorePair.first; - deterministic &= explorePair.second; - ValueType remainingProbability = storm::utility::one() - dependency->probability(); - choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability)); - STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability); - } - outgoingProbabilities.push_back(choiceProbabilities); - } else { - // Set failure rate according to activation - bool isActive = true; - if (mDft.hasRepresentant(nextBE->id())) { - // Active must be checked for the state we are coming from as this state is responsible for the - // rate and not the new state we are going to - isActive = state->isActive(mDft.getRepresentant(nextBE->id())); - } - ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); - STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); - auto resultFind = outgoingRates.find(newStateId); - if (resultFind != outgoingRates.end()) { - // Add to existing transition - resultFind->second += rate; - STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second); - } else { - // Insert new transition - outgoingRates.insert(std::make_pair(newStateId, rate)); - STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate); - } - exitRate += rate; - } - - } // end while failing BE - - // Add state - uint_fast64_t stateId = addState(state); - STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); - STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states."); - - if (hasDependencies) { - // Add all probability transitions - STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty."); - transitionMatrixBuilder.newRowGroup(stateId + rowOffset); - for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) { - STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid."); - for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it) - { - STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second); - transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second); - } - } - rowOffset--; // One increment too many - } else { - // Try to merge pseudo states with their instantiation - // TODO Matthias: improve? - for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) { - if (it->first >= OFFSET_PSEUDO_STATE) { - uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE; - STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid."); - if (mPseudoStatesMapping[newId].first > 0) { - // State exists already - newId = mPseudoStatesMapping[newId].first; - auto itFind = outgoingRates.find(newId); - if (itFind != outgoingRates.end()) { - // Add probability from pseudo state to instantiation - itFind->second += it->second; - STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second); - } else { - // Only change id - outgoingRates.emplace(newId, it->second); - STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second); - } - // Remove pseudo state - it = outgoingRates.erase(it); - } else { - ++it; - } - } else { - ++it; - } - } - - // Add all rate transitions - STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty."); - transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); - STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate); - for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it) - { - ValueType probability = it->second / exitRate; // Transform rate to probability - STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second); - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); - } - - markovianStates.push_back(state->getId()); - } - - STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state)); - exitRates.push_back(exitRate); - STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states."); - return std::make_pair(state->getId(), deterministic); - } - - template - std::pair ExplicitDFTModelBuilder::checkForExploration(DFTStatePointer const& state) { - bool changed = false; - if (mStateGenerationInfo->hasSymmetries()) { - // Order state by symmetry - STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state)); - changed = state->orderBySymmetry(); - STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : "")); - } - - if (mStates.contains(state->status())) { - // State already exists - uint_fast64_t stateId = mStates.getValue(state->status()); - STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists"); - - if (changed || stateId < OFFSET_PSEUDO_STATE) { - // State is changed or an explored "normal" state - return std::make_pair(false, stateId); - } - - stateId -= OFFSET_PSEUDO_STATE; - STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid."); - if (mPseudoStatesMapping[stateId].first > 0) { - // Pseudo state already explored - return std::make_pair(false, mPseudoStatesMapping[stateId].first); - } - - STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide."); - STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now"); - return std::make_pair(true, stateId); - } else { - // State does not exists - if (changed) { - // Remember state for later creation - state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE); - mPseudoStatesMapping.push_back(std::make_pair(0, state->status())); - mStates.findOrAdd(state->status(), state->getId()); - STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state)); - return std::make_pair(false, state->getId()); - } else { - // State needs exploration - return std::make_pair(true, 0); - } - } - } - - template - uint_fast64_t ExplicitDFTModelBuilder::addState(DFTStatePointer const& state) { - uint_fast64_t stateId; - // TODO remove - bool changed = state->orderBySymmetry(); - STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry."); - - // Check if state already exists - if (mStates.contains(state->status())) { - // State already exists - stateId = mStates.getValue(state->status()); - STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists"); - - // Check if possible pseudo state can be created now - STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state."); - stateId -= OFFSET_PSEUDO_STATE; - STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known."); - if (mPseudoStatesMapping[stateId].first == 0) { - // Create pseudo state now - STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide."); - state->setId(newIndex++); - mPseudoStatesMapping[stateId].first = state->getId(); - stateId = state->getId(); - mStates.setOrAdd(state->status(), stateId); - STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId); - return stateId; - } else { - STORM_LOG_ASSERT(false, "Pseudo state already created."); - return 0; - } - } else { - // Create new state - state->setId(newIndex++); - stateId = mStates.findOrAdd(state->status(), state->getId()); - STORM_LOG_TRACE("New state: " << mDft.getStateString(state)); - return stateId; - } - } - - - // Explicitly instantiate the class. - template class ExplicitDFTModelBuilder; - -#ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilder; -#endif - - } // namespace builder -} // namespace storm - - diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h deleted file mode 100644 index 2913a78fa..000000000 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ /dev/null @@ -1,102 +0,0 @@ -#pragma once - -#include -#include -#include -#include - - -#include "storm/models/sparse/StateLabeling.h" -#include "storm/models/sparse/ChoiceLabeling.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-dft/storage/dft/DFT.h" -#include "storm-dft/storage/dft/SymmetricUnits.h" - - - - - -namespace storm { - namespace builder { - - template - class ExplicitDFTModelBuilder { - - using DFTElementPointer = std::shared_ptr>; - using DFTElementCPointer = std::shared_ptr const>; - using DFTGatePointer = std::shared_ptr>; - using DFTStatePointer = std::shared_ptr>; - using DFTRestrictionPointer = std::shared_ptr>; - - - // A structure holding the individual components of a model. - struct ModelComponents { - ModelComponents(); - - // The transition matrix. - storm::storage::SparseMatrix transitionMatrix; - - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; - - // The Markovian states. - storm::storage::BitVector markovianStates; - - // The exit rates. - std::vector exitRates; - - // A vector that stores a labeling for each choice. - boost::optional choiceLabeling; - }; - - const size_t INITIAL_BUCKETSIZE = 20000; - const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2; - - storm::storage::DFT const& mDft; - std::shared_ptr mStateGenerationInfo; - storm::storage::BitVectorHashMap mStates; - std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) - size_t newIndex = 0; - bool mergeFailedStates = false; - bool enableDC = true; - size_t failedIndex = 0; - size_t initialStateIndex = 0; - - public: - struct LabelOptions { - bool buildFailLabel = true; - bool buildFailSafeLabel = false; - std::set beLabels = {}; - }; - - ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); - - std::shared_ptr> buildModel(LabelOptions const& labelOpts); - - private: - std::pair exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); - - /*! - * Adds a state to the explored states and handles pseudo states. - * - * @param state The state to add. - * @return Id of added state. - */ - uint_fast64_t addState(DFTStatePointer const& state); - - /*! - * Check if state needs an exploration and remember pseudo states for later creation. - * - * @param state State which might need exploration. - * @return Pair of flag indicating whether the state needs exploration now and the state id if the state already - * exists. - */ - std::pair checkForExploration(DFTStatePointer const& state); - - }; - } -} diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 45d97baa6..3a69cb5e4 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -5,7 +5,6 @@ #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.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/FaultTreeSettings.h" @@ -342,18 +341,10 @@ namespace storm { } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); - std::shared_ptr> model; - // TODO Matthias: use only one builder if everything works again - if (storm::settings::getModule().isApproximationErrorSet()) { - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); - builder.buildModel(labeloptions, 0, 0.0); - model = builder.getModel(); - } else { - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; - model = builder.buildModel(labeloptions); - } + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); explorationTimer.stop(); From 0913388cd3cb7952d43b37661547efc7abf64072 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 13 Oct 2017 18:11:05 +0200 Subject: [PATCH 11/15] Renamed ExplicitDFTModelBuilderApprox to ExplicitDFTModelBuilder --- ...Approx.cpp => ExplicitDFTModelBuilder.cpp} | 46 +++++++++---------- ...lderApprox.h => ExplicitDFTModelBuilder.h} | 4 +- .../modelchecker/dft/DFTModelChecker.cpp | 19 ++++---- 3 files changed, 34 insertions(+), 35 deletions(-) rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.cpp => ExplicitDFTModelBuilder.cpp} (94%) rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.h => ExplicitDFTModelBuilder.h} (98%) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp similarity index 94% rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index c7d6605f5..2b74432ad 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -1,4 +1,4 @@ -#include "ExplicitDFTModelBuilderApprox.h" +#include "ExplicitDFTModelBuilder.h" #include @@ -17,18 +17,18 @@ namespace storm { namespace builder { template - ExplicitDFTModelBuilderApprox::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { + ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } template - ExplicitDFTModelBuilderApprox::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { + ExplicitDFTModelBuilder::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { // Create matrix builder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); } template - ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { + ExplicitDFTModelBuilder::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { // Get necessary labels from properties std::vector> atomicLabels; for (auto property : properties) { @@ -51,7 +51,7 @@ namespace storm { } template - ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), @@ -124,7 +124,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { + void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { STORM_LOG_TRACE("Generating DFT state space"); if (iteration < 1) { @@ -156,7 +156,7 @@ namespace storm { } // Build initial state - this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); + this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); @@ -214,7 +214,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::initializeNextIteration() { + void ExplicitDFTModelBuilder::initializeNextIteration() { STORM_LOG_TRACE("Refining DFT state space"); // TODO Matthias: should be easier now as skipped states all are at the end of the matrix @@ -316,7 +316,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { + void ExplicitDFTModelBuilder::exploreStateSpace(double approximationThreshold) { size_t nrExpandedStates = 0; size_t nrSkippedStates = 0; // TODO Matthias: do not empty queue every time but break before @@ -364,7 +364,7 @@ namespace storm { } else { // Explore the current state ++nrExpandedStates; - storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); + storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); setMarkovian(behavior.begin()->isMarkovian()); @@ -424,7 +424,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::buildLabeling(LabelOptions const& labelOpts) { + void ExplicitDFTModelBuilder::buildLabeling(LabelOptions const& labelOpts) { // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state @@ -473,13 +473,13 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModel() { + std::shared_ptr> ExplicitDFTModelBuilder::getModel() { STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); return createModel(false); } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound, bool expectedTime) { + std::shared_ptr> ExplicitDFTModelBuilder::getModelApproximation(bool lowerBound, bool expectedTime) { if (expectedTime) { // TODO Matthias: handle case with no skipped states changeMatrixBound(modelComponents.transitionMatrix, lowerBound); @@ -550,7 +550,7 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::createModel(bool copy) { + std::shared_ptr> ExplicitDFTModelBuilder::createModel(bool copy) { std::shared_ptr> model; if (modelComponents.deterministicModel) { @@ -607,7 +607,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const { + void ExplicitDFTModelBuilder::changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const { // Set lower bound for skipped states for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { auto matrixEntry = matrix.getRow(it->first, 0).begin(); @@ -632,7 +632,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::getLowerBound(DFTStatePointer const& state) const { + ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { // Get the lower bound by considering the failure of all possible BEs ValueType lowerBound = storm::utility::zero(); for (size_t index = 0; index < state->nrFailableBEs(); ++index) { @@ -642,7 +642,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { + ValueType ExplicitDFTModelBuilder::getUpperBound(DFTStatePointer const& state) const { if (state->hasFailed(dft.getTopLevelIndex())) { return storm::utility::zero(); } @@ -709,7 +709,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector const& rates, size_t size) const { + ValueType ExplicitDFTModelBuilder::computeMTTFAnd(std::vector const& rates, size_t size) const { ValueType result = storm::utility::zero(); if (size == 0) { return result; @@ -762,7 +762,7 @@ namespace storm { } template - StateType ExplicitDFTModelBuilderApprox::getOrAddStateIndex(DFTStatePointer const& state) { + StateType ExplicitDFTModelBuilder::getOrAddStateIndex(DFTStatePointer const& state) { StateType stateId; bool changed = false; @@ -811,7 +811,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::setMarkovian(bool markovian) { + void ExplicitDFTModelBuilder::setMarkovian(bool markovian) { if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) { // Resize BitVector modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE); @@ -820,7 +820,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::printNotExplored() const { + void ExplicitDFTModelBuilder::printNotExplored() const { std::cout << "states not explored:" << std::endl; for (auto it : statesNotExplored) { std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; @@ -829,10 +829,10 @@ namespace storm { // Explicitly instantiate the class. - template class ExplicitDFTModelBuilderApprox; + template class ExplicitDFTModelBuilder; #ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilderApprox; + template class ExplicitDFTModelBuilder; #endif } // namespace builder diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h similarity index 98% rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h index 802aefe1b..b96dea410 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -26,7 +26,7 @@ namespace storm { * Build a Markov chain from DFT. */ template - class ExplicitDFTModelBuilderApprox { + class ExplicitDFTModelBuilder { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable @@ -177,7 +177,7 @@ namespace storm { * @param symmetries Symmetries in the dft. * @param enableDC Flag indicating if dont care propagation should be used. */ - ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); /*! * Build model from DFT. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 3a69cb5e4..d2b435c1c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -5,7 +5,7 @@ #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" -#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" +#include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" @@ -191,8 +191,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -243,9 +243,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); @@ -276,8 +275,8 @@ namespace storm { approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); // TODO Matthias: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -341,8 +340,8 @@ namespace storm { } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); From 72d58b6155632b30b4910512376bde7f5107e9c0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 13 Oct 2017 20:28:09 +0200 Subject: [PATCH 12/15] fix for sylvan workers not releasing mmap'ed memory --- resources/3rdparty/sylvan/src/lace.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c index 08e9f8843..9315f6895 100755 --- a/resources/3rdparty/sylvan/src/lace.c +++ b/resources/3rdparty/sylvan/src/lace.c @@ -715,6 +715,9 @@ VOID_TASK_1(lace_steal_loop, int*, quit) } while (__lace_worker->enabled == 0); } } + + // Unmap the virtual memory from the worker. + munmap(workers_memory[worker_id], workers_memory_size); } /** From 02c23865da563a2d3eb72a6424188461e82b648a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 14 Oct 2017 14:24:39 +0200 Subject: [PATCH 13/15] reworked memory leak solution in sylvan according to Tom van Dijks hints --- resources/3rdparty/sylvan/src/lace.c | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c index 9315f6895..64443e23b 100755 --- a/resources/3rdparty/sylvan/src/lace.c +++ b/resources/3rdparty/sylvan/src/lace.c @@ -715,9 +715,6 @@ VOID_TASK_1(lace_steal_loop, int*, quit) } while (__lace_worker->enabled == 0); } } - - // Unmap the virtual memory from the worker. - munmap(workers_memory[worker_id], workers_memory_size); } /** @@ -1091,6 +1088,12 @@ void lace_exit() lace_resume(); lace_barrier(); + // Free the memory of the workers. + for (unsigned int i=0; i Date: Sat, 14 Oct 2017 14:13:13 +0200 Subject: [PATCH 14/15] Better error message if expression parser fails --- src/storm/parser/ExpressionParser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp index cd3ccd595..519bc2b9f 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm/parser/ExpressionParser.cpp @@ -197,7 +197,7 @@ namespace storm { try { // Start parsing. bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); - STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression."); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'."); STORM_LOG_DEBUG("Parsed expression successfully."); } catch (qi::expectation_failure const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); From 6832fc805c2d1a7ea4f0e9b2b6478a7024ab0deb Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 14 Oct 2017 15:17:38 +0200 Subject: [PATCH 15/15] parser improvements in changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fafa9849..4005ca0e1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,7 @@ Version 1.1.x - storm-pars: support for welldefinedness constraints in mdps. - symbolic (MT/BDD) bisimulation - Fixed issue related to variable names that can not be used in Exprtk. +- DRN parser improved ### Version 1.1.0 (2017/8)