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,13 +1052,22 @@ 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());
                                                     }
                                                 }
                                             }
-                                          
+
 
                                             if (ioSettings.isExportCheckResultSet()) {
                                                 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The result output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval.");

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();
@@ -103,9 +131,9 @@ namespace storm {
                 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));         
+                    result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
                 }
-                            
+
                 return result;
             }
         }
@@ -120,7 +148,7 @@ namespace storm {
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true));
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));         
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
             }
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
@@ -139,10 +167,10 @@ namespace storm {
             auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
-                
+
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true), storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true));
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
-            } 
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+            }
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }
@@ -160,9 +188,9 @@ namespace storm {
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(),subResult.getTruthValuesVector(), storm::storage::BitVector(ret.maybeStates.size(), true));
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
-                
-            } 
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+
+            }
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }
@@ -313,7 +341,7 @@ namespace storm {
             if(checkTask.isShieldingTask()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
                 auto shield = tempest::shields::createQuantitativeShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, allStatesBv);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
             } else if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
             }
@@ -326,7 +354,7 @@ namespace storm {
             auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
             storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix());
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
-			auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
+			      auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
             if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -7,26 +7,27 @@
 #include "storm/shields/AbstractShield.h"
 
 namespace storm {
-    
+
     class Environment;
-    
+
     namespace modelchecker {
         template<class SparseMdpModelType>
         class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker<SparseMdpModelType> {
         public:
             typedef typename SparseMdpModelType::ValueType ValueType;
             typedef typename SparseMdpModelType::RewardModelType RewardModelType;
-            
+
             explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model);
-            
+
             /*!
              * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
              * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state
              */
             static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
-            
+
             // 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;
@@ -43,7 +44,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) override;
-            
+
         };
     } // namespace modelchecker
 } // namespace storm

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -141,13 +141,14 @@ 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()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
-            } 
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+            }
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }
@@ -165,8 +166,8 @@ namespace storm {
             if(checkTask.isShieldingTask()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
-            } 
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+            }
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }
@@ -202,7 +203,7 @@ namespace storm {
             if(checkTask.isShieldingTask()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
             }
             return result;
         }
@@ -225,7 +226,7 @@ namespace storm {
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 auto shield = tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
             }
             return result;
         }
@@ -246,8 +247,8 @@ namespace storm {
             if(checkTask.isShieldingTask()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
                 auto shield = tempest::shields::createQuantitativeShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition);
-                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));                    
-            } 
+                result->asExplicitQuantitativeCheckResult<ValueType>().setShield(std::move(shield));
+            }
             if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
             }

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,11 +32,62 @@ 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)));
         }
-        
+
         // Explicitly instantiate appropriate
         template class AbstractShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL

src/storm/shields/AbstractShield.h

@@ -16,19 +16,33 @@
 
 #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) {
-                    Compare compare;
-                    if(relative && std::is_same<Compare, storm::utility::ElementLessEqual<ValueType>>::value) {
-                        return compare(v, opt + opt * shieldValue);
-                    } else if(relative && std::is_same<Compare, storm::utility::ElementGreaterEqual<ValueType>>::value) {
-                        return compare(v, opt * 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);
+                        } else if(relative && std::is_same<Compare, storm::utility::ElementGreaterEqual<ValueType>>::value) {
+                            return compare(v, opt * shieldValue);
+                        }
+                        else return compare(v, shieldValue);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot create shields for parametric models");
                     }
-                    else return compare(v, shieldValue);
                 }
             };
         }
@@ -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

@@ -161,11 +161,11 @@ namespace storm {
                             std::string choiceActionLabel = choiceOriginJson["action-label"];
                             std::string choiceCorrectionActionLabel = choiceOriginCorrectionJson["action-label"];
                             choiceOriginJson["action-label"] = choiceActionLabel.append(": ").append(choiceCorrectionActionLabel).append("\n");
-                            choiceJson["origin"] = choiceOriginJson;                            
+                            choiceJson["origin"] = choiceOriginJson;
                         }
                         if (model && model->hasChoiceLabeling()) {
                             auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex);
-                            
+
                             choiceJson["labels"] = std::vector<std::string>(choiceLabels.begin(),
                                                                             choiceLabels.end());
                         }
@@ -179,10 +179,10 @@ namespace storm {
                 } else {
                     choicesJson = "undefined";
                 }
-                
+
                 stateChoicesJson["c"] = std::move(choicesJson);
                 output.push_back(std::move(stateChoicesJson));
-            
+
             }
 
             out << output.dump(4);
@@ -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

@@ -138,7 +138,7 @@ namespace storm {
         }
 
 
-      
+
 
         template <typename ValueType>
         void PreScheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
@@ -194,7 +194,7 @@ namespace storm {
                                     storm::json<storm::RationalNumber> updateJson;
                                     // next model state
                                     if (model && model->hasStateValuations()) {
-                                        updateJson["s'"] = model->getStateValuations().template toJson<storm::RationalNumber>(entryIt->getColumn());    
+                                        updateJson["s'"] = model->getStateValuations().template toJson<storm::RationalNumber>(entryIt->getColumn());
                                     } else {
                                         updateJson["s'"] = entryIt->getColumn();
                                     }
@@ -209,7 +209,7 @@ namespace storm {
                     } else {
                         choicesJson = "undefined";
                     }
-                 
+
                     stateChoicesJson["c"] = std::move(choicesJson);
                     output.push_back(std::move(stateChoicesJson));
                 }
@@ -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: