From 9f5128c4af28ec740a7d6bc195cf81501f57e69c Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 28 Jun 2021 10:26:11 +0200 Subject: [PATCH] Update documentation with fixed choices --- ...SparseDtmcParameterLiftingModelChecker.cpp | 6 ++--- .../IterativeMinMaxLinearEquationSolver.cpp | 14 +++++------ .../solver/MinMaxLinearEquationSolver.cpp | 14 +++++------ src/storm/solver/MinMaxLinearEquationSolver.h | 16 ++++++++++--- .../TopologicalMinMaxLinearEquationSolver.cpp | 24 +++++++++---------- 5 files changed, 42 insertions(+), 32 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index ca9523cd5..44fa2f689 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) { @@ -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) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 5d2ff03d6..85d975c6e 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) { @@ -176,7 +176,7 @@ namespace storm { 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]))) { + if (!this->choiceFixedForState || (this->choiceFixedForState && !(this->choiceFixedForState.get()[group]))) { 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. @@ -201,7 +201,7 @@ namespace storm { } } } else { - STORM_LOG_INFO("Ignoring state" << group << " as this state is locally monotone"); + STORM_LOG_INFO("Ignoring state" << group << " as the choice of this state is fixed"); } } 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..5b2740b8f 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 { @@ -99,14 +99,14 @@ namespace storm { 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,7 +150,7 @@ namespace storm { ValueType& xi = globalX[sccState]; bool firstRow = true; uint64_t bestRow; - if (this->fixedStates && this->fixedStates.get()[sccState]) { + if (this->choiceFixedForState && this->choiceFixedForState.get()[sccState]) { assert (this->hasInitialScheduler()); uint64_t row = this->A->getRowGroupIndices()[sccState] + this->initialScheduler.get()[sccState]; ValueType rowValue = globalB[row]; @@ -175,7 +175,7 @@ namespace storm { } 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]); + STORM_LOG_INFO("Ignoring state" << sccState << " as the choice is fixed, 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]; @@ -277,16 +277,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,7 +294,7 @@ 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); @@ -325,8 +325,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(); } }