Update documentation with fixed choices

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)

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<ValueType> 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");
                     }
                 }
                 

src/storm/solver/MinMaxLinearEquationSolver.cpp

@@ -128,7 +128,7 @@ namespace storm {
                 
         template<typename ValueType>
         void MinMaxLinearEquationSolver<ValueType>::setInitialScheduler(std::vector<uint_fast64_t>&& 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<class ValueType>
-        void MinMaxLinearEquationSolver<ValueType>::setFixedStates(storm::storage::BitVector&& states) {
-            this->fixedStates = std::move(states);
-            assert (this->fixedStates);
+        void MinMaxLinearEquationSolver<ValueType>::setChoiceFixedForStates(storm::storage::BitVector&& states) {
+            this->choiceFixedForState = std::move(states);
+            assert (this->choiceFixedForState);
         }
 
         template<class ValueType>
-        void MinMaxLinearEquationSolver<ValueType>::updateScheduler() {
-            assert (this->initialScheduler && this->fixedStates);
-            for (auto state : this->fixedStates.get()) {
+        void MinMaxLinearEquationSolver<ValueType>::setFixedChoicesToFirst() {
+            assert (this->initialScheduler && this->choiceFixedForState);
+            for (auto state : this->choiceFixedForState.get()) {
                 this->initialScheduler.get()[state] = 0;
             }
         }

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<std::vector<uint_fast64_t>> initialScheduler;
 
-            boost::optional<storm::storage::BitVector> fixedStates;
+            boost::optional<storm::storage::BitVector> choiceFixedForState;
 
         private:
             /// Whether the solver can assume that the min-max equation system has a unique solution

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<ValueType>().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<ValueType> 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();
                 }
             }