diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 3a4e51999..2e2dbbef3 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -27,27 +27,35 @@ namespace storm { template - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { - //todo: check whether both mappings map the same variables + SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { + //check whether both mappings map the same variables and precompute the set of variables + for(auto const& variableWithBound : lowerBounds) { + STORM_LOG_THROW((upperBounds.find(variableWithBound.first)!=upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithBound.first); + this->variables.insert(variableWithBound.first); + } + for(auto const& variableWithBound : upperBounds){ + STORM_LOG_THROW((this->variables.find(variableWithBound.first)!=this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower bound specified for Variable " << variableWithBound.first); + } + } template - void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { + void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { this->violatedPoint = violatedPoint; } template - std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { return violatedPoint; } template - void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { + void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { this->satPoint = satPoint; } template - std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { return satPoint; } @@ -75,42 +83,38 @@ namespace storm { template std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const{ - std::set result; - for(auto const& variableWithBound : lowerBounds) { - result.insert(variableWithBound.first); - } - return result; + return this->variables; } template - typename SparseDtmcRegionModelChecker::BoundType const& SparseDtmcRegionModelChecker::ParameterRegion::getLowerBound(VariableType const& variable) const{ + typename SparseDtmcRegionModelChecker::CoefficientType const& SparseDtmcRegionModelChecker::ParameterRegion::getLowerBound(VariableType const& variable) const{ auto const& result = lowerBounds.find(variable); STORM_LOG_THROW(result!=lowerBounds.end(), storm::exceptions::IllegalArgumentException, "tried to find a lower bound of a variable that is not specified by this region"); return (*result).second; } template - typename SparseDtmcRegionModelChecker::BoundType const& SparseDtmcRegionModelChecker::ParameterRegion::getUpperBound(VariableType const& variable) const{ + typename SparseDtmcRegionModelChecker::CoefficientType const& SparseDtmcRegionModelChecker::ParameterRegion::getUpperBound(VariableType const& variable) const{ auto const& result = upperBounds.find(variable); STORM_LOG_THROW(result!=upperBounds.end(), storm::exceptions::IllegalArgumentException, "tried to find an upper bound of a variable that is not specified by this region"); return (*result).second; } template - const std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getUpperBounds() const { + const std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getUpperBounds() const { return upperBounds; } template - const std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getLowerBounds() const { + const std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getLowerBounds() const { return lowerBounds; } template - std::vector::VariableType, typename SparseDtmcRegionModelChecker::BoundType>> SparseDtmcRegionModelChecker::ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const{ + std::vector::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType>> SparseDtmcRegionModelChecker::ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const{ std::size_t const numOfVariables=consideredVariables.size(); std::size_t const numOfVertices=std::pow(2,numOfVariables); - std::vector> resultingVector(numOfVertices,std::map()); + std::vector> resultingVector(numOfVertices,std::map()); if(numOfVertices==1){ //no variables are given, the returned vector should still contain an empty map return resultingVector; @@ -123,10 +127,10 @@ namespace storm { std::size_t variableIndex=0; for(auto const& variable : consideredVariables){ if( (vertexId>>variableIndex)%2==0 ){ - resultingVector[vertexId].insert(std::pair(variable, getLowerBound(variable))); + resultingVector[vertexId].insert(std::pair(variable, getLowerBound(variable))); } else{ - resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); + resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); } ++variableIndex; } @@ -158,11 +162,11 @@ namespace storm { std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { std::stringstream regionstringstream; for(auto var : this->getVariables()){ - regionstringstream << storm::utility::regions::convertNumber::BoundType,double>(this->getLowerBound(var)); + regionstringstream << storm::utility::regions::convertNumber::CoefficientType,double>(this->getLowerBound(var)); regionstringstream << "<="; regionstringstream << storm::utility::regions::getVariableName(var); regionstringstream << "<="; - regionstringstream << storm::utility::regions::convertNumber::BoundType,double>(this->getUpperBound(var)); + regionstringstream << storm::utility::regions::convertNumber::CoefficientType,double>(this->getUpperBound(var)); regionstringstream << ","; } std::string regionstring = regionstringstream.str(); @@ -364,7 +368,7 @@ namespace storm { storm::storage::sparse::state_type currentMdpRow=0; //go through rows: for(storm::storage::sparse::state_type oldStateIndex : subsys){ - ParametricType valueToSinkState=storm::utility::regions::getNewFunction(storm::utility::one()); + ParametricType valueToSinkState=storm::utility::regions::getNewFunction(storm::utility::one()); // the dtmc and the mdp rows need to sum up to one, therefore the first entry that we add has value one. ConstantType dummyEntry=storm::utility::one(); // store the columns and values that we have added because we need the same information for the next rows in the mdp @@ -760,7 +764,7 @@ namespace storm { } template - bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { + bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { // check whether the property is satisfied or not at the given point bool valueInBoundOfFormula; if(viaReachProbFunction){ @@ -769,7 +773,7 @@ namespace storm { else{ //put the values into the dtmc matrix for( std::pair&>& mappingPair : this->sampleDtmcMapping){ - mappingPair.second.setValue(storm::utility::regions::convertNumber( + mappingPair.second.setValue(storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(mappingPair.first, point) ) ); @@ -782,7 +786,7 @@ namespace storm { //Delete from here // ConstantType result=resultPtr->asExplicitQuantitativeCheckResult().getValueVector()[*this->sampleDtmc->getInitialStates().begin()]; - // ConstantType otherresult=storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(this->reachProbFunction, point)); + // ConstantType otherresult=storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(this->reachProbFunction, point)); // STORM_LOG_THROW((std::abs(result - otherresult) <= 0.01),storm::exceptions::UnexpectedException, "The results of new DTMC algorithm does not match: " << result << " vs. " << otherresult); //To here @@ -927,7 +931,7 @@ namespace storm { template void SparseDtmcRegionModelChecker::buildMdpForApproximation(const ParameterRegion& region) { //instantiate the substitutions for the given region - std::vector> substitutions(this->approxMdpSubstitutions.size()); + std::vector> substitutions(this->approxMdpSubstitutions.size()); for(uint_fast64_t substitutionIndex=0; substitutionIndexapproxMdpSubstitutions.size(); ++substitutionIndex){ for(std::pair const& sub : this->approxMdpSubstitutions[substitutionIndex]){ switch(sub.second){ @@ -945,7 +949,7 @@ namespace storm { //now put the values into the mdp matrix for( std::tuple&, size_t>& mappingTriple : this->approxMdpMapping){ - std::get<1>(mappingTriple).setValue(storm::utility::regions::convertNumber( + std::get<1>(mappingTriple).setValue(storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(std::get<0>(mappingTriple),substitutions[std::get<2>(mappingTriple)]) ) ); @@ -1008,7 +1012,7 @@ namespace storm { selfloopIndex=numStates; // --> selfloop will never be inserted again } for(auto const& entry : this->sparseTransitions.getRow(oldStateIndex)){ - ConstantType value = storm::utility::regions::convertNumber( + ConstantType value = storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(entry.getValue(),substitutions[substitutionIndex]) ); missingProbability-=value; @@ -1022,7 +1026,7 @@ namespace storm { } if(!this->parametricTypeComparator.isZero(this->oneStepProbabilities[oldStateIndex])){ //transition to target state - ConstantType value = storm::utility::regions::convertNumber( + ConstantType value = storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(this->oneStepProbabilities[oldStateIndex],substitutions[substitutionIndex]) ); missingProbability-=value; @@ -1716,7 +1720,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseDtmcRegionModelChecker; #endif - //note: for other template instantiations, add a rule for the typedefs of VariableType and BoundType + //note: for other template instantiations, add a rule for the typedefs of VariableType and CoefficientType } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 5f2de241a..c3fcedfee 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -20,7 +20,7 @@ namespace storm { //The type of variables and bounds depends on the template arguments typedef typename std::conditional<(std::is_same::value), storm::Variable,std::nullptr_t>::type VariableType; - typedef typename std::conditional<(std::is_same::value), storm::Coefficient,std::nullptr_t>::type BoundType; + typedef typename std::conditional<(std::is_same::value), storm::Coefficient,std::nullptr_t>::type CoefficientType; /*! * The possible results for a single region @@ -37,15 +37,15 @@ namespace storm { class ParameterRegion{ public: - ParameterRegion(std::map lowerBounds, std::map upperBounds); + ParameterRegion(std::map lowerBounds, std::map upperBounds); std::set getVariables() const; - BoundType const& getLowerBound(VariableType const& variable) const; - BoundType const& getUpperBound(VariableType const& variable) const; - const std::map getUpperBounds() const; - const std::map getLowerBounds() const; + CoefficientType const& getLowerBound(VariableType const& variable) const; + CoefficientType const& getUpperBound(VariableType const& variable) const; + const std::map getUpperBounds() const; + const std::map getLowerBounds() const; /* * Returns a vector of all possible combinations of lower and upper bounds of the given variables. @@ -56,7 +56,7 @@ namespace storm { * * If the given set of variables is empty, the returned vector will contain an empty map */ - std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; + std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; //returns the currently set check result as a string std::string checkResultToString() const; @@ -70,33 +70,34 @@ namespace storm { /*! * Sets a point in the region for which the considered property is not satisfied. */ - void setViolatedPoint(std::map const& violatedPoint); + void setViolatedPoint(std::map const& violatedPoint); /*! * Retrieves a point in the region for which is considered property is not satisfied. * If such a point is not known, the returned map is empty. */ - std::map getViolatedPoint() const; + std::map getViolatedPoint() const; /*! * Sets a point in the region for which the considered property is satisfied. */ - void setSatPoint(std::map const& satPoint); + void setSatPoint(std::map const& satPoint); /*! * Retrieves a point in the region for which is considered property is satisfied. * If such a point is not known, the returned map is empty. */ - std::map getSatPoint() const; + std::map getSatPoint() const; private: - std::map const lowerBounds; - std::map const upperBounds; + std::map const lowerBounds; + std::map const upperBounds; + std::set variables; RegionCheckResult checkResult; - std::map satPoint; - std::map violatedPoint; + std::map satPoint; + std::map violatedPoint; }; @@ -281,7 +282,7 @@ namespace storm { * * @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH */ - bool checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction=false); + bool checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction=false); /*! * Builds an MDP that is used to compute bounds on the maximal/minimal reachability probability, diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index 14215b0d0..14d261de9 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -20,8 +20,8 @@ namespace storm { template void RegionParser::parseParameterBounds( - std::map& lowerBounds, - std::map& upperBounds, + std::map& lowerBounds, + std::map& upperBounds, std::string const& parameterBoundsString, double const precision){ double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); @@ -46,10 +46,10 @@ namespace storm { } VariableType var = getVariableFromString(parameter); - BoundType lb = convertNumber(lowerBound, true, actualPrecision); - STORM_LOG_WARN_COND((lowerBound==convertNumber(lb, true, actualPrecision)), "The lower bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); - BoundType ub = convertNumber(upperBound, false, actualPrecision); - STORM_LOG_WARN_COND((upperBound==convertNumber(ub, true, actualPrecision)), "The upper bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); + CoefficientType lb = convertNumber(lowerBound, true, actualPrecision); + STORM_LOG_WARN_COND((lowerBound==convertNumber(lb, true, actualPrecision)), "The lower bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); + CoefficientType ub = convertNumber(upperBound, false, actualPrecision); + STORM_LOG_WARN_COND((upperBound==convertNumber(ub, true, actualPrecision)), "The upper bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); lowerBounds.emplace(std::make_pair(var, lb)); upperBounds.emplace(std::make_pair(var, ub)); // std::cout << "parsed bounds " << parameterBoundsString << ": lb=" << lowerBound << " ub=" << upperBound << " param='" << parameter << "' precision=" << actualPrecision << std::endl; @@ -58,8 +58,8 @@ namespace storm { template typename RegionParser::ParameterRegion RegionParser::parseRegion(std::string const& regionString, double precision){ double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); - std::map lowerBounds; - std::map upperBounds; + std::map lowerBounds; + std::map upperBounds; std::vector parameterBounds; boost::split(parameterBounds, regionString, boost::is_any_of(",")); for(auto const& parameterBound : parameterBounds){ @@ -177,10 +177,10 @@ namespace storm { } template<> - typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType evaluateFunction( + typename storm::modelchecker::SparseDtmcRegionModelChecker::CoefficientType evaluateFunction( storm::RationalFunction const& function, std::map::VariableType, - typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType> const& point){ + typename storm::modelchecker::SparseDtmcRegionModelChecker::CoefficientType> const& point){ return function.evaluate(point); } diff --git a/src/utility/regions.h b/src/utility/regions.h index a77bc1bdc..ef7a62469 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -31,26 +31,26 @@ namespace storm { public: typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion ParameterRegion; typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType BoundType; + typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::CoefficientType CoefficientType; /* * Can be used to parse a single parameter with its bounds from a string of the form "0.3<=p<=0.5". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. * If no precision is given, the one from the settings is used. * The results will be inserted in the given maps * */ static void parseParameterBounds( - std::map& lowerBounds, - std::map& upperBounds, + std::map& lowerBounds, + std::map& upperBounds, std::string const& parameterBoundsString, double const precision=0.0 ); /* * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. * If no precision is given, the one from the settings is used. * @@ -61,7 +61,7 @@ namespace storm { /* * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. * If no precision is given, the one from the settings is used. * @@ -73,7 +73,7 @@ namespace storm { /* * Retrieves the regions that are specified in the settings. - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. * If no precision is given, the one from the settings is used. * @@ -115,7 +115,7 @@ namespace storm { std::string getVariableName(VariableType variable); template - typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType evaluateFunction(ParametricType const& function, std::map::VariableType, typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType> const& point); + typename storm::modelchecker::SparseDtmcRegionModelChecker::CoefficientType evaluateFunction(ParametricType const& function, std::map::VariableType, typename storm::modelchecker::SparseDtmcRegionModelChecker::CoefficientType> const& point); /*! * Returns true if the function is rational. Note that the function might be simplified.