Merge pull request #130 from jipspel/fixes

Fixes

src/storm-pars-cli/storm-pars.cpp

@@ -567,7 +567,6 @@ namespace storm {
 
                 auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
                 auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
-                auto engine = regionSettings.getRegionCheckEngine();
 
                 std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> verificationCallback;
                 std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> postprocessingCallback;

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -74,8 +74,8 @@ namespace storm {
         template <typename ValueType, typename ConstantType>
         AssumptionStatus AssumptionChecker<ValueType, ConstantType>::validateAssumption(uint_fast64_t val1, uint_fast64_t val2,std::shared_ptr<expressions::BinaryRelationExpression> assumption, std::shared_ptr<Order> order, storage::ParameterRegion<ValueType> region, std::vector<ConstantType>const minValues, std::vector<ConstantType>const 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);

src/storm-pars/analysis/LocalMonotonicityResult.cpp

@@ -57,7 +57,7 @@ namespace storm {
         template <typename VariableType>
         std::shared_ptr<LocalMonotonicityResult<VariableType>> LocalMonotonicityResult<VariableType>::copy() {
             std::shared_ptr<LocalMonotonicityResult<VariableType>> copy = std::make_shared<LocalMonotonicityResult<VariableType>>(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 <typename VariableType>
         std::string LocalMonotonicityResult<VariableType>::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) {

src/storm-pars/analysis/MonotonicityHelper.cpp

@@ -60,7 +60,7 @@ namespace storm {
 
             this->extender = new analysis::OrderExtender<ValueType, ConstantType>(model, formulas[0]);
 
-            for (auto i = 0; i < matrix.getRowCount(); ++i) {
+            for (size_t i = 0; i < matrix.getRowCount(); ++i) {
                 std::set<VariableType> occurringVariables;
 
                 for (auto &entry : matrix.getRow(i)) {

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);

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<ConstantType> 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;
                     }

src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp

@@ -508,7 +508,6 @@ namespace storm {
                                                                                                              std::set<VariableType>& possibleNotMonotoneParameters,
                                                                                                              std::set<VariableType>const& consideredVariables,
                                                                                                              storm::solver::OptimizationDirection const& dir) {
-            bool minimize = storm::solver::minimize(dir);
             typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation Valuation;
             typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
             ConstantType value = storm::solver::minimize(dir) ? 1 : 0;

src/storm-pars/storage/ParameterRegion.cpp

@@ -283,12 +283,12 @@ namespace storm {
         }
 
         template <typename ParametricType>
-        void ParameterRegion<ParametricType>::setSplitThreshold(int splitThreshold) {
+        void ParameterRegion<ParametricType>::setSplitThreshold(size_t splitThreshold) {
             this->splitThreshold = splitThreshold;
         }
 
         template <typename ParametricType>
-        int ParameterRegion<ParametricType>::getSplitThreshold() const {
+        size_t ParameterRegion<ParametricType>::getSplitThreshold() const {
             return splitThreshold;
         }
 

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;

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) {
@@ -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.

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 {
@@ -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<ValueType>() - entry.getValue();
@@ -165,69 +162,41 @@ namespace storm {
                     }
                 }
                 if (hasDiagonalEntry) {
-                    STORM_LOG_WARN_COND_DEBUG( storm::NumberTraits<ValueType>::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<ValueType>::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<ValueType>() - entry.getValue();
-                        } else {
-                            rowValue += entry.getValue() * globalX[entry.getColumn()];
-                        }
-                    }
-                    if (hasDiagonalEntry) {
-                        STORM_LOG_WARN_COND_DEBUG(
-                                storm::NumberTraits<ValueType>::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<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,15 +263,13 @@ 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);
 
             }
 
-//            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();
                 }
             }
             

src/storm/utility/graph.cpp

@@ -1674,7 +1674,7 @@ namespace storm {
                 std::vector<uint_fast64_t> 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);