a few steps to efficiently analyze multiple regions...

Former-commit-id: ed0b19f77c

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -986,6 +986,26 @@ namespace storm {
             }
         }        
         
+        template<typename ValueType>
+        storm::storage::SparseMatrix<ValueType> SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getSparseMatrix() const {
+            //first get the number of entries
+            index_type numEntries=0;
+            for(index_type rowIndex=0; rowIndex<this->getNumberOfRows(); ++rowIndex){
+                auto const& row=this->getRow(rowIndex);
+                numEntries += row.size();
+            }
+            //fill the data
+            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(this->getNumberOfRows(), this->getNumberOfRows(),numEntries);
+            for(index_type rowIndex=0; rowIndex<this->getNumberOfRows(); ++rowIndex){
+                auto const& row=this->getRow(rowIndex);
+                for(auto const& entry : row){
+                    matrixBuilder.addNextValue(rowIndex,entry.getColumn(),entry.getValue());
+                }
+            }
+            return matrixBuilder.build();
+        }
+
+        
         template<typename ValueType>
         typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix SparseDtmcEliminationModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
             FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -61,6 +61,8 @@ namespace storm {
                  */
                 bool hasSelfLoop(storm::storage::sparse::state_type state) const;
                 
+                storm::storage::SparseMatrix<ValueType> getSparseMatrix() const;
+                
             private:
                 std::vector<row_type> data;
             };

src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp

@@ -85,8 +85,39 @@ namespace storm {
             }
             return resultingVector;
         }
+
+        template<typename ParametricType, typename ConstantType>
+        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getCheckResultAsString() const {
+            switch (this->checkResult) {
+                case RegionCheckResult::UNKNOWN:
+                    return "unknown";
+                case RegionCheckResult::ALLSAT:
+                    return "allSat";
+                case RegionCheckResult::ALLUNSAT:
+                    return "allUnsat";
+                case RegionCheckResult::INCONCLUSIVE:
+                    return "Inconclusive";
+            }
+            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not identify check result")
+            return "ERROR";
+        }
             
-        
+        template<typename ParametricType, typename ConstantType>
+        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getRegionAsString() const {
+            std::stringstream regionstringstream;
+            for(auto var : this->getVariables()){
+                regionstringstream << storm::utility::regions::convertNumber<SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType,double>(this->getLowerBound(var));
+                regionstringstream << "<=";
+                regionstringstream << storm::utility::regions::getVariableName(var);
+                regionstringstream << "<=";
+                regionstringstream << storm::utility::regions::convertNumber<SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType,double>(this->getUpperBound(var));
+                regionstringstream << ",";
+            }
+            std::string regionstring = regionstringstream.str();
+            //the last comma should actually be a semicolon
+            regionstring = regionstring.substr(0,regionstring.length()-1) + ";";
+            return regionstring;
+        }
                 
         
         
@@ -115,10 +146,68 @@ namespace storm {
                 STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected an eventually subformula");
                 return false;
             }
+            if(model.getInitialStates().getNumberOfSetBits() != 1){
+                STORM_LOG_DEBUG("Input model is required to have exactly one initial state.");
+                return false;
+            }
             return true;
         }
             
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::specifyFormula(storm::logic::Formula const& formula) {
+            std::chrono::high_resolution_clock::time_point timeStart = std::chrono::high_resolution_clock::now();
+            STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::IllegalArgumentException, "Tried to specify a formula that can not be handled.");
             
+            //Get subformula, initial state, target states
+            //Note: canHandle already ensures that the formula has the right shape and that the model has a single initial state.
+            this->probabilityOperatorFormula= std::unique_ptr<storm::logic::ProbabilityOperatorFormula>(new storm::logic::ProbabilityOperatorFormula(formula.asStateFormula().asProbabilityOperatorFormula()));
+            storm::logic::EventuallyFormula const& eventuallyFormula = this->probabilityOperatorFormula->getSubformula().asPathFormula().asEventuallyFormula();
+            storm::storage::sparse::state_type initialState = *model.getInitialStates().begin();
+            std::unique_ptr<CheckResult> targetStatesResultPtr = this->eliminationModelChecker.check(eventuallyFormula.getSubformula());
+            storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector();
+
+            // Then, compute the subset of states that has a probability of 0 or 1, respectively.
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates);
+            storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
+            storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
+            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            
+            // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction.
+            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
+                STORM_LOG_DEBUG("The probability of the initial state is constant (0 or 1)");
+                this->reachProbFunction = statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>();
+            }
+            
+            // Determine the set of states that is reachable from the initial state without jumping over a target state.
+            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1);
+            // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
+            maybeStates &= reachableStates;
+            // Create a vector for the probabilities to go to a state with probability 1 in one step.
+            this->oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
+            // Determine the set of initial states of the sub-model.
+            storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
+            // We then build the submatrix that only has the transitions of the maybe states.
+            storm::storage::SparseMatrix<ParametricType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
+            storm::storage::SparseMatrix<ParametricType> submatrixTransposed = submatrix.transpose();
+            
+  //TODO do we need this? 
+            std::vector<std::size_t> statePriorities = this->eliminationModelChecker.getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
+            
+            // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
+            FlexibleMatrix flexibleMatrix = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix);
+            FlexibleMatrix flexibleBackwardTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrixTransposed, true);
+            
+           // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated.
+            storm::storage::BitVector subsystem = storm::storage::BitVector(submatrix.getRowCount(), true);
+            eliminateStates(subsystem, flexibleMatrix, oneStepProbabilities, flexibleBackwardTransitions, newInitialStates, submatrix, statePriorities);
+            
+            
+    //        std::chrono::high_resolution_clock::time_point timeStateElemEnd = std::chrono::high_resolution_clock::now();
+            
+            
+            std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
+        }
+           
             
             
         
@@ -575,6 +664,24 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type");
         }
         
+        template<typename ParametricType, typename ConstantType>
+        template<typename ValueType>
+        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::valueIsInBoundOfFormula(ValueType value){
+            double valueAsDouble = storm::utility::regions::convertNumber<ValueType, double>(value);
+            switch (this->probabilityOperatorFormula->getComparisonType()) {
+                case storm::logic::ComparisonType::Greater:
+                    return (valueAsDouble > this->probabilityOperatorFormula->getBound());
+                case storm::logic::ComparisonType::GreaterEqual:
+                    return (valueAsDouble >= this->probabilityOperatorFormula->getBound());
+                case storm::logic::ComparisonType::Less:
+                    return (valueAsDouble < this->probabilityOperatorFormula->getBound());
+                case storm::logic::ComparisonType::LessEqual:
+                    return (valueAsDouble <= this->probabilityOperatorFormula->getBound());
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+            }
+        }
+        
 #endif
         
 #ifdef STORM_HAVE_CARL

src/modelchecker/reachability/SparseDtmcRegionModelChecker.h

@@ -22,13 +22,30 @@ namespace storm {
             typedef typename std::conditional<(std::is_same<ParametricType,storm::RationalFunction>::value), storm::Variable,std::nullptr_t>::type VariableType;
             typedef typename std::conditional<(std::is_same<ParametricType,storm::RationalFunction>::value), storm::RationalFunction::CoeffType,std::nullptr_t>::type BoundType;
             
-            enum class RegionCheckResult { UNKNOWN, ALLSAT, ALLUNSAT, INCONCLUSIVE};
+            /*!
+             * The possible results for a single region
+             */
+            enum class RegionCheckResult { 
+                UNKNOWN, /*!< the result is unknown */
+                ALLSAT, /*!< the formula is satisfied for all parameters in the given region */
+                ALLUNSAT, /*!< the formula is violated for all parameters in the given region */
+                INCONCLUSIVE /*!< the formula is satisfied for some parameters but also violated for others */
+            };
             
             class ParameterRegion{
             public:
-                
+
                 ParameterRegion(std::map<VariableType, BoundType> lowerBounds, std::map<VariableType, BoundType> upperBounds);
                 
+                void setCheckResult(RegionCheckResult checkResult) {
+                    this->checkResult = checkResult;
+                }
+
+                RegionCheckResult getCheckResult() const {
+                    return checkResult;
+                }
+                
+                
                 std::set<VariableType> getVariables() const;
                 BoundType const& getLowerBound(VariableType const& variable) const;
                 BoundType const& getUpperBound(VariableType const& variable) const;
@@ -42,6 +59,9 @@ namespace storm {
                  */
                 std::vector<std::map<VariableType, BoundType>> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
                 
+                std::string getCheckResultAsString() const;
+                std::string getRegionAsString() const;
+                
             private:
                 
                 std::map<VariableType, BoundType> const lowerBounds;
@@ -52,7 +72,20 @@ namespace storm {
             
             explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model);
 
-            virtual bool canHandle(storm::logic::Formula const& formula) const;
+            /*!
+             * Checks if the given formula can be handled by this
+             * @param formula the formula to be checked
+             */
+            bool canHandle(storm::logic::Formula const& formula) const;
+            
+            /*!
+             * Specifies the considered formula.
+             * A few preprocessing steps are performed.
+             * If another formula has been specified before, all 'context' regarding the old formula is lost.
+             * 
+             * @param formula the formula to be considered.
+             */
+            void specifyFormula(storm::logic::Formula const& formula);
 
             /*!
              * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions
@@ -60,9 +93,18 @@ namespace storm {
              */
             bool checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
         private:
+            
             typedef typename storm::modelchecker::SparseDtmcEliminationModelChecker<ParametricType>::FlexibleSparseMatrix FlexibleMatrix;
             
-                            #ifdef STORM_HAVE_CARL
+            /*!
+             * Represents the current state of this
+             */
+           // enum class RegionCheckerState{
+         //       NOFORMULA, /*!< there is no formula */
+         //       INITIALIZED, /*!< a formula has been specified. Ready to get regions*/
+        //    };
+            
+   #ifdef STORM_HAVE_CARL
                 /*!
                  * Instantiates the matrix, i.e., evaluate the occurring functions according to the given substitutions of the variables.
                  * One row of the given flexible matrix will be one rowgroup in the returned matrix, consisting of one row for every substitution.
@@ -92,7 +134,8 @@ namespace storm {
             
             void restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector<storm::RationalFunction::PolyType> const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector<storm::RationalFunction> const& oneStepProbabilities, ParameterRegion const& region, storm::logic::ComparisonType const& compTypeOfProperty);
 #endif         
-                
+            template <typename ValueType>
+            bool valueIsInBoundOfFormula(ValueType value);
             
             
             // The model this model checker is supposed to analyze.
@@ -101,8 +144,21 @@ namespace storm {
             // Instance of an elimination model checker to access its functions
             storm::modelchecker::SparseDtmcEliminationModelChecker<ParametricType> eliminationModelChecker;
             
+            // 
+            
             // A comparator that can be used to compare constants.
-            storm::utility::ConstantsComparator<ParametricType> comparator;
+            //storm::utility::ConstantsComparator<ParametricType> comparator;
+            
+            //the following members depend on the currently specified formula
+            //the currently specified formula
+            std::unique_ptr<storm::logic::ProbabilityOperatorFormula> probabilityOperatorFormula;
+            // the propabilities to go to a state with probability 1 in one step
+            std::vector<ParametricType> oneStepProbabilities;
+            
+            // The  function for the reachability probability in the initial state 
+            ParametricType reachProbFunction;
+            
+            // running times
             
         };
         

src/utility/cli.h

@@ -477,17 +477,18 @@ namespace storm {
                     std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl;
                     
                     auto regions=storm::utility::regions::RegionParser<storm::RationalFunction, double>::getRegionsFromSettings();                    
-                    
                     storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
                     auto result = modelchecker.checkRegion(*formula.get(), regions);
                     std::cout << "... done." << std::endl;
-                    if (result){
-                    std::cout << "the property holds for all parameters in the given region" << std::endl;
-                    }else{
-                    std::cout << "the property does NOT hold for all parameters in the given region" << std::endl;
+                    if (!result){
+                        std::cout << "The result of one or more regions is still unknown." << std::endl;    
+                    }
+                    for(auto const& reg : regions){
+                        std::cout << reg.getRegionAsString() << "      Result: " << reg.getCheckResultAsString() << std::endl;
                     }
                     
-                }else{
+                }
+                else{
                     // obtain the resulting rational function
                     std::cout << std::endl << "Model checking property: " << *formula << " ...";
                     std::unique_ptr<storm::modelchecker::CheckResult> result;

src/utility/regions.cpp

@@ -126,11 +126,17 @@ namespace storm {
                 return cln::double_approx(number);
             }
             
+            template<>
+            double convertNumber<double, double>(double const& number, bool const& roundDown, double const& precision){
+                return number;
+            }
+            
             template<typename SourceType, typename TargetType>
             TargetType convertNumber(SourceType const& number, bool const& roundDown, double const& precision){
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "number conversion between the given types not implemented");
             }
             
+            
             template<>
             storm::Variable getVariableFromString<storm::Variable>(std::string variableString){
                 storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString);
@@ -140,7 +146,17 @@ namespace storm {
             
             template<typename VariableType>
             VariableType getVariableFromString(std::string variableString){
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Variable from String not implemented for this Type");
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Variable from String not implemented for this type");
+            }
+            
+            template<>
+            std::string getVariableName<storm::Variable>(storm::Variable variable){
+                return carl::VariablePool::getInstance().getName(variable);
+            }
+            
+            template<typename VariableType>
+            std::string getVariableName(VariableType variable){
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "VariableName from Variable not implemented for this type");
             }
             
             //explicit instantiations
@@ -150,8 +166,10 @@ namespace storm {
        template storm::RationalFunction convertNumber<double, storm::RationalFunction>(double const& number, bool const& roundDown, double const& precision);
        template storm::RationalFunction::CoeffType convertNumber<double, storm::RationalFunction::CoeffType>(double const& number, bool const& roundDown, double const& precision);
        template double convertNumber<cln::cl_RA, double>(storm::RationalFunction::CoeffType const& number, bool const& roundDown, double const& precision);
+       template double convertNumber<double, double>(double const& number, bool const& roundDown, double const& precision);
        
        template storm::Variable getVariableFromString<storm::Variable>(std::string variableString);
+       template std::string getVariableName<storm::Variable>(storm::Variable variable);
 #endif 
         }
     }

src/utility/regions.h

@@ -91,6 +91,12 @@ namespace storm {
              */
             template<typename VariableType>
             VariableType getVariableFromString(std::string variableString);
+            
+            /*
+             * retrieves the variable name  from the given variable
+             */
+            template<typename VariableType>
+            std::string getVariableName(VariableType variable);
         }
     }
 }