From d4cd58e9c63ee80d43aaf537b41d225d2b721a37 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 26 Aug 2015 18:36:42 +0200
Subject: [PATCH] upon preserving a new formula, the builders now do not apply
 terminal states

Former-commit-id: b6a5d04cd02870917b27e8ef7374edd2bba5b9ed
---
 src/builder/DdPrismModelBuilder.cpp       | 5 +++++
 src/builder/ExplicitPrismModelBuilder.cpp | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 2815bde0b..9098f285f 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -217,6 +217,11 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         void DdPrismModelBuilder<Type>::Options::preserveFormula(storm::logic::Formula const& formula) {
+            // If we already had terminal states, we need to erase them.
+            if (terminalStates) {
+                terminalStates.reset();
+            }
+
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
                 if (formula.containsRewardOperator()) {
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index fcffe1344..cf02700eb 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -156,6 +156,11 @@ namespace storm {
 
         template <typename ValueType, typename IndexType>
         void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
+            // If we already had terminal states, we need to erase them.
+            if (terminalStates) {
+                terminalStates.reset();
+            }
+            
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
                 if (formula.containsRewardOperator()) {