From ac1ca72094e52fb92e8de988db0eba21f5f2f99f Mon Sep 17 00:00:00 2001
From: JK <klein@tcs.inf.tu-dresden.de>
Date: Thu, 2 Feb 2017 09:57:54 +0100
Subject: [PATCH] Add support for ITE expression in the likelihood part of
 commands (exact, parametric engine)

Support the conversion to rational numbers / rational functions for ITE expressions. Example:

 ... ->  (s<4 ? p : q):(s'=...)

where s is a state variable and p, q are constants or parameters.
---
 src/storm/storage/expressions/ExpressionEvaluator.cpp |  4 ++--
 .../storage/expressions/ToRationalFunctionVisitor.cpp | 11 ++++++++---
 .../storage/expressions/ToRationalFunctionVisitor.h   |  6 +++++-
 .../storage/expressions/ToRationalNumberVisitor.cpp   | 11 ++++++++---
 .../storage/expressions/ToRationalNumberVisitor.h     |  6 +++++-
 5 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/src/storm/storage/expressions/ExpressionEvaluator.cpp b/src/storm/storage/expressions/ExpressionEvaluator.cpp
index abea0ce73..3305ec772 100644
--- a/src/storm/storage/expressions/ExpressionEvaluator.cpp
+++ b/src/storm/storage/expressions/ExpressionEvaluator.cpp
@@ -33,7 +33,7 @@ namespace storm {
         }
 
 #ifdef STORM_HAVE_CARL
-        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager) {
+        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager), rationalNumberVisitor(*this) {
             // Intentionally left empty.
         }
 
@@ -57,7 +57,7 @@ namespace storm {
             return this->rationalNumberVisitor.toRationalNumber(expression);
         }
         
-        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
+        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager), rationalFunctionVisitor(*this) {
             // Intentionally left empty.
         }
         
diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
index 9f8ab16ec..6fa620157 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -11,7 +11,7 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
         template<typename RationalFunctionType>
-        ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
+        ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator) : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()), evaluator(evaluator) {
             // Intentionally left empty.
         }
         
@@ -21,8 +21,13 @@ namespace storm {
         }
         
         template<typename RationalFunctionType>
-        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            bool conditionValue = evaluator.asBool(expression.getCondition());
+            if (conditionValue) {
+                return expression.getThenExpression()->accept(*this, data);
+            } else {
+                return expression.getElseExpression()->accept(*this, data);
+            }
         }
         
         template<typename RationalFunctionType>
diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.h b/src/storm/storage/expressions/ToRationalFunctionVisitor.h
index 7c7cfacf5..6e90d36ce 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.h
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.h
@@ -8,6 +8,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
 #include "storm/storage/expressions/Variable.h"
 
 namespace storm {
@@ -17,7 +18,7 @@ namespace storm {
         template<typename RationalFunctionType>
         class ToRationalFunctionVisitor : public ExpressionVisitor {
         public:
-            ToRationalFunctionVisitor();
+            ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator);
             
             RationalFunctionType toRationalFunction(Expression const& expression);
             
@@ -53,6 +54,9 @@ namespace storm {
             
             // A mapping from variables to their values.
             std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping;
+
+            // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+            ExpressionEvaluatorBase<RationalFunctionType> const& evaluator;
         };
 #endif
     }
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
index d4ba17c06..26ad15b5a 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
@@ -8,7 +8,7 @@
 namespace storm {
     namespace expressions {
         template<typename RationalNumberType>
-        ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor() : ExpressionVisitor() {
+        ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator) : ExpressionVisitor(), evaluator(evaluator) {
             // Intentionally left empty.
         }
         
@@ -18,8 +18,13 @@ namespace storm {
         }
         
         template<typename RationalNumberType>
-        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
+        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            bool conditionValue = evaluator.asBool(expression.getCondition());
+            if (conditionValue) {
+                return expression.getThenExpression()->accept(*this, data);
+            } else {
+                return expression.getElseExpression()->accept(*this, data);
+            }
         }
         
         template<typename RationalNumberType>
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h
index 6177fd2ae..89cb9f81f 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.h
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h
@@ -7,6 +7,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
 #include "storm/storage/expressions/Variable.h"
 
 namespace storm {
@@ -15,7 +16,7 @@ namespace storm {
         template<typename RationalNumberType>
         class ToRationalNumberVisitor : public ExpressionVisitor {
         public:
-            ToRationalNumberVisitor();
+            ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator);
             
             RationalNumberType toRationalNumber(Expression const& expression);
             
@@ -34,6 +35,9 @@ namespace storm {
             
         private:
             std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping;
+
+            // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+            ExpressionEvaluatorBase<RationalNumberType> const& evaluator;
         };
     }
 }