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: 2a30959c21

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();

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());

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<typename ParametricSparseModelType, typename ConstantType>
@@ -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.

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<storm::storage::BitVector, storm::storage::BitVector> 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)) {

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;
                             }
                         }
                     }