diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 31ee02620..a22ac10d0 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -986,6 +986,26 @@ namespace storm { } } + template + storm::storage::SparseMatrix SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getSparseMatrix() const { + //first get the number of entries + index_type numEntries=0; + for(index_type rowIndex=0; rowIndexgetNumberOfRows(); ++rowIndex){ + auto const& row=this->getRow(rowIndex); + numEntries += row.size(); + } + //fill the data + storm::storage::SparseMatrixBuilder matrixBuilder(this->getNumberOfRows(), this->getNumberOfRows(),numEntries); + for(index_type rowIndex=0; rowIndexgetNumberOfRows(); ++rowIndex){ + auto const& row=this->getRow(rowIndex); + for(auto const& entry : row){ + matrixBuilder.addNextValue(rowIndex,entry.getColumn(),entry.getValue()); + } + } + return matrixBuilder.build(); + } + + template typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 3601ef46d..8a4eb4789 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -61,6 +61,8 @@ namespace storm { */ bool hasSelfLoop(storm::storage::sparse::state_type state) const; + storm::storage::SparseMatrix getSparseMatrix() const; + private: std::vector data; }; diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 6f91ace69..eb55943b9 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -85,8 +85,39 @@ namespace storm { } return resultingVector; } + + template + std::string SparseDtmcRegionModelChecker::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 + std::string SparseDtmcRegionModelChecker::ParameterRegion::getRegionAsString() const { + std::stringstream regionstringstream; + for(auto var : this->getVariables()){ + regionstringstream << storm::utility::regions::convertNumber::BoundType,double>(this->getLowerBound(var)); + regionstringstream << "<="; + regionstringstream << storm::utility::regions::getVariableName(var); + regionstringstream << "<="; + regionstringstream << storm::utility::regions::convertNumber::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 + void SparseDtmcRegionModelChecker::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(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 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 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() : storm::utility::one(); + } + + // 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 submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + //TODO do we need this? + std::vector 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 + template + bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType value){ + double valueAsDouble = storm::utility::regions::convertNumber(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 diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 412709ab4..7851883f2 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -22,13 +22,30 @@ namespace storm { typedef typename std::conditional<(std::is_same::value), storm::Variable,std::nullptr_t>::type VariableType; typedef typename std::conditional<(std::is_same::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 lowerBounds, std::map upperBounds); + void setCheckResult(RegionCheckResult checkResult) { + this->checkResult = checkResult; + } + + RegionCheckResult getCheckResult() const { + return checkResult; + } + + std::set getVariables() const; BoundType const& getLowerBound(VariableType const& variable) const; BoundType const& getUpperBound(VariableType const& variable) const; @@ -42,6 +59,9 @@ namespace storm { */ std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; + std::string getCheckResultAsString() const; + std::string getRegionAsString() const; + private: std::map const lowerBounds; @@ -52,7 +72,20 @@ namespace storm { explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc 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 parameterRegions); private: + typedef typename storm::modelchecker::SparseDtmcEliminationModelChecker::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 const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, ParameterRegion const& region, storm::logic::ComparisonType const& compTypeOfProperty); #endif - + template + 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 eliminationModelChecker; + // + // A comparator that can be used to compare constants. - storm::utility::ConstantsComparator comparator; + //storm::utility::ConstantsComparator comparator; + + //the following members depend on the currently specified formula + //the currently specified formula + std::unique_ptr probabilityOperatorFormula; + // the propabilities to go to a state with probability 1 in one step + std::vector oneStepProbabilities; + + // The function for the reachability probability in the initial state + ParametricType reachProbFunction; + + // running times }; diff --git a/src/utility/cli.h b/src/utility/cli.h index eef20473c..32defa498 100644 --- a/src/utility/cli.h +++ b/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::getRegionsFromSettings(); - storm::modelchecker::SparseDtmcRegionModelChecker 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 result; diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index cfe5afa73..c99cb7919 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -126,11 +126,17 @@ namespace storm { return cln::double_approx(number); } + template<> + double convertNumber(double const& number, bool const& roundDown, double const& precision){ + return number; + } + template 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(std::string variableString){ storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString); @@ -140,7 +146,17 @@ namespace storm { template 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 variable){ + return carl::VariablePool::getInstance().getName(variable); + } + + template + 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 const& number, bool const& roundDown, double const& precision); template storm::RationalFunction::CoeffType convertNumber(double const& number, bool const& roundDown, double const& precision); template double convertNumber(storm::RationalFunction::CoeffType const& number, bool const& roundDown, double const& precision); + template double convertNumber(double const& number, bool const& roundDown, double const& precision); template storm::Variable getVariableFromString(std::string variableString); + template std::string getVariableName(storm::Variable variable); #endif } } diff --git a/src/utility/regions.h b/src/utility/regions.h index 0ec0ab383..f32ce62b3 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -91,6 +91,12 @@ namespace storm { */ template VariableType getVariableFromString(std::string variableString); + + /* + * retrieves the variable name from the given variable + */ + template + std::string getVariableName(VariableType variable); } } }