cleaned up jit model builder, added options, added doctor procedure, prepared Markov automata

Former-commit-id: bb8d1d95cc [formerly 6deb9e19a0]
Former-commit-id: d6b8563723

resources/3rdparty/CMakeLists.txt

@@ -74,8 +74,8 @@ link_directories(${Boost_LIBRARY_DIRS})
 include_directories(${Boost_INCLUDE_DIRS})
 list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES})
 message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})")
-#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}")
-#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}")
+# set the information for the config header
+set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}")
 
 #############################################################
 ##

src/builder/BuilderOptions.cpp

@@ -2,6 +2,9 @@
 
 #include "src/logic/Formulas.h"
 
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/IOSettings.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidSettingsException.h"
 
@@ -50,6 +53,8 @@ namespace storm {
                     this->setTerminalStatesFromFormula(*formulas.front());
                 }
             }
+            
+            explorationChecks = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationChecksSet();
         }
         
         void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) {
@@ -146,6 +151,15 @@ namespace storm {
             buildAllRewardModels = true;
             return *this;
         }
+
+        bool BuilderOptions::isExplorationChecksSet() const {
+            return explorationChecks;
+        }
+
+        BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) {
+            explorationChecks = newValue;
+            return *this;
+        }
         
         BuilderOptions& BuilderOptions::addRewardModel(std::string const& rewardModelName) {
             STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway.");

src/builder/BuilderOptions.h

@@ -91,6 +91,7 @@ namespace storm {
             bool isBuildChoiceLabelsSet() const;
             bool isBuildAllRewardModelsSet() const;
             bool isBuildAllLabelsSet() const;
+            bool isExplorationChecksSet() const;
             
             BuilderOptions& setBuildAllRewardModels();
             BuilderOptions& addRewardModel(std::string const& rewardModelName);
@@ -100,6 +101,7 @@ namespace storm {
             BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
             BuilderOptions& addTerminalLabel(std::string const& label, bool value);
             BuilderOptions& setBuildChoiceLabels(bool newValue);
+            BuilderOptions& setExplorationChecks(bool newValue);
             
         private:
             /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are
@@ -123,6 +125,9 @@ namespace storm {
             
             /// A flag indicating whether or not to build choice labels.
             bool buildChoiceLabels;
+            
+            /// A flag that stores whether exploration checks are to be performed.
+            bool explorationChecks;
         };
         
     }

src/builder/jit/Choice.cpp

@@ -7,10 +7,20 @@ namespace storm {
         namespace jit {
             
             template <typename IndexType, typename ValueType>
-            Choice<IndexType, ValueType>::Choice() {
+            Choice<IndexType, ValueType>::Choice() : markovian(false) {
                 // Intentionally left empty.
             }
             
+            template <typename IndexType, typename ValueType>
+            void Choice<IndexType, ValueType>::setMarkovian(bool value) {
+                markovian = value;
+            }
+            
+            template <typename IndexType, typename ValueType>
+            bool Choice<IndexType, ValueType>::isMarkovian() const {
+                return markovian;
+            }
+            
             template <typename IndexType, typename ValueType>
             void Choice<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) {
                 distribution.add(entry);

src/builder/jit/Choice.h

@@ -11,6 +11,9 @@ namespace storm {
             public:
                 Choice();
                 
+                void setMarkovian(bool value);
+                bool isMarkovian() const;
+                
                 void add(DistributionEntry<IndexType, ValueType> const& entry);
                 void add(IndexType const& index, ValueType const& value);
                 void add(Choice<IndexType, ValueType>&& choice);
@@ -66,6 +69,9 @@ namespace storm {
                 
                 /// The reward values associated with this choice.
                 std::vector<ValueType> rewards;
+                
+                /// A flag storing whether this choice is Markovian.
+                bool markovian;
             };
             
         }

src/builder/jit/ExplicitJitJaniModelBuilder.h

@@ -38,74 +38,144 @@ namespace storm {
                 typedef JitModelBuilderInterface<IndexType, ValueType>* (CreateFunctionType)(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder);
                 typedef boost::function<CreateFunctionType> ImportFunctionType;
                 
+                /*!
+                 * Creates a model builder for the given model. The provided options are used to determine which part of
+                 * the model is built.
+                 */
                 ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options = storm::builder::BuilderOptions());
                 
+                /*!
+                 * Builds and returns the sparse model.
+                 */
                 std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
                 
+                /*!
+                 * Performs some checks that can help debug why the model builder does not work. Returns true if the
+                 * general infrastructure for the model builder appears to be working.
+                 */
+                bool doctor() const;
+
             private:
-                void createBuilder(boost::filesystem::path const& dynamicLibraryPath);
-                std::string createSourceCode();
-                boost::filesystem::path writeSourceToTemporaryFile(std::string const& source);
-                boost::filesystem::path compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile);
-                
+                // Helper methods for the doctor() procedure.
+                bool checkTemporaryFileWritable() const;
+                bool checkCompilerWorks() const;
+                bool checkCompilerFlagsWork() const;
+                bool checkBoostAvailable() const;
+                bool checkBoostDllAvailable() const;
+                bool checkStormAvailable() const;
+                
+                /*!
+                 * Executes the given command. If the command fails with a non-zero error code, the error stream content
+                 * is returned and boost::none otherwise.
+                 */
                 static boost::optional<std::string> execute(std::string command);
                 
-                // Functions that generate data maps or data templates.
-                cpptempl::data_list generateInitialStates();
-                
+                /*!
+                 * Writes the given content to a temporary file. The temporary file is created to have the provided suffix.
+                 */
+                static boost::filesystem::path writeToTemporaryFile(std::string const& content, std::string const& suffix = ".cpp");
+
+                /*!
+                 * Assembles the information of the model such that it can be put into the source skeleton.
+                 */
+                cpptempl::data_map generateModelData();
+
+                void generateVariables(cpptempl::data_map& modelData);
                 cpptempl::data_map generateBooleanVariable(storm::jani::BooleanVariable const& variable);
                 cpptempl::data_map generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable);
                 cpptempl::data_map generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable);
                 cpptempl::data_map generateRealVariable(storm::jani::RealVariable const& variable);
                 cpptempl::data_map generateLocationVariable(storm::jani::Automaton const& automaton);
-                void generateVariables(cpptempl::data_map& modelData);
 
-                void generateLocations(cpptempl::data_map& modelData);
+                void generateInitialStates(cpptempl::data_map& modelData);
                 void generateRewards(cpptempl::data_map& modelData);
-                
-                cpptempl::data_list generateLabels();
-                cpptempl::data_list generateTerminalExpressions();
+                void generateLocations(cpptempl::data_map& modelData);
+                void generateLabels(cpptempl::data_map& modelData);
+                void generateTerminalExpressions(cpptempl::data_map& modelData);
+
+                // Functions related to the generation of edge data.
                 void generateEdges(cpptempl::data_map& modelData);
                 cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex);
                 cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments);
-                
                 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;
-                
                 cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const;
-                
                 cpptempl::data_map generateAssignment(storm::jani::Assignment const& assignment);
-                
+
                 // Auxiliary functions that perform regularly needed steps.
                 std::string const& getVariableName(storm::expressions::Variable const& variable) const;
                 std::string const& registerVariable(storm::expressions::Variable const& variable, bool transient = false);
                 storm::expressions::Variable const& getLocationVariable(storm::jani::Automaton const& automaton) const;
-                std::string asString(bool value) const;
                 storm::expressions::Expression shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression);
-
+                
+                // Conversion functions.
                 template <typename ValueTypePrime>
                 std::string asString(ValueTypePrime value) const;
-                
+                std::string asString(bool value) const;
+
+                /*!
+                 * Creates the source code for the shared library that performs the model generation.
+                 *
+                 * @param modelData The assembled data of the model to be put into the blueprint. Note that this is not
+                 * modified in this function, but the data needs to be passed as non-const to cpptempl.
+                 */
+                std::string createSourceCodeFromSkeleton(cpptempl::data_map& modelData);
+                
+                /*!
+                 * Compiles the provided source file to a shared library and returns a path object to the resulting
+                 * binary file.
+                 */
+                boost::filesystem::path compileToSharedLibrary(boost::filesystem::path const& sourceFile);
+
+                /*!
+                 * Loads the given shared library and creates the builder from it.
+                 */
+                void createBuilder(boost::filesystem::path const& dynamicLibraryPath);
+
+                /// The options to use for model building.
                 storm::builder::BuilderOptions options;
+                
+                /// The model specification that is to be built.
                 storm::jani::Model model;
+                
+                /// A vector of automata that is to be put in parallel. The automata are references from the model specification.
                 std::vector<std::reference_wrapper<storm::jani::Automaton const>> parallelAutomata;
                 
+                /// An object that is responsible for building the components of the model. The shared library gets this
+                /// as a mechanism to perform a callback in order to register transitions that were found.
                 ModelComponentsBuilder<IndexType, ValueType> modelComponentsBuilder;
-                typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderGetFunction;
+                
+                /// The function that was loaded from the shared library. We have to keep this function around, because
+                /// otherwise the shared library gets unloaded.
+                typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderCreateFunction;
+                
+                /// The pointer to the builder object created via the shared library.
                 std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>> builder;
                 
+                // Members that store information about the model. They are used in the process of assembling the model
+                // data that is used in the skeleton.
                 std::unordered_map<storm::expressions::Variable, std::string> variableToName;
                 std::map<std::string, storm::expressions::Variable> automatonToLocationVariable;
-                
                 storm::expressions::ToCppVisitor expressionTranslator;
                 std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution;
                 std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
                 std::set<storm::expressions::Variable> transientVariables;
                 std::set<storm::expressions::Variable> nontransientVariables;
                 std::unordered_map<storm::expressions::Variable, std::string> variablePrefixes;
+
+                /// The compiler binary.
+                std::string compiler;
+
+                /// The flags passed to the compiler.
+                std::string compilerFlags;
+                
+                /// The include directory of boost.
+                std::string boostIncludeDirectory;
+                
+                /// The root directory of storm.
+                std::string stormRoot;
             };
 
         }

src/builder/jit/StateBehaviour.cpp

@@ -38,7 +38,7 @@ namespace storm {
             void StateBehaviour<IndexType, ValueType>::addStateRewards(std::vector<ValueType>&& stateRewards) {
                 this->stateRewards = std::move(stateRewards);
             }
-
+            
             template <typename IndexType, typename ValueType>
             std::vector<ValueType> const& StateBehaviour<IndexType, ValueType>::getStateRewards() const {
                 return stateRewards;
@@ -48,49 +48,9 @@ namespace storm {
             void StateBehaviour<IndexType, ValueType>::reduce(storm::jani::ModelType const& modelType) {
                 if (choices.size() > 1) {
                     if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) {
-                        std::size_t totalCount = choices.size();
-
-                        ValueType totalExitRate = modelType == storm::jani::ModelType::DTMC ? static_cast<ValueType>(totalCount) : storm::utility::zero<ValueType>();
-
-                        if (choices.front().getNumberOfRewards() > 0) {
-                            std::vector<ValueType> newRewards(choices.front().getNumberOfRewards());
-                            
-                            if (modelType == storm::jani::ModelType::CTMC) {
-                                for (auto const& choice : choices) {
-                                    ValueType massOfChoice = storm::utility::zero<ValueType>();
-                                    for (auto const& entry : choices.front().getDistribution()) {
-                                        massOfChoice += entry.getValue();
-                                    }
-                                    
-                                    auto outIt = newRewards.begin();
-                                    for (auto const& reward : choice.getRewards()) {
-                                        *outIt += reward * massOfChoice / totalExitRate;
-                                        ++outIt;
-                                    }
-                                }
-                            } else {
-                                for (auto const& choice : choices) {
-                                    auto outIt = newRewards.begin();
-                                    for (auto const& reward : choice.getRewards()) {
-                                        *outIt += reward / totalExitRate;
-                                        ++outIt;
-                                    }
-                                }
-                            }
-
-                            choices.front().setRewards(std::move(newRewards));
-                        }
-                        
-                        for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) {
-                            choices.front().add(std::move(*it));
-                        }
-                        
-                        choices.resize(1);
-                        choices.front().compress();
-
-                        if (modelType == storm::jani::ModelType::DTMC) {
-                            choices.front().divideDistribution(static_cast<ValueType>(totalCount));
-                        }
+                        reduceDeterministic(modelType);
+                    } else if (modelType == storm::jani::ModelType::MA) {
+                        reduceMarkovAutomaton();
                     } else {
                         for (auto& choice : choices) {
                             choice.compress();
@@ -101,6 +61,93 @@ namespace storm {
                 }
             }
             
+            template <typename IndexType, typename ValueType>
+            void StateBehaviour<IndexType, ValueType>::reduceDeterministic(storm::jani::ModelType const& modelType) {
+                std::size_t totalCount = choices.size();
+                
+                ValueType totalExitRate = modelType == storm::jani::ModelType::DTMC ? static_cast<ValueType>(totalCount) : storm::utility::zero<ValueType>();
+                
+                if (choices.front().getNumberOfRewards() > 0) {
+                    std::vector<ValueType> newRewards(choices.front().getNumberOfRewards());
+                    
+                    if (modelType == storm::jani::ModelType::CTMC) {
+                        for (auto const& choice : choices) {
+                            ValueType massOfChoice = storm::utility::zero<ValueType>();
+                            for (auto const& entry : choices.front().getDistribution()) {
+                                massOfChoice += entry.getValue();
+                            }
+                            
+                            auto outIt = newRewards.begin();
+                            for (auto const& reward : choice.getRewards()) {
+                                *outIt += reward * massOfChoice / totalExitRate;
+                                ++outIt;
+                            }
+                        }
+                    } else {
+                        for (auto const& choice : choices) {
+                            auto outIt = newRewards.begin();
+                            for (auto const& reward : choice.getRewards()) {
+                                *outIt += reward / totalExitRate;
+                                ++outIt;
+                            }
+                        }
+                    }
+                    
+                    choices.front().setRewards(std::move(newRewards));
+                }
+                
+                for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) {
+                    choices.front().add(std::move(*it));
+                }
+                
+                choices.resize(1);
+                choices.front().compress();
+                
+                if (modelType == storm::jani::ModelType::DTMC) {
+                    choices.front().divideDistribution(static_cast<ValueType>(totalCount));
+                }
+            }
+            
+            template <typename IndexType, typename ValueType>
+            void StateBehaviour<IndexType, ValueType>::reduceMarkovAutomaton() {
+                // If the model we build is a Markov Automaton, we reduce the choices by summing all Markovian choices
+                // and making the Markovian choice the very first one (if there is any).
+                bool foundPreviousMarkovianChoice = false;
+                uint64_t numberOfChoicesToDelete = 0;
+                
+                for (uint_fast64_t index = 0; index + numberOfChoicesToDelete < this->size();) {
+                    Choice<IndexType, ValueType>& choice = choices[index];
+                    
+                    if (choice.isMarkovian()) {
+                        if (foundPreviousMarkovianChoice) {
+                            // If there was a previous Markovian choice, we need to sum them. Note that we can assume
+                            // that the previous Markovian choice is the very first one in the choices vector.
+                            choices.front().add(std::move(choice));
+                            
+                            // Swap the choice to the end to indicate it can be removed (if it's not already there).
+                            if (index != this->size() - 1) {
+                                choice = std::move(choices[choices.size() - 1 - numberOfChoicesToDelete]);
+                            }
+                            ++numberOfChoicesToDelete;
+                        } else {
+                            // If there is no previous Markovian choice, just move the Markovian choice to the front.
+                            if (index != 0) {
+                                std::swap(choices.front(), choice);
+                                foundPreviousMarkovianChoice = true;
+                            }
+                            ++index;
+                        }
+                    } else {
+                        ++index;
+                    }
+                }
+                
+                // Finally remove the choices that were added to other Markovian choices.
+                if (numberOfChoicesToDelete > 0) {
+                    choices.resize(choices.size() - numberOfChoicesToDelete);
+                }
+            }
+            
             template <typename IndexType, typename ValueType>
             bool StateBehaviour<IndexType, ValueType>::isExpanded() const {
                 return expanded;
@@ -120,7 +167,7 @@ namespace storm {
             std::size_t StateBehaviour<IndexType, ValueType>::size() const {
                 return choices.size();
             }
-
+            
             template <typename IndexType, typename ValueType>
             void StateBehaviour<IndexType, ValueType>::clear() {
                 choices.clear();

src/builder/jit/StateBehaviour.h

@@ -43,9 +43,20 @@ namespace storm {
                 void clear();
                 
             private:
+                /*!
+                 * Reduces the choices of this state to make it a valid DTMC/CTMC behaviour.
+                 */
+                void reduceDeterministic(storm::jani::ModelType const& modelType);
+
+                /*!
+                 * Reduces the choices of this state to make it a valid MA behaviour.
+                 */
+                void reduceMarkovAutomaton();
+
+                /// The actual choices of this behaviour.
                 ContainerType choices;
                 
-                // The state rewards (under the different, selected reward models) of the state.
+                /// The state rewards (under the different, selected reward models) of the state.
                 std::vector<ValueType> stateRewards;
                 
                 bool compressed;

src/generator/JaniNextStateGenerator.cpp

@@ -273,7 +273,10 @@ namespace storm {
                     ++integerIt;
                 }
                 int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
-                STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+                if (this->options.isExplorationChecksSet()) {
+                    STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+                    STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+                }
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
                 STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
             }
@@ -424,15 +427,20 @@ namespace storm {
                             // Update the choice by adding the probability/target state to it.
                             probability = exitRate ? exitRate.get() * probability : probability;
                             choice.addProbability(stateIndex, probability);
-                            probabilitySum += probability;
+                            
+                            if (this->options.isExplorationChecksSet()) {
+                                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 << ").");
+                    if (this->options.isExplorationChecksSet()) {
+                        // 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 << ").");
+                    }
                 }
                 
                 ++automatonIndex;
@@ -450,8 +458,10 @@ namespace storm {
                 
                 // Only process this action, if there is at least one feasible solution.
                 if (!enabledEdges.empty()) {
-                    // Check whether a global variable is written multiple times in any combination.
-                    checkGlobalVariableWritesValid(enabledEdges);
+                    if (this->options.isExplorationChecksSet()) {
+                        // Check whether a global variable is written multiple times in any combination.
+                        checkGlobalVariableWritesValid(enabledEdges);
+                    }
                     
                     std::vector<std::vector<storm::jani::Edge const*>::const_iterator> iteratorList(enabledEdges.size());
                     
@@ -525,8 +535,10 @@ namespace storm {
                             probabilitySum += stateProbabilityPair.second;
                         }
                         
-                        // 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 sum to one for some command (actually sum to " << probabilitySum << ").");
+                        if (this->options.isExplorationChecksSet()) {
+                            // 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 sum to one for some command (actually sum to " << probabilitySum << ").");
+                        }
                         
                         // Dispose of the temporary maps.
                         delete currentTargetStates;

src/generator/JaniNextStateGenerator.h

@@ -115,7 +115,7 @@ namespace storm {
             /// A vector storing information about the corresponding reward models (variables).
             std::vector<storm::builder::RewardModelInformation> rewardModelInformation;
             
-            // A flag that stores whether at least one of the selected reward models has state-action rewards.
+            /// A flag that stores whether at least one of the selected reward models has state-action rewards.
             bool hasStateActionRewards;
         };
         

src/generator/NextStateGenerator.cpp

@@ -120,7 +120,7 @@ namespace storm {
                             
                             // Swap the choice to the end to indicate it can be removed (if it's not already there).
                             if (index != result.getNumberOfChoices() - 1) {
-                                std::swap(choice, result.getChoices().back());
+                                choice = std::move(result.getChoices()[result.getNumberOfChoices() - 1 - numberOfChoicesToDelete]);
                             }
                             ++numberOfChoicesToDelete;
                         } else {

src/generator/PrismNextStateGenerator.cpp

@@ -308,8 +308,10 @@ namespace storm {
                     ++integerIt;
                 }
                 int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression());
-                STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
-                STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
+                if (this->options.isExplorationChecksSet()) {
+                    STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
+                    STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
+                }
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
                 STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
             }
@@ -422,8 +424,10 @@ namespace storm {
                         choice.addReward(stateActionRewardValue);
                     }
                     
-                    // Check that the resulting distribution is in fact a distribution.
-                    STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+                    if (this->options.isExplorationChecksSet()) {
+                        // Check that the resulting distribution is in fact a distribution.
+                        STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+                    }
                 }
             }
             
@@ -508,11 +512,15 @@ namespace storm {
                         for (auto const& stateProbabilityPair : *newTargetStates) {
                             StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
                             choice.addProbability(actualIndex, stateProbabilityPair.second);
-                            probabilitySum += stateProbabilityPair.second;
+                            if (this->options.isExplorationChecksSet()) {
+                                probabilitySum += stateProbabilityPair.second;
+                            }
                         }
                         
-                        // Check that the resulting distribution is in fact a distribution.
-                        STORM_LOG_THROW(!program.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 << ").");
+                        if (this->options.isExplorationChecksSet()) {
+                            // Check that the resulting distribution is in fact a distribution.
+                            STORM_LOG_THROW(!program.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 << ").");
+                        }
                         
                         // Create the state-action reward for the newly created choice.
                         for (auto const& rewardModel : rewardModels) {

src/parser/JaniParser.cpp

@@ -426,7 +426,6 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString);
                 }
             }
-            
         }
         
         storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) {

src/settings/modules/IOSettings.cpp

@@ -24,6 +24,8 @@ namespace storm {
             const std::string IOSettings::jitOptionName = "jit";
             const std::string IOSettings::explorationOrderOptionName = "explorder";
             const std::string IOSettings::explorationOrderOptionShortName = "eo";
+            const std::string IOSettings::explorationChecksOptionName = "explchecks";
+            const std::string IOSettings::explorationChecksOptionShortName = "ec";
             const std::string IOSettings::transitionRewardsOptionName = "transrew";
             const std::string IOSettings::stateRewardsOptionName = "staterew";
             const std::string IOSettings::choiceLabelingOptionName = "choicelab";
@@ -51,13 +53,14 @@ 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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
@@ -141,6 +144,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'.");
             }
             
+            bool IOSettings::isExplorationChecksSet() const {
+                return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
+            }
+            
             bool IOSettings::isTransitionRewardsSet() const {
                 return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet();
             }

src/settings/modules/IOSettings.h

@@ -130,6 +130,13 @@ namespace storm {
                  */
                 bool isExplorationOrderSet() const;
                 
+                /*!
+                 * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.).
+                 *
+                 * @return True if additional checks are to be performed.
+                 */
+                bool isExplorationChecksSet() const;
+                
                 /*!
                  * Retrieves the exploration order if it was set.
                  *
@@ -244,6 +251,8 @@ namespace storm {
                 static const std::string janiInputOptionName;
                 static const std::string prismToJaniOptionName;
                 static const std::string jitOptionName;
+                static const std::string explorationChecksOptionName;
+                static const std::string explorationChecksOptionShortName;
                 static const std::string explorationOrderOptionName;
                 static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;

src/settings/modules/JitBuilderSettings.cpp

@@ -14,22 +14,60 @@ namespace storm {
         namespace modules {
             const std::string JitBuilderSettings::moduleName = "jitbuilder";
             
-            const std::string JitBuilderSettings::noJitOptionName = "nojit";
             const std::string JitBuilderSettings::doctorOptionName = "doctor";
-            
+            const std::string JitBuilderSettings::compilerOptionName = "compiler";
+            const std::string JitBuilderSettings::stormRootOptionName = "storm";
+            const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost";
+            const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags";
+
             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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the executable. Defaults to c++.").setDefaultValueString("c++").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, stormRootOptionName, false, "The root directory of Storm.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the src/ subtree of Storm.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build());
+            }
+            
+            bool JitBuilderSettings::isCompilerSet() const {
+                return this->getOption(compilerOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string JitBuilderSettings::getCompiler() const {
+                return this->getOption(compilerOptionName).getArgumentByName("name").getValueAsString();
+            }
+            
+            bool JitBuilderSettings::isStormRootSet() const {
+                return this->getOption(stormRootOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string JitBuilderSettings::getStormRoot() const {
+                return this->getOption(stormRootOptionName).getArgumentByName("dir").getValueAsString();
+            }
+            
+            bool JitBuilderSettings::isBoostIncludeDirectorySet() const {
+                return this->getOption(boostIncludeDirectoryOptionName).getHasOptionBeenSet();
             }
             
-//            bool JitBuilderSettings::isNoJitSet() const {
-//                return this->getOption(noJitOptionName).getHasOptionBeenSet();
-//            }
+            std::string JitBuilderSettings::getBoostIncludeDirectory() const {
+                return this->getOption(boostIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString();
+            }
 
             bool JitBuilderSettings::isDoctorSet() const {
                 return this->getOption(doctorOptionName).getHasOptionBeenSet();
             }
-                        
+            
+            bool JitBuilderSettings::isCompilerFlagsSet() const {
+                return this->getOption(compilerFlagsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string JitBuilderSettings::getCompilerFlags() const {
+                return this->getOption(compilerFlagsOptionName).getArgumentByName("flags").getValueAsString();
+            }
+            
             void JitBuilderSettings::finalize() {
                 // Intentionally left empty.
             }

src/settings/modules/JitBuilderSettings.h

@@ -12,18 +12,31 @@ namespace storm {
                  * Creates a new JitBuilder settings object.
                  */
                 JitBuilderSettings();
-                
-//                bool isNoJitSet() const;
 
                 bool isDoctorSet() const;
                 
+                bool isCompilerSet() const;
+                std::string getCompiler() const;
+                
+                bool isStormRootSet() const;
+                std::string getStormRoot() const;
+                
+                bool isBoostIncludeDirectorySet() const;
+                std::string getBoostIncludeDirectory() const;
+                
+                bool isCompilerFlagsSet() const;
+                std::string getCompilerFlags() const;
+                
                 bool check() const override;
                 void finalize() override;
                 
                 static const std::string moduleName;
                 
             private:
-                static const std::string noJitOptionName;
+                static const std::string compilerOptionName;
+                static const std::string stormRootOptionName;
+                static const std::string boostIncludeDirectoryOptionName;
+                static const std::string compilerFlagsOptionName;
                 static const std::string doctorOptionName;
             };
             

src/utility/storm.h

@@ -22,7 +22,7 @@
 #include "src/settings/modules/ParametricSettings.h"
 #include "src/settings/modules/RegionSettings.h"
 #include "src/settings/modules/EliminationSettings.h"
-#include "src/settings/modules/CoreSettings.h"
+#include "src/settings/modules/JitBuilderSettings.h"
 
 // Formula headers.
 #include "src/logic/Formulas.h"
@@ -124,7 +124,15 @@ namespace storm {
 
         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::jit::ExplicitJitJaniModelBuilder<ValueType> builder(model.asJaniModel(), options);
+
+            if (storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet()) {
+                bool result = builder.doctor();
+                STORM_LOG_THROW(result, storm::exceptions::InvalidSettingsException, "The JIT-based model builder cannot be used on your system.");
+                STORM_LOG_INFO("The JIT-based model builder seems to be working.");
+            }
+            
             return builder.build();
         } else {
             std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;

storm-config.h.in

@@ -14,6 +14,9 @@
 // The path used in the functional and performance tests to load the supplied example files
 #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@"
 
+// The path to boost used during compilation. 
+#define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@"
+
 // Whether Gurobi is available and to be used (define/undef)
 #cmakedefine STORM_HAVE_GUROBI