From a2c484bba43de66721bd575ad98002eef7fabf0b Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 21:43:02 +0200 Subject: [PATCH] Support for probability approximation without modularisation Former-commit-id: 921c8d310c9eab5b82300c908d3f039e9451500a --- src/modelchecker/dft/DFTModelChecker.cpp | 18 ++++++++++++------ src/modelchecker/dft/DFTModelChecker.h | 6 ++++-- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index ff2148982..e49db7a37 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -158,6 +158,8 @@ namespace storm { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + bool probabilityFormula = formula->isProbabilityOperatorFormula(); + STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -170,7 +172,7 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); - model = builder.getModelApproximation(true); + model = builder.getModelApproximation(probabilityFormula ? false : true); // We only output the info from the lower bound as the info for the upper bound is the same STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); @@ -185,7 +187,7 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); explorationStart = std::chrono::high_resolution_clock::now(); - model = builder.getModelApproximation(false); + model = builder.getModelApproximation(probabilityFormula ? true : false); explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; // Check upper bound result = checkModel(model, formula); @@ -197,7 +199,7 @@ namespace storm { ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); - } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError)); + } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); return approxResult; @@ -251,14 +253,18 @@ namespace storm { } template - bool DFTModelChecker::isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError) { + bool DFTModelChecker::isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); } template<> - bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError) { + bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError, bool relative) { STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); - return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; + if (relative) { + return upperBound - lowerBound <= approximationError; + } else { + return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; + } } template diff --git a/src/modelchecker/dft/DFTModelChecker.h b/src/modelchecker/dft/DFTModelChecker.h index 83df59bfa..b351ab67b 100644 --- a/src/modelchecker/dft/DFTModelChecker.h +++ b/src/modelchecker/dft/DFTModelChecker.h @@ -107,15 +107,17 @@ namespace storm { /*! * Checks if the computed approximation is sufficient, i.e. - * upperBound - lowerBound <= approximationError * mean(upperBound, lowerBound). + * upperBound - lowerBound <= approximationError * mean(lowerBound, upperBound). * * @param lowerBound The lower bound on the result. * @param upperBound The upper bound on the result. * @param approximationError The allowed error for approximating. + * @param relative Flag indicating if the error should be relative to 1 or + to the mean of lower and upper bound. * * @return True, if the approximation is sufficient. */ - bool isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError); + bool isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative); }; }