From a410b6d7bc26235a886fde3f46b14cd9658b3f2d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 19 Mar 2019 14:45:30 +0100 Subject: [PATCH] Heuristic is argument for functions in approximation algorithm --- src/storm-dft-cli/storm-dft.cpp | 2 +- src/storm-dft/api/storm-dft.h | 5 +- .../builder/ExplicitDFTModelBuilder.cpp | 4 +- .../builder/ExplicitDFTModelBuilder.h | 7 ++- .../modelchecker/dft/DFTModelChecker.cpp | 16 +++--- .../modelchecker/dft/DFTModelChecker.h | 56 ++++++++++--------- 6 files changed, 46 insertions(+), 44 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f6a7d3863..eb4b1b837 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -126,7 +126,7 @@ void processOptions() { if (faultTreeSettings.isApproximationErrorSet()) { // Approximate analysis storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), - faultTreeSettings.getApproximationError(), true); + faultTreeSettings.getApproximationError(), faultTreeSettings.getApproximationHeuristic(), true); } else { storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 8b4f0ae9c..e960fb69c 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -101,10 +101,9 @@ namespace storm { template typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, - bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { + bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool printOutput) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); - typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, - approximationError); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 922f680e9..298936440 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -56,7 +56,6 @@ namespace storm { dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), - usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(dft.stateBitVectorSize()), @@ -120,8 +119,9 @@ namespace storm { } template - void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { + void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) { STORM_LOG_TRACE("Generating DFT state space"); + usedHeuristic = approximationHeuristic; if (iteration < 1) { // Initialize diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index 9858000ec..379918f9b 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -181,11 +181,12 @@ namespace storm { /*! * Build model from DFT. * - * @param labelOpts Options for labeling. - * @param iteration Current number of iteration. + * @param labelOpts Options for labeling. + * @param iteration Current number of iteration. * @param approximationThreshold Threshold determining when to skip exploring states. + * @param approximationHeuristic Heuristic used for exploring states. */ - void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0); + void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Get the built model. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index d96aacfc4..467125c35 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -17,7 +17,7 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results 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, storm::builder::ApproximationHeuristic approximationHeuristic) { // Initialize this->approximationError = approximationError; totalTimer.start(); @@ -30,21 +30,21 @@ namespace storm { // Checking DFT if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time - std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError); + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC); // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { checkResults.push_back(result); } } else { - checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError); + checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic); } totalTimer.stop(); return checkResults; } template - typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -138,12 +138,12 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, enableDC, approximationError); + return checkDFT(dft, properties, symred, enableDC, approximationError, approximationHeuristic); } } template - std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC) { // TODO Matthias: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; @@ -258,7 +258,7 @@ namespace storm { } template - typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { explorationTimer.start(); // Find symmetries @@ -297,7 +297,7 @@ namespace storm { } STORM_LOG_DEBUG("Building model..."); // TODO Matthias refine model using existing model and MC results - builder.buildModel(labeloptions, iteration, approximationError); + builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic); explorationTimer.stop(); buildingTimer.start(); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index cf05cbb8f..56d1b4fad 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -31,16 +31,17 @@ namespace storm { /*! * Main method for checking DFTs. * - * @param origDft Original DFT - * @param properties Properties to check for - * @param symred Flag indicating if symmetry reduction should be used - * @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 + * @param origDft Original DFT. + * @param properties Properties to check for. + * @param symred Flag indicating if symmetry reduction should be used. + * @param allowModularisation Flag indicating if modularisation is allowed. + * @param enableDC Flag indicating if Don't Care propagation should be used. + * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. + * @param approximationHeuristic Heuristic used for approximation. * * @return Model checking results for the given properties. */ - 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); + 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, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Print timings of all operations to stream. @@ -76,43 +77,44 @@ namespace storm { /*! * Internal helper for model checking a DFT. * - * @param dft DFT - * @param properties Properties to check for - * @param symred Flag indicating if symmetry reduction should be used - * @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 + * @param dft DFT. + * @param properties Properties to check for. + * @param symred Flag indicating if symmetry reduction should be used. + * @param allowModularisation Flag indicating if modularisation is allowed. + * @param enableDC Flag indicating if Don't Caree propagation should be used. + * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. + * @param approximationHeuristic Heuristic used for approximation. * * @return Model checking results (or in case of approximation two results for lower and upper bound) */ - dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Internal helper for building a CTMC from a DFT via parallel composition. * - * @param dft DFT - * @param properties Properties to check for - * @param symred Flag indicating if symmetry reduction should be used - * @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 + * @param dft DFT. + * @param properties Properties to check for. + * @param symred Flag indicating if symmetry reduction should be used. + * @param allowModularisation Flag indicating if modularisation is allowed. + * @param enableDC Flag indicating if Don't Care propagation should be used. * * @return CTMC representing the DFT */ - std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC); /*! * Check model generated from DFT. * - * @param dft The DFT - * @param properties Properties to check for - * @param symred Flag indicating if symmetry reduction should be used - * @param enableDC Flag indicating if dont care propagation should be used - * @param approximationError Error allowed for approximation. Value 0 indicates no approximation + * @param dft The DFT. + * @param properties Properties to check for. + * @param symred Flag indicating if symmetry reduction should be used. + * @param enableDC Flag indicating if Don't Care propagation should be used. + * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. + * @param approximationHeuristic Heuristic used for approximation. * * @return Model checking result */ - dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Check the given markov model for the given properties.