diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 5aa2d6af9..c66ec582a 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -567,7 +567,6 @@ namespace storm { auto parametricSettings = storm::settings::getModule(); auto regionSettings = storm::settings::getModule(); - auto engine = regionSettings.getRegionCheckEngine(); std::function(std::shared_ptr const& formula)> verificationCallback; std::function const&)> postprocessingCallback; diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index e83c323df..0d8d87cf9 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -74,8 +74,8 @@ namespace storm { template AssumptionStatus AssumptionChecker::validateAssumption(uint_fast64_t val1, uint_fast64_t val2,std::shared_ptr assumption, std::shared_ptr order, storage::ParameterRegion region, std::vectorconst minValues, std::vectorconst maxValues) const { // First check if based on sample points the assumption can be discharged - assert (val1 == std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName())); - assert (val2 == std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName())); + assert (val1 == std::stoull(assumption->getFirstOperand()->asVariableExpression().getVariableName())); + assert (val2 == std::stoull(assumption->getSecondOperand()->asVariableExpression().getVariableName())); AssumptionStatus result = AssumptionStatus::UNKNOWN; if (useSamples) { result = checkOnSamples(assumption); diff --git a/src/storm-pars/analysis/LocalMonotonicityResult.cpp b/src/storm-pars/analysis/LocalMonotonicityResult.cpp index 8a5bb7f18..20a9a7ca3 100644 --- a/src/storm-pars/analysis/LocalMonotonicityResult.cpp +++ b/src/storm-pars/analysis/LocalMonotonicityResult.cpp @@ -57,7 +57,7 @@ namespace storm { template std::shared_ptr> LocalMonotonicityResult::copy() { std::shared_ptr> copy = std::make_shared>(stateMonRes.size()); - for (auto state = 0; state < stateMonRes.size(); state++) { + for (size_t state = 0; state < stateMonRes.size(); state++) { if (stateMonRes[state] != nullptr) { copy->setMonotonicityResult(state, stateMonRes[state]->copy()); } @@ -138,7 +138,7 @@ namespace storm { template std::string LocalMonotonicityResult::toString() const { std::string result = "Local Monotonicity Result: \n"; - for (auto i = 0; i < stateMonRes.size(); ++i) { + for (size_t i = 0; i < stateMonRes.size(); ++i) { result += "state "; result += std::to_string(i); if (stateMonRes[i] != nullptr) { diff --git a/src/storm-pars/analysis/MonotonicityHelper.cpp b/src/storm-pars/analysis/MonotonicityHelper.cpp index 07cf5eb04..34406067d 100644 --- a/src/storm-pars/analysis/MonotonicityHelper.cpp +++ b/src/storm-pars/analysis/MonotonicityHelper.cpp @@ -60,7 +60,7 @@ namespace storm { this->extender = new analysis::OrderExtender(model, formulas[0]); - for (auto i = 0; i < matrix.getRowCount(); ++i) { + for (size_t i = 0; i < matrix.getRowCount(); ++i) { std::set occurringVariables; for (auto &entry : matrix.getRow(i)) { diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index e97005830..324e332c4 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -115,8 +115,6 @@ namespace storm { RegionResult::Unknown); currentRegion.split(currentRegion.getCenterPoint(), newRegions); - - bool first = true; for (auto& newRegion : newRegions) { unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions); refinementDepths.push(currentDepth + 1); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 44fa2f689..9fec51ff5 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -317,7 +317,7 @@ namespace storm { // TODO: this only works since we decided to keep all columns auto const & occuringVariables = parameterLifter->getOccurringVariablesAtState(); - for (auto state = 0; state < parameterLifter->getRowGroupCount(); ++state) { + for (uint_fast64_t state = 0; state < parameterLifter->getRowGroupCount(); ++state) { auto oldStateNumber = parameterLifter->getOriginalStateNumber(state); auto& variables = occuringVariables.at(oldStateNumber); // point at which we start with rows for this state @@ -410,10 +410,6 @@ namespace storm { auto const& matrix = parameterLifter->getMatrix(); auto const& vector = parameterLifter->getVector(); - auto i = 0; - for (auto & x : vector) { - ++i; - } std::vector stateResults; for (uint64_t state = 0; state < schedulerChoices.size(); ++state) { uint64_t rowOffset = matrix.getRowGroupIndices()[state]; @@ -591,7 +587,6 @@ namespace storm { bool done = true; for (auto const& state : states) { done &= order->contains(state) && localMonotonicityResult->getMonotonicity(state, var) != Monotonicity::Unknown; - auto check = localMonotonicityResult->getMonotonicity(state, var); if (!done) { break; } diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 14856299b..d43cd23ea 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -508,7 +508,6 @@ namespace storm { std::set& possibleNotMonotoneParameters, std::setconst& consideredVariables, storm::solver::OptimizationDirection const& dir) { - bool minimize = storm::solver::minimize(dir); typedef typename storm::storage::ParameterRegion::Valuation Valuation; typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; ConstantType value = storm::solver::minimize(dir) ? 1 : 0; diff --git a/src/storm-pars/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp index ba64bf30e..a6c1f16ee 100644 --- a/src/storm-pars/storage/ParameterRegion.cpp +++ b/src/storm-pars/storage/ParameterRegion.cpp @@ -283,12 +283,12 @@ namespace storm { } template - void ParameterRegion::setSplitThreshold(int splitThreshold) { + void ParameterRegion::setSplitThreshold(size_t splitThreshold) { this->splitThreshold = splitThreshold; } template - int ParameterRegion::getSplitThreshold() const { + size_t ParameterRegion::getSplitThreshold() const { return splitThreshold; } diff --git a/src/storm-pars/storage/ParameterRegion.h b/src/storm-pars/storage/ParameterRegion.h index 7545bb2ab..ded2515b0 100644 --- a/src/storm-pars/storage/ParameterRegion.h +++ b/src/storm-pars/storage/ParameterRegion.h @@ -57,8 +57,8 @@ namespace storm { */ Valuation getCenterPoint() const; - void setSplitThreshold(int splitThreshold); - int getSplitThreshold() const; + void setSplitThreshold(size_t splitThreshold); + size_t getSplitThreshold() const; /*! * Returns the area of this region @@ -89,7 +89,7 @@ namespace storm { void init(); bool lastSplitMonotone = false; - int splitThreshold; + size_t splitThreshold; Valuation lowerBoundaries; Valuation upperBoundaries;