From 2bf640272542f66dbd12502b7888bb185e548324 Mon Sep 17 00:00:00 2001
From: Lukas Posch <lukas.posch@student.tugraz.at>
Date: Tue, 9 Feb 2021 22:14:47 +0100
Subject: [PATCH] implemented until formulae

---
 src/storm/logic/FragmentSpecification.cpp     |  1 +
 .../rpatl/SparseSmgRpatlModelChecker.cpp      |  2 +
 .../rpatl/helper/SparseSmgRpatlHelper.cpp     | 41 +++++++++++++++++--
 3 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index 836b020aa..2487dcd86 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -65,6 +65,7 @@ namespace storm {
 
             rpatl.setProbabilityOperatorsAllowed(true);
             rpatl.setReachabilityProbabilityFormulasAllowed(true);
+            rpatl.setUntilFormulasAllowed(true);
 
             return rpatl;
         }
diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index c075ab6af..97dc26054 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/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.");
         }
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 9bf5a10e8..cbbcbed3e 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -23,13 +23,46 @@ 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);
+
+                STORM_LOG_DEBUG("phiStates are " << phiStates);
+                STORM_LOG_DEBUG("psiStates are " << psiStates);
+                STORM_LOG_DEBUG("~psiStates are " <<~psiStates);
+
+                // states are those states which are phiStates and not PsiStates
+                // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates
+                storm::storage::BitVector states(phiStates.size());
+                for(int counter = 0; counter < states.size(); counter++)
+                {
+                    if(phiStates.get(counter) && !psiStates.get(counter))
+                    {
+                        states.set(counter);
+                    }
+                }
+
+                STORM_LOG_DEBUG("states are " << states);
+
+                // TRY to change b to the new states
+                // TODO: only states in the phiStates can be chosen as initial states, e.g. the output is for initial states = 0, 1, 4
+                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(states, psiStates);
+/*                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates);
+                for(int counter = 0; counter < states.size(); counter++)
+                {
+                    if(!phiStates.get(counter))
+                    {
+                        b.at(counter) = 0;
+                    }
+                }*/
+                //std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates);
+
+                //STORM_LOG_DEBUG("\n" << b);
 
                 // 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);
+                //storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false);
 
+                // Reduce TRY to use only the states from phi which satisfy the left side and psi which satisfy the right side
+                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, states, states, false);
+                //STORM_LOG_DEBUG("\n" << submatrix);
 
                 //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x));
                 //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b));
@@ -60,6 +93,8 @@ namespace storm {
 
                 viHelper.performValueIteration(env, x, b, goal.direction());
 
+                // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out?
+
                 STORM_LOG_DEBUG(storm::utility::vector::toString(x));
                 if (produceScheduler) {
                     scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates));