introduce bounded globally mc for MDPs

src/storm-cli-utilities/model-handling.h

@@ -49,6 +49,11 @@
 #include "storm/settings/modules/HintSettings.h"
 #include "storm/storage/Qvbs.h"
 
+#include "storm/shields/AbstractShield.h"
+#include "storm/shields/PreShield.h"
+#include "storm/shields/PostShield.h"
+#include "storm/shields/OptimalShield.h"
+
 #include "storm/utility/Stopwatch.h"
 
 namespace storm {
@@ -1047,9 +1052,18 @@ namespace storm {
                                                 if (result->isExplicitQuantitativeCheckResult()) {
                                                     if (result-> template asExplicitQuantitativeCheckResult<ValueType>().hasShield()) {
                                                         auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().getShield();
+                                                        if(shield->isPreShield()) {
+                                                            shield->asPreShield().construct();
+                                                        } else if(shield->isPostShield()) {
+                                                            shield->asPostShield().construct();
+                                                        } else if(shield->isOptimalShield()) {
+                                                            shield->asOptimalShield().construct();
+                                                        }
+
                                                         STORM_PRINT_AND_LOG("Exporting shield ... ");
 
-                                                        storm::api::exportShield(sparseModel, shield, ioSettings.getExportShieldFilename());
+                                                        STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
+                                                        storm::api::exportShield(sparseModel, shield, (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportShieldFilename());
                                                     }
                                                 }
                                             }

src/storm/api/verification.h

@@ -458,7 +458,7 @@ namespace storm {
 
         template<storm::dd::DdType DdType, typename ValueType>
         typename std::enable_if<std::is_same<ValueType, storm::RationalFunction>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithDdEngine(storm::Environment const&, std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const&, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const&) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "");
         }
 
         template<storm::dd::DdType DdType, typename ValueType>

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -45,7 +45,7 @@ namespace storm {
         template<typename SparseMdpModelType>
         bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
+            if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setBoundedGloballyFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
                 return true;
             } else if (checkTask.isOnlyInitialStatesRelevantSet()) {
                 auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
@@ -69,6 +69,34 @@ namespace storm {
             }
         }
 
+        template<typename SparseMdpModelType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask) {
+            storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula();
+            STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
+            STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral.");
+            STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper<ValueType> helper;
+            std::vector<ValueType> numericResult;
+
+            //This works only with empty vectors, no nullptr
+            storm::storage::BitVector resultMaybeStates;
+            std::vector<ValueType> choiceValues;
+
+            storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
+            numericResult = helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), allStatesBv, ~subResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), resultMaybeStates, choiceValues, checkTask.getHint());
+            // flip directions TODO
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            if(checkTask.isShieldingTask()) {
+                auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true));
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+            }
+
+            return result;
+        }
+
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
             storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -27,6 +27,7 @@ namespace storm {
 
             // The implemented methods of the AbstractModelChecker interface.
             virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
+            std::unique_ptr<CheckResult> computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -141,6 +141,7 @@ namespace storm {
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
+
             auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {

src/storm/shields/AbstractShield.cpp

@@ -1,4 +1,7 @@
 #include "storm/shields/AbstractShield.h"
+#include "storm/shields/PreShield.h"
+#include "storm/shields/PostShield.h"
+#include "storm/shields/OptimalShield.h"
 
 #include <boost/core/typeinfo.hpp>
 
@@ -29,6 +32,57 @@ namespace tempest {
             return optimizationDirection;
         }
 
+        template<typename ValueType, typename IndexType>
+        void AbstractShield<ValueType, IndexType>::setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
+            this->shieldingExpression = shieldingExpression;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isPreShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isPostShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isOptimalShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        PreShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asPreShield() {
+            return dynamic_cast<PreShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PreShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asPreShield() const {
+            return dynamic_cast<PreShield<ValueType, IndexType> const&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PostShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asPostShield() {
+            return dynamic_cast<PostShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PostShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asPostShield() const {
+            return dynamic_cast<PostShield<ValueType, IndexType> const&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        OptimalShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asOptimalShield() {
+            return dynamic_cast<OptimalShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        OptimalShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asOptimalShield() const {
+            return dynamic_cast<OptimalShield<ValueType, IndexType> const&>(*this);
+        }
+
+
         template<typename ValueType, typename IndexType>
         std::string AbstractShield<ValueType, IndexType>::getClassName() const {
             return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));

src/storm/shields/AbstractShield.h

@@ -16,12 +16,23 @@
 
 #include "storm/logic/ShieldExpression.h"
 
+#include "storm/exceptions/NotSupportedException.h"
+
+
 namespace tempest {
     namespace shields {
+        template<typename ValueType, typename IndexType>
+        class PreShield;
+        template<typename ValueType, typename IndexType>
+        class PostShield;
+        template<typename ValueType, typename IndexType>
+        class OptimalShield;
+
         namespace utility {
             template<typename ValueType, typename Compare, bool relative>
             struct ChoiceFilter {
                 bool operator()(ValueType v, ValueType opt, double shieldValue) {
+                    if constexpr (std::is_same_v<ValueType, storm::RationalNumber> || std::is_same_v<ValueType, double>) {
                         Compare compare;
                         if(relative && std::is_same<Compare, storm::utility::ElementLessEqual<ValueType>>::value) {
                             return compare(v, opt + opt * shieldValue);
@@ -29,6 +40,9 @@ namespace tempest {
                             return compare(v, opt * shieldValue);
                         }
                         else return compare(v, shieldValue);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot create shields for parametric models");
+                    }
                 }
             };
         }
@@ -47,9 +61,24 @@ namespace tempest {
             std::vector<IndexType> computeRowGroupSizes();
 
             storm::OptimizationDirection getOptimizationDirection();
+            void setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
 
             std::string getClassName() const;
 
+            virtual bool isPreShield() const;
+            virtual bool isPostShield() const;
+            virtual bool isOptimalShield() const;
+
+            PreShield<ValueType, IndexType>& asPreShield();
+            PreShield<ValueType, IndexType> const& asPreShield() const;
+
+            PostShield<ValueType, IndexType>& asPostShield();
+            PostShield<ValueType, IndexType> const& asPostShield() const;
+
+            OptimalShield<ValueType, IndexType>& asOptimalShield();
+            OptimalShield<ValueType, IndexType> const& asOptimalShield() const;
+
+
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
 

src/storm/shields/OptimalShield.cpp

@@ -64,21 +64,40 @@ namespace tempest {
             return shield;
         }
 
+
         template<typename ValueType, typename IndexType>
-        void OptimalShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PostScheduler<ValueType>> OptimalShield<ValueType, IndexType>::getScheduler() const {
+            return optimalScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool OptimalShield<ValueType, IndexType>::isOptimalShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void OptimalShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            optimalScheduler->printJsonToStream(out, model);
+        }
+
+        template<typename ValueType, typename IndexType>
+        void OptimalShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            optimalScheduler->printToStream(out, this->shieldingExpression, model);
         }
 
+        //template<typename ValueType, typename IndexType>
+        //template<typename VT>
+        //std::enable_if_t<std::is_same<VT, storm::RationalFunction>::value, storm::storage::PostScheduler<VT>> OptimalShield<ValueType, IndexType>::construct() {
+        //    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+        //}
+
+
+
         // Explicitly instantiate appropriate classes
         template class OptimalShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class OptimalShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-       // template class OptimalShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
+        template class OptimalShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
 
 #endif
     }

src/storm/shields/OptimalShield.h

@@ -14,11 +14,16 @@ namespace tempest {
             storm::storage::PostScheduler<ValueType> construct();
             template<typename Compare, bool relative>
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isOptimalShield() const override;
+
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> optimalScheduler;
         };
     }
 }

src/storm/shields/PostShield.cpp

@@ -45,7 +45,7 @@ namespace tempest {
                     }
                     ValueType optProbability = *(choice_it + optProbabilityIndex);
                     if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) {
-                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
                         shield.setChoice(storm::storage::PostSchedulerChoice<ValueType>(), state, 0);
                         choice_it += rowGroupSize;
                         continue;
@@ -69,21 +69,37 @@ namespace tempest {
 
 
         template<typename ValueType, typename IndexType>
-        void PostShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PostScheduler<ValueType>> PostShield<ValueType, IndexType>::getScheduler() const {
+            return postScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool PostShield<ValueType, IndexType>::isPostShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void PostShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            postScheduler->printJsonToStream(out, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PostShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            postScheduler->printToStream(out, this->shieldingExpression, model);
+        }
+
+        //template<typename ValueType, typename IndexType>
+        //template<typename VT>
+        //std::enable_if_t<std::is_same<VT, storm::RationalFunction>::value, storm::storage::PostScheduler<VT>> PostShield<ValueType, IndexType>::construct() {
+        //    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+        //}
+
 
         // Explicitly instantiate appropriate classes
         template class PostShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PostShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-       // template class PostShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
+        template class PostShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
 
 #endif
     }

src/storm/shields/PostShield.h

@@ -14,12 +14,16 @@ namespace tempest {
             storm::storage::PostScheduler<ValueType> construct();
             template<typename Compare, bool relative>
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isPostShield() const override;
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> postScheduler;
         };
     }
 }

src/storm/shields/PreShield.cpp

@@ -10,8 +10,12 @@ namespace tempest {
             // Intentionally left empty.
         }
 
+
         template<typename ValueType, typename IndexType>
         storm::storage::PreScheduler<ValueType> PreShield<ValueType, IndexType>::construct() {
+            if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+            }
             if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
                 if(this->shieldingExpression->isRelative()) {
                     return constructWithCompareType<storm::utility::ElementLessEqual<ValueType>, true>();
@@ -38,7 +42,7 @@ namespace tempest {
             }
             for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) {
                 uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state];
-                if(this->relevantStates.get(state)) {
+                if(true){ //if(this->relevantStates.get(state)) {
                     storm::storage::PreSchedulerChoice<ValueType> enabledChoices;
                     ValueType optProbability;
                     if(std::is_same<Compare, storm::utility::ElementGreaterEqual<ValueType>>::value) {
@@ -47,7 +51,7 @@ namespace tempest {
                         optProbability = *std::min_element(choice_it, choice_it + rowGroupSize);
                     }
                     if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) {
-                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
                         shield.setChoice(storm::storage::PreSchedulerChoice<ValueType>(), state, 0);
                         choice_it += rowGroupSize;
                         continue;
@@ -65,27 +69,38 @@ namespace tempest {
                 }
 
             }
+            preScheduler = std::make_shared<storm::storage::PreScheduler<ValueType>>(shield);
             return shield;
         }
 
 
         template<typename ValueType, typename IndexType>
-        void PreShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PreScheduler<ValueType>> PreShield<ValueType, IndexType>::getScheduler() const {
+            return preScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool PreShield<ValueType, IndexType>::isPreShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void PreShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            preScheduler->printJsonToStream(out, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PreShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            preScheduler->printToStream(out, this->shieldingExpression, model);
+        }
+
+
 
         // Explicitly instantiate appropriate classes
         template class PreShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PreShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-        //template class PreShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
-
+        template class PreShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
 #endif
     }
 }

src/storm/shields/PreShield.h

@@ -11,15 +11,22 @@ namespace tempest {
         public:
             PreShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
 
+
             storm::storage::PreScheduler<ValueType> construct();
+
             template<typename Compare, bool relative>
             storm::storage::PreScheduler<ValueType> constructWithCompareType();
+            void setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
+            std::shared_ptr<storm::storage::PreScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isPreShield() const override;
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PreScheduler<ValueType>> preScheduler;
         };
     }
 }

src/storm/storage/PostScheduler.cpp

@@ -192,6 +192,7 @@ namespace storm {
         template class PostScheduler<double>;
 #ifdef STORM_HAVE_CARL
         template class PostScheduler<storm::RationalNumber>;
+        template class PostScheduler<storm::RationalFunction>;
 #endif
     }
 }

src/storm/storage/PreScheduler.cpp

@@ -223,6 +223,7 @@ namespace storm {
         template class PreScheduler<double>;
 #ifdef STORM_HAVE_CARL
         template class PreScheduler<storm::RationalNumber>;
+        template class PreScheduler<storm::RationalFunction>;
 #endif
     }
 }

src/storm/storage/PreScheduler.h

@@ -13,6 +13,7 @@ namespace storm {
         /*
          * TODO needs obvious changes in all comment blocks
          */
+        // TODO inherit from Scheduler?
         template <typename ValueType>
         class PreScheduler {
         public: