From 240faff1250c9469099e13aacca306bfc3c9c910 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Sun, 2 Dec 2018 17:46:08 +0100
Subject: [PATCH] BuilderOptions: Added terminal states for bounded until and
 reachability reward formulas.

---
 src/storm/builder/BuilderOptions.cpp | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp
index 8ea24379d..9a5b4737c 100644
--- a/src/storm/builder/BuilderOptions.cpp
+++ b/src/storm/builder/BuilderOptions.cpp
@@ -115,9 +115,35 @@ namespace storm {
                 } else if (left.isAtomicLabelFormula()) {
                     addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false);
                 }
+            } else if (formula.isBoundedUntilFormula()) {
+                storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula();
+                bool hasLowerBound = false;
+                for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) {
+                    if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) {
+                        hasLowerBound = true;
+                        break;
+                    }
+                }
+                if (!hasLowerBound) {
+                    storm::logic::Formula const& right = boundedUntil.getRightSubformula();
+                    if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
+                        this->setTerminalStatesFromFormula(right);
+                    }
+                }
+                storm::logic::Formula const& left = boundedUntil.getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false);
+                } else if (left.isAtomicLabelFormula()) {
+                    addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false);
+                }
             } else if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
-                if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
+                if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) {
+                    this->setTerminalStatesFromFormula(sub);
+                }
+            } else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) {
+                storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula();
+                if (sub.isEventuallyFormula()) {
                     this->setTerminalStatesFromFormula(sub);
                 }
             }