Merge pull request 'until formulae' (#14) from until_formulae into main

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/14

src/storm/logic/FragmentSpecification.cpp

@@ -65,6 +65,7 @@ namespace storm {
 
             rpatl.setProbabilityOperatorsAllowed(true);
             rpatl.setReachabilityProbabilityFormulasAllowed(true);
+            rpatl.setUntilFormulasAllowed(true);
 
             return rpatl;
         }

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -110,6 +110,8 @@ namespace storm {
             storm::logic::Formula const& formula = checkTask.getFormula();
             if (formula.isReachabilityProbabilityFormula()) {
                 return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
+            } else if (formula.isUntilFormula()) {
+                return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@@ -23,34 +23,18 @@ namespace storm {
 
                 // Initialize the solution vector.
                 std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
-                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates);
 
-                // Reduce matrix to ~Prob1 states-
-                //STORM_LOG_DEBUG("\n" << transitionMatrix);
-                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false);
-                //STORM_LOG_DEBUG("\n" << submatrix);
+                // Relevant states are those states which are phiStates and not PsiStates.
+                storm::storage::BitVector relevantStates = phiStates & ~psiStates;
 
+                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
 
-                //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x));
-                //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b));
+                // Reduce the matrix to relevant states
+                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
 
-                storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits());
-                //STORM_LOG_DEBUG(psiStates);
-                //STORM_LOG_DEBUG(statesOfCoalition);
-                //STORM_LOG_DEBUG(clippedStatesOfCoalition);
-
-                // TODO move this to BitVector-class
-                auto clippedStatesCounter = 0;
-                for(uint i = 0; i < psiStates.size(); i++) {
-                    std::cout << i << " : " << psiStates.get(i) << "  -> " << statesOfCoalition[i] << std::endl;
-                    if(!psiStates.get(i)) {
-                        clippedStatesOfCoalition.set(clippedStatesCounter, statesOfCoalition[i]);
-                        clippedStatesCounter++;
-                    }
-                }
-                //STORM_LOG_DEBUG(clippedStatesOfCoalition);
+                storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
+                clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
                 clippedStatesOfCoalition.complement();
-                //STORM_LOG_DEBUG(clippedStatesOfCoalition);
 
                 storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
                 std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
@@ -59,27 +43,26 @@ namespace storm {
                 }
 
                 viHelper.performValueIteration(env, x, b, goal.direction());
+                viHelper.fillResultVector(x, relevantStates, psiStates);
 
-                STORM_LOG_DEBUG(storm::utility::vector::toString(x));
                 if (produceScheduler) {
-                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates));
-                    STORM_LOG_DEBUG("IsPartial?" << scheduler->isPartialScheduler());
+                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
                 }
                 return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
             }
 
             template<typename ValueType>
-            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates) {
-                //STORM_LOG_DEBUG(psiStates.size());
-                for(uint i = 0; i < 2; i++) {
-                    //STORM_LOG_DEBUG(scheduler.getChoice(i));
-                }
+            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) {
                 storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());
                 uint_fast64_t maybeStatesCounter = 0;
-                for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) {
-                    //STORM_LOG_DEBUG(stateCounter << " : " << psiStates.get(stateCounter));
+                uint schedulerSize = psiStates.size();
+                for(uint stateCounter = 0; stateCounter < schedulerSize; stateCounter++) {
+                    // psiStates already fulfill formulae so we can set an arbitrary action
                     if(psiStates.get(stateCounter)) {
                         completeScheduler.setChoice(0, stateCounter);
+                    // ~phiStates do not fulfill formulae so we can set an arbitrary action
+                    } else if(notPhiStates.get(stateCounter)) {
+                        completeScheduler.setChoice(0, stateCounter);
                     } else {
                         completeScheduler.setChoice(scheduler.getChoice(maybeStatesCounter), stateCounter);
                         maybeStatesCounter++;

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

@@ -39,7 +39,7 @@ namespace storm {
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
 
             private:
-                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates);
+                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
 
             };
         }

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@@ -82,11 +82,11 @@ namespace storm {
                         //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
                         //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
                         //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
-                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew());
+                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition);
                         //std::cin.get();
                     } else {
                         // Also keep track of the choices made.
-                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices);
+                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition);
                     }
 
                     // compare applyPointwise
@@ -133,6 +133,23 @@ namespace storm {
                     return true;
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates)
+                {
+                    std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
+                    uint bitIndex = 0;
+                    for(uint i = 0; i < filledVector.size(); i++) {
+                        if (relevantStates.get(i)) {
+                            filledVector.at(i) = result.at(bitIndex);
+                            bitIndex++;
+                        }
+                        else if (psiStates.get(i)) {
+                            filledVector.at(i) = 1;
+                        }
+                    }
+                    result = filledVector;
+                }
+
                 template <typename ValueType>
                 void GameViHelper<ValueType>::setProduceScheduler(bool value) {
                     _produceScheduler = value;

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -25,6 +25,11 @@ namespace storm {
 
                     void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
 
+                    /*!
+                     * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
+                     */
+                    void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
+
                     /*h
                      * Sets whether an optimal scheduler shall be constructed during the computation
                      */

src/storm/storage/BitVector.cpp

@@ -1026,6 +1026,16 @@ namespace storm {
             }
         }
 
+        void BitVector::setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition)
+        {
+            auto clippedStatesCounter = 0;
+            for(uint i = 0; i < relevantStates.size(); i++) {
+                if(relevantStates.get(i)) {
+                    this->set(clippedStatesCounter, statesOfCoalition[i]);
+                    clippedStatesCounter++;
+                }
+            }
+        }
 
         void BitVector::truncateLastBucket() {
             if ((bitCount & mod64mask) != 0) {

src/storm/storage/BitVector.h

@@ -536,6 +536,14 @@ namespace storm {
              */
             bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length);
 
+            /*!
+             * Set clipped states of coalition for all states which are not in the winning region.
+             *
+             * @param psiStates Bitvector of states which are in the winning region.
+             * @param statesOfCoalition Bitvector of states which belong to the coalition.
+             */
+            void setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition);
+
             friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
 
             void store(std::ostream&) const;