Investigating Matrix Multiplier for SMG solving

randriu · Jul 12, 2024 · 77dcec2 · 77dcec2
1 parent 4f99949
commit 77dcec2
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 8 deletions.
diff --git a/payntbind/src/synthesis/smg/modelchecker/SparseSmgRpatlModelChecker.cpp b/payntbind/src/synthesis/smg/modelchecker/SparseSmgRpatlModelChecker.cpp
@@ -20,11 +20,35 @@
 #include <storm/exceptions/InvalidPropertyException.h>
 #include <storm/exceptions/InvalidArgumentException.h>
 #include <storm/modelchecker/results/ExplicitParetoCurveCheckResult.h>
+#include <storm/logic/FragmentSpecification.h>
 
 #include "helper/SparseSmgRpatlHelper.h"
 #include "helper/SparseNondeterministicGameInfiniteHorizonHelper.h"
 
 namespace synthesis {
+
+    storm::logic::FragmentSpecification rpatl() {
+        storm::logic::FragmentSpecification rpatl = storm::logic::propositional();
+
+        // TODO: Only allow OperatorFormulas when they are inside of a GameFormula?
+        // TODO: Require that operator formulas are required at the top level of a GameFormula?
+        rpatl.setGameFormulasAllowed(true);
+        rpatl.setRewardOperatorsAllowed(true);
+        rpatl.setLongRunAverageRewardFormulasAllowed(true);
+        rpatl.setLongRunAverageOperatorsAllowed(true);
+
+        rpatl.setProbabilityOperatorsAllowed(true);
+        rpatl.setReachabilityProbabilityFormulasAllowed(true);
+        rpatl.setUntilFormulasAllowed(true);
+        rpatl.setGloballyFormulasAllowed(true);
+        rpatl.setNextFormulasAllowed(true);
+        rpatl.setBoundedUntilFormulasAllowed(true);
+        rpatl.setStepBoundedUntilFormulasAllowed(true);
+        rpatl.setTimeBoundedUntilFormulasAllowed(true);
+
+        return rpatl;
+    }
+
     template<typename SparseSmgModelType>
     SparseSmgRpatlModelChecker<SparseSmgModelType>::SparseSmgRpatlModelChecker(SparseSmgModelType const& model) : storm::modelchecker::SparsePropositionalModelChecker<SparseSmgModelType>(model) {
         // Intentionally left empty.
@@ -33,7 +57,7 @@ namespace synthesis {
     template<typename SparseSmgModelType>
     bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
         storm::logic::Formula const& formula = checkTask.getFormula();
-        return formula.isInFragment(storm::logic::rpatl());
+        return formula.isInFragment(synthesis::rpatl());
     }
 
     template<typename SparseSmgModelType>

diff --git a/payntbind/src/synthesis/smg/modelchecker/helper/internal/NativeMultiplier.cpp b/payntbind/src/synthesis/smg/modelchecker/helper/internal/NativeMultiplier.cpp
@@ -18,12 +18,12 @@ namespace synthesis {
     template<typename Compare>
     void multiplyAndReduceBackward(storm::storage::SparseMatrix<double> const& matrix, std::vector<uint64_t> const& rowGroupIndices, std::vector<double> const& vector, std::vector<double> const* summand, std::vector<double>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride) {
         Compare compare;
-        auto elementIt = matrix.end() - 1;
-        auto rowGroupIt = rowGroupIndices.end() - 2;
 
         // Using SynthesisMatrix class as I can't modify the SparseMatrix class to access private member!!!
         synthesis::SynthesisMatrix tempMatrix(matrix);
 
+        auto elementIt = matrix.end() - 1;
+        auto rowGroupIt = rowGroupIndices.end() - 2;
         auto rowIt = tempMatrix.getRowIndications().end() - 2;
         typename std::vector<double>::const_iterator summandIt;
         if (summand) {
@@ -121,12 +121,12 @@ namespace synthesis {
     template<typename Compare>
     void multiplyAndReduceForward(storm::storage::SparseMatrix<double> const& matrix, std::vector<uint64_t> const& rowGroupIndices, std::vector<double> const& vector, std::vector<double> const* summand, std::vector<double>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride) {
         Compare compare;
-        auto elementIt = matrix.begin();
-        auto rowGroupIt = rowGroupIndices.begin();
 
-        // Using SynthesisMatrix class as I can't modify the SparseMatrix class to access private member!!!
+        // Using SynthesisMatrix class as I can't modify the SparseMatrix class to access private member rowIndications!!!
         synthesis::SynthesisMatrix tempMatrix(matrix);
 
+        auto elementIt = matrix.begin();
+        auto rowGroupIt = rowGroupIndices.begin();
         auto rowIt = tempMatrix.getRowIndications().begin();
         typename std::vector<double>::const_iterator summandIt;
         if (summand) {

diff --git a/payntbind/src/synthesis/smg/modelchecker/helper/internal/SynthesisMatrix.cpp b/payntbind/src/synthesis/smg/modelchecker/helper/internal/SynthesisMatrix.cpp
@@ -4,7 +4,15 @@
 namespace synthesis {
 
     SynthesisMatrix::SynthesisMatrix(storm::storage::SparseMatrix<double> const& other) : storm::storage::SparseMatrix<double>(other) {
-        // left intentionally empty
+        this->rowIndications.reserve(other.getRowCount() + 1);
+        this->rowIndications.push_back(0);
+        storm::storage::sparse::state_type indicationCounter = 0;
+        for (index_type row = 0; row < other.getRowCount(); row++) {
+            for (auto const &entry: other.getRow(row)) {
+                indicationCounter++;
+            }
+            this->rowIndications.push_back(indicationCounter);
+        }
     }
 
     std::vector<storm::storage::sparse::state_type> SynthesisMatrix::getRowIndications() {

diff --git a/payntbind/src/synthesis/smg/modelchecker/helper/internal/SynthesisMatrix.h b/payntbind/src/synthesis/smg/modelchecker/helper/internal/SynthesisMatrix.h
@@ -5,7 +5,7 @@
 namespace synthesis
 {
 
-    class SynthesisMatrix : storm::storage::SparseMatrix<double> {
+    class SynthesisMatrix : public storm::storage::SparseMatrix<double> {
 
        public:
 
@@ -16,4 +16,5 @@ namespace synthesis
         std::vector<index_type> rowIndications;
 
     };
+
 }