added memory incorporation transformer

src/storm/transformer/MemoryIncorporation.cpp

@@ -0,0 +1,100 @@
+#include "MemoryIncorporation.h"
+
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
+#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
+#include "storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h"
+#include "storm/logic/Formulas.h"
+#include "storm/logic/FragmentSpecification.h"
+#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/NotSupportedException.h"
+namespace storm {
+    namespace transformer {
+
+        template <class SparseModelType>
+        storm::storage::MemoryStructure getGoalMemory(SparseModelType const& model, storm::logic::Formula const& propositionalGoalStateFormula) {
+            STORM_LOG_THROW(propositionalGoalStateFormula.isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The  subformula " << propositionalGoalStateFormula << " should be propositional.");
+            
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(model);
+            storm::storage::BitVector goalStates = mc.check(propositionalGoalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
+        
+            // Check if the formula is already satisfied for all initial states. In such a case the trivial memory structure suffices.
+            if (model.getInitialStates().isSubsetOf(goalStates)) {
+                STORM_LOG_INFO("One objective is already satisfied for all initial states.");
+                return storm::storage::MemoryStructureBuilder<typename SparseModelType::ValueType, typename SparseModelType::RewardModelType>::buildTrivialMemoryStructure(model);
+            }
+            
+            
+            // Create a memory structure that stores whether a goal state has already been reached
+            storm::storage::MemoryStructureBuilder<typename SparseModelType::ValueType, typename SparseModelType::RewardModelType> builder(2, model);
+            builder.setTransition(0, 0, ~goalStates);
+            builder.setTransition(0, 1, goalStates);
+            builder.setTransition(1, 1, storm::storage::BitVector(model.getNumberOfStates(), true));
+            for (auto const& initState : model.getInitialStates()) {
+                builder.setInitialMemoryState(initState, goalStates.get(initState) ? 1 : 0);
+            }
+            return builder.build();
+        }
+        
+        template <class SparseModelType>
+        storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& model, storm::logic::Formula const& leftSubFormula, storm::logic::Formula const& rightSubFormula) {
+            auto notLeftOrRight = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or,
+                                        std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, leftSubFormula.asSharedPointer()),
+                                        rightSubFormula.asSharedPointer());
+            return getGoalMemory<SparseModelType>(model, *notLeftOrRight);
+        
+        }
+        
+        template <class SparseModelType>
+        std::shared_ptr<SparseModelType> MemoryIncorporation<SparseModelType>::incorporateGoalMemory(SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+            storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model);
+            
+            for (auto const& subFormula : formulas) {
+                STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << *subFormula << " is not supported.");
+                auto const& subsubFormula = subFormula->asOperatorFormula().getSubformula();
+                if (subsubFormula.isEventuallyFormula()) {
+                    memory = memory.product(getGoalMemory(model, subsubFormula.asEventuallyFormula().getSubformula()));
+                } else if (subsubFormula.isUntilFormula()) {
+                    memory = memory.product(getUntilFormulaMemory(model, subsubFormula.asUntilFormula().getLeftSubformula(), subsubFormula.asUntilFormula().getRightSubformula()));
+                } else if (subsubFormula.isBoundedUntilFormula()) {
+                    // For bounded formulas it is only reasonable to add the goal memory if it considers a single upper step/time bound.
+                    auto const& buf = subsubFormula.asBoundedUntilFormula();
+                    if (!buf.isMultiDimensional() && !buf.getTimeBoundReference().isRewardBound() && (!buf.hasLowerBound() || (!buf.isLowerBoundStrict() && storm::utility::isZero(buf.template getLowerBound<storm::RationalNumber>())))) {
+                        memory = memory.product(getUntilFormulaMemory(model, buf.getLeftSubformula(), buf.getRightSubformula()));
+                    }
+                } else if (subsubFormula.isGloballyFormula()) {
+                    auto notPhi = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subsubFormula.asGloballyFormula().getSubformula().asSharedPointer());
+                    memory = memory.product(getGoalMemory(model, *notPhi));
+                } else {
+                    STORM_LOG_THROW(subsubFormula.isTotalRewardFormula() || subsubFormula.isCumulativeRewardFormula(), storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported.");
+                }
+            }
+
+            storm::storage::SparseModelMemoryProduct<ValueType> product = memory.product(model);
+            return std::dynamic_pointer_cast<SparseModelType>(product.build());
+        }
+        
+        template <class SparseModelType>
+        std::shared_ptr<SparseModelType> MemoryIncorporation<SparseModelType>::incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates) {
+            auto memory = storm::storage::NondeterministicMemoryStructureBuilder().build(storm::storage::NondeterministicMemoryStructurePattern::Full, memoryStates);
+            return storm::storage::SparseModelNondeterministicMemoryProduct<SparseModelType>(model, memory).build();
+        }
+
+        template class MemoryIncorporation<storm::models::sparse::Mdp<double>>;
+        template class MemoryIncorporation<storm::models::sparse::MarkovAutomaton<double>>;
+        
+        template class MemoryIncorporation<storm::models::sparse::Mdp<storm::RationalNumber>>;
+        template class MemoryIncorporation<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+                
+    }
+}
+
+

src/storm/transformer/MemoryIncorporation.h

@@ -0,0 +1,41 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/storage/memorystructure/MemoryStructure.h"
+#include "storm/logic/MultiObjectiveFormula.h"
+#include "storm/logic/Formula.h"
+
+namespace storm {
+    namespace transformer {
+        
+        /*!
+         * Incorporates Memory into the state space of the given model, that is
+         * the resulting model is the crossproduct of of the given model plus
+         * some type of memory structure
+         */
+        template <class SparseModelType>
+        class MemoryIncorporation {
+        
+        typedef typename SparseModelType::ValueType ValueType;
+        typedef typename SparseModelType::RewardModelType RewardModelType;
+        
+        
+
+        public:
+            
+            /*!
+             * Incorporates memory that stores whether a 'goal' state has already been reached.
+             */
+            static std::shared_ptr<SparseModelType> incorporateGoalMemory(SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+            
+            /*!
+             * Incorporates a memory structure where the nondeterminism of the model decides which successor state to choose.
+             */
+            static std::shared_ptr<SparseModelType> incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates);
+
+        };
+    }
+}
+
+