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 ca9523cd5..9fec51ff5 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -305,7 +305,7 @@ namespace storm { solver->setTrackScheduler(true); if (localMonotonicityResult != nullptr && !this->isOnlyGlobalSet()) { - storm::storage::BitVector fixedStates(parameterLifter->getRowGroupCount(), false); + storm::storage::BitVector choiceFixedForStates(parameterLifter->getRowGroupCount(), false); bool useMinimize = storm::solver::minimize(dirForParameters); if (useMinimize && !minSchedChoices) { @@ -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 @@ -346,10 +346,10 @@ namespace storm { } } if (allMonotone) { - fixedStates.set(state); + choiceFixedForStates.set(state); } } - solver->setFixedStates(std::move(fixedStates)); + solver->setChoiceFixedForStates(std::move(choiceFixedForStates)); } if (storm::solver::minimize(dirForParameters) && minSchedChoices) @@ -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; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 5d2ff03d6..d6a088785 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -98,11 +98,11 @@ namespace storm { // Resolve the nondeterminism according to the given scheduler. bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat(env) == LinearEquationSolverProblemFormat::EquationSystem; storm::storage::SparseMatrix submatrix; - if (this->fixedStates) { - for (auto state : this->fixedStates.get()) { - assert (this->A->getRowGroupSize(state) == 1); - } - } +// if (this->choiceFixedForState) { +// for (auto state : this->choiceFixedForState.get()) { +// assert (this->A->getRowGroupSize(state) == 1); +// } +// } submatrix = this->A->selectRowsFromRowGroups(scheduler, convertToEquationSystem); if (convertToEquationSystem) { @@ -175,8 +175,7 @@ namespace storm { // Group staat voor de states? for (uint_fast64_t group = 0; group < this->A->getRowGroupCount(); ++group) { uint_fast64_t currentChoice = scheduler[group]; - // TODO: remove, as this should already be fixed by implementation to determine matrix/vector - if (!this->fixedStates || (this->fixedStates && !(this->fixedStates.get()[group]))) { + assert (!this->choiceFixedForState || (this->choiceFixedForState && (!(this->choiceFixedForState.get()[group]) || this->A->getRowGroupSize(group) == 1))); for (uint_fast64_t choice = this->A->getRowGroupIndices()[group]; choice < this->A->getRowGroupIndices()[group + 1]; ++choice) { // If the choice is the currently selected one, we can skip it. @@ -200,9 +199,6 @@ namespace storm { x[group] = std::move(choiceValue); } } - } else { - STORM_LOG_INFO("Ignoring state" << group << " as this state is locally monotone"); - } } // If the scheduler did not improve, we are done. diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 4366fa0db..3b88b7360 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -128,7 +128,7 @@ namespace storm { template void MinMaxLinearEquationSolver::setInitialScheduler(std::vector&& choices) { - assert (!this->fixedStates || this->fixedStates.get().size() == choices.size()); + assert (!this->choiceFixedForState || this->choiceFixedForState.get().size() == choices.size()); initialScheduler = std::move(choices); } @@ -158,15 +158,15 @@ namespace storm { } template - void MinMaxLinearEquationSolver::setFixedStates(storm::storage::BitVector&& states) { - this->fixedStates = std::move(states); - assert (this->fixedStates); + void MinMaxLinearEquationSolver::setChoiceFixedForStates(storm::storage::BitVector&& states) { + this->choiceFixedForState = std::move(states); + assert (this->choiceFixedForState); } template - void MinMaxLinearEquationSolver::updateScheduler() { - assert (this->initialScheduler && this->fixedStates); - for (auto state : this->fixedStates.get()) { + void MinMaxLinearEquationSolver::setFixedChoicesToFirst() { + assert (this->initialScheduler && this->choiceFixedForState); + for (auto state : this->choiceFixedForState.get()) { this->initialScheduler.get()[state] = 0; } } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 836570ffc..cb603a34c 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -70,8 +70,18 @@ namespace storm { */ void unsetOptimizationDirection(); - void setFixedStates(storm::storage::BitVector&& states); - void updateScheduler(); + /*! + * Sets the states for which the choices are fixed. + * Expecting the matrix to only have one choice for the states which are fixed. + * @param states bitvector with the states where the choices are fixed. + */ + void setChoiceFixedForStates(storm::storage::BitVector&& states); + + /*! + * Sets the initialChoices for the states of which the choices are fixed on the first choice available (0) + * Expecting the matrix to only have one choice for the state + */ + void setFixedChoicesToFirst(); /*! * Sets whether the solution to the min max equation system is known to be unique. @@ -186,7 +196,7 @@ namespace storm { // A scheduler that can be used by solvers that require a valid initial scheduler. boost::optional> initialScheduler; - boost::optional fixedStates; + boost::optional choiceFixedForState; private: /// Whether the solver can assume that the min-max equation system has a unique solution diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 548ef2d75..27d2de8a0 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -69,7 +69,7 @@ namespace storm { } bool returnValue = true; - if (this->sortedSccDecomposition->size() == 1 && (!this->fixedStates || this->fixedStates.get().empty())) { + if (this->sortedSccDecomposition->size() == 1 && (!this->choiceFixedForState || this->choiceFixedForState.get().empty())) { // Handle the case where there is just one large SCC, as there are no fixed states, we solve it like this returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b); } else { @@ -89,24 +89,22 @@ namespace storm { progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { - // TODO: directly use localMonRes on this returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; } else { STORM_LOG_TRACE("Solving SCC of size " << scc.size() << "."); sccRowGroupsAsBitVector.clear(); sccRowsAsBitVector.clear(); for (auto const& group : scc) { // Group refers to state - bool allIgnored = true; sccRowGroupsAsBitVector.set(group, true); - if (!this->fixedStates || !this->fixedStates.get()[group]) { + if (!this->choiceFixedForState || !this->choiceFixedForState.get()[group]) { for (uint64_t row = this->A->getRowGroupIndices()[group]; row < this->A->getRowGroupIndices()[group + 1]; ++row) { sccRowsAsBitVector.set(row, true); } } else { auto row = this->A->getRowGroupIndices()[group]+this->getInitialScheduler()[group]; sccRowsAsBitVector.set(row, true); - STORM_LOG_INFO("Fixing state " << group << " to option " << this->getInitialScheduler()[group] << " because of local monotonicity."); + STORM_LOG_INFO("Fixing state " << group << " to choice " << this->getInitialScheduler()[group] << "."); } } returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue; @@ -150,13 +148,12 @@ namespace storm { ValueType& xi = globalX[sccState]; bool firstRow = true; uint64_t bestRow; - if (this->fixedStates && this->fixedStates.get()[sccState]) { - assert (this->hasInitialScheduler()); - uint64_t row = this->A->getRowGroupIndices()[sccState] + this->initialScheduler.get()[sccState]; + assert (!this->choiceFixedForState || !this->choiceFixedForState.get()[sccState] || (this->hasInitialScheduler() && this->A->getRowGroupSize(sccState) == 1)); + for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { ValueType rowValue = globalB[row]; bool hasDiagonalEntry = false; ValueType denominator; - for (auto const &entry : this->A->getRow(row)) { + for (auto const& entry : this->A->getRow(row)) { if (entry.getColumn() == sccState) { hasDiagonalEntry = true; denominator = storm::utility::one() - entry.getValue(); @@ -165,69 +162,41 @@ namespace storm { } } if (hasDiagonalEntry) { - STORM_LOG_WARN_COND_DEBUG( storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || - storm::utility::isZero(denominator), "State " << sccState << " has a selfloop with probability '1-(" << denominator << ")'. This could be an indication for numerical issues."); - assert (!storm::utility::isZero(denominator)); - rowValue /= denominator; + STORM_LOG_WARN_COND_DEBUG( + storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || storm::utility::isZero(denominator), + "State " << sccState << " has a selfloop with probability '1-(" << denominator + << ")'. This could be an indication for numerical issues."); + if (storm::utility::isZero(denominator)) { + // In this case we have a selfloop on this state. This can never an optimal choice: + // When minimizing, we are looking for the largest fixpoint (which will never be attained by this action) + // When maximizing, this choice reflects probability zero (non-optimal) or reward infinity (should already be handled during preprocessing). + continue; + } else { + rowValue /= denominator; + } } - if (minimize(dir)) { + if (firstRow) { xi = std::move(rowValue); + bestRow = row; + firstRow = false; } else { - xi = std::move(rowValue); - } - STORM_LOG_INFO("Ignoring state" << sccState << " as the scheduler is fixed by monotonicity, current probability for this state is: " << this->schedulerChoices.get()[sccState]); - } else { - for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { - ValueType rowValue = globalB[row]; - bool hasDiagonalEntry = false; - ValueType denominator; - for (auto const &entry : this->A->getRow(row)) { - if (entry.getColumn() == sccState) { - hasDiagonalEntry = true; - denominator = storm::utility::one() - entry.getValue(); - } else { - rowValue += entry.getValue() * globalX[entry.getColumn()]; - } - } - if (hasDiagonalEntry) { - STORM_LOG_WARN_COND_DEBUG( - storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || - storm::utility::isZero(denominator), - "State " << sccState << " has a selfloop with probability '1-(" << denominator - << ")'. This could be an indication for numerical issues."); - if (storm::utility::isZero(denominator)) { - // In this case we have a selfloop on this state. This can never an optimal choice: - // When minimizing, we are looking for the largest fixpoint (which will never be attained by this action) - // When maximizing, this choice reflects probability zero (non-optimal) or reward infinity (should already be handled during preprocessing). - continue; - } else { - rowValue /= denominator; + if (minimize(dir)) { + if (rowValue < xi) { + xi = std::move(rowValue); + bestRow = row; } - } - if (firstRow) { - xi = std::move(rowValue); - bestRow = row; - firstRow = false; } else { - if (minimize(dir)) { - if (rowValue < xi) { - xi = std::move(rowValue); - bestRow = row; - } - } else { - if (rowValue > xi) { - xi = std::move(rowValue); - bestRow = row; - } + if (rowValue > xi) { + xi = std::move(rowValue); + bestRow = row; } } } - if (this->isTrackSchedulerSet()) { - this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState]; - } - STORM_LOG_THROW(!firstRow, storm::exceptions::UnexpectedException, "Empty row group in MinMax equation system."); } - //std::cout << "Solved trivial scc " << sccState << " with result " << globalX[sccState] << std::endl; + if (this->isTrackSchedulerSet()) { + this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState]; + } + STORM_LOG_THROW(!firstRow, storm::exceptions::UnexpectedException, "Empty row group in MinMax equation system."); return true; } @@ -277,16 +246,16 @@ namespace storm { this->sccSolver = GeneralMinMaxLinearEquationSolverFactory().create(sccSolverEnvironment); this->sccSolver->setCachingEnabled(true); } - if (this->fixedStates) { + if (this->choiceFixedForState) { // convert fixed states to only fixed states of sccs - storm::storage::BitVector fixedStatesSCC(sccRowGroups.getNumberOfSetBits()); + storm::storage::BitVector choiceFixedForStateSCC(sccRowGroups.getNumberOfSetBits()); auto j = 0; for (auto i : sccRowGroups) { - fixedStatesSCC.set(j, this->fixedStates.get()[i]); + choiceFixedForStateSCC.set(j, this->choiceFixedForState.get()[i]); j++; } assert (j = sccRowGroups.getNumberOfSetBits()); - this->sccSolver->setFixedStates(std::move(fixedStatesSCC)); + this->sccSolver->setChoiceFixedForStates(std::move(choiceFixedForStateSCC)); } this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents()); @@ -294,15 +263,13 @@ namespace storm { // SCC Matrix storm::storage::SparseMatrix sccA; - if (this->fixedStates) { + if (this->choiceFixedForState) { sccA = this->A->getSubmatrix(false, sccRows, sccRowGroups); } else { sccA = this->A->getSubmatrix(true, sccRowGroups, sccRowGroups); } -// std::cout << "Matrix is " << sccA << std::endl; - this->sccSolver->setMatrix(std::move(sccA)); // x Vector @@ -325,8 +292,8 @@ namespace storm { if (this->hasInitialScheduler()) { auto sccInitChoices = storm::utility::vector::filterVector(this->getInitialScheduler(), sccRowGroups); this->sccSolver->setInitialScheduler(std::move(sccInitChoices)); - if (this->fixedStates) { - this->sccSolver->updateScheduler(); + if (this->choiceFixedForState) { + this->sccSolver->setFixedChoicesToFirst(); } } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 3d97bf778..5df06c585 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1674,7 +1674,7 @@ namespace storm { std::vector result; result.reserve(matrix.getRowGroupCount()); - storm::storage::sparse::state_type currentPosition = 0; +// storm::storage::sparse::state_type currentPosition = 0; auto count = matrix.getRowGroupCount() - 1; for (auto const& state : firstStates) { stateQueue.push_back(state);