diff --git a/CMakeLists.txt b/CMakeLists.txt
index 57e94b8b8..2f4aa6536 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -295,7 +295,7 @@ SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
 ##
 #############################################################
 if ("${CMAKE_GENERATOR}" STREQUAL "Xcode")
-	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++11")
+	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++14")
 	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++")
 endif()
 
diff --git a/resources/3rdparty/exprtk/exprtk.hpp b/resources/3rdparty/exprtk/exprtk.hpp
index 079ee1b6f..a86c45509 100755
--- a/resources/3rdparty/exprtk/exprtk.hpp
+++ b/resources/3rdparty/exprtk/exprtk.hpp
@@ -99,7 +99,7 @@ namespace exprtk
             return (('a' <= c) && (c <= 'z')) ||
             (('A' <= c) && (c <= 'Z'))
 #ifdef MODIFICATION
-            || ('.' == c) || ('_' == c)
+            || ('_' == c)
 #endif
             ;
         }
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index d743d9ced..4101359d3 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -186,7 +186,7 @@ namespace storm {
                     return std::make_shared<storm::logic::AtomicLabelFormula>(propertyStructure.get<std::string>());
                 }
             }
-            storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true);
+            storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), true);
             if(expr.isInitialized()) {
                 assert(bound == boost::none);
                 return std::make_shared<storm::logic::AtomicExpressionFormula>(expr);
diff --git a/src/storm/parser/JaniParser.h b/src/storm/parser/JaniParser.h
index 627a056dd..2ac6c8366 100644
--- a/src/storm/parser/JaniParser.h
+++ b/src/storm/parser/JaniParser.h
@@ -59,8 +59,8 @@ namespace storm {
              */
             void parseActions(json const& actionStructure, storm::jani::Model& parentModel);
             std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none);
-            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
-            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
+            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
+            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
 
             std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext,  std::string const& opstring, std::string const& context);
             std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context);
@@ -68,7 +68,7 @@ namespace storm {
                 
             
             std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
-            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
+            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>());
 
             
             /**
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index 5dfbd2b4a..9dcd7f1ea 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -5,12 +5,42 @@
 #include "storm/storage/dd/Bdd.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
-
 #include "storm/models/sparse/StandardRewardModel.h"
 
 namespace storm {
     namespace transformer {
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
+            storm::dd::Odd odd = symbolicDtmc.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicDtmc.getRewardModels()) {
+                boost::optional<std::vector<ValueType>> stateRewards;
+                boost::optional<std::vector<ValueType>> stateActionRewards;
+                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
+                if (rewardModelNameAndModel.second.hasStateRewards()) {
+                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
+                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
+                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
+
+            labelling.addLabel("init", symbolicDtmc.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicDtmc.getLabels()) {
+                labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Dtmc<ValueType>>(transitionMatrix, labelling, rewardModels);
+        }
+
         template<storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(
                 storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp) {
@@ -40,11 +70,44 @@ namespace storm {
                 labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
             }
             return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
+        }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc) {
+            storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicCtmc.getRewardModels()) {
+                boost::optional<std::vector<ValueType>> stateRewards;
+                boost::optional<std::vector<ValueType>> stateActionRewards;
+                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
+                if (rewardModelNameAndModel.second.hasStateRewards()) {
+                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
+                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
+                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
 
+            labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicCtmc.getLabels()) {
+                labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
+        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, double>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h
index 7ea46fff4..414d4454b 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.h
+++ b/src/storm/transformer/SymbolicToSparseTransformer.h
@@ -1,15 +1,31 @@
 #pragma once
 
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/symbolic/Ctmc.h"
 
 namespace storm {
     namespace transformer {
 
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicDtmcToSparseDtmcTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc);
+        };
+        
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicMdpToSparseMdpTransformer {
         public:
             static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
         };
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicCtmcToSparseCtmcTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc);
+        };
     }
 }
diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index bedaf086d..e9a04f187 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -68,7 +68,7 @@ namespace storm {
                     for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
                         // Only explore the state if the transition was actually there and the successor has not yet
                         // been visited.
-                        if (!storm::utility::isZero(successor.getValue()) && !reachableStates.get(successor.getColumn()) || (useStepBound && remainingSteps[successor.getColumn()] < currentStepBound - 1)) {
+                        if (!storm::utility::isZero(successor.getValue()) && (!reachableStates.get(successor.getColumn()) || (useStepBound && remainingSteps[successor.getColumn()] < currentStepBound - 1))) {
                             // If the successor is one of the target states, we need to include it, but must not explore
                             // it further.
                             if (targetStates.get(successor.getColumn())) {