diff --git a/src/storm/modelchecker/parametric/RegionChecker.cpp b/src/storm/modelchecker/parametric/RegionChecker.cpp index ca270537b..78eccbccc 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.cpp +++ b/src/storm/modelchecker/parametric/RegionChecker.cpp @@ -276,8 +276,11 @@ namespace storm { bool currRegionComplete = false; CoefficientType coveredArea = storm::utility::zero(); for (auto const& r : result) { - CoefficientType instersectionArea = std::max(storm::utility::zero(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y))); - instersectionArea *= std::max(storm::utility::zero(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x))); + CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)); + interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero()); + CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)); + interesctionSizeX = std::max(interesctionSizeX, storm::utility::zero()); + CoefficientType instersectionArea = interesctionSizeY * interesctionSizeX; if(!storm::utility::isZero(instersectionArea)) { currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat; currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated; diff --git a/src/storm/storage/geometry/HyproPolytope.h b/src/storm/storage/geometry/HyproPolytope.h index f959cba6c..0517389ba 100644 --- a/src/storm/storage/geometry/HyproPolytope.h +++ b/src/storm/storage/geometry/HyproPolytope.h @@ -48,7 +48,7 @@ namespace storm { HyproPolytope(HyproPolytopeType const& polytope); HyproPolytope(HyproPolytopeType&& polytope); - ~HyproPolytope(); + virtual ~HyproPolytope(); /*! * Returns the vertices of this polytope. diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index a88563b73..11ed760fc 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -22,12 +22,12 @@ namespace storm { // The polytope is universal emptyStatus = EmptyStatus::Nonempty; } else { - uint_fast64_t maxCol = halfspaces.front().normalVector().size(); - uint_fast64_t maxRow = halfspaces.size(); + StormEigen::Index maxCol = halfspaces.front().normalVector().size(); + StormEigen::Index maxRow = halfspaces.size(); A = EigenMatrix(maxRow, maxCol); b = EigenVector(maxRow); - for (int_fast64_t row = 0; row < A.rows(); ++row ){ - assert(halfspaces[row].normalVector().size() == maxCol); + for (StormEigen::Index row = 0; row < A.rows(); ++row ){ + assert((StormEigen::Index) halfspaces[row].normalVector().size() == maxCol); b(row) = halfspaces[row].offset(); A.row(row) = storm::adapters::EigenAdapter::toEigenVector(halfspaces[row].normalVector()); } @@ -107,7 +107,7 @@ namespace storm { std::vector> result; result.reserve(A.rows()); - for (int_fast64_t row=0; row < A.rows(); ++row){ + for (StormEigen::Index row=0; row < A.rows(); ++row){ result.emplace_back(storm::adapters::EigenAdapter::toStdVector(EigenVector(A.row(row))), b(row)); } return result; @@ -145,7 +145,7 @@ namespace storm { template bool NativePolytope::contains(Point const& point) const{ EigenVector x = storm::adapters::EigenAdapter::toEigenVector(point); - for (int_fast64_t row=0; row < A.rows(); ++row){ + for (StormEigen::Index row=0; row < A.rows(); ++row){ if ((A.row(row) * x)(0) > b(row)){ return false; } @@ -252,7 +252,7 @@ namespace storm { resultConstraints.reserve(A.rows() + nativeRhs.A.rows()); // evaluation of rhs in directions of lhs - for (int_fast64_t i = 0; i < A.rows(); ++i) { + for (StormEigen::Index i = 0; i < A.rows(); ++i) { auto optimizationRes = nativeRhs.optimize(A.row(i)); if ( optimizationRes.second ) { resultConstraints.emplace_back(A.row(i), b(i) + (A.row(i) * optimizationRes.first)(0)); @@ -261,7 +261,7 @@ namespace storm { } // evaluation of lhs in directions of rhs - for (int_fast64_t i = 0; i < nativeRhs.A.rows(); ++i) { + for (StormEigen::Index i = 0; i < nativeRhs.A.rows(); ++i) { auto optimizationRes = optimize(nativeRhs.A.row(i)); if ( optimizationRes.second ) { resultConstraints.emplace_back(nativeRhs.A.row(i), nativeRhs.b(i) + (nativeRhs.A.row(i) * optimizationRes.first)(0)); @@ -274,7 +274,7 @@ namespace storm { } else { EigenMatrix newA(resultConstraints.size(), resultConstraints.front().first.rows()); EigenVector newb(resultConstraints.size()); - for (int_fast64_t i = 0; i < newA.rows(); ++i) { + for (StormEigen::Index i = 0; i < newA.rows(); ++i) { newA.row(i) = resultConstraints[i].first; newb(i) = resultConstraints[i].second; } @@ -285,9 +285,11 @@ namespace storm { template std::shared_ptr> NativePolytope::affineTransformation(std::vector const& matrix, Point const& vector) const { STORM_LOG_THROW(!matrix.empty(), storm::exceptions::InvalidArgumentException, "Invoked affine transformation with a matrix without rows."); - - EigenMatrix eigenMatrix(matrix.size(), matrix.front().size()); - for (uint_fast64_t row = 0; row < matrix.size(); ++row) { + + StormEigen::Index rows = matrix.size(); + StormEigen::Index columns = matrix.front().size(); + EigenMatrix eigenMatrix(rows, columns); + for (StormEigen::Index row = 0; row < rows; ++row) { eigenMatrix.row(row) = storm::adapters::EigenAdapter::toEigenVector(matrix[row]); } EigenVector eigenVector = storm::adapters::EigenAdapter::toEigenVector(vector); @@ -308,7 +310,7 @@ namespace storm { storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); - for (int_fast64_t i = 0; i < A.cols(); ++i) { + for (StormEigen::Index i = 0; i < A.cols(); ++i) { variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction[i])); } std::vector constraints = getConstraints(solver.getManager(), variables); @@ -339,7 +341,7 @@ namespace storm { storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); - for (int_fast64_t i = 0; i < A.cols(); ++i) { + for (StormEigen::Index i = 0; i < A.cols(); ++i) { variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction(i))); } std::vector constraints = getConstraints(solver.getManager(), variables); @@ -349,8 +351,8 @@ namespace storm { solver.update(); solver.optimize(); if (solver.isOptimal()) { - auto result = std::make_pair(EigenVector(variables.size()), true); - for (uint_fast64_t i = 0; i < variables.size(); ++i) { + auto result = std::make_pair(EigenVector(A.cols()), true); + for (StormEigen::Index i = 0; i < A.cols(); ++i) { result.first(i) = storm::utility::convertNumber(solver.getExactContinuousValue(variables[i])); } return result; @@ -375,7 +377,7 @@ namespace storm { std::vector NativePolytope::declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const { std::vector result; result.reserve(A.cols()); - for (int_fast64_t col=0; col < A.cols(); ++col){ + for (StormEigen::Index col=0; col < A.cols(); ++col){ result.push_back(manager.declareVariable(namePrefix + std::to_string(col), manager.getRationalType())); } return result; @@ -384,9 +386,9 @@ namespace storm { template std::vector NativePolytope::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const { std::vector result; - for (int_fast64_t row = 0; row < A.rows(); ++row) { + for (StormEigen::Index row = 0; row < A.rows(); ++row) { storm::expressions::Expression lhs = manager.rational(A(row,0)) * variables[0].getExpression(); - for (int_fast64_t col=1; col < A.cols(); ++col) { + for (StormEigen::Index col=1; col < A.cols(); ++col) { lhs = lhs + manager.rational(A(row,col)) * variables[col].getExpression(); } result.push_back(lhs <= manager.rational(b(row))); diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h index 28add2cf6..11931a7d8 100644 --- a/src/storm/storage/geometry/NativePolytope.h +++ b/src/storm/storage/geometry/NativePolytope.h @@ -58,7 +58,7 @@ namespace storm { NativePolytope(EmptyStatus&& emptyStatus, EigenMatrix&& halfspaceMatrix, EigenVector&& halfspaceVector); - ~NativePolytope(); + virtual ~NativePolytope(); /*! * Returns the vertices of this polytope. diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h index 7aadfbcbb..d467af99d 100644 --- a/src/storm/storage/geometry/Polytope.h +++ b/src/storm/storage/geometry/Polytope.h @@ -17,7 +17,7 @@ namespace storm { typedef std::vector Point; - ~Polytope(); + virtual ~Polytope(); /*! * Creates a polytope from the given halfspaces. diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 9537346c4..8a6277e13 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -11,8 +11,8 @@ namespace storm { template void HyperplaneEnumeration::generateVerticesFromConstraints(EigenMatrix const& constraintMatrix, EigenVector const& constraintVector, bool generateRelevantHyperplanesAndVertexSets) { STORM_LOG_DEBUG("Invoked Hyperplane enumeration with " << constraintMatrix.rows() << " constraints."); - const uint_fast64_t dimension = constraintMatrix.cols(); - if(dimension == 0) { + StormEigen::Index dimension = constraintMatrix.cols(); + if (dimension == 0) { // No halfspaces means no vertices resultVertices.clear(); relevantMatrix = constraintMatrix; @@ -22,40 +22,40 @@ namespace storm { } std::unordered_map> vertexCollector; storm::storage::geometry::SubsetEnumerator subsetEnum(constraintMatrix.rows(), dimension, constraintMatrix, this->linearDependenciesFilter); - if(subsetEnum.setToFirstSubset()){ + if (subsetEnum.setToFirstSubset()){ do{ std::vector const& subset = subsetEnum.getCurrentSubset(); EigenMatrix subMatrix(dimension, dimension); - EigenVector subVector(static_cast(dimension)); - for (uint_fast64_t i = 0; i < dimension; ++i){ + EigenVector subVector(dimension); + for (StormEigen::Index i = 0; i < dimension; ++i){ subMatrix.row(i) = constraintMatrix.row(subset[i]); subVector(i) = constraintVector(subset[i]); } EigenVector point = subMatrix.fullPivLu().solve(subVector); bool pointContained = true; - for(int_fast64_t row=0; row < constraintMatrix.rows(); ++row){ - if((constraintMatrix.row(row) * point)(0) > constraintVector(row)){ + for (StormEigen::Index row=0; row < constraintMatrix.rows(); ++row){ + if ((constraintMatrix.row(row) * point)(0) > constraintVector(row)){ pointContained = false; break; } } - if(pointContained) { + if (pointContained) { //Note that the map avoids duplicates. auto hyperplaneIndices = vertexCollector.insert(typename std::unordered_map>::value_type(std::move(point), std::set())).first; - if(generateRelevantHyperplanesAndVertexSets){ + if (generateRelevantHyperplanesAndVertexSets){ hyperplaneIndices->second.insert(subset.begin(), subset.end()); } } } while (subsetEnum.incrementSubset()); } - if(generateRelevantHyperplanesAndVertexSets){ + if (generateRelevantHyperplanesAndVertexSets){ //For each hyperplane, get the number of (unique) vertices that lie on it. - std::vector verticesOnHyperplaneCounter(constraintMatrix.rows(), 0); - for(auto const& mapEntry : vertexCollector){ - for(auto const& hyperplaneIndex : mapEntry.second){ + std::vector verticesOnHyperplaneCounter(constraintMatrix.rows(), 0); + for (auto const& mapEntry : vertexCollector){ + for (auto const& hyperplaneIndex : mapEntry.second){ ++verticesOnHyperplaneCounter[hyperplaneIndex]; } } @@ -64,8 +64,8 @@ namespace storm { //Note that this will change the indices of the Hyperplanes. //Therefore, we additionally store the old indices for every hyperplane to be able to translate from old to new indices storm::storage::geometry::HyperplaneCollector hyperplaneCollector; - for(uint_fast64_t hyperplaneIndex = 0; hyperplaneIndex < verticesOnHyperplaneCounter.size(); ++hyperplaneIndex){ - if(verticesOnHyperplaneCounter[hyperplaneIndex] >= dimension){ + for (uint_fast64_t hyperplaneIndex = 0; hyperplaneIndex < verticesOnHyperplaneCounter.size(); ++hyperplaneIndex){ + if (verticesOnHyperplaneCounter[hyperplaneIndex] >= dimension){ std::vector oldIndex; oldIndex.push_back(hyperplaneIndex); hyperplaneCollector.insert(constraintMatrix.row(hyperplaneIndex), constraintVector(hyperplaneIndex), &oldIndex); @@ -78,8 +78,8 @@ namespace storm { //Get the mapping from old to new indices std::vector oldToNewIndexMapping (constraintMatrix.rows(), constraintMatrix.rows()); //Initialize with some illegal value std::vector> newToOldIndexMapping(hyperplaneCollector.getIndexLists()); - for(uint_fast64_t newIndex = 0; newIndex < newToOldIndexMapping.size(); ++newIndex){ - for(auto const& oldIndex : newToOldIndexMapping[newIndex]){ + for (uint_fast64_t newIndex = 0; newIndex < newToOldIndexMapping.size(); ++newIndex){ + for (auto const& oldIndex : newToOldIndexMapping[newIndex]){ oldToNewIndexMapping[oldIndex] = newIndex; } } @@ -88,10 +88,10 @@ namespace storm { std::vector> vertexSets(relevantMatrix.rows()); resultVertices.clear(); resultVertices.reserve(vertexCollector.size()); - for(auto const& mapEntry : vertexCollector){ - for(auto const& oldHyperplaneIndex : mapEntry.second){ + for (auto const& mapEntry : vertexCollector){ + for (auto const& oldHyperplaneIndex : mapEntry.second){ //ignore the hyperplanes which are redundant, i.e. for which there is no new index - if((int_fast64_t) oldToNewIndexMapping[oldHyperplaneIndex] < relevantVector.rows()){ + if ((StormEigen::Index) oldToNewIndexMapping[oldHyperplaneIndex] < relevantVector.rows()){ vertexSets[oldToNewIndexMapping[oldHyperplaneIndex]].insert(resultVertices.size()); } } @@ -99,14 +99,14 @@ namespace storm { } this->vertexSets.clear(); this->vertexSets.reserve(vertexSets.size()); - for(auto const& vertexSet : vertexSets){ + for (auto const& vertexSet : vertexSets){ this->vertexSets.emplace_back(vertexSet.begin(), vertexSet.end()); } } else { resultVertices.clear(); resultVertices.reserve(vertexCollector.size()); - for(auto const& mapEntry : vertexCollector){ + for (auto const& mapEntry : vertexCollector){ resultVertices.push_back(mapEntry.first); } this->vertexSets.clear(); @@ -118,9 +118,9 @@ namespace storm { template bool HyperplaneEnumeration::linearDependenciesFilter(std::vector const& subset, uint_fast64_t const& item, EigenMatrix const& A) { - EigenMatrix subMatrix(subset.size() +1, A.cols()); + EigenMatrix subMatrix(subset.size() + 1, A.cols()); for (uint_fast64_t i = 0; i < subset.size(); ++i){ - subMatrix.row(i) = A.row(subset[i]); + subMatrix.row((StormEigen::Index) i) = A.row(StormEigen::Index (subset[i])); } subMatrix.row(subset.size()) = A.row(item); StormEigen::FullPivLU lUMatrix( subMatrix ); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index 3dc8172d5..2f6e524f9 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -117,7 +117,7 @@ namespace storm { vectorMatrix.col(i) << points[subset[i]], storm::utility::one(); } vectorMatrix.col(subset.size()) << points[item], storm::utility::one(); - return (vectorMatrix.fullPivLu().rank() > (int_fast64_t) subset.size()); + return (vectorMatrix.fullPivLu().rank() > (StormEigen::Index) subset.size()); } template @@ -166,7 +166,7 @@ namespace storm { // clear the additionally added points. Note that the order of the points might have changed storm::storage::BitVector keptPoints(points.size(), true); for (uint_fast64_t pointIndex = 0; pointIndex < points.size(); ++pointIndex) { - for (int_fast64_t row = 0; row < resultMatrix.rows(); ++row) { + for (StormEigen::Index row = 0; row < resultMatrix.rows(); ++row) { if ((resultMatrix.row(row) * points[pointIndex])(0) > resultVector(row)) { keptPoints.set(pointIndex, false); break; @@ -178,7 +178,7 @@ namespace storm { if (generateRelevantVerticesAndVertexSets) { storm::storage::BitVector keptVertices(relevantVertices.size(), true); for (uint_fast64_t vertexIndex = 0; vertexIndex < relevantVertices.size(); ++vertexIndex) { - for (int_fast64_t row = 0; row < resultMatrix.rows(); ++row) { + for (StormEigen::Index row = 0; row < resultMatrix.rows(); ++row) { if ((resultMatrix.row(row) * relevantVertices[vertexIndex])(0) > resultVector(row)) { keptVertices.set(vertexIndex, false); break; @@ -383,7 +383,7 @@ namespace storm { std::unordered_map> relevantVerticesMap; relevantVerticesMap.reserve(points.size()); for (uint_fast64_t vertexIndex = 0; vertexIndex < hyperplanesOnVertexCounter.size(); ++vertexIndex){ - if ((int_fast64_t) hyperplanesOnVertexCounter[vertexIndex] >= points.front().rows()){ + if ((StormEigen::Index) hyperplanesOnVertexCounter[vertexIndex] >= points.front().rows()){ auto mapEntry = relevantVerticesMap.insert(typename std::unordered_map>::value_type(points[vertexIndex], std::vector())).first; mapEntry->second.push_back(vertexIndex); } @@ -402,7 +402,7 @@ namespace storm { for (auto& vertexVector : vertexSets){ std::set vertexSet; for (auto const& oldIndex : vertexVector){ - if ((int_fast64_t) hyperplanesOnVertexCounter[oldIndex] >= points.front().rows()){ + if ((StormEigen::Index) hyperplanesOnVertexCounter[oldIndex] >= points.front().rows()){ vertexSet.insert(oldToNewIndexMapping[oldIndex]); } } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 72d95eb06..368a09618 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -418,10 +418,12 @@ namespace storm { break; } } + typename storm::storage::ParameterRegion::CoefficientType satAreaFraction = satArea / parameterSpace.area(); + typename storm::storage::ParameterRegion::CoefficientType unsatAreaFraction = unsatArea / parameterSpace.area(); STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions and " << numOfUnsatRegions << " unsafe regions." << std::endl); - STORM_PRINT_AND_LOG(storm::utility::convertNumber(satArea / parameterSpace.area()) * 100 << "% of the parameter space is safe, and " - << storm::utility::convertNumber(unsatArea / parameterSpace.area()) * 100 << "% of the parameter space is unsafe." << std::endl); + STORM_PRINT_AND_LOG(storm::utility::convertNumber(satAreaFraction) * 100 << "% of the parameter space is safe, and " + << storm::utility::convertNumber(unsatAreaFraction) * 100 << "% of the parameter space is unsafe." << std::endl); STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl); STORM_PRINT_AND_LOG(resultVisualization);