From 3849c59d6b402678a288166feabd87d2794f08be Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 26 Aug 2015 16:44:21 +0200
Subject: [PATCH] formula parser now correctly accepts variables of a loaded
 model

Former-commit-id: 9d6312b529bd47f4a3a229ed59433d9cd5882880
---
 src/builder/DdPrismModelBuilder.cpp | 18 ++++++++++--------
 src/utility/cli.cpp                 |  2 +-
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 41adb09a2..2815bde0b 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -1017,13 +1017,6 @@ namespace storm {
             ModuleDecisionDiagram const& globalModule = system.globalModule;
             storm::dd::Add<Type> stateActionDd = system.stateActionDd;
             
-            // Cut the transitions and rewards to the reachable fragment of the state space.
-            storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
-            storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
-            if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
-            }
-            
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
             if (options.terminalStates) {
                 storm::expressions::Expression terminalExpression;
@@ -1033,7 +1026,16 @@ namespace storm {
                     std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
                     terminalExpression = preparedProgram.getLabelExpression(labelName);
                 }
-                // TODO
+                STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+                storm::dd::Add<Type> terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
+                transitionMatrix *= !terminalStatesAdd;
+            }
+            
+            // Cut the transitions and rewards to the reachable fragment of the state space.
+            storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
+            storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
+            if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
+                transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
             }
             
             storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp
index 219e566ae..d21e21420 100644
--- a/src/utility/cli.cpp
+++ b/src/utility/cli.cpp
@@ -222,7 +222,7 @@ namespace storm {
                 if (settings.isPropertySet()) {
                     storm::parser::FormulaParser formulaParser;
                     if (program) {
-                        storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
+                        storm::parser::FormulaParser formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer());
                     }
                     
                     // If the given property looks like a file (containing a dot and there exists a file with that name),