From 8297c51d736ab6083b828d223ca0b8a72314c902 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 16 Jan 2016 17:02:09 +0100 Subject: [PATCH] Fixed a bug that was not yet fixed for some reason... Approximation is now also used if a non-linear function is detected. This is a quick 'solution' to allow functions of the form p times q. Former-commit-id: 2a30959c2141a5bc4d96ec96704335b6236e3239 --- .../region/AbstractSparseRegionModelChecker.cpp | 10 +++++++++- src/modelchecker/region/ApproximationModel.cpp | 2 +- src/modelchecker/region/SamplingModel.cpp | 11 ++++++++++- .../region/SparseDtmcRegionModelChecker.cpp | 1 + .../region/SparseMdpRegionModelChecker.cpp | 3 ++- 5 files changed, 23 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index f6c52095f..a97be5ce4 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -124,6 +124,14 @@ namespace storm { std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now(); this->preprocess(this->simpleModel, this->simpleFormula, isApproximationApplicable, constantResult); std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); + + //TODO: Currently we are not able to detect functions of the form p*q correctly as these functions are not linear but approximation is still applicable. + //This is just a quick fix to work with such models anyway. + if(!this->isApproximationApplicable){ + STORM_LOG_ERROR("There are non-linear functions that occur in the given model. Approximation is still correct for functions that are linear w.r.t. a single parameter (assuming the remaining parameters are constants), e.g., p*q is okay. Currently, the implementation is not able to validate this.."); + this->isApproximationApplicable=true; + } + //Check if the approximation and the sampling model needs to be computed if(!this->isResultConstant()){ if(this->isApproximationApplicable && storm::settings::regionSettings().doApprox()){ @@ -197,7 +205,7 @@ namespace storm { //switches for the different steps. bool done=false; - STORM_LOG_WARN_COND( (!storm::settings::regionSettings().doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions. As this is not the case, approximation is deactivated"); + STORM_LOG_WARN_COND( (!storm::settings::regionSettings().doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated"); bool doApproximation=storm::settings::regionSettings().doApprox() && this->isApproximationApplicable; bool doSampling=storm::settings::regionSettings().doSample(); bool doSmt=storm::settings::regionSettings().doSmt(); diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 5a0ec1316..528391b41 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -145,7 +145,7 @@ namespace storm { } } //Build the matrix. Override the row count (required e.g. when there are only transitions to target for the last matrixrow) - this->matrixData.matrix=matrixBuilder.build(this->matrixData.rowSubstitutions.size()); + this->matrixData.matrix=matrixBuilder.build(curRow); //Now run again through both matrices to get the remaining ingredients of the matrixData and vectorData this->matrixData.assignment.reserve(this->matrixData.matrix.getEntryCount()); diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 58baed2b9..36fd97440 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -78,6 +78,14 @@ namespace storm { formula->getBound(), filter ); + /* std::cout << "occurring functions:" << std::endl; + for(auto const& funcVal : this->functions){ + std::string funcStr = " (" + + funcVal.first.nominator().toString() + ") / (" + + funcVal.first.denominator().toString() + + " )"; + std::cout << funcStr << std::endl; + }*/ } template @@ -123,7 +131,8 @@ namespace storm { ++curRow; } } - this->matrixData.matrix=matrixBuilder.build(); + //Build the matrix. Override the row count (required e.g. when there are only transitions to target for the last matrixrow) + this->matrixData.matrix=matrixBuilder.build(curRow); //Now run again through both matrices to get the remaining ingredients of the matrixData and vectorData. //Note that we need the matrix (I-P) in case of a dtmc. diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 2f224279a..ce2c1e8dd 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -257,6 +257,7 @@ namespace storm { //maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates); maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states. Total number of states is " << maybeStates.size() << "."); // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates().begin()); if (!maybeStates.get(initialState)) { diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index 3653c8e97..ca13a5ae6 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -215,6 +215,7 @@ namespace storm { statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel()->getTransitionMatrix(), this->getModel()->getTransitionMatrix().getRowGroupIndices(), this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates); } maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states. Total number of states is " << maybeStates.size() << "."); // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates().begin()); if (!maybeStates.get(initialState)) { @@ -234,7 +235,7 @@ namespace storm { isResultConstant=false; if(!storm::utility::region::functionIsLinear(entry.getValue())){ isApproximationApplicable=false; - break; + //break; } } }