more work on jit-thing: transitioning to proper handling of synchronizing edges

Former-commit-id: 3af1772192 [formerly 890c529dd1]
Former-commit-id: 818295a085

src/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -158,6 +158,57 @@ namespace storm {
                             private:
                                 std::queue<StateType> storage;
                             };
+
+                            {% for edge in nonSynchronizingEdges %}static bool enabled_{$edge.name}(StateType const& state) {
+                                if ({$edge.guard}) {
+                                    return true;
+                                }
+                                return false;
+                            }
+                            
+                            static void perform_{$edge.name}(StateType const& state) {
+                                
+                            }
+                            
+                            static void lowestLevel_{$edge.name}() {
+                                return {$edge.lowestLevel};
+                            }
+
+                            static void highestLevel_{$edge.name}() {
+                                return {$edge.highestLevel};
+                            }
+                            {% endfor %}
+                            
+                            
+                            {% for edge in nonSynchronizingEdges %}class Edge_{$edge.name} {
+                            public:
+                                bool isEnabled(StateType const& state) {
+                                    if ({$edge.guard}) {
+                                        return true;
+                                    }
+                                    return false;
+                                }
+                                
+                                {% for destination in edge.destinations %}class Destination_{$destination.name} {
+                                public:
+                                    int_fast64_t lowestLevel() const {
+                                        return {$destination.lowestLevel};
+                                    }
+
+                                    int_fast64_t highestLevel() const {
+                                        return {$destination.highestLevel};
+                                    }
+
+                                    void performAssignments(int_fast64_t level, StateType& state) {
+                                        {% for level in destination.levels %}if (level == {$level.index}) {
+                                            {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
+                                            {% endfor %}
+                                        }{% endfor %}
+                                    }
+                                };
+                                {% endfor %}
+                            };
+                            {% endfor %}
                             
                             class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
                             public:
@@ -166,8 +217,7 @@ namespace storm {
                                         StateType state;
                                         {% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
                                         {% endfor %}initialStates.push_back(state);
-                                    }
-                                    {% endfor %}
+                                    }{% endfor %}
                                 }
                                 
                                 virtual storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* build() override {
@@ -243,22 +293,12 @@ namespace storm {
                                     {% for expression in terminalExpressions %}if ({$expression}) {
                                         return true;
                                     }
+                                    {% endfor %}
                                     return false;
                                 }
                                 
                                 void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, StateBehaviour<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
-                                    {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) {
-                                        Choice<IndexType, ValueType>& choice = behaviour.addChoice();
-                                        {% for destination in edge.destinations %}{
-                                            StateType targetState(sourceState);
-                                            {% for assignment in destination.nonTransientAssignments %}targetState.{$assignment.variable} = {$assignment.value};
-                                            {% endfor %}
-                                            IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);
-                                            choice.add(targetStateIndex, {$destination.value});
-                                        }
-                                        {% endfor %}
-                                    }
-                                    {% endfor %}
+
                                 }
                                 
                                 IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) {
@@ -444,7 +484,14 @@ namespace storm {
                     std::string variableName = getQualifiedVariableName(variable);
                     variableToName[variable.getExpressionVariable()] = variableName;
                     
-                    uint64_t range = static_cast<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt() + 1);
+                    int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+                    int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+                    
+                    lowerBounds[variable.getExpressionVariable()] = lowerBound;
+                    if (lowerBound != 0) {
+                        lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound);
+                    }
+                    uint64_t range = static_cast<uint64_t>(upperBound - lowerBound + 1);
                     uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
                     
                     boundedIntegerVariable["name"] = variableName;
@@ -463,8 +510,15 @@ namespace storm {
                         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());
+
+                        int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+                        int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+
+                        lowerBounds[variable.getExpressionVariable()] = lowerBound;
+                        if (lowerBound != 0) {
+                            lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound);
+                        }
+                        uint64_t range = static_cast<uint64_t>(upperBound - lowerBound);
                         uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
                         
                         boundedIntegerVariable["name"] = variableName;
@@ -499,7 +553,7 @@ namespace storm {
                         if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) {
                             cpptempl::data_map label;
                             label["name"] = variable->getName();
-                            label["predicate"] = expressionTranslator.translate(model.getLabelExpression(variable->asBooleanVariable(), locationVariables), storm::expressions::ToCppTranslationOptions("state."));
+                            label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable->asBooleanVariable(), locationVariables)), storm::expressions::ToCppTranslationOptions("state."));
                             labels.push_back(label);
                         }
                     }
@@ -508,7 +562,7 @@ namespace storm {
                 for (auto const& expression : this->options.getExpressionLabels()) {
                     cpptempl::data_map label;
                     label["name"] = expression.toString();
-                    label["predicate"] = expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state."));
+                    label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("state."));
                     labels.push_back(label);
                 }
                 
@@ -531,10 +585,10 @@ namespace storm {
                         if (terminalEntry.second) {
                             labelExpression = !labelExpression;
                         }
-                        terminalExpressions.push_back(expressionTranslator.translate(labelExpression, storm::expressions::ToCppTranslationOptions("state.")));
+                        terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions("state.")));
                     } else {
                         auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression();
-                        terminalExpressions.push_back(expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state.")));
+                        terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("state.")));
                     }
                 }
 
@@ -545,10 +599,12 @@ namespace storm {
             cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateNonSynchronizingEdges() {
                 cpptempl::data_list edges;
                 for (auto const& automaton : this->model.getAutomata()) {
+                    uint64_t edgeIndex = 0;
                     for (auto const& edge : automaton.getEdges()) {
                         if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
-                            edges.push_back(generateEdge(edge));
+                            edges.push_back(generateEdge(automaton, edgeIndex, edge));
                         }
+                        ++edgeIndex;
                     }
                 }
                 
@@ -556,31 +612,74 @@ namespace storm {
             }
             
             template <typename ValueType, typename RewardModelType>
-            cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdge(storm::jani::Edge const& edge) {
+            cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge) {
                 cpptempl::data_map edgeData;
                 
                 cpptempl::data_list destinations;
+                uint64_t destinationIndex = 0;
                 for (auto const& destination : edge.getDestinations()) {
-                    destinations.push_back(generateDestination(destination));
+                    destinations.push_back(generateDestination(destinationIndex, destination));
+                    ++destinationIndex;
                 }
                 
-                edgeData["guard"] = expressionTranslator.translate(edge.getGuard(), storm::expressions::ToCppTranslationOptions("sourceState."));
+                edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions("state."));
                 edgeData["destinations"] = cpptempl::make_data(destinations);
+                edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex);
                 return edgeData;
             }
             
             template <typename ValueType, typename RewardModelType>
-            cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateDestination(storm::jani::EdgeDestination const& destination) {
+            cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateDestination(uint64_t destinationIndex, 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."));
+                cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments());
+                destinationData["name"] = asString(destinationIndex);
+                destinationData["levels"] = cpptempl::make_data(levels);
+                destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel());
+                destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel());
+
+                return destinationData;
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLevels(storm::jani::OrderedAssignments const& orderedAssignments) {
+                cpptempl::data_list levels;
+                
+                auto const& assignments = orderedAssignments.getAllAssignments();
+                if (!assignments.empty()) {
+                    int_fast64_t currentLevel = assignments.begin()->getLevel();
+                    
+                    cpptempl::data_list nonTransientAssignmentData;
+                    cpptempl::data_list transientAssignmentData;
+                    for (auto const& assignment : assignments) {
+                        if (assignment.getLevel() != currentLevel) {
+                            cpptempl::data_map level;
+                            level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData);
+                            level["transientAssignments"] = cpptempl::make_data(transientAssignmentData);
+                            level["index"] = asString(currentLevel);
+                            levels.push_back(level);
+                            
+                            nonTransientAssignmentData = cpptempl::data_list();
+                            transientAssignmentData = cpptempl::data_list();
+                            currentLevel = assignment.getLevel();
+                        }
+                        
+                        if (assignment.isTransient()) {
+                            transientAssignmentData.push_back(generateAssignment(assignment, "state."));
+                        } else {
+                            nonTransientAssignmentData.push_back(generateAssignment(assignment, "state."));
+                        }
+                    }
+
+                    // Close the last (open) level.
+                    cpptempl::data_map level;
+                    level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData);
+                    level["transientAssignments"] = cpptempl::make_data(transientAssignmentData);
+                    level["index"] = asString(currentLevel);
+                    levels.push_back(level);
                 }
                 
-                destinationData["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignments);
-                destinationData["value"] = expressionTranslator.translate(destination.getProbability(), storm::expressions::ToCppTranslationOptions("sourceState.", "double"));
-                return destinationData;
+                return levels;
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -604,7 +703,18 @@ namespace storm {
             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);
+                auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable());
+                if (lowerBoundIt != lowerBounds.end()) {
+                    if (lowerBoundIt->second < 0) {
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), prefix);
+                    } else if (lowerBoundIt->second == 0) {
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix);
+                    } else {
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), prefix);
+                    }
+                } else {
+                    result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix);
+                }
                 return result;
             }
             
@@ -640,6 +750,11 @@ namespace storm {
                 return out.str();
             }
             
+            template <typename ValueType, typename RewardModelType>
+            storm::expressions::Expression ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression) {
+                return expression.substitute(lowerBoundShiftSubstitution);
+            }
+            
             template <typename ValueType, typename RewardModelType>
             template <typename ValueTypePrime>
             std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const {

src/builder/jit/ExplicitJitJaniModelBuilder.h

@@ -55,9 +55,10 @@ namespace storm {
                 cpptempl::data_list generateLabels();
                 cpptempl::data_list generateTerminalExpressions();
                 cpptempl::data_list generateNonSynchronizingEdges();
+                cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments);
                 
-                cpptempl::data_map generateEdge(storm::jani::Edge const& edge);
-                cpptempl::data_map generateDestination(storm::jani::EdgeDestination const& destination);
+                cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge);
+                cpptempl::data_map generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination);
                 
                 template <typename ValueTypePrime>
                 cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const;
@@ -73,7 +74,8 @@ namespace storm {
                 std::string getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const;
                 std::string getLocationVariableName(storm::jani::Automaton const& automaton) const;
                 std::string asString(bool value) const;
-                
+                storm::expressions::Expression shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression);
+
                 template <typename ValueTypePrime>
                 std::string asString(ValueTypePrime value) const;
                 
@@ -87,6 +89,8 @@ namespace storm {
                 
                 std::unordered_map<storm::expressions::Variable, std::string> variableToName;
                 storm::expressions::ToCppVisitor expressionTranslator;
+                std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution;
+                std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
             };
 
         }

src/generator/JaniNextStateGenerator.cpp

@@ -92,7 +92,7 @@ namespace storm {
                             storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel());
                             STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
-
+                            
                             this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
                         }
                     }
@@ -188,7 +188,7 @@ namespace storm {
                     blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
                     initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
                 }
-                                
+                
                 // Gather iterators to the initial locations of all the automata.
                 std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
                 uint64_t currentLocationVariable = 0;
@@ -270,7 +270,7 @@ namespace storm {
             
             // Check that we processed all assignments.
             STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
-
+            
             return newState;
         }
         
@@ -281,7 +281,7 @@ namespace storm {
             
             // Retrieve the locations from the state.
             std::vector<uint64_t> locations = getLocations(*this->state);
-
+            
             // First, construct the state rewards, as we may return early if there are no choices later and we already
             // need the state rewards then.
             std::vector<ValueType> stateRewards(this->rewardVariables.size(), storm::utility::zero<ValueType>());
@@ -327,7 +327,7 @@ namespace storm {
                 // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
                 // this is equal to the number of choices, which is why we initialize it like this here.
                 ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
-
+                
                 // Iterate over all choices and combine the probabilities/rates into one choice.
                 for (auto const& choice : allChoices) {
                     for (auto const& stateProbabilityPair : choice) {
@@ -346,7 +346,7 @@ namespace storm {
                         globalChoice.addLabels(choice.getLabels());
                     }
                 }
-             
+                
                 std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
                 for (auto const& choice : allChoices) {
                     for (uint_fast64_t rewardVariableIndex = 0; rewardVariableIndex < rewardVariables.size(); ++rewardVariableIndex) {
@@ -354,7 +354,7 @@ namespace storm {
                     }
                 }
                 globalChoice.addRewards(std::move(stateActionRewards));
-                                
+                
                 // Move the newly fused choice in place.
                 allChoices.clear();
                 allChoices.push_back(std::move(globalChoice));
@@ -404,20 +404,23 @@ namespace storm {
                     // Iterate over all updates of the current command.
                     ValueType probabilitySum = storm::utility::zero<ValueType>();
                     for (auto const& destination : edge.getDestinations()) {
-                        // Obtain target state index and add it to the list of known states. If it has not yet been
-                        // seen, we also add it to the set of states that have yet to be explored.
-                        StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
-                        
-                        // Update the choice by adding the probability/target state to it.
                         ValueType probability = this->evaluator->asRational(destination.getProbability());
-                        probability = exitRate ? exitRate.get() * probability : probability;
-                        choice.addProbability(stateIndex, probability);
-                        probabilitySum += probability;
+                        
+                        if (probability != storm::utility::zero<ValueType>()) {
+                            // Obtain target state index and add it to the list of known states. If it has not yet been
+                            // seen, we also add it to the set of states that have yet to be explored.
+                            StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
+                            
+                            // Update the choice by adding the probability/target state to it.
+                            probability = exitRate ? exitRate.get() * probability : probability;
+                            choice.addProbability(stateIndex, probability);
+                            probabilitySum += probability;
+                        }
                     }
                     
                     // Create the state-action reward for the newly created choice.
                     performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } );
-
+                    
                     // Check that the resulting distribution is in fact a distribution.
                     STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
                 }
@@ -467,11 +470,14 @@ namespace storm {
                                     
                                     // If the new state was already found as a successor state, update the probability
                                     // and otherwise insert it.
-                                    auto targetStateIt = newTargetStates->find(newTargetState);
-                                    if (targetStateIt != newTargetStates->end()) {
-                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
-                                    } else {
-                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()));
+                                    auto probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
+                                    if (probability != storm::utility::zero<ValueType>()) {
+                                        auto targetStateIt = newTargetStates->find(newTargetState);
+                                        if (targetStateIt != newTargetStates->end()) {
+                                            targetStateIt->second += probability;
+                                        } else {
+                                            newTargetStates->emplace(newTargetState, probability);
+                                        }
                                     }
                                 }
                                 
@@ -500,7 +506,7 @@ namespace storm {
                         
                         // Add the rewards to the choice.
                         choice.addRewards(std::move(stateActionRewards));
-
+                        
                         // Add the probabilities/rates to the newly created choice.
                         ValueType probabilitySum = storm::utility::zero<ValueType>();
                         for (auto const& stateProbabilityPair : *newTargetStates) {
@@ -510,7 +516,7 @@ namespace storm {
                         }
                         
                         // Check that the resulting distribution is in fact a distribution.
-                        STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+                        STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ").");
                         
                         // Dispose of the temporary maps.
                         delete currentTargetStates;
@@ -689,7 +695,7 @@ namespace storm {
                         }
                     }
                 }
-
+                
                 for (auto const& edge : automaton.getEdges()) {
                     auto rewardVariableIt = rewardVariables.begin();
                     auto rewardVariableIte = rewardVariables.end();
@@ -717,35 +723,35 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
             if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) {
 #else
-            if (model.hasUndefinedConstants()) {
+                if (model.hasUndefinedConstants()) {
 #endif
-                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
-                std::stringstream stream;
-                bool printComma = false;
-                for (auto const& constant : undefinedConstants) {
-                    if (printComma) {
-                        stream << ", ";
-                    } else {
-                        printComma = true;
+                    std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+                    std::stringstream stream;
+                    bool printComma = false;
+                    for (auto const& constant : undefinedConstants) {
+                        if (printComma) {
+                            stream << ", ";
+                        } else {
+                            printComma = true;
+                        }
+                        stream << constant.get().getName() << " (" << constant.get().getType() << ")";
                     }
-                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    stream << ".";
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
                 }
-                stream << ".";
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
-            }
                 
 #ifdef STORM_HAVE_CARL
-            else if (std::is_same<ValueType, storm::RationalFunction>::value && !model.undefinedConstantsAreGraphPreserving()) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
-            }
+                else if (std::is_same<ValueType, storm::RationalFunction>::value && !model.undefinedConstantsAreGraphPreserving()) {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
+                }
 #endif
-        }
-        
-        template class JaniNextStateGenerator<double>;
-
+            }
+            
+            template class JaniNextStateGenerator<double>;
+            
 #ifdef STORM_HAVE_CARL
-        template class JaniNextStateGenerator<storm::RationalNumber>;
-        template class JaniNextStateGenerator<storm::RationalFunction>;
+            template class JaniNextStateGenerator<storm::RationalNumber>;
+            template class JaniNextStateGenerator<storm::RationalFunction>;
 #endif
+        }
     }
-}

src/generator/PrismNextStateGenerator.cpp

@@ -395,15 +395,17 @@ namespace storm {
                     ValueType probabilitySum = storm::utility::zero<ValueType>();
                     for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
                         storm::prism::Update const& update = command.getUpdate(k);
-                        
-                        // Obtain target state index and add it to the list of known states. If it has not yet been
-                        // seen, we also add it to the set of states that have yet to be explored.
-                        StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
-                        
-                        // Update the choice by adding the probability/target state to it.
+
                         ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression());
-                        choice.addProbability(stateIndex, probability);
-                        probabilitySum += probability;
+                        if (probability != storm::utility::zero<ValueType>()) {
+                            // Obtain target state index and add it to the list of known states. If it has not yet been
+                            // seen, we also add it to the set of states that have yet to be explored.
+                            StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
+                            
+                            // Update the choice by adding the probability/target state to it.
+                            choice.addProbability(stateIndex, probability);
+                            probabilitySum += probability;
+                        }
                     }
                     
                     // Create the state-action reward for the newly created choice.
@@ -458,16 +460,20 @@ namespace storm {
                                 storm::prism::Update const& update = command.getUpdate(j);
                                 
                                 for (auto const& stateProbabilityPair : *currentTargetStates) {
-                                    // Compute the new state under the current update and add it to the set of new target states.
-                                    CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+                                    auto probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
                                     
-                                    // If the new state was already found as a successor state, update the probability
-                                    // and otherwise insert it.
-                                    auto targetStateIt = newTargetStates->find(newTargetState);
-                                    if (targetStateIt != newTargetStates->end()) {
-                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
-                                    } else {
-                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()));
+                                    if (probability != storm::utility::zero<ValueType>()) {
+                                        // Compute the new state under the current update and add it to the set of new target states.
+                                        CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+                                        
+                                        // If the new state was already found as a successor state, update the probability
+                                        // and otherwise insert it.
+                                        auto targetStateIt = newTargetStates->find(newTargetState);
+                                        if (targetStateIt != newTargetStates->end()) {
+                                            targetStateIt->second += probability;
+                                        } else {
+                                            newTargetStates->emplace(newTargetState, probability);
+                                        }
                                     }
                                 }
                             }

src/settings/SettingsManager.cpp

@@ -34,6 +34,7 @@
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 #include "src/settings/modules/ExplorationSettings.h"
 #include "src/settings/modules/JaniExportSettings.h"
+#include "src/settings/modules/JitBuilderSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -526,6 +527,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::Smt2SmtSolverSettings>();
             storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
             storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+            storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
         }
 
     }

src/settings/modules/JitBuilderSettings.cpp

@@ -0,0 +1,42 @@
+#include "src/settings/modules/JitBuilderSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            const std::string JitBuilderSettings::moduleName = "jitbuilder";
+            
+            const std::string JitBuilderSettings::noJitOptionName = "nojit";
+            const std::string JitBuilderSettings::doctorOptionName = "doctor";
+            
+            JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) {
+//                this->addOption(storm::settings::OptionBuilder(moduleName, noJitOptionName, false, "Don't use the jit-based explicit model builder.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show information on why the jit-based explicit model builder is not usable on the current system.").build());
+            }
+            
+//            bool JitBuilderSettings::isNoJitSet() const {
+//                return this->getOption(noJitOptionName).getHasOptionBeenSet();
+//            }
+
+            bool JitBuilderSettings::isDoctorSet() const {
+                return this->getOption(doctorOptionName).getHasOptionBeenSet();
+            }
+                        
+            void JitBuilderSettings::finalize() {
+                // Intentionally left empty.
+            }
+            
+            bool JitBuilderSettings::check() const {
+                return true;
+            }
+        }
+    }
+}

src/settings/modules/JitBuilderSettings.h

@@ -0,0 +1,32 @@
+#pragma once
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            class JitBuilderSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new JitBuilder settings object.
+                 */
+                JitBuilderSettings();
+                
+//                bool isNoJitSet() const;
+
+                bool isDoctorSet() const;
+                
+                bool check() const override;
+                void finalize() override;
+                
+                static const std::string moduleName;
+                
+            private:
+                static const std::string noJitOptionName;
+                static const std::string doctorOptionName;
+            };
+            
+        }
+    }
+}

src/storage/jani/Assignment.cpp

@@ -48,20 +48,20 @@ namespace storm  {
             return stream;
         }
         
-        bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, Assignment const& right) const {
-            return left.getExpressionVariable() < right.getExpressionVariable();
+        bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, Assignment const& right) const {
+            return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getExpressionVariable() < right.getExpressionVariable());
         }
 
-        bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
-            return left.getExpressionVariable() < right->getExpressionVariable();
+        bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
+            return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getExpressionVariable() < right->getExpressionVariable());
         }
         
-        bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
-            return left->getExpressionVariable() < right->getExpressionVariable();
+        bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
+            return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getExpressionVariable() < right->getExpressionVariable());
         }
         
-        bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
-            return left->getExpressionVariable() < right.getExpressionVariable();
+        bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
+            return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getExpressionVariable() < right.getExpressionVariable());
         }
     }
-}
+}

src/storage/jani/Assignment.h

@@ -66,9 +66,10 @@ namespace storm {
         };
         
         /*!
-         * This functor enables ordering the assignments by variable. Note that this is a partial order.
+         * This functor enables ordering the assignments first by the assignment level and then by variable.
+         * Note that this is a partial order.
          */
-        struct AssignmentPartialOrderByVariable {
+        struct AssignmentPartialOrderByLevelAndVariable {
             bool operator()(Assignment const& left, Assignment const& right) const;
             bool operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const;
             bool operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const;
@@ -76,4 +77,4 @@ namespace storm {
         };
     
     }
-}
+}

src/storage/jani/OrderedAssignments.cpp

@@ -70,18 +70,26 @@ namespace storm {
         }
         
         bool OrderedAssignments::hasMultipleLevels() const {
-            if(allAssignments.empty()) {
+            if (allAssignments.empty()) {
                 return false;
             }
             uint64_t firstLevel = allAssignments.front()->getLevel();
-            for(auto const& assignment : allAssignments) {
-                if(assignment->getLevel() != firstLevel) {
+            for (auto const& assignment : allAssignments) {
+                if (assignment->getLevel() != firstLevel) {
                     return true;
                 }
             }
             return false;
         }
         
+        int_fast64_t OrderedAssignments::getLowestLevel() const {
+            return allAssignments.front()->getLevel();
+        }
+        
+        int_fast64_t OrderedAssignments::getHighestLevel() const {
+            return allAssignments.back()->getLevel();
+        }
+        
         bool OrderedAssignments::contains(Assignment const& assignment) const {
             auto it = lowerBound(assignment, allAssignments);
             if (it != allAssignments.end() && assignment == **it) {
@@ -126,8 +134,8 @@ namespace storm {
         }
         
         std::vector<std::shared_ptr<Assignment>>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments) {
-            return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByVariable());
+            return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
         }
         
     }
-}
+}

src/storage/jani/OrderedAssignments.h

@@ -42,6 +42,18 @@ namespace storm {
              */
             bool hasMultipleLevels() const;
             
+            /*!
+             * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
+             * one assignment.
+             */
+            int_fast64_t getLowestLevel() const;
+
+            /*!
+             * Retrieves the highest level among all assignments. Note that this may only be called if there is at least
+             * one assignment.
+             */
+            int_fast64_t getHighestLevel() const;
+
             /*!
              * Retrieves whether the given assignment is contained in this set of assignments.
              */
@@ -97,4 +109,4 @@ namespace storm {
         };
         
     }
-}
+}

src/storage/prism/Command.cpp

@@ -73,14 +73,13 @@ namespace storm {
             return true;
         }
         
-        Command Command::removeIdentityAssignmentsFromUpdates() const {
+        Command Command::simplify() const {
             std::vector<Update> newUpdates;
             newUpdates.reserve(this->getNumberOfUpdates());
             for (auto const& update : this->getUpdates()) {
                 newUpdates.emplace_back(update.removeIdentityAssignments());
             }
             return copyWithNewUpdates(std::move(newUpdates));
-            
         }
         
         Command Command::copyWithNewUpdates(std::vector<Update> && newUpdates) const {

src/storage/prism/Command.h

@@ -128,12 +128,11 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& stream, Command const& command);
             
-            /**
-             * Removes identity assignments from the updates
-             * @return The resulting command
+            /*!
+             * Simplifies this command.
              */
-            Command removeIdentityAssignmentsFromUpdates() const;
-            
+            Command simplify() const;
+                        
         private:
             //  The index of the action associated with this command.
             uint_fast64_t actionIndex;

src/storage/prism/Program.cpp

@@ -1231,7 +1231,7 @@ namespace storm {
                 std::vector<Command> newCommands;
                 for (auto const& command : module.getCommands()) {
                     if (!command.getGuardExpression().isFalse()) {
-                        newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
+                        newCommands.emplace_back(command.simplify());
                     }
                 }
                 

test/functional/builder/ExplicitJitJaniModelBuilderTest.cpp

@@ -2,11 +2,11 @@
 #include "storm-config.h"
 #include "src/parser/PrismParser.h"
 #include "src/storage/jani/Model.h"
-#include "src/builder/ExplicitJitJaniModelBuilder.h"
+#include "src/builder/jit/ExplicitJitJaniModelBuilder.h"
 
 TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     storm::jani::Model janiModel = program.toJani();
     
-    storm::builder::ExplicitJitJaniModelBuilder<double>(janiModel).build();
+    storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
 }