Merge branch 'master' into reward-bounded-multi-objective

CMakeLists.txt

@@ -14,7 +14,8 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmak
 include(ExternalProject)
 include(RegisterSourceGroup)
 include(imported)
-
+include(CheckCXXSourceCompiles)
+include(CheckCSourceCompiles)
 
 #############################################################
 ##
@@ -292,6 +293,31 @@ else()
 	set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fomit-frame-pointer")
 endif()
 
+# Test compiler by compiling small program.
+CHECK_C_SOURCE_COMPILES("
+	#include <stdio.h>
+	int main() {
+		const char* text = \"A Storm is coming.\";
+		return 0;
+	}"
+	COMPILER_C_WORKS
+)
+CHECK_CXX_SOURCE_COMPILES("
+	#include <string>
+	int main() {
+		const std::string text = \"A Storm is coming.\";
+		return 0;
+	}"
+	COMPILER_CXX_WORKS
+)
+if ((NOT COMPILER_CXX_WORKS) OR (NOT COMPILER_C_WORKS))
+	if (MACOSX)
+		message(FATAL_ERROR "The C/C++ compiler is not configured correctly.\nTry running 'xcode-select --install'.")
+	else()
+		message(FATAL_ERROR "The C/C++ compiler is not configured correctly.")
+	endif()
+endif()
+
 #############################################################
 ##
 ##	RPATH settings

src/storm-cli-utilities/model-handling.h

@@ -27,6 +27,7 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/ResourceSettings.h"
 #include "storm/settings/modules/JitBuilderSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -50,7 +51,7 @@ namespace storm {
         void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) {
             if (ioSettings.isPrismOrJaniInputSet()) {
                 if (ioSettings.isPrismInputSet()) {
-                    input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename());
+                    input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled());
                 } else {
                     auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename());
                     input.model = janiInput.first;
@@ -95,6 +96,7 @@ namespace storm {
 
         SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
 
             SymbolicInput output = input;
@@ -113,7 +115,7 @@ namespace storm {
             // Check whether conversion for PRISM to JANI is requested or necessary.
             if (input.model && input.model.get().isPrismProgram()) {
                 bool transformToJani = ioSettings.isPrismToJaniSet();
-                bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet();
+                bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && buildSettings.isJitSet();
                 STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model.");
                 transformToJani |= transformToJaniForJit;
 
@@ -171,22 +173,22 @@ namespace storm {
 
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
-            return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet());
+            return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildFullModelSet());
         }
 
         template <typename ValueType>
-        std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
+        std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) {
             auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             storm::builder::BuilderOptions options(createFormulasToRespect(input.properties));
-            options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet());
-            options.setBuildStateValuations(ioSettings.isBuildStateValuationsSet());
+            options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet());
+            options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet());
             options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
-            options.setBuildAllLabels(ioSettings.isBuildFullModelSet());
-            options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet());
-            if (ioSettings.isBuildFullModelSet()) {
+            options.setBuildAllLabels(buildSettings.isBuildFullModelSet());
+            options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet());
+            if (buildSettings.isBuildFullModelSet()) {
                 options.clearTerminalStates();
             }
-            return storm::api::buildSparseModel<ValueType>(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
+            return storm::api::buildSparseModel<ValueType>(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
         }
 
         template <typename ValueType>
@@ -206,13 +208,14 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
             storm::utility::Stopwatch modelBuildingWatch(true);
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
 
             std::shared_ptr<storm::models::ModelBase> result;
             if (input.model) {
                 if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
                     result = buildModelDd<DdType, ValueType>(input);
                 } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
-                    result = buildModelSparse<ValueType>(input, ioSettings);
+                    result = buildModelSparse<ValueType>(input, buildSettings);
                 }
             } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
                 STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
@@ -254,18 +257,17 @@ namespace storm {
         std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
         auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
         auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
-        auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
 
         std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
 
         if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-        result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
-        result.second = true;
+            result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+            result.second = true;
         }
 
         if (generalSettings.isBisimulationSet()) {
-        result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
-        result.second = true;
+            result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
+            result.second = true;
         }
 
         return result;
@@ -597,8 +599,9 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
-            if (!ioSettings.isNoBuildModelSet()) {
+            if (!buildSettings.isNoBuildModelSet()) {
                 model = buildModel<DdType, ValueType>(engine, input, ioSettings);
             }
 

src/storm-dft/settings/DftSettings.cpp

@@ -16,8 +16,8 @@
 #include "storm/settings/modules/BisimulationSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 #include "storm/settings/modules/JaniExportSettings.h"
-#include "storm/settings/modules/GSPNSettings.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
+#include "storm-gspn/settings/modules/GSPNSettings.h"
+#include "storm-gspn/settings/modules/GSPNExportSettings.h"
 
 
 namespace storm {

src/storm-gspn-cli/storm-gspn.cpp

@@ -28,8 +28,8 @@
 #include "storm/exceptions/FileIoException.h"
 
 #include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/GSPNSettings.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
+#include "storm-gspn/settings/modules/GSPNSettings.h"
+#include "storm-gspn/settings/modules/GSPNExportSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/JaniExportSettings.h"

src/storm/settings/modules/GSPNExportSettings.cpp → src/storm-gspn/settings/modules/GSPNExportSettings.cpp

@@ -1,5 +1,5 @@
-#include "GSPNExportSettings.h"
-#include "JaniExportSettings.h"
+#include "storm-gspn/settings/modules/GSPNExportSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/SettingMemento.h"

src/storm/settings/modules/GSPNSettings.cpp → src/storm-gspn/settings/modules/GSPNSettings.cpp

@@ -1,4 +1,4 @@
-#include "GSPNSettings.h"
+#include "storm-gspn/settings/modules/GSPNSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/SettingMemento.h"

src/storm-gspn/storm-gspn.h

@@ -6,7 +6,7 @@
 #include "storm-gspn/storage/gspn/GSPN.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
+#include "storm-gspn/settings/modules/GSPNExportSettings.h"
 
 #include "storm/utility/file.h"
 

src/storm-pars-cli/storm-pars.cpp

@@ -29,34 +29,6 @@ namespace storm {
     
         typedef typename storm::cli::SymbolicInput SymbolicInput;
 
-        template <typename ValueType>
-        std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
-            return storm::api::buildSparseModel<ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet());
-        }
-
-        template <storm::dd::DdType DdType, typename ValueType>
-        std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
-            storm::utility::Stopwatch modelBuildingWatch(true);
-
-            std::shared_ptr<storm::models::ModelBase> result;
-            if (input.model) {
-                if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
-                    result = storm::cli::buildModelDd<DdType, ValueType>(input);
-                } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
-                    result = storm::pars::buildModelSparse<ValueType>(input, ioSettings);
-                }
-            } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) {
-                STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
-                result = storm::cli::buildModelExplicit<ValueType>(ioSettings);
-            }
-
-            modelBuildingWatch.stop();
-            if (result) {
-                STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
-            }
-
-            return result;
-        }
 
         
         template <typename ValueType>
@@ -271,14 +243,16 @@ namespace storm {
         void processInputWithValueTypeAndDdlib(SymbolicInput& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
             
             auto engine = coreSettings.getEngine();
             STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
             
             std::shared_ptr<storm::models::ModelBase> model;
-            if (!ioSettings.isNoBuildModelSet()) {
-                model = storm::pars::buildModel<DdType, ValueType>(engine, input, ioSettings);
+            if (!buildSettings.isNoBuildModelSet()) {
+                model = storm::cli::buildModel<DdType, ValueType>(engine, input, ioSettings);
             }
             
             if (model) {

src/storm-pars/settings/ParsSettings.cpp

@@ -1,3 +1,4 @@
+#include <storm/settings/modules/CounterexampleGeneratorSettings.h>
 #include "storm-pars/settings/ParsSettings.h"
 
 #include "storm-pars/settings/modules/ParametricSettings.h"
@@ -7,6 +8,7 @@
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/SylvanSettings.h"
 #include "storm/settings/modules/EigenEquationSolverSettings.h"
@@ -33,7 +35,10 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::CoreSettings>();
             storm::settings::addModule<storm::settings::modules::ParametricSettings>();
             storm::settings::addModule<storm::settings::modules::RegionSettings>();
-            
+            storm::settings::addModule<storm::settings::modules::BuildSettings>();
+            storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+
+
             storm::settings::addModule<storm::settings::modules::DebugSettings>();
             storm::settings::addModule<storm::settings::modules::SylvanSettings>();
             storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();

src/storm-pgcl-cli/storm-pgcl.cpp

@@ -15,7 +15,7 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
-#include "storm/settings/modules/PGCLSettings.h"
+#include "storm-pgcl/settings/modules/PGCLSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/JaniExportSettings.h"

src/storm/settings/modules/PGCLSettings.cpp → src/storm-pgcl/settings/modules/PGCLSettings.cpp

@@ -1,4 +1,4 @@
-#include "storm/settings/modules/PGCLSettings.h"
+#include "PGCLSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/SettingMemento.h"

src/storm/adapters/Z3ExpressionAdapter.cpp

@@ -237,7 +237,7 @@ namespace storm {
             }
             
             boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&)  {
-                return context.int_val(static_cast<int>(expression.getValue()));
+                return context.int_val(static_cast<long long>(expression.getValue()));
             }
             
             boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data)  {

src/storm/api/model_descriptions.cpp

@@ -6,11 +6,15 @@
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/Property.h"
 
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/BuildSettings.h"
+
 namespace storm {
     namespace api {
         
-        storm::prism::Program parseProgram(std::string const& filename) {
-            storm::prism::Program program = storm::parser::PrismParser::parse(filename).simplify().simplify();
+        storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility) {
+            storm::prism::Program program = storm::parser::PrismParser::parse(filename, prismCompatibility).simplify().simplify();
             program.checkValidity();
             return program;
         }

src/storm/api/model_descriptions.h

@@ -14,7 +14,7 @@ namespace storm {
     
     namespace api {
         
-        storm::prism::Program parseProgram(std::string const& filename);
+        storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false);
         
         std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename);
         

src/storm/builder/BuilderOptions.cpp

@@ -3,7 +3,7 @@
 #include "storm/logic/Formulas.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/settings/modules/GeneralSettings.h"
 
 #include "storm/utility/macros.h"
@@ -55,9 +55,9 @@ namespace storm {
                 }
             }
             
-            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto const& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            explorationChecks = ioSettings.isExplorationChecksSet();
+            explorationChecks = buildSettings.isExplorationChecksSet();
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
         }

src/storm/builder/ExplicitModelBuilder.cpp

@@ -11,7 +11,7 @@
 #include "storm/storage/expressions/ExpressionManager.h"
 
 #include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 
 #include "storm/builder/RewardModelBuilder.h"
 #include "storm/builder/ChoiceInformationBuilder.h"
@@ -43,7 +43,7 @@ namespace storm {
     namespace builder {
                         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::IOSettings>().getExplorationOrder()) {
+        ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) {
             // Intentionally left empty.
         }
         
@@ -89,20 +89,22 @@ namespace storm {
             // Check, if the state was already registered.
             std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
             
-            if (actualIndexBucketPair.first == newIndex) {
+            StateType actualIndex = actualIndexBucketPair.first;
+            
+            if (actualIndex == newIndex) {
                 if (options.explorationOrder == ExplorationOrder::Dfs) {
-                    statesToExplore.push_front(state);
+                    statesToExplore.emplace_front(state, actualIndex);
 
                     // Reserve one slot for the new state in the remapping.
                     stateRemapping.get().push_back(storm::utility::zero<StateType>());
                 } else if (options.explorationOrder == ExplorationOrder::Bfs) {
-                    statesToExplore.push_back(state);
+                    statesToExplore.emplace_back(state, actualIndex);
                 } else {
                     STORM_LOG_ASSERT(false, "Invalid exploration order.");
                 }
             }
             
-            return actualIndexBucketPair.first;
+            return actualIndex;
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
@@ -139,8 +141,8 @@ namespace storm {
             // Perform a search through the model.
             while (!statesToExplore.empty()) {
                 // Get the first state in the queue.
-                CompressedState currentState = statesToExplore.front();
-                StateType currentIndex = stateStorage.stateToId.getValue(currentState);
+                CompressedState currentState = statesToExplore.front().first;
+                StateType currentIndex = statesToExplore.front().second;
                 statesToExplore.pop_front();
                 
                 // If the exploration order differs from breadth-first, we remember that this row group was actually
@@ -149,7 +151,9 @@ namespace storm {
                     stateRemapping.get()[currentIndex] = currentRowGroup;
                 }
                 
-                STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
+                if (currentIndex % 100000 == 0) {
+                    STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
+                }
                 
                 generator->load(currentState);
                 storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
@@ -304,7 +308,7 @@ namespace storm {
             
             buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates);
             
-            // initialize the model components with the obtained information.
+            // Initialize the model components with the obtained information.
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
             
             // Now finalize all reward models.
@@ -314,7 +318,7 @@ namespace storm {
             // Build the choice labeling
             modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
             
-            // if requested, build the state valuations and choice origins
+            // If requested, build the state valuations and choice origins
             if (generator->getOptions().isBuildStateValuationsSet()) {
                 std::vector<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount());
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
@@ -332,7 +336,7 @@ namespace storm {
         
         template <typename ValueType, typename RewardModelType, typename StateType>
         storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
-            return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
+            return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
         }
         
         // Explicitly instantiate the class.

src/storm/builder/ExplicitModelBuilder.h

@@ -136,7 +136,7 @@ namespace storm {
             storm::storage::sparse::StateStorage<StateType> stateStorage;
             
             /// A set of states that still need to be explored.
-            std::deque<CompressedState> statesToExplore;
+            std::deque<std::pair<CompressedState, StateType>> statesToExplore;
             
             /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be
             /// built in case the exploration order is not BFS.

src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -451,7 +451,7 @@ namespace storm {
                             // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
                             // to add an additional clause that says that the right-hand side of the implication is also true if all commands
                             // of the current choice have enabled synchronization options.
-                            storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false);
+                            storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(true);
                             for (auto label : labelSetFollowingSetsPair.first) {
                                 storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false);
                                 std::set<boost::container::flat_set<uint_fast64_t>> const& synchsForCommand = synchronizingLabels.at(label);

src/storm/exceptions/InternalException.h

@@ -0,0 +1,12 @@
+#pragma once
+
+#include "storm/exceptions/BaseException.h"
+#include "storm/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+        
+        STORM_NEW_EXCEPTION(InternalException)
+        
+    }
+}

src/storm/generator/JaniNextStateGenerator.cpp

@@ -608,7 +608,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
+        storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
             // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
             // create a list of boolean transient variables and the expressions that define them.
             std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
@@ -625,7 +625,7 @@ namespace storm {
                 transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
             }
             
-            return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
+            return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
         }
         
         template<typename ValueType, typename StateType>

src/storm/generator/JaniNextStateGenerator.h

@@ -30,7 +30,7 @@ namespace storm {
             virtual std::size_t getNumberOfRewardModels() const override;
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
                         
-            virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
+            virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
             
         private:
             /*!

src/storm/generator/NextStateGenerator.cpp

@@ -53,7 +53,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
+        storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
             
             for (auto const& expression : this->options.getExpressionLabels()) {
                 std::stringstream stream;
@@ -67,12 +67,14 @@ namespace storm {
             labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it));
             
             // Prepare result.
-            storm::models::sparse::StateLabeling result(states.size());
+            storm::models::sparse::StateLabeling result(stateStorage.getNumberOfStates());
             
             // Initialize labeling.
             for (auto const& label : labelsAndExpressions) {
                 result.addLabel(label.first);
             }
+            
+            storm::storage::BitVectorHashMap<StateType> const& states = stateStorage.stateToId;
             for (auto const& stateIndexPair : states) {
                 unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
                 

src/storm/generator/NextStateGenerator.h

@@ -7,7 +7,7 @@
 #include <boost/variant.hpp>
 
 #include "storm/storage/expressions/Expression.h"
-#include "storm/storage/BitVectorHashMap.h"
+#include "storm/storage/sparse/StateStorage.h"
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/storage/sparse/ChoiceOrigins.h"
 
@@ -61,7 +61,7 @@ namespace storm {
             
             storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
             
-            virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
+            virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
             
             NextStateGeneratorOptions const& getOptions() const;
             
@@ -71,7 +71,7 @@ namespace storm {
             /*!
              * Creates the state labeling for the given states using the provided labels and expressions.
              */
-            storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
+            storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
             
             void postprocess(StateBehavior<ValueType, StateType>& result);
             

src/storm/generator/PrismNextStateGenerator.cpp

@@ -575,7 +575,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
+        storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
             // Gather a vector of labels and their expressions.
             std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
             if (this->options.isBuildAllLabelsSet()) {
@@ -592,7 +592,7 @@ namespace storm {
                 }
             }
             
-            return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, labels);
+            return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
         }
         
         template<typename ValueType, typename StateType>

src/storm/generator/PrismNextStateGenerator.h

@@ -28,7 +28,7 @@ namespace storm {
             virtual std::size_t getNumberOfRewardModels() const override;
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
             
-            virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
+            virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
 
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
 

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -104,7 +104,7 @@ namespace storm {
                     for (uint64_t i = 0; i < this->objectives.size(); ++i) {
                         headers.push_back("obj" + std::to_string(i));
                     }
-                    storm::utility::exportDataToCSVFile<ValueType, ValueType, std::string>("cdf" + std::to_string(numChecks) + ".csv", cdfData, weightVector, headers);
+                    storm::utility::exportDataToCSVFile<ValueType, ValueType, std::string>(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportCdfDirectory() + "cdf" + std::to_string(numChecks) + ".csv", cdfData, weightVector, headers);
                 }
                 auto solution = rewardUnfolding.getInitialStateResult(initEpoch);
                 auto solutionIt = solution.begin();

src/storm/parser/ImcaMarkovAutomatonParser.cpp

@@ -1,7 +1,7 @@
 #include "storm/parser/ImcaMarkovAutomatonParser.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/utility/file.h"
 #include "storm/utility/builder.h"
@@ -11,7 +11,7 @@ namespace storm {
 
         template <typename ValueType, typename StateType>
         ImcaParserGrammar<ValueType, StateType>::ImcaParserGrammar() : ImcaParserGrammar<ValueType, StateType>::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) {
-            buildChoiceLabels = storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildChoiceLabelsSet();
+            buildChoiceLabels = storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildChoiceLabelsSet();
             initialize();
         }
         

src/storm/parser/PrismParser.cpp

@@ -2,7 +2,6 @@
 
 #include "storm/storage/prism/Compositions.h"
 
-#include "storm/settings/SettingsManager.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidTypeException.h"
@@ -16,7 +15,7 @@
 
 namespace storm {
     namespace parser {
-        storm::prism::Program PrismParser::parse(std::string const& filename) {
+        storm::prism::Program PrismParser::parse(std::string const& filename, bool prismCompatibility) {
             // Open file and initialize result.
             std::ifstream inputFileStream;
             storm::utility::openFile(filename, inputFileStream);
@@ -25,7 +24,7 @@ namespace storm {
             // Now try to parse the contents of the file.
             try {
                 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
-                result = parseFromString(fileContent, filename);
+                result = parseFromString(fileContent, filename, prismCompatibility);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
                 storm::utility::closeFile(inputFileStream);
@@ -37,7 +36,7 @@ namespace storm {
             return result;
         }
         
-        storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) {
+        storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) {
             PositionIteratorType first(input.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(input.end());
@@ -47,7 +46,7 @@ namespace storm {
             storm::prism::Program result;
             
             // Create grammar.
-            storm::parser::PrismParser grammar(filename, first);
+            storm::parser::PrismParser grammar(filename, first, prismCompatibility);
             try {
                 // Start first run.
                 bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
@@ -74,7 +73,7 @@ namespace storm {
             return result;
         }
         
-        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) {
+        PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) {
             
             ExpressionParser& expression_ = *expressionParser;
             // Parse simple identifier.
@@ -671,8 +670,9 @@ namespace storm {
                 STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'.");
                 finalModelType = storm::prism::Program::ModelType::MDP;
             }
+
             
-            return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun);
+            return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
         }
         
         void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {

src/storm/parser/PrismParser.h

@@ -77,7 +77,7 @@ namespace storm {
              * @param filename the name of the file to parse.
              * @return The resulting PRISM program.
              */
-            static storm::prism::Program parse(std::string const& filename);
+            static storm::prism::Program parse(std::string const& filename, bool prismCompatability = false);
             
             /*!
              * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
@@ -86,7 +86,7 @@ namespace storm {
              * @param filename The name of the file from which the input was read.
              * @return The resulting PRISM program.
              */
-            static storm::prism::Program parseFromString(std::string const& input, std::string const& filename);
+            static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool prismCompatability = false);
             
         private:
             struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
@@ -150,7 +150,7 @@ namespace storm {
              * @param filename The filename that is to be read. This is used for proper error reporting.
              * @param first The iterator to the beginning of the input.
              */
-            PrismParser(std::string const& filename, Iterator first);
+            PrismParser(std::string const& filename, Iterator first, bool prismCompatibility);
             
             /*!
              * Sets an internal flag that indicates the second run is now taking place.
@@ -159,6 +159,8 @@ namespace storm {
             
             // A flag that stores whether the grammar is currently doing the second run.
             bool secondRun;
+
+            bool prismCompatibility;
             
             /*!
              * Sets whether doubles literals are allowed in the parsed expression.

src/storm/settings/SettingsManager.cpp

@@ -1,7 +1,6 @@
 #include "storm/settings/SettingsManager.h"
 
 #include <cstring>
-#include <cctype>
 #include <mutex>
 #include <iomanip>
 #include <fstream>
@@ -19,6 +18,7 @@
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/CounterexampleGeneratorSettings.h"
 #include "storm/settings/modules/CuddSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/settings/modules/SylvanSettings.h"
 #include "storm/settings/modules/EigenEquationSolverSettings.h"
 #include "storm/settings/modules/GmmxxEquationSolverSettings.h"
@@ -511,6 +511,7 @@ namespace storm {
             // Register all known settings modules.
             storm::settings::addModule<storm::settings::modules::GeneralSettings>();
             storm::settings::addModule<storm::settings::modules::IOSettings>();
+            storm::settings::addModule<storm::settings::modules::BuildSettings>();
             storm::settings::addModule<storm::settings::modules::CoreSettings>();
             storm::settings::addModule<storm::settings::modules::DebugSettings>();
             storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();

src/storm/settings/modules/BuildSettings.cpp

@@ -0,0 +1,95 @@
+#include "storm/settings/modules/BuildSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+#include "storm/parser/CSVParser.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            const std::string BuildSettings::moduleName = "build";
+
+            const std::string jitOptionName = "jit";
+            const std::string explorationOrderOptionName = "explorder";
+            const std::string explorationOrderOptionShortName = "eo";
+            const std::string explorationChecksOptionName = "explchecks";
+            const std::string explorationChecksOptionShortName = "ec";
+            const std::string prismCompatibilityOptionName = "prismcompat";
+            const std::string prismCompatibilityOptionShortName = "pc";
+            const std::string noBuildOptionName = "nobuild";
+            const std::string fullModelBuildOptionName = "buildfull";
+            const std::string buildChoiceLabelOptionName = "buildchoicelab";
+            const std::string buildStateValuationsOptionName = "buildstateval";
+            BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
+
+                std::vector<std::string> explorationOrders = {"dfs", "bfs"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).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, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
+
+                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.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(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());
+
+            }
+
+
+            bool BuildSettings::isJitSet() const {
+                return this->getOption(jitOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isExplorationOrderSet() const {
+                return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isPrismCompatibilityEnabled() const {
+                return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isBuildFullModelSet() const {
+                return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isNoBuildModelSet() const {
+                return this->getOption(noBuildOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isBuildChoiceLabelsSet() const {
+                return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet();
+            }
+
+            bool BuildSettings::isBuildStateValuationsSet() const {
+                return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet();
+            }
+
+
+            storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const {
+                std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
+                if (explorationOrderAsString == "dfs") {
+                    return storm::builder::ExplorationOrder::Dfs;
+                } else if (explorationOrderAsString == "bfs") {
+                    return storm::builder::ExplorationOrder::Bfs;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'.");
+            }
+
+            bool BuildSettings::isExplorationChecksSet() const {
+                return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
+            }
+        }
+
+
+    }
+}

src/storm/settings/modules/BuildSettings.h

@@ -0,0 +1,84 @@
+#pragma once
+
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm/builder/ExplorationOrder.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            class BuildSettings : public ModuleSettings {
+
+            public:
+
+                /*!
+                 * Creates a new set of core settings.
+                 */
+                BuildSettings();
+                /*!
+                 * Retrieves whether the option to use the JIT builder is set.
+                 *
+                 * @return True iff the JIT builder is to be used.
+                 */
+                bool isJitSet() const;
+
+                /*!
+                 * Retrieves whether the model exploration order was set.
+                 *
+                 * @return True if the model exploration option was set.
+                 */
+                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.
+                 *
+                 * @return The chosen exploration order.
+                 */
+                storm::builder::ExplorationOrder getExplorationOrder() const;
+
+                /*!
+                 * Retrieves whether the PRISM compatibility mode was enabled.
+                 *
+                 * @return True iff the PRISM compatibility mode was enabled.
+                 */
+                bool isPrismCompatibilityEnabled() const;
+
+                /**
+                 * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file.
+                 */
+                bool isNoBuildModelSet() const;
+
+                /*!
+                 * Retrieves whether the full model should be build, that is, the model including all labels and rewards.
+                 *
+                 * @return true iff the full model should be build.
+                 */
+                bool isBuildFullModelSet() const;
+
+                /*!
+                 * Retrieves whether the choice labels should be build
+                 * @return
+                 */
+                bool isBuildChoiceLabelsSet() const;
+
+                /*!
+                 * Retrieves whether the choice labels should be build
+                 * @return
+                 */
+                bool isBuildStateValuationsSet() const;
+
+
+                // The name of the module.
+                static const std::string moduleName;
+            };
+        }
+    }
+}

src/storm/settings/modules/CoreSettings.h

@@ -117,9 +117,9 @@ namespace storm {
                 bool isDdLibraryTypeSetFromDefaultValue() const;
                 
                 /*!
-                 * Retrieves whether statistics are to be shown for counterexample generation.
+                 * Retrieves whether statistics are to be shown
                  *
-                 * @return True iff statistics are to be shown for counterexample generation.
+                 * @return True iff statistics are to be shown
                  */
                 bool isShowStatisticsSet() const;
 

src/storm/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -29,7 +29,6 @@ namespace storm {
                 return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
             }
             
-            
             bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const {
                 return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp";
             }

src/storm/settings/modules/IOSettings.cpp

@@ -31,22 +31,13 @@ namespace storm {
             const std::string IOSettings::prismInputOptionName = "prism";
             const std::string IOSettings::janiInputOptionName = "jani";
             const std::string IOSettings::prismToJaniOptionName = "prism2jani";
-            const std::string IOSettings::jitOptionName = "jit";
-            const std::string IOSettings::explorationOrderOptionName = "explorder";
-            const std::string IOSettings::explorationOrderOptionShortName = "eo";
-            const std::string IOSettings::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";
             const std::string IOSettings::constantsOptionName = "constants";
             const std::string IOSettings::constantsOptionShortName = "const";
-            const std::string IOSettings::prismCompatibilityOptionName = "prismcompat";
-            const std::string IOSettings::prismCompatibilityOptionShortName = "pc";
-            const std::string IOSettings::noBuildOptionName = "nobuild";
-            const std::string IOSettings::fullModelBuildOptionName = "buildfull";
-            const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab";
-            const std::string IOSettings::buildStateValuationsOptionName = "buildstateval";
+
             const std::string IOSettings::janiPropertyOptionName = "janiproperty";
             const std::string IOSettings::janiPropertyOptionShortName = "jprop";
             const std::string IOSettings::propertyOptionName = "prop";
@@ -54,12 +45,11 @@ namespace storm {
 
             
             IOSettings::IOSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.")
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
@@ -76,19 +66,10 @@ 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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).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.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
                                         .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.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
@@ -105,7 +86,7 @@ namespace storm {
             bool IOSettings::isExportDotSet() const {
                 return this->getOption(exportDotOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getExportDotFilename() const {
                 return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString();
             }
@@ -117,23 +98,35 @@ namespace storm {
             std::string IOSettings::getExportJaniDotFilename() const {
                 return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString();
             }
-            
+
             bool IOSettings::isExportExplicitSet() const {
                 return this->getOption(exportExplicitOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getExportExplicitFilename() const {
                 return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString();
             }
-
+            
+            bool IOSettings::isExportCdfSet() const {
+                return this->getOption(exportCdfOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string IOSettings::getExportCdfDirectory() const {
+                std::string result = this->getOption(exportCdfOptionName).getArgumentByName("directory").getValueAsString();
+                if (result.back() != '/') {
+                    result.push_back('/');
+                }
+                return result;
+            }
+            
             bool IOSettings::isExplicitSet() const {
                 return this->getOption(explicitOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getTransitionFilename() const {
                 return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString();
             }
-                        
+
             std::string IOSettings::getLabelingFilename() const {
                 return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString();
             }
@@ -157,15 +150,15 @@ namespace storm {
             bool IOSettings::isPrismInputSet() const {
                 return this->getOption(prismInputOptionName).getHasOptionBeenSet();
             }
-            
+
             bool IOSettings::isPrismOrJaniInputSet() const {
                 return isJaniInputSet() || isPrismInputSet();
             }
-            
+
             bool IOSettings::isPrismToJaniSet() const {
                 return this->getOption(prismToJaniOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getPrismInputFilename() const {
                 return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString();
             }
@@ -177,97 +170,47 @@ namespace storm {
             std::string IOSettings::getJaniInputFilename() const {
                 return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString();
             }
-            
-            bool IOSettings::isJitSet() const {
-                return this->getOption(jitOptionName).getHasOptionBeenSet();
-            }
 
-            bool IOSettings::isExplorationOrderSet() const {
-                return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
-            }
-            
-            storm::builder::ExplorationOrder IOSettings::getExplorationOrder() const {
-                std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
-                if (explorationOrderAsString == "dfs") {
-                    return storm::builder::ExplorationOrder::Dfs;
-                } else if (explorationOrderAsString == "bfs") {
-                    return storm::builder::ExplorationOrder::Bfs;
-                }
-                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();
             }
-            
+
             std::string IOSettings::getTransitionRewardsFilename() const {
                 return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString();
             }
-            
+
             bool IOSettings::isStateRewardsSet() const {
                 return this->getOption(stateRewardsOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getStateRewardsFilename() const {
                 return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString();
             }
-            
+
             bool IOSettings::isChoiceLabelingSet() const {
                 return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet();
             }
-                
+
             std::string IOSettings::getChoiceLabelingFilename() const {
                 return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString();
             }
-            
-            std::unique_ptr<storm::settings::SettingMemento> IOSettings::overridePrismCompatibilityMode(bool stateToSet) {
-                return this->overrideOption(prismCompatibilityOptionName, stateToSet);
-            }
-            
+
             bool IOSettings::isConstantsSet() const {
                 return this->getOption(constantsOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getConstantDefinitionString() const {
                 return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
             }
-            
+
             bool IOSettings::isJaniPropertiesSet() const {
                 return this->getOption(janiPropertyOptionName).getHasOptionBeenSet();
             }
-            
+
             std::vector<std::string> IOSettings::getJaniProperties() const {
                 return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
             }
 
-            bool IOSettings::isPrismCompatibilityEnabled() const {
-                return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
-            }
-            
-            bool IOSettings::isBuildFullModelSet() const {
-                return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet();
-            }
-            
-            bool IOSettings::isNoBuildModelSet() const {
-                return this->getOption(noBuildOptionName).getHasOptionBeenSet();
-            }
-
-            bool IOSettings::isBuildChoiceLabelsSet() const {
-                return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet();
-            }
-            
-            bool IOSettings::isBuildStateValuationsSet() const {
-                return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet();
-            }
-
-            bool IOSettings::isExportCdfSet() const {
-                return this->getOption(exportCdfOptionName).getHasOptionBeenSet();
-            }
-
             bool IOSettings::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -63,6 +63,16 @@ namespace storm {
                  */
                 std::string getExportExplicitFilename() const;
                 
+                /*!
+                 * Retrieves whether the cumulative density function for reward bounded properties should be exported
+                 */
+                bool isExportCdfSet() const;
+                
+                /*!
+                 * Retrieves a path to a directory in which the cdf files will be stored
+                 */
+                 std::string getExportCdfDirectory() const;
+                
                 /*!
                  * Retrieves whether the explicit option was set.
                  *
@@ -158,34 +168,6 @@ namespace storm {
                  */
                 std::string getJaniInputFilename() const;
 
-                /*!
-                 * Retrieves whether the option to use the JIT builder is set.
-                 *
-                 * @return True iff the JIT builder is to be used.
-                 */
-                bool isJitSet() const;
-                
-                /*!
-                 * Retrieves whether the model exploration order was set.
-                 *
-                 * @return True if the model exploration option was set.
-                 */
-                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.
-                 *
-                 * @return The chosen exploration order.
-                 */
-                storm::builder::ExplorationOrder getExplorationOrder() const;
-
                 /*!
                  * Retrieves whether the transition reward option was set.
                  *
@@ -218,7 +200,7 @@ namespace storm {
 
                 /*!
                  * Retrieves whether the choice labeling option was set.
-                 * 
+                 *
                  * @return True iff the choice labeling option was set.
                  */
                 bool isChoiceLabelingSet() const;
@@ -231,15 +213,6 @@ namespace storm {
                  */
                 std::string getChoiceLabelingFilename() const;
 
-                /*!
-                 * Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As
-                 * soon as the returned memento goes out of scope, the original value is restored.
-                 *
-                 * @param stateToSet The value that is to be set for the option.
-                 * @return The memento that will eventually restore the original value.
-                 */
-                std::unique_ptr<storm::settings::SettingMemento> overridePrismCompatibilityMode(bool stateToSet);
-                
                 /*!
                  * Retrieves whether the export-to-dot option was set.
                  *
@@ -286,39 +259,6 @@ namespace storm {
                  */
                 std::string getPropertyFilter() const;
 
-                /*!
-                 * Retrieves whether the PRISM compatibility mode was enabled.
-                 *
-                 * @return True iff the PRISM compatibility mode was enabled.
-                 */
-                bool isPrismCompatibilityEnabled() const;
-                
-                /**
-                 * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file.
-                 */
-                bool isNoBuildModelSet() const;
-                
-                /*!
-                 * Retrieves whether the full model should be build, that is, the model including all labels and rewards.
-                 *
-                 * @return true iff the full model should be build.
-                 */
-                bool isBuildFullModelSet() const;
-
-                /*!
-                 * Retrieves whether the choice labels should be build
-                 * @return
-                 */
-                bool isBuildChoiceLabelsSet() const;
-
-                /*!
-                 * Retrieves whether the choice labels should be build
-                 * @return
-                 */
-                bool isBuildStateValuationsSet() const;
-                
-                bool isExportCdfSet() const;
-
                 bool check() const override;
                 void finalize() override;
 
@@ -341,22 +281,11 @@ namespace storm {
                 static const std::string prismInputOptionName;
                 static const std::string janiInputOptionName;
                 static const std::string prismToJaniOptionName;
-                static const std::string jitOptionName;
-                static const std::string explorationChecksOptionName;
-                static const std::string explorationChecksOptionShortName;
-                static const std::string explorationOrderOptionName;
-                static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;
                 static const std::string stateRewardsOptionName;
                 static const std::string choiceLabelingOptionName;
                 static const std::string constantsOptionName;
                 static const std::string constantsOptionShortName;
-                static const std::string prismCompatibilityOptionName;
-                static const std::string prismCompatibilityOptionShortName;
-                static const std::string fullModelBuildOptionName;
-                static const std::string noBuildOptionName;
-                static const std::string buildChoiceLabelOptionName;
-                static const std::string buildStateValuationsOptionName;
                 static const std::string janiPropertyOptionName;
                 static const std::string janiPropertyOptionShortName;
                 static const std::string propertyOptionName;

src/storm/settings/modules/MultiObjectiveSettings.cpp

@@ -21,7 +21,7 @@ namespace storm {
                 std::vector<std::string> methods = {"pcaa", "constraintbased"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will be saved.").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory in which the results will be saved.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.")
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).")

src/storm/solver/AbstractEquationSolver.cpp

@@ -4,7 +4,6 @@
 #include "storm/adapters/RationalFunctionAdapter.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/GeneralSettings.h"
 
 #include "storm/utility/constants.h"

src/storm/storage/BitVector.cpp

@@ -1031,22 +1031,6 @@ namespace storm {
             out << std::endl;
         }
 
-        std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const {
-            STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size.");
-            std::size_t result = 0;
-
-            for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) {
-                result ^= result << 3;
-                result ^= result >> bitvector.getAsInt(index << 6, 5);
-            }
-
-            // Erase the last bit and add one to definitely make this hash value non-zero.
-            result &= ~1ull;
-            result += 1;
-
-            return result;
-        }
-
         // All necessary explicit template instantiations.
         template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end);
         template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::const_iterator begin, std::vector<uint_fast64_t>::const_iterator end);
@@ -1060,7 +1044,6 @@ namespace storm {
 }
 
 namespace std {
-
     std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
         return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
     }

src/storm/storage/BitVector.h

@@ -513,7 +513,6 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
             friend struct std::hash<storm::storage::BitVector>;
-            friend struct NonZeroBitVectorHash;
             
         private:
             /*!
@@ -583,11 +582,6 @@ namespace storm {
             static const uint_fast64_t mod64mask = (1 << 6) - 1;
         };
         
-        // A hashing functor that guarantees that the result of the hash is never going to be -1.
-        struct NonZeroBitVectorHash {
-            std::size_t operator()(storm::storage::BitVector const& bv) const;
-        };
-        
     } // namespace storage
 } // namespace storm
 

src/storm/storage/BitVectorHashMap.cpp

@@ -5,46 +5,47 @@
 #include <algorithm>
 
 #include "storm/utility/macros.h"
+#include "storm/exceptions/InternalException.h"
 
 namespace storm {
     namespace storage {
-        template<class ValueType, class Hash1, class Hash2>
-        const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003};
+        template<class ValueType, class Hash>
+        const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223};
         
-        template<class ValueType, class Hash1, class Hash2>
-        BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {
+        template<class ValueType, class Hash>
+        BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {
             // Intentionally left empty.
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) {
+        template<class ValueType, class Hash>
+        bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) {
             return &map == &other.map && *indexIt == *other.indexIt;
         }
 
-        template<class ValueType, class Hash1, class Hash2>
-        bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) {
+        template<class ValueType, class Hash>
+        bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) {
             return !(*this == other);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++(int) {
+        template<class ValueType, class Hash>
+        typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++(int) {
             ++indexIt;
             return *this;
         }
 
-        template<class ValueType, class Hash1, class Hash2>
-        typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++() {
+        template<class ValueType, class Hash>
+        typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++() {
             ++indexIt;
             return *this;
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const {
+        template<class ValueType, class Hash>
+        std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator*() const {
             return map.getBucketAndValue(*indexIt);
         }
                 
-        template<class ValueType, class Hash1, class Hash2>
-        BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
+        template<class ValueType, class Hash>
+        BitVectorHashMap<ValueType, Hash>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
             STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64.");
             currentSizeIterator = std::find_if(sizes.begin(), sizes.end(), [=] (uint64_t value) { return value > initialSize; } );
             
@@ -52,27 +53,42 @@ namespace storm {
             buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator);
             occupied = storm::storage::BitVector(*currentSizeIterator);
             values = std::vector<ValueType>(*currentSizeIterator);
+            
+#ifndef NDEBUG
+            for (uint64_t i = 0; i < sizes.size() - 1; ++i) {
+                STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes.");
+            }
+            numberOfInsertions = 0;
+            numberOfInsertionProbingSteps = 0;
+            numberOfFinds = 0;
+            numberOfFindProbingSteps = 0;
+#endif
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        bool BitVectorHashMap<ValueType, Hash1, Hash2>::isBucketOccupied(uint_fast64_t bucket) const {
+        template<class ValueType, class Hash>
+        bool BitVectorHashMap<ValueType, Hash>::isBucketOccupied(uint_fast64_t bucket) const {
             return occupied.get(bucket);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::size() const {
+        template<class ValueType, class Hash>
+        std::size_t BitVectorHashMap<ValueType, Hash>::size() const {
             return numberOfElements;
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::capacity() const {
+        template<class ValueType, class Hash>
+        std::size_t BitVectorHashMap<ValueType, Hash>::capacity() const {
             return *currentSizeIterator;
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() {
+        template<class ValueType, class Hash>
+        void BitVectorHashMap<ValueType, Hash>::increaseSize() {
             ++currentSizeIterator;
             STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big.");
+#ifndef NDEBUG
+            STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast<double>(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast<double>(numberOfInsertions)) << " probing steps).");
+#else
+            STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ".");
+#endif
             
             // Create new containers and swap them with the old ones.
             numberOfElements = 0;
@@ -97,10 +113,10 @@ namespace storm {
             uint_fast64_t failCount = 0;
             while (fail) {
                 ++failCount;
-                STORM_LOG_ASSERT(failCount < 2, "Increasing size failed too often.");
+                STORM_LOG_THROW(failCount < 2, storm::exceptions::InternalException, "Increasing size failed too often.");
                 
                 ++currentSizeIterator;
-                STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big.");
+                STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big.");
                 
                 numberOfElements = 0;
                 buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator);
@@ -112,14 +128,14 @@ namespace storm {
                     
                     // If we failed to insert just one element, we have to redo the procedure with a larger container size.
                     if (fail) {
-                        continue;
+                        break;
                     }
                 }
             }
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        bool BitVectorHashMap<ValueType, Hash1, Hash2>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) {
+        template<class ValueType, class Hash>
+        bool BitVectorHashMap<ValueType, Hash>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) {
             std::tuple<bool, std::size_t, bool> flagBucketTuple = this->findBucketToInsert<false>(key);
             if (std::get<2>(flagBucketTuple)) {
                 return false;
@@ -137,18 +153,18 @@ namespace storm {
             }
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
+        template<class ValueType, class Hash>
+        ValueType BitVectorHashMap<ValueType, Hash>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
             return findOrAddAndGetBucket(key, value).first;
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        void BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
+        template<class ValueType, class Hash>
+        void BitVectorHashMap<ValueType, Hash>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
             setOrAddAndGetBucket(key, value);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
+        template<class ValueType, class Hash>
+        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
             // If the load of the map is too high, we increase the size.
             if (numberOfElements >= loadFactor * *currentSizeIterator) {
                 this->increaseSize();
@@ -168,8 +184,8 @@ namespace storm {
             }
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
+        template<class ValueType, class Hash>
+        std::size_t BitVectorHashMap<ValueType, Hash>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
             // If the load of the map is too high, we increase the size.
             if (numberOfElements >= loadFactor * *currentSizeIterator) {
                 this->increaseSize();
@@ -187,41 +203,56 @@ namespace storm {
             return std::get<1>(flagBucketTuple);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const {
+        template<class ValueType, class Hash>
+        ValueType BitVectorHashMap<ValueType, Hash>::getValue(storm::storage::BitVector const& key) const {
             std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
             STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key.");
             return values[flagBucketPair.second];
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        bool BitVectorHashMap<ValueType, Hash1, Hash2>::contains(storm::storage::BitVector const& key) const {
+        template<class ValueType, class Hash>
+        ValueType BitVectorHashMap<ValueType, Hash>::getValue(std::size_t bucket) const {
+            return values[bucket];
+        }
+        
+        template<class ValueType, class Hash>
+        bool BitVectorHashMap<ValueType, Hash>::contains(storm::storage::BitVector const& key) const {
             return findBucket(key).first;
         }
 
-        template<class ValueType, class Hash1, class Hash2>
-        typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::begin() const {
+        template<class ValueType, class Hash>
+        typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::begin() const {
             return const_iterator(*this, occupied.begin());
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::end() const {
+        template<class ValueType, class Hash>
+        typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::end() const {
             return const_iterator(*this, occupied.end());
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucket(storm::storage::BitVector const& key) const {
-            uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator;
+        template<class ValueType, class Hash>
+        uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t, uint_fast64_t currentValue, uint_fast64_t step) const {
+            return (currentValue + step + step*step) % *currentSizeIterator;
+        }
+        
+        template<class ValueType, class Hash>
+        std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash>::findBucket(storm::storage::BitVector const& key) const {
+#ifndef NDEBUG
+            ++numberOfFinds;
+#endif
+            uint_fast64_t initialHash = hasher(key) % *currentSizeIterator;
             uint_fast64_t bucket = initialHash;
-
-            uint_fast64_t counter = 0;
+            
+            uint_fast64_t i = 0;
             while (isBucketOccupied(bucket)) {
-                ++counter;
+                ++i;
+#ifndef NDEBUG
+                ++numberOfFindProbingSteps;
+#endif
                 if (buckets.matches(bucket * bucketSize, key)) {
                     return std::make_pair(true, bucket);
                 }
-                bucket += hasher2(key);
-                bucket %= *currentSizeIterator;
+                bucket = getNextBucketInProbingSequence(initialHash, bucket, i);
                 
                 if (bucket == initialHash) {
                     return std::make_pair(false, bucket);
@@ -231,41 +262,46 @@ namespace storm {
             return std::make_pair(false, bucket);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
+        template<class ValueType, class Hash>
         template<bool increaseStorage>
-        std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucketToInsert(storm::storage::BitVector const& key) {
-            uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator;
+        std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash>::findBucketToInsert(storm::storage::BitVector const& key) {
+#ifndef NDEBUG
+            ++numberOfInsertions;
+#endif
+            uint_fast64_t initialHash = hasher(key) % *currentSizeIterator;
             uint_fast64_t bucket = initialHash;
-            
-            uint_fast64_t counter = 0;
+
+            uint64_t i = 0;
             while (isBucketOccupied(bucket)) {
-                ++counter;
+                ++i;
+#ifndef NDEBUG
+                ++numberOfInsertionProbingSteps;
+#endif
                 if (buckets.matches(bucket * bucketSize, key)) {
                     return std::make_tuple(true, bucket, false);
                 }
-                bucket += hasher2(key);
-                bucket %= *currentSizeIterator;
+                bucket = getNextBucketInProbingSequence(initialHash, bucket, i);
                 
                 if (bucket == initialHash) {
                     if (increaseStorage) {
                         this->increaseSize();
-                        bucket = initialHash = hasher1(key) % *currentSizeIterator;
+                        bucket = initialHash = hasher(key) % *currentSizeIterator;
                     } else {
                         return std::make_tuple(false, bucket, true);
                     }
                 }
             }
-            
+
             return std::make_tuple(false, bucket, false);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::getBucketAndValue(std::size_t bucket) const {
+        template<class ValueType, class Hash>
+        std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::getBucketAndValue(std::size_t bucket) const {
             return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
+        template<class ValueType, class Hash>
+        void BitVectorHashMap<ValueType, Hash>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
             for (auto pos : occupied) {
                 values[pos] = remapping(values[pos]);
             }

src/storm/storage/BitVectorHashMap.h

@@ -14,7 +14,7 @@ namespace storm {
          * queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of
          * 64.
          */
-        template<typename ValueType, typename Hash1 = std::hash<storm::storage::BitVector>, class Hash2 = storm::storage::NonZeroBitVectorHash>
+        template<typename ValueType, typename Hash = std::hash<storm::storage::BitVector>>
         class BitVectorHashMap {
         public:
             class BitVectorHashMapIterator {
@@ -113,6 +113,13 @@ namespace storm {
              * @return The value associated with the given key (if any).
              */
             ValueType getValue(storm::storage::BitVector const& key) const;
+
+            /*!
+             * Retrieves the value associated with the given bucket.
+             *
+             * @return The value associated with the given bucket (if any).
+             */
+            ValueType getValue(std::size_t bucket) const;
             
             /*!
              * Checks if the given key is already contained in the map.
@@ -204,6 +211,11 @@ namespace storm {
              */
             void increaseSize();
             
+            /*!
+             * Computes the next bucket in the probing sequence.
+             */
+            uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t initialValue, uint_fast64_t currentValue, uint_fast64_t step) const;
+
             // The load factor determining when the size of the map is increased.
             double loadFactor;
             
@@ -229,11 +241,18 @@ namespace storm {
             std::vector<std::size_t>::const_iterator currentSizeIterator;
             
             // Functor object that are used to perform the actual hashing.
-            Hash1 hasher1;
-            Hash2 hasher2;
+            Hash hasher;
             
             // A static table that produces the next possible size of the hash table.
             static const std::vector<std::size_t> sizes;
+            
+#ifndef NDEBUG
+            // Some performance metrics.
+            mutable uint64_t numberOfInsertions;
+            mutable uint64_t numberOfInsertionProbingSteps;
+            mutable uint64_t numberOfFinds;
+            mutable uint64_t numberOfFindProbingSteps;
+#endif
         };
 
     }

src/storm/storage/SparseMatrix.cpp

@@ -897,12 +897,11 @@ namespace storm {
             // Start by creating a temporary vector that stores for each index whose bit is set to true the number of
             // bits that were set before that particular index.
             std::vector<index_type> columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices();
-            std::vector<index_type>* rowBitsSetBeforeIndex;
-            if (&rowGroupConstraint == &columnConstraint) {
-                rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex;
-            } else {
-                rowBitsSetBeforeIndex = new std::vector<index_type>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices());
+            std::unique_ptr<std::vector<index_type>> tmp;
+            if (rowGroupConstraint != columnConstraint) {
+                tmp = std::make_unique<std::vector<index_type>>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices());
             }
+            std::vector<index_type> const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex;
             
             // Then, we need to determine the number of entries and the number of rows of the submatrix.
             index_type subEntries = 0;
@@ -917,7 +916,7 @@ namespace storm {
                         if (columnConstraint.get(it->getColumn())) {
                             ++subEntries;
                             
-                            if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) {
+                            if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
                                 foundDiagonalElement = true;
                             }
                         }
@@ -946,9 +945,9 @@ namespace storm {
                     
                     for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) {
                         if (columnConstraint.get(it->getColumn())) {
-                            if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) {
+                            if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
                                 insertedDiagonalElement = true;
-                            } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > (*rowBitsSetBeforeIndex)[index]) {
+                            } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > rowBitsSetBeforeIndex[index]) {
                                 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
                                 insertedDiagonalElement = true;
                             }
@@ -956,18 +955,13 @@ namespace storm {
                         }
                     }
                     if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) {
-                        matrixBuilder.addNextValue(rowGroupCount, rowGroupCount, storm::utility::zero<ValueType>());
+                        matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
                     }
                     ++rowCount;
                 }
                 ++rowGroupCount;
             }
             
-            // If the constraints were not the same, we have allocated some additional memory we need to free now.
-            if (&rowGroupConstraint != &columnConstraint) {
-                delete rowBitsSetBeforeIndex;
-            }
-            
             return matrixBuilder.build();
         }
         

src/storm/storage/expressions/CompiledExpression.cpp

@@ -0,0 +1,21 @@
+#include "storm/storage/expressions/CompiledExpression.h"
+
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
+namespace storm {
+    namespace expressions {
+        
+        bool CompiledExpression::isExprtkCompiledExpression() const {
+            return false;
+        }
+        
+        ExprtkCompiledExpression& CompiledExpression::asExprtkCompiledExpression() {
+            return static_cast<ExprtkCompiledExpression&>(*this);
+        }
+        
+        ExprtkCompiledExpression const& CompiledExpression::asExprtkCompiledExpression() const {
+            return static_cast<ExprtkCompiledExpression const&>(*this);
+        }
+        
+    }
+}

src/storm/storage/expressions/CompiledExpression.h

@@ -0,0 +1,20 @@
+#pragma once
+
+namespace storm {
+    namespace expressions {
+        
+        class ExprtkCompiledExpression;
+        
+        class CompiledExpression {
+        public:
+            
+            virtual bool isExprtkCompiledExpression() const;
+            ExprtkCompiledExpression& asExprtkCompiledExpression();
+            ExprtkCompiledExpression const& asExprtkCompiledExpression() const;
+            
+        private:
+            // Currently empty.
+        };
+        
+    }
+}

src/storm/storage/expressions/Expression.cpp

@@ -9,6 +9,7 @@
 #include "storm/storage/expressions/ChangeManagerVisitor.h"
 #include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
 #include "storm/storage/expressions/Expressions.h"
+#include "storm/storage/expressions/CompiledExpression.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/utility/macros.h"
@@ -26,6 +27,11 @@ namespace storm {
             STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager.");
         }
         
+        // Spell out destructor explicitly so we can use forward declarations in the header.
+        Expression::~Expression() {
+            // Intentionally left empty.
+        }
+        
         Expression::Expression(std::shared_ptr<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) {
             // Intentionally left empty.
         }
@@ -196,7 +202,19 @@ namespace storm {
                 return true;
             }
             SyntacticalEqualityCheckVisitor checker;
-            return checker.isSyntaticallyEqual(*this, other);
+            return checker.isSyntacticallyEqual(*this, other);
+        }
+        
+        bool Expression::hasCompiledExpression() const {
+            return static_cast<bool>(compiledExpression);
+        }
+        
+        void Expression::setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const {
+            this->compiledExpression = compiledExpression;
+        }
+        
+        CompiledExpression const& Expression::getCompiledExpression() const {
+            return *compiledExpression;
         }
 
         std::string Expression::toString() const {

src/storm/storage/expressions/Expression.h

@@ -15,6 +15,7 @@ namespace storm {
         class ExpressionManager;
         class Variable;
         class ExpressionVisitor;
+        class CompiledExpression;
         
         class Expression {
         public:
@@ -58,6 +59,7 @@ namespace storm {
             friend Expression maximum(Expression const& first, Expression const& second);
 
             Expression() = default;
+            ~Expression();
             
             /*!
              * Creates an expression representing the given variable.
@@ -358,11 +360,29 @@ namespace storm {
              */
             bool isSyntacticallyEqual(storm::expressions::Expression const& other) const;
             
+            /*!
+             * Retrieves whether this expression object has an associated compiled expression.
+             */
+            bool hasCompiledExpression() const;
+            
+            /*!
+             * Associates the given compiled expression with this expression object.
+             */
+            void setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const;
+            
+            /*!
+             * Retrieves the associated compiled expression object (if there is any).
+             */
+            CompiledExpression const& getCompiledExpression() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Expression const& expression);
 
         private:
             // A pointer to the underlying base expression.
             std::shared_ptr<BaseExpression const> expressionPtr;
+            
+            // A pointer to an associated compiled expression object (if any).
+            mutable std::shared_ptr<CompiledExpression> compiledExpression;
         };
         
         // Provide operator overloads to conveniently construct new expressions from other expressions.

src/storm/storage/expressions/ExprtkCompiledExpression.cpp

@@ -0,0 +1,19 @@
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
+namespace storm {
+    namespace expressions {
+        
+        ExprtkCompiledExpression::ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression) : exprtkCompiledExpression(exprtkCompiledExpression) {
+            // Intentionally left empty.
+        }
+        
+        ExprtkCompiledExpression::CompiledExpressionType const& ExprtkCompiledExpression::getCompiledExpression() const {
+            return exprtkCompiledExpression;
+        }
+        
+        bool ExprtkCompiledExpression::isExprtkCompiledExpression() const {
+            return true;
+        }
+        
+    }
+}

src/storm/storage/expressions/ExprtkCompiledExpression.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/storage/expressions/CompiledExpression.h"
+
+#include "storm/utility/exprtk.h"
+
+namespace storm {
+    namespace expressions {
+        
+        class ExprtkCompiledExpression : public CompiledExpression {
+        public:
+            typedef exprtk::expression<double> CompiledExpressionType;
+
+            ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression);
+            
+            CompiledExpressionType const& getCompiledExpression() const;
+
+            virtual bool isExprtkCompiledExpression() const override;
+            
+        private:
+            CompiledExpressionType exprtkCompiledExpression;
+        };
+        
+    }
+}

src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp

@@ -26,34 +26,26 @@ namespace storm {
         
         template<typename RationalType>
         bool ExprtkExpressionEvaluatorBase<RationalType>::asBool(Expression const& expression) const {
-            std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
-            auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
-            if (expressionPair == this->compiledExpressions.end()) {
-                CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
-                return compiledExpression.value() == ValueType(1);
-            }
-            return expressionPair->second.value() == ValueType(1);
+            auto const& compiledExpression = getCompiledExpression(expression);
+            return compiledExpression.value() == ValueType(1);
         }
         
         template<typename RationalType>
         int_fast64_t ExprtkExpressionEvaluatorBase<RationalType>::asInt(Expression const& expression) const {
-            std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
-            auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
-            if (expressionPair == this->compiledExpressions.end()) {
-                CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
-                return static_cast<int_fast64_t>(compiledExpression.value());
-            }
-            return static_cast<int_fast64_t>(expressionPair->second.value());
+            auto const& compiledExpression = getCompiledExpression(expression);
+            return static_cast<int_fast64_t>(compiledExpression.value());
         }
         
         template<typename RationalType>
-        typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
-            std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType());
-            CompiledExpressionType& compiledExpression = result.first->second;
-            compiledExpression.register_symbol_table(*symbolTable);
-            bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
-            STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")");
-            return compiledExpression;
+        typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType const& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
+            if (!expression.hasCompiledExpression() || !expression.getCompiledExpression().isExprtkCompiledExpression()) {
+                CompiledExpressionType compiledExpression;
+                compiledExpression.register_symbol_table(*symbolTable);
+                bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
+                STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")");
+                expression.setCompiledExpression(std::make_shared<ExprtkCompiledExpression>(compiledExpression));
+            }
+            return expression.getCompiledExpression().asExprtkCompiledExpression().getCompiledExpression();
         }
         
         template<typename RationalType>
@@ -76,13 +68,8 @@ namespace storm {
         }
         
         double ExprtkExpressionEvaluator::asRational(Expression const& expression) const {
-            std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
-            auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
-            if (expressionPair == this->compiledExpressions.end()) {
-                CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
-                return static_cast<double>(compiledExpression.value());
-            }
-            return static_cast<double>(expressionPair->second.value());
+            auto const& compiledExpression = getCompiledExpression(expression);
+            return static_cast<double>(compiledExpression.value());
         }
         
         template class ExprtkExpressionEvaluatorBase<double>;

src/storm/storage/expressions/ExprtkExpressionEvaluator.h

@@ -6,18 +6,12 @@
 
 #include "storm/storage/expressions/ExpressionEvaluatorBase.h"
 
-#pragma clang diagnostic push
-#pragma clang diagnostic ignored "-Wunused-variable"
-
-#pragma GCC diagnostic push
-
-#include "exprtk.hpp"
-
-#pragma GCC diagnostic pop
-#pragma clang diagnostic pop
+#include "storm/utility/exprtk.h"
 
 #include "storm/storage/expressions/ToExprtkStringVisitor.h"
 
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
 namespace storm {
     namespace expressions {
         template <typename RationalType>
@@ -34,15 +28,14 @@ namespace storm {
 
         protected:
             typedef double ValueType;
-            typedef exprtk::expression<ValueType> CompiledExpressionType;
-            typedef std::unordered_map<std::shared_ptr<BaseExpression const>, CompiledExpressionType> CacheType;
+            typedef ExprtkCompiledExpression::CompiledExpressionType CompiledExpressionType;
             
             /*!
-             * Adds a compiled version of the given expression to the internal storage.
+             * Retrieves a compiled version of the given expression.
              *
              * @param expression The expression that is to be compiled.
              */
-            CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const;
+            CompiledExpressionType const& getCompiledExpression(storm::expressions::Expression const& expression) const;
             
             // The parser used.
             mutable std::unique_ptr<exprtk::parser<ValueType>> parser;
@@ -54,9 +47,6 @@ namespace storm {
             std::vector<ValueType> booleanValues;
             std::vector<ValueType> integerValues;
             std::vector<ValueType> rationalValues;
-            
-            // A mapping of expressions to their compiled counterpart.
-            mutable CacheType compiledExpressions;
         };
         
         class ExprtkExpressionEvaluator : public ExprtkExpressionEvaluatorBase<double> {

src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp

@@ -5,7 +5,7 @@
 namespace storm {
     namespace expressions {
         
-        bool SyntacticalEqualityCheckVisitor::isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) {
+        bool SyntacticalEqualityCheckVisitor::isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) {
             return boost::any_cast<bool>(expression1.accept(*this, std::ref(expression2.getBaseExpression())));
         }
         

src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h

@@ -9,7 +9,7 @@ namespace storm {
         
         class SyntacticalEqualityCheckVisitor : public ExpressionVisitor {
         public:
-            bool isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2);
+            bool isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2);
             
             virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;

src/storm/storage/prism/Program.cpp

@@ -8,8 +8,6 @@
 #include "storm/storage/jani/Property.h"
 
 #include "storm/storage/expressions/ExpressionManager.h"
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/vector.h"
@@ -138,7 +136,7 @@ namespace storm {
             std::set<std::string> appearingModules;
         };
         
-        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
+        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
         : LocatedInformation(filename, lineNumber), manager(manager),
         modelType(modelType), constants(constants), constantToIndexMap(),
         globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
@@ -146,7 +144,7 @@ namespace storm {
         formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
         rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
         labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
-        synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
+        synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
         {
             
             // Start by creating the necessary mappings from the given ones.
@@ -166,7 +164,7 @@ namespace storm {
             if (finalModel) {
                 // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
                 // commands and issue a warning.
-                if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismCompatibilityEnabled()) {
+                if (modelType == storm::prism::Program::ModelType::CTMC && prismCompatibility) {
                     bool hasProbabilisticCommands = false;
                     for (auto& module : this->modules) {
                         for (auto& command : module.getCommands()) {
@@ -689,7 +687,7 @@ namespace storm {
                 newModules.push_back(module.restrictCommands(indexSet));
             }
             
-            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct());
+            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
         
         void Program::createMappings() {
@@ -783,7 +781,7 @@ namespace storm {
                 }
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct());
+            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
         
         Program Program::substituteConstants() const {
@@ -846,7 +844,7 @@ namespace storm {
                 newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
+            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
         
         void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1122,7 +1120,7 @@ namespace storm {
             }
             
             if (hasLabeledMarkovianCommand) {
-                if (storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismCompatibilityEnabled()) {
+                if (prismCompatibility) {
                     STORM_LOG_WARN_COND(false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
@@ -1362,7 +1360,7 @@ namespace storm {
                 }
             }
             
-            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct());
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
         
         Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@@ -1558,7 +1556,7 @@ namespace storm {
             
             // Finally, we can create the module and the program and return it.
             storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
-            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), this->getFilename(), 0, true);
+            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
         }
         
         std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {

src/storm/storage/prism/Program.h

@@ -57,7 +57,7 @@ namespace storm {
              * @param lineNumber The line number in which the program is defined.
              * @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
              */
-            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
+            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -697,6 +697,8 @@ namespace storm {
             
             // A mapping from variable names to the modules in which they were declared.
             std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
+
+            bool prismCompatibility;
         };
         
         std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);

src/storm/storage/sparse/StateStorage.h

@@ -27,7 +27,7 @@ namespace storm {
                 // The number of bits of each state.
                 uint64_t bitsPerState;
                 
-                // The number of states that were found in the exploration so far.
+                // Get the number of states that were found in the exploration so far.
                 uint_fast64_t getNumberOfStates() const;
             };
             

src/storm/utility/KwekMehlhorn.cpp

@@ -73,6 +73,9 @@ namespace storm {
                 }
             }
          
+            template storm::RationalNumber sharpen(uint64_t precision, double const& input);
+            template storm::RationalNumber sharpen(uint64_t precision, storm::RationalNumber const& input);
+
             template void sharpen(uint64_t precision, std::vector<double> const& input, std::vector<storm::RationalNumber>& output);
             template void sharpen(uint64_t precision, std::vector<storm::RationalNumber> const& input, std::vector<storm::RationalNumber>& output);
             

src/storm/utility/cli.cpp

@@ -55,7 +55,7 @@ namespace storm {
                                     throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << ".";
                                 }
                             } else if (variable.hasIntegerType()) {
-                                int_fast64_t integerValue = std::stoi(value);
+                                int_fast64_t integerValue = std::stoll(value);
                                 constantDefinitions[variable] = manager.integer(integerValue);
                             } else if (variable.hasRationalType()) {
                                 try {

src/storm/utility/exprtk.h

@@ -0,0 +1,11 @@
+#pragma once
+
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-Wunused-variable"
+
+#pragma GCC diagnostic push
+
+#include "exprtk.hpp"
+
+#pragma GCC diagnostic pop
+#pragma clang diagnostic pop

src/storm/utility/shortestPaths.cpp

@@ -11,7 +11,6 @@
 #include "storm/utility/shortestPaths.h"
 
 // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required!
-// Accessing zero should trigger a warning!
 // (Also, did I document this? I think so, somewhere. I went with k>=1 because
 // that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...)
 
@@ -336,6 +335,10 @@ namespace storm {
 
             template <typename T>
             void ShortestPathsGenerator<T>::computeKSP(unsigned long k) {
+                if (k == 0) {
+                    throw std::invalid_argument("Index 0 is invalid, since we use 1-based indices (sorry)!");
+                }
+
                 unsigned long alreadyComputedK = kShortestPaths[metaTarget].size();
 
                 for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) {

src/test/storm/builder/DdJaniModelBuilderTest.cpp

@@ -15,7 +15,6 @@
 
 #include "storm/settings/SettingMemento.h"
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
 
 #include "storm/exceptions/InvalidSettingsException.h"
 
@@ -89,35 +88,32 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(66ul, model->getNumberOfStates());
@@ -125,35 +121,33 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     model = builder.build(janiModel);
     EXPECT_EQ(66ul, model->getNumberOfStates());

src/test/storm/builder/DdPrismModelBuilderTest.cpp

@@ -2,7 +2,7 @@
 #include "storm-config.h"
 #include "storm/settings/SettingMemento.h"
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/BuildSettings.h"
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Ctmc.h"
@@ -78,35 +78,33 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
 }
 
 TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
 
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     EXPECT_EQ(66ul, model->getNumberOfStates());
@@ -114,35 +112,33 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) {
 }
 
 TEST(DdPrismModelBuilderTest_Cudd, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
 
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     EXPECT_EQ(66ul, model->getNumberOfStates());

src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp

@@ -8,7 +8,6 @@
 #include "storm/generator/JaniNextStateGenerator.h"
 #include "storm/storage/jani/Model.h"
 
-#include "storm/settings/modules/IOSettings.h"
 
 TEST(ExplicitJaniModelBuilderTest, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
@@ -44,35 +43,32 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) {
 }
 
 TEST(ExplicitJaniModelBuilderTest, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::jani::Model janiModel = program.toJani();
 
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     janiModel = program.toJani();
     model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
     EXPECT_EQ(66ul, model->getNumberOfStates());

src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp

@@ -8,7 +8,6 @@
 #include "storm/storage/jani/Model.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
 
 TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
@@ -44,35 +43,33 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
 }
 
 TEST(ExplicitJitJaniModelBuilderTest, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::jani::Model janiModel = program.toJani();
     
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     janiModel = program.toJani();
     model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     janiModel = program.toJani();
     model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
     EXPECT_EQ(66ul, model->getNumberOfStates());

src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp

@@ -2,11 +2,9 @@
 #include "storm-config.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/settings/SettingMemento.h"
 #include "storm/parser/PrismParser.h"
 #include "storm/builder/ExplicitModelBuilder.h"
 
-#include "storm/settings/modules/IOSettings.h"
 
 TEST(ExplicitPrismModelBuilderTest, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
@@ -37,31 +35,29 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) {
 }
 
 TEST(ExplicitPrismModelBuilderTest, Ctmc) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
 
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
 
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
     model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(66ul, model->getNumberOfStates());
     EXPECT_EQ(189ul, model->getNumberOfTransitions());

src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp

@@ -13,7 +13,6 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/IOSettings.h"
 
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 #include "storm/settings/modules/GmmxxEquationSolverSettings.h"
@@ -21,11 +20,8 @@
 #include "storm/storage/expressions/ExpressionManager.h"
 
 TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -98,11 +94,8 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
 }
 
 TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -160,11 +153,8 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
 }
 
 TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -194,18 +184,13 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
 }
 
 TEST(GmmxxCtmcCslModelCheckerTest, Fms) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // No properties to check at this point.
 }
 
 TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     

src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp

@@ -17,18 +17,15 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/GmmxxEquationSolverSettings.h"
 
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -122,11 +119,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -220,11 +214,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -300,11 +291,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -380,11 +368,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -417,11 +402,9 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -454,18 +437,13 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // No properties to check at this point.
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -550,11 +528,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
 }
 
 TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);

src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
     result = stateAndTransitionRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 

src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp

@@ -14,14 +14,10 @@
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/IOSettings.h"
 
 TEST(NativeCtmcCslModelCheckerTest, Cluster) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -86,11 +82,9 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
 }
 
 TEST(NativeCtmcCslModelCheckerTest, Embedded) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -143,11 +137,8 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
 }
 
 TEST(NativeCtmcCslModelCheckerTest, Polling) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -170,18 +161,14 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
 }
 
 TEST(NativeCtmcCslModelCheckerTest, Fms) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // No properties to check at this point.
 }
 
 TEST(NativeCtmcCslModelCheckerTest, Tandem) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     

src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp

@@ -17,16 +17,12 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/IOSettings.h"
 
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -120,11 +116,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -218,11 +211,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -298,11 +288,9 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
+
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -378,11 +366,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -415,11 +400,9 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -452,18 +435,14 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Fms) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // No properties to check at this point.
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@@ -550,11 +529,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
 }
 
 TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
-    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
-    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
-    
     // Parse the model description.
-    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program);
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);

src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = stateAndTransitionRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");