From 6821d3c76c4a4ca672161ba5c5ccbd72bbc6dcaa Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 16 Mar 2018 18:06:05 +0100 Subject: [PATCH] Different function for exact and approximate DFT analysis --- src/storm-dft-cli/storm-dft.cpp | 13 ++++---- src/storm-dft/api/storm-dft.h | 30 +++++++++++++++++-- .../modelchecker/dft/DFTModelChecker.cpp | 4 +-- .../modelchecker/dft/DFTModelChecker.h | 7 +++-- 4 files changed, 39 insertions(+), 15 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 2d2e24b8e..f051570dc 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -95,12 +95,6 @@ void processOptions() { } } - // Set possible approximation error - double approximationError = 0.0; - if (faultTreeSettings.isApproximationErrorSet()) { - approximationError = faultTreeSettings.getApproximationError(); - } - // Build properties STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given."); std::string propString = properties[0]; @@ -111,7 +105,12 @@ void processOptions() { STORM_LOG_ASSERT(props.size() > 0, "No properties found."); // Carry out the actual analysis - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); + if (faultTreeSettings.isApproximationErrorSet()) { + // Approximate analysis + storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError()); + } else { + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC()); + } } /*! diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index fc88fe792..30b06a1e8 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -50,14 +50,38 @@ namespace storm { * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param enableDC Flag whether Don't Care propagation should be used. - * @param approximationError Allowed approximation error, 0 indicates no approximation. + * + * @return Result. + */ + template + typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC) { + storm::modelchecker::DFTModelChecker modelChecker; + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); + modelChecker.printTimings(); + modelChecker.printResults(); + return results; + } + + /*! + * Approximate the analysis result of the given DFT according to the given properties. + * First the Markov model is built from the DFT and then this model is checked against the given properties. + * + * @param dft DFT. + * @param properties PCTL formulas capturing the properties to check. + * @param symred Flag whether symmetry reduction should be used. + * @param allowModularisation Flag whether modularisation should be applied if possible. + * @param enableDC Flag whether Don't Care propagation should be used. + * @param approximationError Allowed approximation error. + * + * @return Result. */ template - void analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); modelChecker.printTimings(); modelChecker.printResults(); + return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index d2b435c1c..c3e7996c7 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -14,7 +14,7 @@ namespace storm { namespace modelchecker { template - void DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize this->approximationError = approximationError; totalTimer.start(); @@ -33,11 +33,11 @@ namespace storm { for (ValueType result : resultsValue) { checkResults.push_back(result); } - } else { checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError); } totalTimer.stop(); + return checkResults; } template diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 597feb3cb..6da5d5aaa 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -17,12 +17,11 @@ namespace storm { template class DFTModelChecker { + public: typedef std::pair approximation_result; typedef std::vector> dft_results; typedef std::vector> property_vector; - public: - /*! * Constructor. */ @@ -38,8 +37,10 @@ namespace storm { * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation + * + * @return Model checking results for the given properties. */ - void check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); + dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); /*! * Print timings of all operations to stream.