more work on jit-based model builder

Former-commit-id: 150ac22d6b [formerly 85061a73c7]
Former-commit-id: cd18eec45b

src/builder/ExplicitJitJaniModelBuilder.cpp

@@ -2,74 +2,679 @@
 
 #include <iostream>
 #include <cstdio>
+#include <chrono>
 
-#include "cpptempl.h"
+#include "src/adapters/CarlAdapter.h"
+
+#include "src/solver/SmtSolver.h"
 
 #include "src/utility/macros.h"
+#include "src/utility/solver.h"
 #include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/NotSupportedException.h"
+#include "src/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace builder {
         
         static const std::string CXX_COMPILER = "clang++";
         static const std::string DYLIB_EXTENSION = ".dylib";
-        static const std::string COMPILER_FLAGS = "-std=c++11 -stdlib=libc++ -fPIC -O3 -shared";
-        static const std::string STORM_ROOT = "/Users/chris/work/storm2";
-        static const std::string BOOST_ROOT = "/usr/local/Cellar/boost/1.61.0_1/include";
+        static const std::string COMPILER_FLAGS = "-std=c++11 -stdlib=libc++ -fPIC -O3 -shared -funroll-loops -undefined dynamic_lookup";
+        static const std::string STORM_ROOT = "/Users/chris/work/storm";
+        static const std::string L3PP_ROOT = "/Users/chris/work/storm/resources/3rdparty/l3pp";
+        static const std::string BOOST_ROOT = "/usr/local/Cellar/boost/1.62.0/include";
+        static const std::string GMP_ROOT = "/usr/local/Cellar/gmp/6.1.1";
+        static const std::string CARL_ROOT = "/Users/chris/work/carl";
+        static const std::string CLN_ROOT = "/usr/local/Cellar/cln/1.3.4";
+        static const std::string GINAC_ROOT = "/usr/local/Cellar/ginac/1.6.7_1";
         
-        template <typename ValueType>
-        ExplicitJitJaniModelBuilder<ValueType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model) : model(model) {
+        template <typename ValueType, typename RewardModelType>
+        ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model) : model(model) {
             // Intentionally left empty.
         }
         
-        template <typename ValueType>
-        std::string ExplicitJitJaniModelBuilder<ValueType>::createSourceCode() {
+        template <typename ValueType, typename RewardModelType>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createSourceCode() {
             std::string sourceTemplate = R"(
             
-            #include <cstdint>
-            #include <iostream>
-            #include <boost/dll/alias.hpp>
+#define NDEBUG
+            
+#include <cstdint>
+#include <iostream>
+#include <vector>
+#include <cmath>
+#include <unordered_map>
+#include <boost/dll/alias.hpp>
+
+#include "resources/3rdparty/sparsepp/sparsepp.h"
+
+#include "src/builder/JitModelBuilderInterface.h"
+#include "src/storage/SparseMatrix.h"
+#include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/StandardRewardModel.h"
+            
+namespace storm {
+    namespace builder {
+        
+        typedef uint32_t IndexType;
+
+        struct StateType {
+            // Boolean variables.
+            {% for variable in stateVariables.boolean %}bool {$variable.name} : 1;
+            {% endfor %}
+            // Bounded integer variables.
+            {% for variable in stateVariables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits};
+            {% endfor %}
+            // Location variables.
+            {% for variable in stateVariables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits};
+            {% endfor %}
+        };
+        
+        bool operator==(StateType const& first, StateType const& second) {
+            bool result = true;
+            {% for variable in stateVariables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name});
+            {% endfor %}
+            {% for variable in stateVariables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name};
+            {% endfor %}
+            {% for variable in stateVariables.locations %}result &= first.{$variable.name} == second.{$variable.name};
+            {% endfor %}
+            return result;
+        }
+        
+        std::ostream& operator<<(std::ostream& out, StateType const& state) {
+            out << "<";
+            {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << state.{$variable.name} << ", ";
+            {% endfor %}
+            {% for variable in stateVariables.boundedInteger %}out << "{$variable.name}=" << state.{$variable.name} << ", ";
+            {% endfor %}
+            {% for variable in stateVariables.locations %}out << "{$variable.name}=" << state.{$variable.name} << ", ";
+            {% endfor %}
+            out << ">";
+            return out;
+        }
+        
+    }
+}
+
+namespace std {
+    template <>
+    struct hash<storm::builder::StateType> {
+        std::size_t operator()(storm::builder::StateType const& state) const {
+            // Note: this is faster than viewing the struct as a bit field and taking hash_combine of the bytes.
+            std::size_t seed = 0;
+            {% for variable in stateVariables.boolean %}spp::hash_combine(seed, state.{$variable.name});
+            {% endfor %}
+            {% for variable in stateVariables.boundedInteger %}spp::hash_combine(seed, state.{$variable.name});
+            {% endfor %}
+            {% for variable in stateVariables.locations %}spp::hash_combine(seed, state.{$variable.name});
+            {% endfor %}
+            return seed;
+        }
+    };
+}
+            
+namespace storm {
+    namespace builder {
+    
+        typedef double ValueType;
+        
+        static bool model_is_deterministic() {
+            return {$deterministic_model};
+        }
+        
+        static bool model_is_discrete_time() {
+            return {$discrete_time_model};
+        }
+        
+        class Entry {
+        public:
+            Entry() : column(0), value(0) {
+                // Intentionally left empty.
+            }
+            
+            Entry(IndexType const& column, ValueType const& value) : column(column), value(value) {
+                // Intentionally left empty.
+            }
+            
+            IndexType const& getColumn() const {
+                return column;
+            }
+            
+            ValueType const& getValue() const {
+                return value;
+            }
+            
+            void addToValue(ValueType const& value) {
+                this->value += value;
+            }
+            
+            void scaleValue(ValueType const& divisor) {
+                this->value /= divisor;
+            }
+            
+        private:
+            IndexType column;
+            ValueType value;
+        };
+        
+        class Choice {
+        public:
+            typedef std::vector<Entry> ContainerType;
+            
+            void add(IndexType const& stateIndex, ValueType const& value) {
+                distribution.push_back(Entry(stateIndex, value));
+            }
+
+            void add(Choice&& choice) {
+                distribution.insert(distribution.end(), std::make_move_iterator(choice.getDistribution().begin()), std::make_move_iterator(choice.getDistribution().end()));
+            }
+
+            void makeUniqueAndShrink() {
+                std::sort(distribution.begin(), distribution.end(),
+                          [] (Entry const& a, Entry const& b) {
+                              return a.getColumn() < b.getColumn();
+                          }
+                          );
+                
+                // Code taken from std::unique and modified to fit needs.
+                auto first = distribution.begin();
+                auto last = distribution.end();
+                
+                if (first != last) {
+                    auto result = first;
+                    while (++first != last) {
+                        if (!(result->getColumn() == first->getColumn())) {
+                            if (++result != first) {
+                                *result = std::move(*first);
+                            }
+                        } else {
+                            result->addToValue(first->getValue());
+                        }
+                    }
+                    ++result;
+                    
+                    distribution.resize(std::distance(distribution.begin(), result));
+                }
+            }
+            
+            ContainerType const& getDistribution() const {
+                return distribution;
+            }
+            
+            ContainerType& getDistribution() {
+                return distribution;
+            }
             
-            #include "src/builder/JitModelBuilderInterface.h"
-            #include "resources/3rdparty/sparsepp/sparsepp.h"
+        private:
+            ContainerType distribution;
+        };
+        
+        class StateSet {
+        public:
+            StateType const& peek() const {
+                return storage.back();
+            }
+            
+            StateType get() {
+                StateType result = std::move(storage.back());
+                storage.pop_back();
+                return result;
+            }
+            
+            void add(StateType const& state) {
+                storage.push_back(state);
+            }
             
-            namespace storm {
-                namespace builder {
+            bool empty() const {
+                return storage.empty();
+            }
+            
+        private:
+            std::vector<StateType> storage;
+        };
+        
+        struct ModelComponents {
+            ModelComponents() : transitionMatrixBuilder(0, 0, 0, true, !model_is_deterministic()), stateLabeling(), rewardModels(), choiceLabeling() {
+                // Intentionally left empty.
+            }
+            
+            storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder;
+            storm::models::sparse::StateLabeling stateLabeling;
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
+            
+            storm::models::sparse::Model<ValueType>* createModel() {
+                if (model_is_discrete_time()) {
+                    if (model_is_deterministic()) {
+                        return new storm::models::sparse::Dtmc<ValueType>(std::move(this->transitionMatrixBuilder.build()), std::move(this->stateLabeling), std::move(this->rewardModels), std::move(this->choiceLabeling));
+                    } else {
+                        return nullptr;
+                    }
+                } else {
+                    return nullptr;
+                }
+            }
+        };
                     
-                    struct StateType {
-                        {% for stateVariable in stateVariables %}int64_t {$stateVariable.name} : {$stateVariable.bitwidth};{% endfor %}
-                    };
+        class JitBuilder : public JitModelBuilderInterface<ValueType> {
+        public:
+            JitBuilder() : currentRow(0), modelComponents() {
+                {% for state in initialStates %}{
+                    StateType state;
+                    {% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
+                    {% endfor %}initialStates.push_back(state);
+                }
+                {% endfor %}
+            }
+            
+            virtual storm::models::sparse::Model<ValueType>* build() override {
+                std::cout << "starting building process" << std::endl;
+                explore(initialStates);
+                std::cout << "finished building process with " << stateIds.size() << " states" << std::endl;
+                return modelComponents.createModel();
+            }
+            
+            void explore(std::vector<StateType> const& initialStates) {
+                for (auto const& state : initialStates) {
+                    explore(state);
+                }
+            }
+            
+            void explore(StateType const& initialState) {
+                StateSet statesToExplore;
+                getOrAddIndex(initialState, statesToExplore);
+
+                std::vector<Choice> choices;
+                while (!statesToExplore.empty()) {
+                    StateType currentState = statesToExplore.get();
+                    IndexType currentIndex = getIndex(currentState);
+#ifndef NDEBUG
+                    std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl;
+#endif
+                    
+                    exploreNonSynchronizingEdges(currentState, currentIndex, choices, statesToExplore);
+                    
+                    addChoicesForState(currentIndex, choices);
+                    choices.clear();
+                }
+            }
+            
+            void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, std::vector<Choice>& choices, StateSet& statesToExplore) {
+                {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) {
+                    choices.emplace_back();
+                    {% for destination in edge.destinations %}{
+                        StateType targetState(sourceState);
+                        {% for assignment in destination.nonTransientAssignments %}targetState.{$assignment.variable} = {$assignment.value};
+                        {% endfor %}
+                        IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);
+                        choices.back().add(targetStateIndex, {$destination.value});
+                    }
+                    {% endfor %}
+                }
+                {% endfor %}
+            }
+            
+            void addChoicesForState(IndexType const& stateId, std::vector<Choice>& choices) {
+                // If there is more than one choice in a deterministic model, we need to combine the choices into one
+                // global choice.
+                bool choiceIsGuaranteedDistribution = false;
+                if (model_is_deterministic() && choices.size() > 1) {
+                    uint64_t choiceCount = choices.size();
+                    
+                    // We do this by adding the entries of choices after the first one to the first one and then making
+                    // the distribution unique again.
+                    for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) {
+                        choices.front().add(std::move(*it));
+                    }
+                    choices.resize(1);
+                    choices.front().makeUniqueAndShrink();
                     
-                    class JitBuilder : public JitModelBuilderInterface<double> {
-                    public:
-                        JitBuilder() {
-                            // Intentionally left empty.
+                    // If we are dealing with a discrete-time model, we need to scale the probabilities such that they
+                    // form a probability distribution.
+                    if (model_is_discrete_time()) {
+                        for (auto& element : choices.front().getDistribution()) {
+                            element.scaleValue(choiceCount);
                         }
+                    }
+                    choiceIsGuaranteedDistribution = true;
+                }
+                
+                for (auto& choice : choices) {
+                    if (!choiceIsGuaranteedDistribution) {
+                        // Create a proper distribution without duplicate entries.
+                        choice.makeUniqueAndShrink();
+                    }
+                    
+                    // Add the elements to the transition matrix.
+                    for (auto const& element : choice.getDistribution()) {
+                        modelComponents.transitionMatrixBuilder.addNextValue(currentRow, element.getColumn(), element.getValue());
+                    }
+                    
+                    // Proceed to next row.
+                    ++currentRow;
+                }
+            }
+            
+            IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) {
+                auto it = stateIds.find(state);
+                if (it != stateIds.end()) {
+                    return it->second;
+                } else {
+                    IndexType newIndex = static_cast<IndexType>(stateIds.size());
+                    stateIds.insert(std::make_pair(state, newIndex));
+#ifndef NDEBUG
+                    std::cout << "inserting state " << state << std::endl;
+#endif
+                    statesToExplore.add(state);
+                    return newIndex;
+                }
+            }
+            
+            IndexType getIndex(StateType const& state) const {
+                auto it = stateIds.find(state);
+                if (it != stateIds.end()) {
+                    return it->second;
+                } else {
+                    return stateIds.at(state);
+                }
+            }
+            
+            static JitModelBuilderInterface<ValueType>* create() {
+                return new JitBuilder();
+            }
                         
-                        virtual void build() override {
-                            std::cout << "building in progress" << std::endl;
-                        }
+            private:
+                spp::sparse_hash_map<StateType, IndexType> stateIds;
+                std::vector<StateType> initialStates;
+            
+                uint64_t currentRow;
+                ModelComponents modelComponents;
+            };
+        
+        BOOST_DLL_ALIAS(storm::builder::JitBuilder::create, create_builder)
+                    
+    }
+}
+)";
+            
+            cpptempl::data_map modelData;
+            modelData["stateVariables"] = generateStateVariables();
+            cpptempl::data_list initialStates = generateInitialStates();
+            modelData["initialStates"] = cpptempl::make_data(initialStates);
+            cpptempl::data_list nonSynchronizingEdges = generateNonSynchronizingEdges();
+            modelData["nonSynchronizingEdges"] = cpptempl::make_data(nonSynchronizingEdges);
+            modelData["deterministic_model"] = model.isDeterministicModel() ? "true" : "false";
+            modelData["discrete_time_model"] = model.isDiscreteTimeModel() ? "true" : "false";
+            return cpptempl::parse(sourceTemplate, modelData);
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateInitialStates() {
+            cpptempl::data_list initialStates;
+            
+            // Prepare an SMT solver to enumerate all initial states.
+            storm::utility::solver::SmtSolverFactory factory;
+            std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(model.getExpressionManager());
+            
+            std::vector<storm::expressions::Expression> rangeExpressions = model.getAllRangeExpressions();
+            for (auto const& expression : rangeExpressions) {
+                solver->add(expression);
+            }
+            solver->add(model.getInitialStatesExpression(true));
+            
+            // Proceed as long as the solver can still enumerate initial states.
+            while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
+                // Create fresh state.
+                cpptempl::data_list initialStateAssignment;
+                
+                // Read variable assignment from the solution of the solver. Also, create an expression we can use to
+                // prevent the variable assignment from being enumerated again.
+                storm::expressions::Expression blockingExpression;
+                std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
+                for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) {
+                    storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable();
+                    bool variableValue = model->getBooleanValue(expressionVariable);
+                    initialStateAssignment.push_back(generateAssignment(variable, variableValue));
+                    
+                    storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable;
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                }
+                for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) {
+                    storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable();
+                    int_fast64_t variableValue = model->getIntegerValue(expressionVariable);
+                    initialStateAssignment.push_back(generateAssignment(variable, variableValue));
+                    
+                    storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue);
+                    blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                }
+                for (auto const& automaton : this->model.getAutomata()) {
+                    for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+                        storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable();
+                        bool variableValue = model->getBooleanValue(expressionVariable);
+                        initialStateAssignment.push_back(generateAssignment(variable, variableValue));
                         
-                        static JitModelBuilderInterface<double>* create() {
-                            return new JitBuilder();
-                        }
+                        storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable;
+                        blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    }
+                    for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                        storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable();
+                        int_fast64_t variableValue = model->getIntegerValue(expressionVariable);
+                        initialStateAssignment.push_back(generateAssignment(variable, variableValue));
                         
-                    private:
-                        spp::sparse_hash_map<StateType, uint32_t> stateIds;
-                    };
+                        storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue);
+                        blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
+                    }
+                }
+                
+                // Gather iterators to the initial locations of all the automata.
+                std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
+                for (auto const& automaton : this->model.getAutomata()) {
+                    initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin());
+                }
+                
+                // Now iterate through all combinations of initial locations.
+                while (true) {
+                    cpptempl::data_list completeAssignment(initialStateAssignment);
+                    
+                    for (uint64_t index = 0; index < initialLocationsIterators.size(); ++index) {
+                        storm::jani::Automaton const& automaton = this->model.getAutomata()[index];
+                        if (automaton.getNumberOfLocations() > 1) {
+                            completeAssignment.push_back(generateLocationAssignment(automaton, *initialLocationsIterators[index]));
+                        }
+                    }
+                    initialStates.push_back(cpptempl::make_data(completeAssignment));
                     
-                    BOOST_DLL_ALIAS(storm::builder::JitBuilder::create, create_builder)
+                    uint64_t index = 0;
+                    for (; index < initialLocationsIterators.size(); ++index) {
+                        ++initialLocationsIterators[index];
+                        if (initialLocationsIterators[index] == this->model.getAutomata()[index].getInitialLocationIndices().cend()) {
+                            initialLocationsIterators[index] = this->model.getAutomata()[index].getInitialLocationIndices().cbegin();
+                        } else {
+                            break;
+                        }
+                    }
                     
+                    // If we are at the end, leave the loop.
+                    if (index == initialLocationsIterators.size()) {
+                        break;
+                    }
+                }
+                
+                // Block the current initial state to search for the next one.
+                if (!blockingExpression.isInitialized()) {
+                    break;
                 }
+                solver->add(blockingExpression);
             }
-            )";
             
-            cpptempl::data_map modelData;
-            return cpptempl::parse(sourceTemplate, modelData);
+            return initialStates;
         }
         
-        template <typename ValueType>
-        boost::optional<std::string> ExplicitJitJaniModelBuilder<ValueType>::execute(std::string command) {
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateStateVariables() {
+            cpptempl::data_list booleanVariables;
+            cpptempl::data_list boundedIntegerVariables;
+            cpptempl::data_list locationVariables;
+            
+            for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
+                cpptempl::data_map booleanVariable;
+                std::string variableName = getQualifiedVariableName(variable);
+                variableToName[variable.getExpressionVariable()] = variableName;
+                booleanVariable["name"] = variableName;
+                booleanVariables.push_back(booleanVariable);
+            }
+            for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
+                cpptempl::data_map boundedIntegerVariable;
+                std::string variableName = getQualifiedVariableName(variable);
+                variableToName[variable.getExpressionVariable()] = variableName;
+
+                uint64_t range = static_cast<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt() + 1);
+                uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
+                
+                boundedIntegerVariable["name"] = variableName;
+                boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits);
+                boundedIntegerVariables.push_back(boundedIntegerVariable);
+            }
+            for (auto const& automaton : model.getAutomata()) {
+                for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+                    cpptempl::data_map booleanVariable;
+                    std::string variableName = getQualifiedVariableName(automaton, variable);
+                    variableToName[variable.getExpressionVariable()] = variableName;
+                    booleanVariable["name"] = variableName;
+                    booleanVariables.push_back(booleanVariable);
+                }
+                for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    cpptempl::data_map boundedIntegerVariable;
+                    std::string variableName = getQualifiedVariableName(automaton, variable);
+                    variableToName[variable.getExpressionVariable()] = variableName;
+                    
+                    uint64_t range = static_cast<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt());
+                    uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
+                    
+                    boundedIntegerVariable["name"] = variableName;
+                    boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits);
+                    boundedIntegerVariables.push_back(boundedIntegerVariable);
+                }
+                
+                // Only generate a location variable if there is more than one location for the automaton.
+                if (automaton.getNumberOfLocations() > 1) {
+                    cpptempl::data_map locationVariable;
+                    locationVariable["name"] = getLocationVariableName(automaton);
+                    locationVariable["numberOfBits"] = static_cast<uint64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
+                    locationVariables.push_back(locationVariable);
+                }
+            }
+            
+            cpptempl::data_map stateVariables;
+            stateVariables["boolean"] = cpptempl::make_data(booleanVariables);
+            stateVariables["boundedInteger"] = cpptempl::make_data(boundedIntegerVariables);
+            stateVariables["locations"] = cpptempl::make_data(locationVariables);
+            return stateVariables;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateNonSynchronizingEdges() {
+            cpptempl::data_list edges;
+            for (auto const& automaton : this->model.getAutomata()) {
+                for (auto const& edge : automaton.getEdges()) {
+                    if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
+                        edges.push_back(generateEdge(edge));
+                    }
+                }
+            }
+            
+            return edges;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdge(storm::jani::Edge const& edge) {
+            cpptempl::data_map edgeData;
+            
+            cpptempl::data_list destinations;
+            for (auto const& destination : edge.getDestinations()) {
+                destinations.push_back(generateDestination(destination));
+            }
+            
+            edgeData["guard"] = expressionTranslator.translate(edge.getGuard(), storm::expressions::ToCppTranslationOptions("sourceState."));
+            edgeData["destinations"] = cpptempl::make_data(destinations);
+            return edgeData;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateDestination(storm::jani::EdgeDestination const& destination) {
+            cpptempl::data_map destinationData;
+            
+            cpptempl::data_list nonTransientAssignments;
+            for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
+                nonTransientAssignments.push_back(generateAssignment(assignment, "targetState."));
+            }
+
+            destinationData["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignments);
+            destinationData["value"] = expressionTranslator.translate(destination.getProbability(), storm::expressions::ToCppTranslationOptions("sourceState.", "double"));
+            return destinationData;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        template <typename ValueTypePrime>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const {
+            cpptempl::data_map result;
+            result["variable"] = getVariableName(variable.getExpressionVariable());
+            result["value"] = asString(value);
+            return result;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const {
+            cpptempl::data_map result;
+            result["variable"] = getLocationVariableName(automaton);
+            result["value"] = asString(value);
+            return result;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix) {
+            cpptempl::data_map result;
+            result["variable"] = getVariableName(assignment.getExpressionVariable());
+            result["value"] = expressionTranslator.translate(assignment.getAssignedExpression(), prefix);
+            return result;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getVariableName(storm::expressions::Variable const& variable) const {
+            return variableToName.at(variable);
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Variable const& variable) const {
+            return variable.getName();
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const {
+            return automaton.getName() + variable.getName();
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getLocationVariableName(storm::jani::Automaton const& automaton) const {
+            return automaton.getName() + "_location";
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(bool value) const {
+            std::stringstream out;
+            out << std::boolalpha << value;
+            return out.str();
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        template <typename ValueTypePrime>
+        std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const {
+            return std::to_string(value);
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        boost::optional<std::string> ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::execute(std::string command) {
+            auto start = std::chrono::high_resolution_clock::now();
             char buffer[128];
             std::stringstream output;
             command += " 2>&1";
@@ -85,22 +690,25 @@ namespace storm {
             }
             int result = pclose(pipe.get());
             pipe.release();
-            
+
+            auto end = std::chrono::high_resolution_clock::now();
+            std::cout << "Executing command took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms" << std::endl;
+
             if (WEXITSTATUS(result) == 0) {
                 return boost::none;
             } else {
                 return "Executing command failed. Got response: " + output.str();
             }
         }
-
-        template <typename ValueType>
-        void ExplicitJitJaniModelBuilder<ValueType>::createBuilder(boost::filesystem::path const& dynamicLibraryPath) {
-            jitBuilderGetFunction = boost::dll::import_alias<typename ExplicitJitJaniModelBuilder<ValueType>::CreateFunctionType>(dynamicLibraryPath, "create_builder");
+        
+        template <typename ValueType, typename RewardModelType>
+        void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createBuilder(boost::filesystem::path const& dynamicLibraryPath) {
+            jitBuilderGetFunction = boost::dll::import_alias<typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::CreateFunctionType>(dynamicLibraryPath, "create_builder");
             builder = std::unique_ptr<JitModelBuilderInterface<ValueType>>(jitBuilderGetFunction());
         }
         
-        template <typename ValueType>
-        boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType>::writeSourceToTemporaryFile(std::string const& source) {
+        template <typename ValueType, typename RewardModelType>
+        boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::writeSourceToTemporaryFile(std::string const& source) {
             boost::filesystem::path temporaryFile = boost::filesystem::unique_path("%%%%-%%%%-%%%%-%%%%.cpp");
             std::ofstream out(temporaryFile.native());
             out << source << std::endl;
@@ -108,14 +716,14 @@ namespace storm {
             return temporaryFile;
         }
         
-        template <typename ValueType>
-        boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType>::compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile) {
+        template <typename ValueType, typename RewardModelType>
+        boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile) {
             std::string sourceFilename = boost::filesystem::absolute(sourceFile).string();
             auto dynamicLibraryPath = sourceFile;
             dynamicLibraryPath += DYLIB_EXTENSION;
             std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string();
             
-            std::string command = CXX_COMPILER + " " + sourceFilename + " " + COMPILER_FLAGS + " -I" + STORM_ROOT + " -I" + BOOST_ROOT + " -o " + dynamicLibraryFilename;
+            std::string command = CXX_COMPILER + " " + sourceFilename + " " + COMPILER_FLAGS + " -I" + STORM_ROOT + " -I" + STORM_ROOT + "/build_xcode/include -I" + L3PP_ROOT + " -I" + BOOST_ROOT + " -I" + GMP_ROOT + "/include -I" + CARL_ROOT + "/src -I" + CLN_ROOT + "/include -I" + GINAC_ROOT + "/include -o " + dynamicLibraryFilename;
             boost::optional<std::string> error = execute(command);
             
             if (error) {
@@ -126,11 +734,16 @@ namespace storm {
             return dynamicLibraryPath;
         }
         
-        template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>> ExplicitJitJaniModelBuilder<ValueType>::build() {
-         
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::build() {
+            
             // (1) generate the source code of the shared library
-            std::string source = createSourceCode();
+            std::string source;
+            try {
+                source = createSourceCode();
+            } catch (std::exception const& e) {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The model could not be successfully built (error: " << e.what() << ").");
+            }
             std::cout << "created source code: " << source << std::endl;
             
             // (2) write the source code to a temporary file
@@ -146,20 +759,20 @@ namespace storm {
             
             // (5) create the loader from the shared library
             createBuilder(dynamicLibraryPath);
-                
+            
             // (6) execute the function in the shared lib
-            builder->build();
-                
-            // (7) use result to build the model
-                
-            // (8) delete the shared library
+            auto sparseModel = builder->build();
+            
+            // (7) delete the shared library
             boost::filesystem::remove(dynamicLibraryPath);
             
-            // FIXME
-            return nullptr;
+            // Return the constructed model.
+            return std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(sparseModel);
         }
- 
-        template class ExplicitJitJaniModelBuilder<double>;
+        
+        template class ExplicitJitJaniModelBuilder<double, storm::models::sparse::StandardRewardModel<double>>;
+        template class ExplicitJitJaniModelBuilder<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalNumber>>;
+        template class ExplicitJitJaniModelBuilder<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>;
         
     }
 }

src/builder/ExplicitJitJaniModelBuilder.h

@@ -6,7 +6,12 @@
 #include <boost/dll/import.hpp>
 #include <boost/function.hpp>
 
+#include "cpptempl.h"
+
 #include "src/storage/jani/Model.h"
+#include "src/storage/expressions/ToCppVisitor.h"
+
+#include "src/models/sparse/StandardRewardModel.h"
 
 #include "src/builder/JitModelBuilderInterface.h"
 
@@ -23,7 +28,7 @@ namespace storm {
     
     namespace builder {
         
-        template <typename ValueType>
+        template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
         class ExplicitJitJaniModelBuilder {
         public:
             typedef JitModelBuilderInterface<ValueType>* (CreateFunctionType)();
@@ -31,7 +36,7 @@ namespace storm {
             
             ExplicitJitJaniModelBuilder(storm::jani::Model const& model);
             
-            std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>> build();
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
             
         private:
             void createBuilder(boost::filesystem::path const& dynamicLibraryPath);
@@ -41,9 +46,37 @@ namespace storm {
 
             static boost::optional<std::string> execute(std::string command);
             
-            storm::jani::Model const& model;
-            typename ExplicitJitJaniModelBuilder<ValueType>::ImportFunctionType jitBuilderGetFunction;
+            // Functions that generate data maps or data templates.
+            cpptempl::data_list generateInitialStates();
+            cpptempl::data_map generateStateVariables();
+            cpptempl::data_list generateNonSynchronizingEdges();
+
+            cpptempl::data_map generateEdge(storm::jani::Edge const& edge);
+            cpptempl::data_map generateDestination(storm::jani::EdgeDestination const& destination);
+            
+            template <typename ValueTypePrime>
+            cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const;
+            
+            cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const;
+
+            cpptempl::data_map generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix = "");
+            
+            // Auxiliary functions that perform regularly needed steps.
+            std::string const& getVariableName(storm::expressions::Variable const& variable) const;
+            std::string getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const;
+            std::string getQualifiedVariableName(storm::jani::Variable const& variable) const;
+            std::string getLocationVariableName(storm::jani::Automaton const& automaton) const;
+            std::string asString(bool value) const;
+            
+            template <typename ValueTypePrime>
+            std::string asString(ValueTypePrime value) const;
+            
+            storm::jani::Model model;
+            typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderGetFunction;
             std::unique_ptr<JitModelBuilderInterface<ValueType>> builder;
+            
+            std::unordered_map<storm::expressions::Variable, std::string> variableToName;
+            storm::expressions::ToCppVisitor expressionTranslator;
         };
         
     }

src/builder/JitModelBuilderInterface.h

@@ -1,5 +1,9 @@
 #pragma once
 
+#include <memory>
+
+#include "src/models/sparse/Model.h"
+
 namespace storm {
     namespace builder {
         
@@ -10,8 +14,8 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            virtual void build() {
-                // Intentionally left empty.
+            virtual storm::models::sparse::Model<ValueType>* build() {
+                return nullptr;
             }
         };
         

src/cli/entrypoints.h

@@ -7,6 +7,7 @@
 
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidSettingsException.h"
+#include "src/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace cli {
@@ -201,6 +202,8 @@ namespace storm {
         void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
             // Start by building the model.
             std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
+
+            STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built.");
             
             // Print some information about the model.
             markovModel->printModelInformationToStream(std::cout);

src/settings/modules/IOSettings.cpp

@@ -20,6 +20,7 @@ namespace storm {
             const std::string IOSettings::prismInputOptionName = "prism";
             const std::string IOSettings::janiInputOptionName = "jani";
             const std::string IOSettings::prismToJaniOptionName = "prism2jani";
+            const std::string IOSettings::jitOptionName = "jit";
             const std::string IOSettings::explorationOrderOptionName = "explorder";
             const std::string IOSettings::explorationOrderOptionShortName = "eo";
             const std::string IOSettings::transitionRewardsOptionName = "transrew";
@@ -44,6 +45,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder if available.").build());
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
@@ -102,6 +104,10 @@ namespace storm {
             std::string IOSettings::getJaniInputFilename() const {
                 return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString();
             }
+            
+            bool IOSettings::isJitSet() const {
+                return this->getOption(jitOptionName).getHasOptionBeenSet();
+            }
 
             bool IOSettings::isExplorationOrderSet() const {
                 return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();

src/settings/modules/IOSettings.h

@@ -102,6 +102,13 @@ namespace storm {
                  */
                 std::string getJaniInputFilename() const;
 
+                /*!
+                 * Retrieves whether the option to use the JIT builder is set.
+                 *
+                 * @return True iff the JIT builder is to be used.
+                 */
+                bool isJitSet() const;
+                
                 /*!
                  * Retrieves whether the model exploration order was set.
                  *
@@ -206,6 +213,7 @@ namespace storm {
                 static const std::string prismInputOptionName;
                 static const std::string janiInputOptionName;
                 static const std::string prismToJaniOptionName;
+                static const std::string jitOptionName;
                 static const std::string explorationOrderOptionName;
                 static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;

src/storage/SparseMatrix.h

@@ -24,20 +24,19 @@ namespace storm {
 		template<typename T>
 		class TopologicalValueIterationMinMaxLinearEquationSolver;
 	}
-        
-        
 }
 
 namespace storm {
     namespace storage {
         
         class BitVector;
+        
         // Forward declare matrix class.
-        template<typename T> class SparseMatrix;
+        template<typename T>
+        class SparseMatrix;
         
         typedef uint_fast64_t SparseMatrixIndexType;
         
-        
         template<typename IndexType, typename ValueType>
         class MatrixEntry {
         public:

src/storage/bisimulation/BisimulationDecomposition.h

@@ -90,7 +90,6 @@ namespace storm {
                  */
                 void preserveFormula(ModelType const& model, storm::logic::Formula const& formula);
                 
-                
                 /**
                  * Sets the bisimulation type. If the bisimulation type is set to weak,
                  * we also change the bounded flag (as bounded properties are not preserved under 
@@ -123,6 +122,7 @@ namespace storm {
                     assert(optimalityType);
                     return optimalityType.get();
                 }
+                
                 // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
                 // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
                 // measure driven initial partition wrt. to the states phi and psi is taken.

src/storage/expressions/ToCppVisitor.cpp

@@ -0,0 +1,268 @@
+#include "src/storage/expressions/ToCppVisitor.h"
+
+#include "src/storage/expressions/Expressions.h"
+
+namespace storm {
+    namespace expressions {
+        
+        ToCppTranslationOptions::ToCppTranslationOptions(std::string const& prefix, std::string const& valueTypeCast) : valueTypeCast(valueTypeCast), prefix(prefix) {
+            // Intentionally left empty.
+        }
+        
+        std::string const& ToCppTranslationOptions::getPrefix() const {
+            return prefix;
+        }
+        
+        bool ToCppTranslationOptions::hasValueTypeCast() const {
+            return !valueTypeCast.empty();
+        }
+        
+        std::string const& ToCppTranslationOptions::getValueTypeCast() const {
+            return valueTypeCast;
+        }
+        
+        void ToCppTranslationOptions::clearValueTypeCast() {
+            valueTypeCast = "";
+        }
+        
+        std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) {
+            expression.accept(*this, options);
+            std::string result = stream.str();
+            stream.str("");
+            return result;
+        }
+        
+        boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions conditionOptions = boost::any_cast<ToCppTranslationOptions>(data);
+            conditionOptions.clearValueTypeCast();
+            stream << "(";
+            expression.getCondition()->accept(*this, conditionOptions);
+            stream << " ? ";
+            expression.getThenExpression()->accept(*this, data);
+            stream << " : ";
+            expression.getElseExpression()->accept(*this, data);
+            stream << ")";
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
+            newOptions.clearValueTypeCast();
+            
+            switch (expression.getOperatorType()) {
+                    case BinaryBooleanFunctionExpression::OperatorType::And:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " && ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryBooleanFunctionExpression::OperatorType::Or:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " || ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryBooleanFunctionExpression::OperatorType::Xor:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " ^ ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryBooleanFunctionExpression::OperatorType::Implies:
+                    stream << "(!";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " || ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryBooleanFunctionExpression::OperatorType::Iff:
+                    stream << "!(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " ^ ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            switch (expression.getOperatorType()) {
+                case BinaryNumericalFunctionExpression::OperatorType::Plus:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << " + ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Minus:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << " - ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Times:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << " * ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Divide:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << " / ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Min:
+                    stream << "std::min(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << ", ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Max:
+                    stream << "std::max(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << ", ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case BinaryNumericalFunctionExpression::OperatorType::Power:
+                    stream << "std::pow(";
+                    expression.getFirstOperand()->accept(*this, data);
+                    stream << ", ";
+                    expression.getSecondOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
+            newOptions.clearValueTypeCast();
+
+            switch (expression.getRelationType()) {
+                case BinaryRelationExpression::RelationType::Equal:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " == ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryRelationExpression::RelationType::NotEqual:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " != ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryRelationExpression::RelationType::Less:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " < ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryRelationExpression::RelationType::LessOrEqual:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " <= ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryRelationExpression::RelationType::Greater:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " > ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+                case BinaryRelationExpression::RelationType::GreaterOrEqual:
+                    stream << "(";
+                    expression.getFirstOperand()->accept(*this, newOptions);
+                    stream << " >= ";
+                    expression.getSecondOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
+            if (options.hasValueTypeCast()) {
+                stream << "static_cast<" << options.getValueTypeCast() << ">(";
+            }
+            stream << options.getPrefix() << expression.getVariableName();
+            if (options.hasValueTypeCast()) {
+                stream << ")";
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
+            newOptions.clearValueTypeCast();
+            
+            switch (expression.getOperatorType()) {
+                case UnaryBooleanFunctionExpression::OperatorType::Not:
+                    stream << "!(";
+                    expression.getOperand()->accept(*this, newOptions);
+                    stream << ")";
+                    break;
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            switch (expression.getOperatorType()) {
+                case UnaryNumericalFunctionExpression::OperatorType::Minus:
+                    stream << "-(";
+                    expression.getOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case UnaryNumericalFunctionExpression::OperatorType::Floor:
+                    stream << "std::floor(";
+                    expression.getOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+                case UnaryNumericalFunctionExpression::OperatorType::Ceil:
+                    stream << "std::ceil(";
+                    expression.getOperand()->accept(*this, data);
+                    stream << ")";
+                    break;
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+            stream << std::boolalpha << expression.getValue();
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
+            if (options.hasValueTypeCast()) {
+                stream << "static_cast<" << options.getValueTypeCast() << ">(";
+            }
+            stream << expression.getValue();
+            if (options.hasValueTypeCast()) {
+                stream << ")";
+            }
+            return boost::none;
+        }
+        
+        boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
+            stream << expression.getValueAsDouble();
+            return boost::none;
+        }
+
+    }
+}

src/storage/expressions/ToCppVisitor.h

@@ -0,0 +1,46 @@
+#pragma once
+
+#include <sstream>
+
+#include "src/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        class Expression;
+        
+        class ToCppTranslationOptions {
+        public:
+            ToCppTranslationOptions(std::string const& prefix = "", std::string const& valueTypeCast = "");
+            
+            std::string const& getPrefix() const;
+            
+            bool hasValueTypeCast() const;
+            std::string const& getValueTypeCast() const;
+            void clearValueTypeCast();
+            
+        private:
+            std::string valueTypeCast;
+            std::string prefix;
+        };
+        
+        class ToCppVisitor : public ExpressionVisitor {
+        public:
+            std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options = ToCppTranslationOptions());
+            
+            virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+            
+        private:
+            std::stringstream stream;
+        };
+        
+    }
+}

src/utility/storm.h

@@ -47,6 +47,7 @@
 
 // Headers of builders.
 #include "src/builder/ExplicitModelBuilder.h"
+#include "src/builder/ExplicitJitJaniModelBuilder.h"
 #include "src/builder/DdPrismModelBuilder.h"
 #include "src/builder/DdJaniModelBuilder.h"
 
@@ -115,16 +116,22 @@ namespace storm {
             options.setBuildChoiceLabels(true);
         }
 
-        std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
-        if (model.isPrismProgram()) {
-            generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
-        } else if (model.isJaniModel()) {
-            generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
+        if (storm::settings::getModule<storm::settings::modules::IOSettings>().isJitSet()) {
+            STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model.");
+            storm::builder::ExplicitJitJaniModelBuilder<ValueType> builder(model.asJaniModel());
+            return builder.build();
         } else {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
+            std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
+            if (model.isPrismProgram()) {
+                generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
+            } else if (model.isJaniModel()) {
+                generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
+            }
+            storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
+            return builder.build();
         }
-        storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
-        return builder.build();
     }
 
     template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>