started to implement conditional rewards for dtmcs

Former-commit-id: 0400ea21ef

src/logic/ConditionalFormula.cpp

@@ -1,11 +1,13 @@
 #include "src/logic/ConditionalFormula.h"
-
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        ConditionalFormula::ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, Context context) : subformula(subformula), conditionFormula(conditionFormula), context(context)  {
-            // Intentionally left empty.
+        ConditionalFormula::ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, FormulaContext context) : subformula(subformula), conditionFormula(conditionFormula), context(context)  {
+            STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
         }
         
         Formula const& ConditionalFormula::getSubformula() const {
@@ -17,11 +19,11 @@ namespace storm {
         }
         
         bool ConditionalFormula::isConditionalProbabilityFormula() const {
-            return context == Context::Probability;
+            return context == FormulaContext::Probability;
         }
         
         bool ConditionalFormula::isConditionalRewardFormula() const {
-            return context == Context::Reward;
+            return context == FormulaContext::Reward;
         }
         
         boost::any ConditionalFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
@@ -29,7 +31,22 @@ namespace storm {
         }
         
         std::shared_ptr<Formula> ConditionalFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ConditionalFormula>(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution));
+            return std::make_shared<ConditionalFormula>(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution), context);
+        }
+        
+        void ConditionalFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            this->getConditionFormula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void ConditionalFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+            this->getConditionFormula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
+        
+        void ConditionalFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
+            this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
         std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const {

src/logic/ConditionalFormula.h

@@ -2,6 +2,7 @@
 #define STORM_LOGIC_CONDITIONALFORMULA_H_
 
 #include "src/logic/BinaryPathFormula.h"
+#include "src/logic/FormulaContext.h"
 
 namespace storm {
     namespace logic {
@@ -9,7 +10,7 @@ namespace storm {
         public:
             enum class Context { Probability, Reward };
             
-            ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, Context context = Context::Probability);
+            ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, FormulaContext context = FormulaContext::Probability);
             
             virtual ~ConditionalFormula() {
                 // Intentionally left empty.
@@ -27,10 +28,14 @@ namespace storm {
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            
         private:
             std::shared_ptr<Formula const> subformula;
             std::shared_ptr<Formula const> conditionFormula;
-            Context context;
+            FormulaContext context;
         };
     }
 }

src/logic/EventuallyFormula.cpp

@@ -1,23 +1,25 @@
 #include "src/logic/EventuallyFormula.h"
-
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, Context context) : UnaryPathFormula(subformula), context(context) {
-            // Intentionally left empty.
+        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) {
+            STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::ExpectedTime, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
         }
         
         bool EventuallyFormula::isEventuallyFormula() const {
-            return context == Context::Probability;
+            return context == FormulaContext::Probability;
         }
         
         bool EventuallyFormula::isReachabilityRewardFormula() const {
-            return context == Context::Reward;
+            return context == FormulaContext::Reward;
         }
         
         bool EventuallyFormula::isReachbilityExpectedTimeFormula() const {
-            return context == Context::ExpectedTime;
+            return context == FormulaContext::ExpectedTime;
         }
         
         bool EventuallyFormula::isProbabilityPathFormula() const {
@@ -37,7 +39,7 @@ namespace storm {
         }
         
         std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<EventuallyFormula>(this->getSubformula().substitute(substitution));
+            return std::make_shared<EventuallyFormula>(this->getSubformula().substitute(substitution), context);
         }
         
         std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {

src/logic/EventuallyFormula.h

@@ -2,14 +2,13 @@
 #define STORM_LOGIC_EVENTUALLYFORMULA_H_
 
 #include "src/logic/UnaryPathFormula.h"
+#include "src/logic/FormulaContext.h"
 
 namespace storm {
     namespace logic {
         class EventuallyFormula : public UnaryPathFormula {
-        public:
-            enum class Context { Probability, Reward, ExpectedTime };
-            
-            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, Context context = Context::Probability);
+        public:            
+            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context = FormulaContext::Probability);
             
             virtual ~EventuallyFormula() {
                 // Intentionally left empty.
@@ -29,7 +28,7 @@ namespace storm {
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
 
         private:
-            Context context;
+            FormulaContext context;
         };
     }
 }

src/logic/Formula.cpp

@@ -256,6 +256,14 @@ namespace storm {
             return dynamic_cast<EventuallyFormula const&>(*this);
         }
         
+        EventuallyFormula& Formula::asReachabilityRewardFormula() {
+            return dynamic_cast<EventuallyFormula&>(*this);
+        }
+        
+        EventuallyFormula const& Formula::asReachabilityRewardFormula() const {
+            return dynamic_cast<EventuallyFormula const&>(*this);
+        }
+        
         GloballyFormula& Formula::asGloballyFormula() {
             return dynamic_cast<GloballyFormula&>(*this);
         }
@@ -382,7 +390,7 @@ namespace storm {
             return;
         }
         
-        void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicExpressionFormulas) const {
+        void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
             return;
         }
         

src/logic/Formula.h

@@ -126,6 +126,9 @@ namespace storm {
             EventuallyFormula& asEventuallyFormula();
             EventuallyFormula const& asEventuallyFormula() const;
             
+            EventuallyFormula& asReachabilityRewardFormula();
+            EventuallyFormula const& asReachabilityRewardFormula() const;
+            
             GloballyFormula& asGloballyFormula();
             GloballyFormula const& asGloballyFormula() const;
             
@@ -178,7 +181,7 @@ namespace storm {
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
-            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicExpressionFormulas) const;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
             
         private:

src/logic/FormulaContext.h

@@ -0,0 +1,12 @@
+#ifndef STORM_LOGIC_FORMULACONTEXT_H_
+#define STORM_LOGIC_FORMULACONTEXT_H_
+
+namespace storm {
+    namespace logic {
+        
+        enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, ExpectedTime };
+        
+    }
+}
+
+#endif /* STORM_LOGIC_FORMULACONTEXT_H_ */

src/logic/FragmentChecker.cpp

@@ -68,11 +68,15 @@ namespace storm {
             bool result = true;
             if (f.isConditionalProbabilityFormula()) {
                 result = result && inherited.getSpecification().areConditionalProbabilityFormulasAllowed();
-            } else if (f.Formula::isConditionalRewardFormula()) {
+            } else if (f.isConditionalRewardFormula()) {
                 result = result && inherited.getSpecification().areConditionalRewardFormulasFormulasAllowed();
             }
             if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) {
-                result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
+                if (f.isConditionalProbabilityFormula()) {
+                    result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
+                } else if (f.isConditionalRewardFormula()) {
+                    result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula();
+                }
             }
             result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
             result = result && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
@@ -172,7 +176,7 @@ namespace storm {
         boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areRewardOperatorsAllowed();
-            result = result && f.getSubformula().isRewardPathFormula();
+            result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {

src/modelchecker/AbstractModelChecker.cpp

@@ -20,7 +20,7 @@ namespace storm {
                 if (formula.isProbabilityPathFormula()) {
                     return this->computeProbabilities(checkTask);
                 } else if (formula.isRewardPathFormula()) {
-                    return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula()));
+                    return this->computeRewards(checkTask);
                 }
             } else if (formula.isConditionalProbabilityFormula()) {
                 return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula()));
@@ -74,18 +74,20 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::PathFormula> const& checkTask) {
-            storm::logic::PathFormula const& rewardPathFormula = checkTask.getFormula();
-            if (rewardPathFormula.isCumulativeRewardFormula()) {
-                return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula()));
-            } else if (rewardPathFormula.isInstantaneousRewardFormula()) {
-                return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula()));
-            } else if (rewardPathFormula.isReachabilityRewardFormula()) {
-                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula()));
-            } else if (rewardPathFormula.isLongRunAverageRewardFormula()) {
-                return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula()));
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::Formula> const& checkTask) {
+            storm::logic::Formula const& rewardFormula = checkTask.getFormula();
+            if (rewardFormula.isCumulativeRewardFormula()) {
+                return this->computeCumulativeRewards(checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
+            } else if (rewardFormula.isInstantaneousRewardFormula()) {
+                return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
+            } else if (rewardFormula.isReachabilityRewardFormula()) {
+                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula()));
+            } else if (rewardFormula.isLongRunAverageRewardFormula()) {
+                return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
+            } else if (rewardFormula.isConditionalRewardFormula()) {
+                return this->computeConditionalRewards(checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
             }
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid.");
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
@@ -191,7 +193,7 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
             storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
+            std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");

src/modelchecker/AbstractModelChecker.h

@@ -44,7 +44,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask);
             
             // The methods to compute the rewards for path formulas.
-            virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::PathFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::Formula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -36,7 +36,7 @@ namespace storm {
         template<typename SparseDtmcModelType>
         bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
         }
         
         template<typename SparseDtmcModelType>
@@ -130,6 +130,21 @@ namespace storm {
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
+        template<typename SparseDtmcModelType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+            storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
+            STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+            STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+            
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeConditionalRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+        }
+        
         template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>;
     }
 }

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -25,11 +25,13 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
+
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
-            
+            virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
+
         private:
             // An object that is used for retrieving linear equation solvers.
             std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;

src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -46,7 +46,7 @@ namespace storm {
                 
                 return result;
             }
-        
+            
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // We need to identify the states which have to be taken out of the matrix, i.e.
@@ -154,7 +154,7 @@ namespace storm {
                 
                 return result;
             }
-
+            
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory);
@@ -170,7 +170,7 @@ namespace storm {
                                                   },
                                                   targetStates, qualitative, linearEquationSolverFactory);
             }
-          
+            
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                                 
@@ -222,23 +222,26 @@ namespace storm {
                 
                 return result;
             }
-
+            
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 return SparseCtmcCslHelper<ValueType>::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory);
             }
             
             template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeConditionalProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
-                std::vector<ValueType> probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory);
+            typename SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeBaierTransformation(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional<std::vector<ValueType>> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+                
+                BaierTransformedModel result;
                 
                 // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined.
-                storm::storage::BitVector beforeStates(targetStates.size(), true);
+                std::vector<ValueType> probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory);
+                
+                result.beforeStates = storm::storage::BitVector(targetStates.size(), true);
                 uint_fast64_t state = 0;
                 uint_fast64_t beforeStateIndex = 0;
                 for (auto const& value : probabilitiesToReachConditionStates) {
                     if (value == storm::utility::zero<ValueType>()) {
-                        beforeStates.set(state, false);
+                        result.beforeStates.set(state, false);
                     } else {
                         probabilitiesToReachConditionStates[beforeStateIndex] = value;
                         ++beforeStateIndex;
@@ -246,35 +249,33 @@ namespace storm {
                     ++state;
                 }
                 probabilitiesToReachConditionStates.resize(beforeStateIndex);
-
-                // If there were any before states, we can compute their conditional probabilities. If not, the result
-                // is undefined for all states.
-                std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::infinity<ValueType>());
+                
                 if (targetStates.empty()) {
-                    storm::utility::vector::setVectorValues(result, beforeStates, storm::utility::zero<ValueType>());
-                } else if (!beforeStates.empty()) {
+                    result.noTargetStates = true;
+                    return result;
+                } else if (!result.beforeStates.empty()) {
                     // If there are some states for which the conditional probability is defined and there are some
                     // states that can reach the target states without visiting condition states first, we need to
                     // do more work.
-
+                    
                     // First, compute the relevant states and some offsets.
                     storm::storage::BitVector allStates(targetStates.size(), true);
-                    std::vector<uint_fast64_t> numberOfBeforeStatesUpToState = beforeStates.getNumberOfSetBitsBeforeIndices();
+                    std::vector<uint_fast64_t> numberOfBeforeStatesUpToState = result.beforeStates.getNumberOfSetBitsBeforeIndices();
                     storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates);
                     statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates);
-                    uint_fast64_t normalStatesOffset = beforeStates.getNumberOfSetBits();
+                    uint_fast64_t normalStatesOffset = result.beforeStates.getNumberOfSetBits();
                     std::vector<uint_fast64_t> numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices();
                     
                     // All transitions going to states with probability zero, need to be redirected to a deadlock state.
                     bool addDeadlockState = false;
                     uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits();
-
+                    
                     // Now, we create the matrix of 'before' and 'normal' states.
                     storm::storage::SparseMatrixBuilder<ValueType> builder;
                     
                     // Start by creating the transitions of the 'before' states.
                     uint_fast64_t currentRow = 0;
-                    for (auto beforeState : beforeStates) {
+                    for (auto beforeState : result.beforeStates) {
                         if (conditionStates.get(beforeState)) {
                             // For condition states, we move to the 'normal' states.
                             ValueType zeroProbability = storm::utility::zero<ValueType>();
@@ -291,7 +292,7 @@ namespace storm {
                         } else {
                             // For non-condition states, we scale the probabilities going to other before states.
                             for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) {
-                                if (beforeStates.get(successorEntry.getColumn())) {
+                                if (result.beforeStates.get(successorEntry.getColumn())) {
                                     builder.addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()], successorEntry.getValue() * probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] / probabilitiesToReachConditionStates[currentRow]);
                                 }
                             }
@@ -320,21 +321,84 @@ namespace storm {
                     }
                     
                     // Build the new transition matrix and the new targets.
-                    storm::storage::SparseMatrix<ValueType> newTransitionMatrix = builder.build();
-                    storm::storage::BitVector newTargetStates = targetStates % beforeStates;
-                    newTargetStates.resize(newTransitionMatrix.getRowCount());
+                    result.transitionMatrix = builder.build();
+                    storm::storage::BitVector newTargetStates = targetStates % result.beforeStates;
+                    newTargetStates.resize(result.transitionMatrix.get().getRowCount());
                     for (auto state : targetStates % statesWithProbabilityGreater0) {
                         newTargetStates.set(normalStatesOffset + state, true);
                     }
+                    result.targetStates = std::move(newTargetStates);
+
+                    // If a reward model was given, we need to compute the rewards for the transformed model.
+                    if (stateRewards) {
+                        std::vector<ValueType> newStateRewards(result.beforeStates.getNumberOfSetBits());
+                        storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get());
+                        
+                        newStateRewards.reserve(newStateRewards.size() + statesWithProbabilityGreater0.getNumberOfSetBits() + 1);
+                        for (auto state : statesWithProbabilityGreater0) {
+                            newStateRewards.push_back(stateRewards.get()[state]);
+                        }
+                        // Add a zero reward to the deadlock state.
+                        newStateRewards.push_back(storm::utility::zero<ValueType>());
+                        result.stateRewards = std::move(newStateRewards);
+                    }
                     
-                    // Finally, compute the conditional probabiltities by a reachability query.
-                    std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), newTargetStates, qualitative, linearEquationSolverFactory);
-                    storm::utility::vector::setVectorValues(result, beforeStates, conditionalProbabilities);
                 }
-
+                
                 return result;
             }
-
+            
+            template<typename ValueType, typename RewardModelType>
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeConditionalProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+                
+                // Prepare result vector.
+                std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::infinity<ValueType>());
+                
+                if (!conditionStates.empty()) {
+                    BaierTransformedModel transformedModel = computeBaierTransformation(transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none, linearEquationSolverFactory);
+                    
+                    if (transformedModel.noTargetStates) {
+                        storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero<ValueType>());
+                    } else {
+                        // At this point, we do not need to check whether there are 'before' states, since the condition
+                        // states were non-empty so there is at least one state with a positive probability of satisfying
+                        // the condition.
+                        
+                        // Now compute reachability probabilities in the transformed model.
+                        storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix = transformedModel.transitionMatrix.get();
+                        std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory);
+                        storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities);
+                    }
+                }
+                
+                return result;
+            }
+            
+            template<typename ValueType, typename RewardModelType>
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeConditionalRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+                // Prepare result vector.
+                std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::infinity<ValueType>());
+                
+                if (!conditionStates.empty()) {
+                    BaierTransformedModel transformedModel = computeBaierTransformation(transitionMatrix, backwardTransitions, targetStates, conditionStates, rewardModel.getTotalRewardVector(transitionMatrix), linearEquationSolverFactory);
+                    
+                    if (transformedModel.noTargetStates) {
+                        storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero<ValueType>());
+                    } else {
+                        // At this point, we do not need to check whether there are 'before' states, since the condition
+                        // states were non-empty so there is at least one state with a positive probability of satisfying
+                        // the condition.
+                        
+                        // Now compute reachability probabilities in the transformed model.
+                        storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix = transformedModel.transitionMatrix.get();
+                        std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory);
+                        storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities);
+                    }
+                }
+                
+                return result;
+            }
+            
             template class SparseDtmcPrctlHelper<double>;
         }
     }

src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

@@ -39,8 +39,20 @@ namespace storm {
                 
                 static std::vector<ValueType> computeConditionalProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
+                static std::vector<ValueType> computeConditionalRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+                
             private:
                 static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+                
+                struct BaierTransformedModel {
+                    storm::storage::BitVector beforeStates;
+                    boost::optional<storm::storage::SparseMatrix<ValueType>> transitionMatrix;
+                    boost::optional<storm::storage::BitVector> targetStates;
+                    boost::optional<std::vector<ValueType>> stateRewards;
+                    bool noTargetStates;
+                };
+                
+                static BaierTransformedModel computeBaierTransformation(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional<std::vector<ValueType>> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
             };
             
         }

src/parser/FormulaParser.cpp

@@ -105,8 +105,8 @@ namespace storm {
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simpleFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> stateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormulaWithoutUntil;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> pathFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simplePathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> operatorFormula;
@@ -120,11 +120,11 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expressionFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
             
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::ConditionalFormula::Context), Skipper> conditionalFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::EventuallyFormula::Context), Skipper> eventuallyFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> nextFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> globallyFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> untilFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> conditionalFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> eventuallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> nextFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> globallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::FormulaContext), Skipper> untilFormula;
             qi::rule<Iterator, boost::variant<std::pair<double, double>, uint_fast64_t>(), Skipper> timeBound;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardPathFormula;
@@ -142,11 +142,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
             std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
             std::shared_ptr<storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const;
-            std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
-            std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::ConditionalFormula::Context context) const;
+            std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::FormulaContext context) const;
             std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
             std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
@@ -253,7 +253,7 @@ namespace storm {
             cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
             cumulativeRewardFormula.name("cumulative reward formula");
             
-            rewardPathFormula = eventuallyFormula(storm::logic::EventuallyFormula::Context::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(storm::logic::ConditionalFormula::Context::Reward);
+            rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula;
             rewardPathFormula.name("reward path formula");
             
             expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
@@ -277,28 +277,28 @@ namespace storm {
             notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
             notStateFormula.name("negation formula");
             
-            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
+            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
             eventuallyFormula.name("eventually formula");
             
-            globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
+            globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
             globallyFormula.name("globally formula");
             
-            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
+            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
             nextFormula.name("next formula");
             
-            pathFormulaWithoutUntil = eventuallyFormula(storm::logic::EventuallyFormula::Context::Probability) | globallyFormula | nextFormula | stateFormula;
+            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
             pathFormulaWithoutUntil.name("path formula");
             
-            untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
             untilFormula.name("until formula");
             
-            conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
+            conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
             conditionalFormula.name("conditional formula");
             
             timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") >  qi::uint_)[qi::_val = qi::_1];
             timeBound.name("time bound");
             
-            pathFormula = conditionalFormula(storm::logic::ConditionalFormula::Context::Probability);
+            pathFormula = conditionalFormula(qi::_r1);
             pathFormula.name("path formula");
             
             operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
@@ -313,10 +313,10 @@ namespace storm {
             rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
             rewardOperator.name("reward operator");
             
-            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::EventuallyFormula::Context::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             expectedTimeOperator.name("expected time operator");
             
-            probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
             
             andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
@@ -342,10 +342,10 @@ namespace storm {
             debug(longRunAverageOperator);
             debug(pathFormulaWithoutUntil);
             debug(pathFormula);
-            debug(conditionalFormula);
+//            debug(conditionalFormula);
             debug(nextFormula);
             debug(globallyFormula);
-            debug(eventuallyFormula);
+//            debug(eventuallyFormula);
             debug(atomicStateFormula);
             debug(booleanLiteralFormula);
             debug(labelFormula);
@@ -421,7 +421,7 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula> const& subformula) const {
             if (timeBound) {
                 if (timeBound.get().which() == 0) {
                     std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
@@ -455,7 +455,7 @@ namespace storm {
             }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::ConditionalFormula::Context context) const {
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::FormulaContext context) const {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
         }