Fixed issue where variable names were reserved symbols of Exprtk

CHANGELOG.md

@@ -13,6 +13,7 @@ Long run average computation via ValueIteration, LP based MDP model checking, pa
 - storm-cli-utilities now contains cli related stuff, instead of storm-lib
 - storm-pars: support for welldefinedness constraints in mdps.
 - symbolic (MT/BDD) bisimulation 
+- Fixed issue related to variable names that can not be used in Exprtk.
 
 ### Version 1.1.0 (2017/8)
 

src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp

@@ -1,3 +1,5 @@
+#include <string>
+
 #include "storm/storage/expressions/ExprtkExpressionEvaluator.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
@@ -13,11 +15,11 @@ namespace storm {
 
             for (auto const& variableTypePair : manager) {
                 if (variableTypePair.second.isBooleanType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->booleanValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isIntegerType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->integerValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isRationalType()) {
-                    symbolTable->add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->rationalValues[variableTypePair.first.getOffset()]);
                 }
             }
         }

src/storm/storage/expressions/ToExprtkStringVisitor.cpp

@@ -167,7 +167,7 @@ namespace storm {
         }
         
         boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const&) {
-            stream << expression.getVariableName();
+            stream << "v" + std::to_string(expression.getVariable().getIndex());
             return boost::any();
         }