Merge branch 'master' into ddbisim_partial_quotient

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"
@@ -54,7 +55,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;
@@ -99,6 +100,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;
@@ -117,7 +119,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;
                 
@@ -175,22 +177,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>
@@ -210,13 +212,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 || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
                     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.");
@@ -613,8 +616,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-cli/storm-dft.cpp

@@ -85,7 +85,7 @@ void processOptions() {
         // Start by setting some urgent options (log levels, resources, etc.)
         storm::cli::setUrgentOptions();
 
-        storm::cli::processOptions();
+       // storm::cli::processOptions();
         
         storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
         storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();

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/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -146,9 +146,9 @@ namespace storm {
             lowerResultBound = storm::utility::zero<ConstantType>();
             upperResultBound = storm::utility::one<ConstantType>();
             
-            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+            // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
+            auto req = solverFactory->getRequirements(true);
             req.clearBounds();
-            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
             STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
             solverFactory->setRequirementsChecked(true);
         }
@@ -185,8 +185,8 @@ namespace storm {
             // We only know a lower bound for the result
             lowerResultBound = storm::utility::zero<ConstantType>();
         
-            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
-            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+            // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
+            auto req = solverFactory->getRequirements(true);
             req.clearLowerBounds();
             if (req.requiresUpperBounds()) {
                 solvingRequiresUpperRewardBounds = true;
@@ -253,6 +253,7 @@ namespace storm {
                 solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration);
             }
             auto solver = solverFactory->create(parameterLifter->getMatrix());
+            solver->setHasUniqueSolution();
             if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
             if (upperResultBound) {
                 solver->setUpperBound(upperResultBound.get());

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/builder/jit/Distribution.cpp

@@ -2,6 +2,8 @@
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 
+#include "storm/storage/BitVector.h"
+
 namespace storm {
     namespace builder {
         namespace jit {
@@ -11,16 +13,48 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            template <typename IndexType, typename ValueType>
+            Distribution<IndexType, ValueType>::Distribution(Distribution<IndexType, ValueType> const& other) {
+                this->storage = other.storage;
+                this->compressed = other.compressed;
+            }
+            
+            template <typename IndexType, typename ValueType>
+            Distribution<IndexType, ValueType>::Distribution(Distribution<IndexType, ValueType>&& other) {
+                this->storage = std::move(other.storage);
+                this->compressed = other.compressed;
+                other.compressed = true;
+            }
+            
+            template <typename IndexType, typename ValueType>
+            Distribution<IndexType, ValueType>& Distribution<IndexType, ValueType>::operator=(Distribution<IndexType, ValueType> const& other) {
+                if (this != &other) {
+                    this->storage = other.storage;
+                    this->compressed = other.compressed;
+                }
+                return *this;
+            }
+            
+            template <typename IndexType, typename ValueType>
+            Distribution<IndexType, ValueType>& Distribution<IndexType, ValueType>::operator=(Distribution<IndexType, ValueType>&& other) {
+                if (this != &other) {
+                    this->storage = std::move(other.storage);
+                    this->compressed = other.compressed;
+                    other.compressed = true;
+                }
+                return *this;
+            }
+            
             template <typename IndexType, typename ValueType>
             void Distribution<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) {
                 storage.push_back(entry);
-                compressed &= storage.back().getIndex() < entry.getIndex();
+                compressed &= storage.back().getState() < entry.getState();
             }
 
             template <typename IndexType, typename ValueType>
             void Distribution<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) {
                 storage.emplace_back(index, value);
-                compressed &= storage.back().getIndex() < index;
+                compressed &= storage.back().getState() < index;
             }
 
             template <typename IndexType, typename ValueType>
@@ -34,7 +68,7 @@ namespace storm {
                 if (!compressed) {
                     std::sort(storage.begin(), storage.end(),
                               [] (DistributionEntry<IndexType, ValueType> const& a, DistributionEntry<IndexType, ValueType> const& b) {
-                                  return a.getIndex() < b.getIndex();
+                                  return a.getState() < b.getState();
                               }
                               );
                     
@@ -45,7 +79,7 @@ namespace storm {
                     if (first != last) {
                         auto result = first;
                         while (++first != last) {
-                            if (!(result->getIndex() == first->getIndex())) {
+                            if (!(result->getState() == first->getState())) {
                                 if (++result != first) {
                                     *result = std::move(*first);
                                 }
@@ -68,6 +102,12 @@ namespace storm {
                 }
             }
             
+            template <typename IndexType, typename ValueType>
+            void Distribution<IndexType, ValueType>::clear() {
+                this->storage.clear();
+                this->compressed = true;
+            }
+            
             template <typename IndexType, typename ValueType>
             typename Distribution<IndexType, ValueType>::ContainerType::iterator Distribution<IndexType, ValueType>::begin() {
                 return storage.begin();
@@ -91,7 +131,11 @@ namespace storm {
             template class Distribution<uint32_t, double>;
             template class Distribution<uint32_t, storm::RationalNumber>;
             template class Distribution<uint32_t, storm::RationalFunction>;
-            
+
+            template class Distribution<storm::storage::BitVector, double>;
+            template class Distribution<storm::storage::BitVector, storm::RationalNumber>;
+            template class Distribution<storm::storage::BitVector, storm::RationalFunction>;
+
         }
     }
 }

src/storm/builder/jit/Distribution.h

@@ -15,6 +15,11 @@ namespace storm {
                 
                 Distribution();
                 
+                Distribution(Distribution const&);
+                Distribution(Distribution&&);
+                Distribution& operator=(Distribution const&);
+                Distribution& operator=(Distribution&&);
+
                 /*!
                  * Adds the given entry to the distribution.
                  */
@@ -41,6 +46,11 @@ namespace storm {
                  */
                 void divide(ValueType const& value);
                 
+                /*!
+                 * Clears this distribution.
+                 */
+                void clear();
+                
                 /*!
                  * Access to iterators over the entries of the distribution. Note that there may be multiple entries for
                  * the same index. Also, no order is guaranteed. After a call to compress, the order is guaranteed to be

src/storm/builder/jit/DistributionEntry.cpp

@@ -2,37 +2,39 @@
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 
+#include "storm/storage/BitVector.h"
+
 namespace storm {
     namespace builder {
         namespace jit {
             
-            template <typename IndexType, typename ValueType>
-            DistributionEntry<IndexType, ValueType>::DistributionEntry() : index(0), value(0) {
+            template <typename StateType, typename ValueType>
+            DistributionEntry<StateType, ValueType>::DistributionEntry() : state(0), value(0) {
                 // Intentionally left empty.
             }
             
-            template <typename IndexType, typename ValueType>
-            DistributionEntry<IndexType, ValueType>::DistributionEntry(IndexType const& index, ValueType const& value) : index(index), value(value) {
+            template <typename StateType, typename ValueType>
+            DistributionEntry<StateType, ValueType>::DistributionEntry(StateType const& state, ValueType const& value) : state(state), value(value) {
                 // Intentionally left empty.
             }
             
-            template <typename IndexType, typename ValueType>
-            IndexType const& DistributionEntry<IndexType, ValueType>::getIndex() const {
-                return index;
+            template <typename StateType, typename ValueType>
+            StateType const& DistributionEntry<StateType, ValueType>::getState() const {
+                return state;
             }
             
-            template <typename IndexType, typename ValueType>
-            ValueType const& DistributionEntry<IndexType, ValueType>::getValue() const {
+            template <typename StateType, typename ValueType>
+            ValueType const& DistributionEntry<StateType, ValueType>::getValue() const {
                 return value;
             }
             
-            template <typename IndexType, typename ValueType>
-            void DistributionEntry<IndexType, ValueType>::addToValue(ValueType const& value) {
+            template <typename StateType, typename ValueType>
+            void DistributionEntry<StateType, ValueType>::addToValue(ValueType const& value) {
                 this->value += value;
             }
             
-            template <typename IndexType, typename ValueType>
-            void DistributionEntry<IndexType, ValueType>::divide(ValueType const& value) {
+            template <typename StateType, typename ValueType>
+            void DistributionEntry<StateType, ValueType>::divide(ValueType const& value) {
                 this->value /= value;
             }
          
@@ -40,6 +42,11 @@ namespace storm {
             template class DistributionEntry<uint32_t, storm::RationalNumber>;
             template class DistributionEntry<uint32_t, storm::RationalFunction>;
 
+            template class DistributionEntry<storm::storage::BitVector, double>;
+            template class DistributionEntry<storm::storage::BitVector, storm::RationalNumber>;
+            template class DistributionEntry<storm::storage::BitVector, storm::RationalFunction>;
+
+            
         }
     }
 }

src/storm/builder/jit/DistributionEntry.h

@@ -4,20 +4,20 @@ namespace storm {
     namespace builder {
         namespace jit {
             
-            template <typename IndexType, typename ValueType>
+            template <typename StateType, typename ValueType>
             class DistributionEntry {
             public:
                 DistributionEntry();
-                DistributionEntry(IndexType const& index, ValueType const& value);
+                DistributionEntry(StateType const& state, ValueType const& value);
                 
-                IndexType const& getIndex() const;
+                StateType const& getState() const;
                 ValueType const& getValue() const;
                 
                 void addToValue(ValueType const& value);
                 void divide(ValueType const& value);
 
             private:
-                IndexType index;
+                StateType state;
                 ValueType value;
             };
             

src/storm/builder/jit/ModelComponentsBuilder.cpp

@@ -58,7 +58,7 @@ namespace storm {
                     for (auto const& choice : behaviour.getChoices()) {
                         // Add the elements to the transition matrix.
                         for (auto const& element : choice.getDistribution()) {
-                            transitionMatrixBuilder->addNextValue(currentRow, element.getIndex(), element.getValue());
+                            transitionMatrixBuilder->addNextValue(currentRow, element.getState(), element.getValue());
                         }
                         
                         // Add state-action reward entries.

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

@@ -6,7 +6,6 @@
 
 #include "storm/solver/SmtSolver.h"
 
-
 #include "storm/storage/jani/Edge.h"
 #include "storm/storage/jani/EdgeDestination.h"
 #include "storm/storage/jani/Model.h"
@@ -16,6 +15,8 @@
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
 
+#include "storm/builder/jit/Distribution.h"
+
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/solver.h"
@@ -414,36 +415,32 @@ namespace storm {
                 iteratorList[i] = edgeCombination[i].second.cbegin();
             }
             
+            storm::builder::jit::Distribution<CompressedState, ValueType> currentDistribution;
+            storm::builder::jit::Distribution<CompressedState, ValueType> nextDistribution;
+
             // As long as there is one feasible combination of commands, keep on expanding it.
             bool done = false;
             while (!done) {
-                boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
-                boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
                 std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
                 
-                currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+                currentDistribution.add(state, storm::utility::one<ValueType>());
                 
                 for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
                     storm::jani::Edge const& edge = **iteratorList[i];
                     
                     for (auto const& destination : edge.getDestinations()) {
-                        for (auto const& stateProbabilityPair : *currentTargetStates) {
+                        for (auto const& stateProbability : currentDistribution) {
                             // Compute the new state under the current update and add it to the set of new target states.
-                            CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, this->variableInformation.locationVariables[edgeCombination[i].first]);
+                            CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first]);
                             
                             // If the new state was already found as a successor state, update the probability
                             // and otherwise insert it.
-                            ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
+                            ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability());
                             if (edge.hasRate()) {
                                 probability *= this->evaluator->asRational(edge.getRate());
                             }
                             if (probability != storm::utility::zero<ValueType>()) {
-                                auto targetStateIt = newTargetStates->find(newTargetState);
-                                if (targetStateIt != newTargetStates->end()) {
-                                    targetStateIt->second += probability;
-                                } else {
-                                    newTargetStates->emplace(newTargetState, probability);
-                                }
+                                nextDistribution.add(newTargetState, probability);
                             }
                         }
                         
@@ -452,11 +449,11 @@ namespace storm {
                         performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
                     }
                     
+                    nextDistribution.compress();
+                    
                     // If there is one more command to come, shift the target states one time step back.
                     if (i < iteratorList.size() - 1) {
-                        delete currentTargetStates;
-                        currentTargetStates = newTargetStates;
-                        newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                        currentDistribution = std::move(nextDistribution);
                     }
                 }
                 
@@ -473,12 +470,12 @@ namespace storm {
                 
                 // Add the probabilities/rates to the newly created choice.
                 ValueType probabilitySum = storm::utility::zero<ValueType>();
-                for (auto const& stateProbabilityPair : *newTargetStates) {
-                    StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
-                    choice.addProbability(actualIndex, stateProbabilityPair.second);
+                for (auto const& stateProbability : nextDistribution) {
+                    StateType actualIndex = stateToIdCallback(stateProbability.getState());
+                    choice.addProbability(actualIndex, stateProbability.getValue());
                     
                     if (this->options.isExplorationChecksSet()) {
-                        probabilitySum += stateProbabilityPair.second;
+                        probabilitySum += stateProbability.getValue();
                     }
                 }
                 
@@ -487,10 +484,6 @@ namespace storm {
                     STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ").");
                 }
                 
-                // Dispose of the temporary maps.
-                delete currentTargetStates;
-                delete newTargetStates;
-                
                 // Now, check whether there is one more command combination to consider.
                 bool movedIterator = false;
                 for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) {
@@ -608,7 +601,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 +618,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);
             }
+            
+            auto 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

@@ -8,6 +8,8 @@
 #include "storm/storage/expressions/SimpleValuation.h"
 #include "storm/storage/sparse/PrismChoiceOrigins.h"
 
+#include "storm/builder/jit/Distribution.h"
+
 #include "storm/solver/SmtSolver.h"
 
 #include "storm/utility/constants.h"
@@ -449,6 +451,9 @@ namespace storm {
         std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
             std::vector<Choice<ValueType>> result;
 
+            storm::builder::jit::Distribution<CompressedState, ValueType> currentDistribution;
+            storm::builder::jit::Distribution<CompressedState, ValueType> nextDistribution;
+
             for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
                 boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
                 
@@ -465,40 +470,32 @@ namespace storm {
                     // As long as there is one feasible combination of commands, keep on expanding it.
                     bool done = false;
                     while (!done) {
-                        boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
-                        boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
-                        
-                        currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+                        currentDistribution.clear();
+                        nextDistribution.clear();
+
+                        currentDistribution.add(state, storm::utility::one<ValueType>());
                         
                         for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
                             storm::prism::Command const& command = *iteratorList[i];
                             for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
                                 storm::prism::Update const& update = command.getUpdate(j);
                                 
-                                for (auto const& stateProbabilityPair : *currentTargetStates) {
-                                    ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
+                                for (auto const& stateProbability : currentDistribution) {
+                                    ValueType probability = stateProbability.getValue() * this->evaluator->asRational(update.getLikelihoodExpression());
 
                                     if (!storm::utility::isZero<ValueType>(probability)) {
                                         // Compute the new state under the current update and add it to the set of new target states.
-                                        CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
-                                        
-                                        // If the new state was already found as a successor state, update the probability
-                                        // and otherwise insert it.
-                                        auto targetStateIt = newTargetStates->find(newTargetState);
-                                        if (targetStateIt != newTargetStates->end()) {
-                                            targetStateIt->second += probability;
-                                        } else {
-                                            newTargetStates->emplace(newTargetState, probability);
-                                        }
+                                        CompressedState newTargetState = applyUpdate(stateProbability.getState(), update);
+                                        nextDistribution.add(newTargetState, probability);
                                     }
                                 }
                             }
                             
+                            nextDistribution.compress();
+                            
                             // If there is one more command to come, shift the target states one time step back.
                             if (i < iteratorList.size() - 1) {
-                                delete currentTargetStates;
-                                currentTargetStates = newTargetStates;
-                                newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                                currentDistribution = std::move(nextDistribution);
                             }
                         }
                         
@@ -524,11 +521,11 @@ namespace storm {
                         
                         // Add the probabilities/rates to the newly created choice.
                         ValueType probabilitySum = storm::utility::zero<ValueType>();
-                        for (auto const& stateProbabilityPair : *newTargetStates) {
-                            StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
-                            choice.addProbability(actualIndex, stateProbabilityPair.second);
+                        for (auto const& stateProbability : nextDistribution) {
+                            StateType actualIndex = stateToIdCallback(stateProbability.getState());
+                            choice.addProbability(actualIndex, stateProbability.getValue());
                             if (this->options.isExplorationChecksSet()) {
-                                probabilitySum += stateProbabilityPair.second;
+                                probabilitySum += stateProbability.getValue();
                             }
                         }
                         
@@ -550,10 +547,6 @@ namespace storm {
                             choice.addReward(stateActionRewardValue);
                         }
                         
-                        // Dispose of the temporary maps.
-                        delete currentTargetStates;
-                        delete newTargetStates;
-                        
                         // Now, check whether there is one more command combination to consider.
                         bool movedIterator = false;
                         for (int_fast64_t j = iteratorList.size() - 1; !movedIterator && j >= 0; --j) {
@@ -575,7 +568,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 +585,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/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -89,10 +89,14 @@ namespace storm {
                 }
 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+                // The solution is unique as we assume non-zeno MAs.
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic);
+                solver->setHasUniqueSolution();
+                solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
                 solver->setRequirementsChecked();
                 solver->setCachingEnabled(true);
                 
@@ -376,10 +380,14 @@ namespace storm {
                 std::vector<ValueType> x(numberOfSspStates);
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
+                solver->setHasUniqueSolution();
+                solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
                 solver->setRequirementsChecked();
                 solver->solveEquations(dir, x, b);
                 
@@ -584,10 +592,14 @@ namespace storm {
                 std::vector<ValueType> b = probabilisticChoiceRewards;
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+                // The solution is unique as we assume non-zeno MAs.
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearLowerBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic));
+                solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setHasUniqueSolution(true);
                 solver->setRequirementsChecked(true);
                 solver->setCachingEnabled(true);
                 

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -108,8 +108,8 @@ namespace storm {
                     oneStepProbabilities = std::move(subvector);
                 } else {
                     STORM_LOG_DEBUG("Not eliminating ECs as there are none.");
-                    eliminateExtendedStatesFromExplicitRepresentation(explicitRepresentation, solverRequirementsData.initialScheduler, solverRequirementsData.properMaybeStates);
                     oneStepProbabilities = explicitRepresentation.first.getConstrainedRowGroupSumVector(solverRequirementsData.properMaybeStates, targetStates);
+                    eliminateExtendedStatesFromExplicitRepresentation(explicitRepresentation, solverRequirementsData.initialScheduler, solverRequirementsData.properMaybeStates);
                 }
             }
             
@@ -135,8 +135,10 @@ namespace storm {
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
+                        // If we minimize, we know that the solution to the equation system is unique.
+                        bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize;
                         // Check for requirements of the solver early so we can adjust the maybe state computation accordingly.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir);
                         storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
                         SolverRequirementsData<ValueType> solverRequirementsData;
                         bool extendMaybeStates = false;
@@ -212,6 +214,10 @@ namespace storm {
                         std::vector<ValueType> x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero<ValueType>());
                         
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
+                        
+                        // Set whether the equation system will have a unique solution
+                        solver->setHasUniqueSolution(uniqueSolution);
+
                         if (solverRequirementsData.initialScheduler) {
                             solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get()));
                         }
@@ -487,8 +493,10 @@ namespace storm {
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
+                        // If we maximize, we know that the solution to the equation system is unique.
+                        bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize;
                         // Check for requirements of the solver this early so we can adapt the maybe states accordingly.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir);
                         storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
                         bool extendMaybeStates = false;
                         if (!clearedRequirements.empty()) {
@@ -568,6 +576,9 @@ namespace storm {
                         // Now solve the resulting equation system.
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create();
                         
+                        // Set whether the equation system will have a unique solution
+                        solver->setHasUniqueSolution(uniqueSolution);
+                        
                         // If the solver requires upper bounds, compute them now.
                         if (requirements.requiresUpperBounds()) {
                             setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get());

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -22,7 +22,7 @@
 
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/solver/LpSolver.h"
- 
+
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/MinMaxEquationSolverSettings.h"
 
@@ -38,6 +38,11 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
 
+            enum class EquationSystemType {
+                UntilProbabilities,
+                ExpectedRewards
+            };
+            
             template<typename ValueType>
             std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
@@ -91,12 +96,12 @@ namespace storm {
             }
             
             template<typename ValueType>
-            std::vector<uint_fast64_t> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
+            std::vector<uint_fast64_t> computeValidSchedulerHint(EquationSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
                 storm::storage::Scheduler<ValueType> validScheduler(maybeStates.size());
 
-                if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (type == EquationSystemType::UntilProbabilities) {
                     storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler, boost::none);
-                } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                } else if (type == EquationSystemType::ExpectedRewards) {
                     storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler);
                 } else {
                     STORM_LOG_ASSERT(false, "Unexpected equation system type.");
@@ -114,7 +119,7 @@ namespace storm {
             
             template<typename ValueType>
             struct SparseMdpHintType {
-                SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false) {
+                SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) {
                     // Intentionally left empty.
                 }
                 
@@ -169,6 +174,10 @@ namespace storm {
                 bool getComputeUpperBounds() {
                     return computeUpperBounds;
                 }
+
+                bool hasUniqueSolution() const {
+                    return uniqueSolution;
+                }
                 
                 boost::optional<std::vector<uint64_t>> schedulerHint;
                 boost::optional<std::vector<ValueType>> valueHint;
@@ -177,6 +186,7 @@ namespace storm {
                 boost::optional<std::vector<ValueType>> upperResultBounds;
                 bool eliminateEndComponents;
                 bool computeUpperBounds;
+                bool uniqueSolution;
             };
             
             template<typename ValueType>
@@ -230,19 +240,22 @@ namespace storm {
             }
             
             template<typename ValueType>
-            SparseMdpHintType<ValueType> computeHints(storm::solver::EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
+            SparseMdpHintType<ValueType> computeHints(EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
                 SparseMdpHintType<ValueType> result;
 
+                // The solution to the min-max equation system is unique if we minimize until probabilities or
+                // maximize reachability rewards or if the hint tells us that there are no end-compontnes.
+                result.uniqueSolution = (dir == storm::solver::OptimizationDirection::Minimize && type == EquationSystemType::UntilProbabilities)
+                                      || (dir == storm::solver::OptimizationDirection::Maximize && type == EquationSystemType::ExpectedRewards)
+                                      || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
+                
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type, dir);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(result.uniqueSolution, dir);
                 if (!requirements.empty()) {
-                    // If the hint tells us that there are no end-components, we can clear that requirement.
-                    if (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()) {
-                        requirements.clearNoEndComponents();
-                    }
                     
                     // If the solver still requires no end-components, we have to eliminate them later.
                     if (requirements.requiresNoEndComponents()) {
+                        STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
                         STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
                         result.eliminateEndComponents = true;
                         requirements.clearNoEndComponents();
@@ -256,9 +269,9 @@ namespace storm {
                     }
                     
                     // Finally, we have information on the bounds depending on the problem type.
-                    if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                    if (type == EquationSystemType::UntilProbabilities) {
                         requirements.clearBounds();
-                    } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                    } else if (type == EquationSystemType::ExpectedRewards) {
                         requirements.clearLowerBounds();
                     }
                     if (requirements.requiresUpperBounds()) {
@@ -273,8 +286,7 @@ namespace storm {
                 // Only if there is no end component decomposition that we will need to do later, we use value and scheduler
                 // hints from the provided hint.
                 if (!result.eliminateEndComponents) {
-                    bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
-                    extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck);
+                    extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution);
                 } else {
                     STORM_LOG_WARN_COND(hint.isEmpty(), "A non-empty hint was provided, but its information will be disregarded.");
                 }
@@ -283,7 +295,7 @@ namespace storm {
                 if (!result.hasLowerResultBound()) {
                     result.lowerResultBound = storm::utility::zero<ValueType>();
                 }
-                if (!result.hasUpperResultBound() && type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (!result.hasUpperResultBound() && type == EquationSystemType::UntilProbabilities) {
                     result.upperResultBound = storm::utility::one<ValueType>();
                 }
                 
@@ -326,6 +338,7 @@ namespace storm {
                 // Set up the solver.
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
                 solver->setRequirementsChecked();
+                solver->setHasUniqueSolution(hint.hasUniqueSolution());
                 if (hint.hasLowerResultBound()) {
                     solver->setLowerBound(hint.getLowerResultBound());
                 }
@@ -526,7 +539,7 @@ namespace storm {
                         // In this case we have have to compute the remaining probabilities.
                         
                         // Obtain proper hint information either from the provided hint or from requirements of the solver.
-                        SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory);
+                        SparseMdpHintType<ValueType> hintInformation = computeHints(EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory);
                         
                         // Declare the components of the equation system we will solve.
                         storm::storage::SparseMatrix<ValueType> submatrix;
@@ -882,7 +895,7 @@ namespace storm {
                         }
                         
                         // Obtain proper hint information either from the provided hint or from requirements of the solver.
-                        SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
+                        SparseMdpHintType<ValueType> hintInformation = computeHints(EquationSystemType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
                         
                         // Declare the components of the equation system we will solve.
                         storm::storage::SparseMatrix<ValueType> submatrix;
@@ -1089,14 +1102,16 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
-                requirements.clearLowerBounds();
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, goal.direction());
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
                 
                 std::vector<ValueType> sspResult(numberOfSspStates);
                 goal.restrictRelevantValues(statesNotContainedInAnyMec);
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix);
                 solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
+                solver->setHasUniqueSolution();
                 solver->setRequirementsChecked();
                 solver->solveEquations(sspResult, b);
                 

src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -21,15 +21,21 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
+       
+            enum class EquationSystemType {
+                UntilProbabilities,
+                ExpectedRewards
+            };
+
             
             template<storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) {
+            storm::dd::Bdd<DdType> computeValidSchedulerHint(EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) {
             
                 storm::dd::Bdd<DdType> result;
                 
-                if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (type == EquationSystemType::UntilProbabilities) {
                     result = storm::utility::graph::computeSchedulerProbGreater0E(model, transitionMatrix.notZero(), maybeStates, targetStates);
-                } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                } else if (type == EquationSystemType::ExpectedRewards) {
                     result = storm::utility::graph::computeSchedulerProb1E(model, transitionMatrix.notZero(), maybeStates, targetStates, maybeStates || targetStates);
                 }
                 
@@ -60,12 +66,12 @@ namespace storm {
                 std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
                 
                 // Check requirements of solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir);
                 boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
                 if (!requirements.empty()) {
                     if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
                         STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
-                        initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability1);
+                        initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability1);
                         requirements.clearValidInitialScheduler();
                     }
                     requirements.clearBounds();
@@ -217,12 +223,12 @@ namespace storm {
                 std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
                 
                 // Check requirements of solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir);
                 boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
                 if (!requirements.empty()) {
                     if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
                         STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
-                        initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates);
+                        initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates);
                         requirements.clearValidInitialScheduler();
                     }
                     requirements.clearLowerBounds();

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

@@ -29,22 +29,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";
@@ -52,7 +43,6 @@ 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.")
@@ -73,19 +63,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());
@@ -102,7 +83,7 @@ namespace storm {
             bool IOSettings::isExportDotSet() const {
                 return this->getOption(exportDotOptionName).getHasOptionBeenSet();
             }
-            
+
             std::string IOSettings::getExportDotFilename() const {
                 return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString();
             }
@@ -114,11 +95,11 @@ 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();
             }
@@ -126,11 +107,11 @@ namespace storm {
             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();
             }
@@ -154,15 +135,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();
             }
@@ -174,93 +155,48 @@ 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::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -158,34 +158,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 +190,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 +203,7 @@ 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,36 +250,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 check() const override;
                 void finalize() override;
@@ -337,22 +271,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/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"
@@ -168,6 +167,16 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const {
+            STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
+            if (this->hasUpperBound(BoundType::Global)) {
+                upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound());
+            } else {
+                upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end());
+            }
+        }
+        
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const {
             STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
@@ -179,17 +188,7 @@ namespace storm {
                     upperBoundsVector = std::make_unique<std::vector<ValueType>>(length, this->getUpperBound());
                 }
             } else {
-                if (this->hasUpperBound(BoundType::Global)) {
-                    for (auto& e : *upperBoundsVector) {
-                        e = this->getUpperBound();
-                    }
-                } else {
-                    auto upperBoundsIt = this->getUpperBounds().begin();
-                    for (auto& e : *upperBoundsVector) {
-                        e = *upperBoundsIt;
-                        ++upperBoundsIt;
-                    }
-                }
+                createUpperBoundsVector(*upperBoundsVector);
             }
         }
         

src/storm/solver/AbstractEquationSolver.h

@@ -160,6 +160,7 @@ namespace storm {
             TerminationCondition<ValueType> const& getTerminationCondition() const;
             std::unique_ptr<TerminationCondition<ValueType>> const& getTerminationConditionPointer() const;
             
+            void createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const;
             void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const;
             void createLowerBoundsVector(std::vector<ValueType>& lowerBoundsVector) const;
 

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -45,7 +45,6 @@ namespace storm {
             switch (solutionMethod) {
                 case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break;
                 case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break;
-                case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break;
                 case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver.");
@@ -136,9 +135,6 @@ namespace storm {
                 case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
                     result = solveEquationsPolicyIteration(dir, x, b);
                     break;
-                case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::Acyclic:
-                    result = solveEquationsAcyclic(dir, x, b);
-                    break;
                 case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch:
                     result = solveEquationsRationalSearch(dir, x, b);
                     break;
@@ -268,67 +264,44 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             // Start by copying the requirements of the linear equation solver.
             MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
 
-            // General requirements.
             if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                requirements.requireLowerBounds();
-            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
-                // As rational search needs to approach the solution from below, we cannot start with a valid scheduler hint as we would otherwise do.
-                // Instead, we need to require no end components.
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                if (this->getSettings().getForceSoundness()) {
+                    // Interval iteration requires a unique solution and lower+upper bounds
+                    if (!this->hasUniqueSolution()) {
                         requirements.requireNoEndComponents();
                     }
-                }
-            }
-            
-            // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
-            if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
-                requirements.requireNoEndComponents();
-            }
-            
-            // Guide requirements by whether or not we force soundness.
-            if (this->getSettings().getForceSoundness()) {
-                if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                    // Require both bounds now.
                     requirements.requireBounds();
-                    
-                    // If we need to also converge from above, we cannot deal with end components in the notorious cases.
-                    if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                        if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireNoEndComponents();
-                        }
-                    } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                        if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                            requirements.requireNoEndComponents();
-                        }
-                    }
-                } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                    if (equationSystemType == EquationSystemType::UntilProbabilities) {
+                } else if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique.
+                    // Computing a scheduler is only possible if the solution is unique
+                    if (this->isTrackSchedulerSet()) {
+                        requirements.requireNoEndComponents();
+                    } else {
+                        // As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above).
                         if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireValidInitialScheduler();
+                            requirements.requireLowerBounds();
                         }
-                    } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
                         if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                            requirements.requireValidInitialScheduler();
+                            requirements.requireUpperBounds();
                         }
                     }
                 }
-            } else {
-                if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                    if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                        if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireValidInitialScheduler();
-                        }
-                    }
-                } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireValidInitialScheduler();
-                    }
+            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
+                // Rational search needs to approach the solution from below.
+                requirements.requireLowerBounds();
+                // The solution needs to be unique in case of minimizing or in cases where we want a scheduler.
+                if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) {
+                    requirements.requireNoEndComponents();
+                }
+            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
+                if (!this->hasUniqueSolution()) {
+                    requirements.requireValidInitialScheduler();
                 }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver.");
             }
         
             return requirements;
@@ -394,9 +367,8 @@ namespace storm {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
             }
             
-            // By default, the guarantee that we can provide is that our solution is always less-or-equal than the
-            // actual solution.
-            SolverGuarantee guarantee = SolverGuarantee::LessOrEqual;
+            // By default, we can not provide any guarantee
+            SolverGuarantee guarantee = SolverGuarantee::None;
             
             if (this->hasInitialScheduler()) {
                 // Resolve the nondeterminism according to the initial scheduler.
@@ -418,14 +390,21 @@ namespace storm {
                 }
                 submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
                 
-                // If we were given an initial scheduler and are in fact minimizing, our current solution becomes
-                // always greater-or-equal than the actual solution.
-                if (dir == storm::OptimizationDirection::Minimize) {
+                // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes
+                // always less-or-equal (greater-or-equal) than the actual solution.
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    guarantee = SolverGuarantee::GreaterOrEqual;
+                }
+            } else if (!this->hasUniqueSolution()) {
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    this->createLowerBoundsVector(x);
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    this->createUpperBoundsVector(x);
                     guarantee = SolverGuarantee::GreaterOrEqual;
                 }
-            } else {
-                // If no initial scheduler is given, we start from the lower bound.
-                this->createLowerBoundsVector(x);
             }
 
             std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
@@ -934,83 +913,6 @@ namespace storm {
             return solveEquationsRationalSearchHelper<double>(dir, x, b);
         }
         
-        template<typename ValueType>
-        bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsAcyclic(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
-            uint64_t numGroups = this->A->getRowGroupCount();
-
-            // Allocate memory for the scheduler (if required)
-            if (this->isTrackSchedulerSet()) {
-                if (this->schedulerChoices) {
-                    this->schedulerChoices->resize(numGroups);
-                } else {
-                    this->schedulerChoices = std::vector<uint_fast64_t>(numGroups);
-                }
-            }
-            
-            // We now compute a topological sort of the row groups.
-            // If caching is enabled, it might be possible to obtain this sort from the cache.
-            if (this->isCachingEnabled()) {
-                if (rowGroupOrdering) {
-                    for (auto const& group : *rowGroupOrdering) {
-                        computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr);
-                    }
-                    return true;
-                } else {
-                    rowGroupOrdering = std::make_unique<std::vector<uint64_t>>();
-                    rowGroupOrdering->reserve(numGroups);
-                }
-            }
-            
-            auto transposedMatrix = this->A->transpose(true);
-            
-            // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value.
-            storm::storage::BitVector processedGroups(numGroups, false);
-            // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now.
-            // A group can be processed if all successors have already been processed.
-            // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true.
-            // This is due to the observation that groups with higher indices usually need to be processed earlier.
-            storm::storage::BitVector candidates(numGroups, true);
-            uint64_t candidate = numGroups - 1;
-            for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) {
-                candidates.set(numGroups - candidate - 1, false);
-                
-                // Check if the candidate row group has an unprocessed successor
-                bool hasUnprocessedSuccessor = false;
-                for (auto const& entry : this->A->getRowGroup(candidate)) {
-                    if (!processedGroups.get(entry.getColumn())) {
-                        hasUnprocessedSuccessor = true;
-                        break;
-                    }
-                }
-                
-                uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1;
-                
-                if (!hasUnprocessedSuccessor) {
-                    // This candidate can be processed.
-                    processedGroups.set(candidate);
-                    computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr);
-                    if (this->isCachingEnabled()) {
-                        rowGroupOrdering->push_back(candidate);
-                    }
-                    
-                    // Add new candidates
-                    for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) {
-                        uint64_t predecessor = predecessorEntry.getColumn();
-                        if (!candidates.get(numGroups - predecessor - 1)) {
-                            candidates.set(numGroups - predecessor - 1, true);
-                            nextCandidate = std::max(nextCandidate, predecessor);
-                            ++numCandidates;
-                        }
-                    }
-                }
-                candidate = nextCandidate;
-            }
-            
-            assert(candidates.empty());
-            STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic.");
-            return true;
-        }
-        
         template<typename ValueType>
         void IterativeMinMaxLinearEquationSolver<ValueType>::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, uint_fast64_t* choice) const {
             uint64_t row = this->A->getRowGroupIndices()[group];

src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@@ -62,7 +62,7 @@ namespace storm {
             ValueType getPrecision() const;
             bool getRelative() const;
             
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
             
         private:
             bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -110,12 +110,12 @@ namespace storm {
         
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             
             MinMaxLinearEquationSolverRequirements requirements;
             
-            // In case we need to retrieve a scheduler, end components are forbidden
-            if (this->isTrackSchedulerSet()) {
+            // In case we need to retrieve a scheduler, the solution has to be unique
+            if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) {
                 requirements.requireNoEndComponents();
             }
             

src/storm/solver/LpMinMaxLinearEquationSolver.h

@@ -18,7 +18,7 @@ namespace storm {
 
             virtual void clearCache() const override;
 
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
             
         private:
             std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;

src/storm/solver/MinMaxLinearEquationSolver.cpp

@@ -19,7 +19,7 @@ namespace storm {
     namespace solver {
         
         template<typename ValueType>
-        MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) {
+        MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
@@ -56,6 +56,16 @@ namespace storm {
             direction = OptimizationDirectionSetting::Unset;
         }
         
+        template<typename ValueType>
+        void MinMaxLinearEquationSolver<ValueType>::setHasUniqueSolution(bool value) {
+            uniqueSolution = value;
+        }
+        
+        template<typename ValueType>
+        bool MinMaxLinearEquationSolver<ValueType>::hasUniqueSolution() const {
+            return uniqueSolution;
+        }
+        
         template<typename ValueType>
         void MinMaxLinearEquationSolver<ValueType>::setTrackScheduler(bool trackScheduler) {
             this->trackScheduler = trackScheduler;
@@ -127,7 +137,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             return MinMaxLinearEquationSolverRequirements();
         }
         
@@ -199,10 +209,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             // Create dummy solver and ask it for requirements.
             std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create();
-            return solver->getRequirements(equationSystemType, direction);
+            solver->setHasUniqueSolution(hasUniqueSolution);
+            return solver->getRequirements(direction);
         }
         
         template<typename ValueType>

src/storm/solver/MinMaxLinearEquationSolver.h

@@ -12,7 +12,6 @@
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/Scheduler.h"
 #include "storm/solver/OptimizationDirection.h"
-#include "storm/solver/EquationSystemType.h"
 #include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
 
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -94,6 +93,16 @@ namespace storm {
              */
             void unsetOptimizationDirection();
             
+            /*!
+             * Sets whether the solution to the min max equation system is known to be unique.
+             */
+            void setHasUniqueSolution(bool value = true);
+            
+            /*!
+             * Retrieves whether the solution to the min max equation system is assumed to be unique
+             */
+            bool hasUniqueSolution() const;
+            
             /*!
              * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently
              * stored scheduler (if any) is deleted.
@@ -155,7 +164,7 @@ namespace storm {
              * Retrieves the requirements of this solver for solving equations with the current settings. The requirements
              * are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             
             /*!
              * Notifies the solver that the requirements for solving equations have been checked. If this has not been
@@ -184,6 +193,9 @@ namespace storm {
             boost::optional<std::vector<uint_fast64_t>> initialScheduler;
             
         private:
+            // Whether the solver can assume that the min-max equation system has a unique solution
+            bool uniqueSolution;
+            
             /// Whether some of the generated data during solver calls should be cached.
             bool cachingEnabled;
             
@@ -212,7 +224,7 @@ namespace storm {
              * Retrieves the requirements of the solver that would be created when calling create() right now. The
              * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             void setRequirementsChecked(bool value = true);
             bool isRequirementsCheckedSet() const;
 

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -86,12 +86,12 @@ namespace storm {
         }
 
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), requirementsChecked(false) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), uniqueSolution(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), uniqueSolution(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
@@ -280,11 +280,15 @@ namespace storm {
             // Set up the environment.
             storm::dd::Add<DdType, ValueType> localX;
             
-            // If we were given an initial scheduler, we take its solution as the starting point.
-            if (this->hasInitialScheduler()) {
-                localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+            if (this->hasUniqueSolution()) {
+                localX = x;
             } else {
-                localX = this->getLowerBoundsVector();
+                // If we were given an initial scheduler, we take its solution as the starting point.
+                if (this->hasInitialScheduler()) {
+                    localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+                } else {
+                    localX = this->getLowerBoundsVector();
+                }
             }
             
             ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());
@@ -419,39 +423,42 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             MinMaxLinearEquationSolverRequirements requirements;
 
             if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                    if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                        requirements.requireValidInitialScheduler();
-                    }
-                }
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireValidInitialScheduler();
-                    }
+                if (!this->hasUniqueSolution()) {
+                    requirements.requireValidInitialScheduler();
                 }
             } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                requirements.requireLowerBounds();
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                if (!this->hasUniqueSolution()) {
+                    if (!direction || direction.get() == storm::solver::OptimizationDirection::Maximize) {
+                        requirements.requireLowerBounds();
+                    }
+                    if (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize) {
                         requirements.requireValidInitialScheduler();
                     }
                 }
             } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
                 requirements.requireLowerBounds();
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireNoEndComponents();
-                    }
+                if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) {
+                    requirements.requireNoEndComponents();
                 }
             }
 
             return requirements;
         }
         
+        template<storm::dd::DdType DdType, typename ValueType>
+        void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setHasUniqueSolution(bool value) {
+            this->uniqueSolution = value;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::hasUniqueSolution() const {
+            return this->uniqueSolution;
+        }
+        
         template<storm::dd::DdType DdType, typename ValueType>
         void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setRequirementsChecked(bool value) {
             this->requirementsChecked = value;
@@ -484,9 +491,10 @@ namespace storm {
         }
 
         template<storm::dd::DdType DdType, typename ValueType>
-        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = this->create();
-            return solver->getRequirements(equationSystemType, direction);
+            solver->setHasUniqueSolution(hasUniqueSolution);
+            return solver->getRequirements(direction);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/storm/solver/SymbolicMinMaxLinearEquationSolver.h

@@ -127,7 +127,17 @@ namespace storm {
             /*!
              * Retrieves the requirements of the solver.
              */
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            
+                        /*!
+             * Sets whether the solution to the min max equation system is known to be unique.
+             */
+            void setHasUniqueSolution(bool value = true);
+            
+            /*!
+             * Retrieves whether the solution to the min max equation system is assumed to be unique
+             */
+            bool hasUniqueSolution() const;
             
             /*!
              * Notifies the solver that the requirements for solving equations have been checked. If this has not been
@@ -208,6 +218,9 @@ namespace storm {
             // The settings to use.
             SymbolicMinMaxLinearEquationSolverSettings<ValueType> settings;
             
+            // Whether the solver can assume that the min-max equation system has a unique solution
+            bool uniqueSolution;
+            
             // A flag indicating whether the requirements were checked.
             bool requirementsChecked;
             
@@ -230,7 +243,7 @@ namespace storm {
              * Retrieves the requirements of the solver that would be created when calling create() right now. The
              * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             
         private:
             virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create() const = 0;

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -119,7 +119,9 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsJacobi(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
             storm::dd::DdManager<DdType>& manager = this->getDdManager();
-            
+
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (jacobi)");
+
             // Start by computing the Jacobi decomposition of the matrix A.
             storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
             diagonal &= this->allRows;
@@ -185,6 +187,7 @@ namespace storm {
         
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsPower(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (power)");
             PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
             
             if (result.status == SolverStatus::Converged) {
@@ -311,6 +314,7 @@ namespace storm {
         
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearch(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (rational search)");
             return solveEquationsRationalSearchHelper<double>(x, b);
         }
         

src/storm/storage/BitVector.cpp

@@ -116,7 +116,10 @@ namespace storm {
             // Only perform the assignment if the source and target are not identical.
             if (this != &other) {
                 bitCount = other.bitCount;
-                buckets = new uint64_t[other.bucketCount()];
+                if (buckets && bucketCount() != other.bucketCount()) {
+                    delete[] buckets;
+                    buckets = new uint64_t[other.bucketCount()];
+                }
                 std::copy_n(other.buckets, other.bucketCount(), buckets);
             }
             return *this;
@@ -999,22 +1002,22 @@ 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);
+        std::size_t FNV1aBitVectorHash::operator()(storm::storage::BitVector const& bv) const {
+            std::size_t seed = 14695981039346656037ull;
+            
+            unsigned char const* it = reinterpret_cast<unsigned char const*>(bv.buckets);
+            unsigned char const* ite = it + 8 * bv.bucketCount();
+            
+            while (it < ite) {
+                seed ^= *it++;
+                
+                // Multiplication with magic prime.
+                seed += (seed << 1) + (seed << 4) + (seed << 5) + (seed << 7) + (seed << 8) + (seed << 40);
             }
-
-            // Erase the last bit and add one to definitely make this hash value non-zero.
-            result &= ~1ull;
-            result += 1;
-
-            return result;
+            
+            return seed;
         }
-
+        
         // 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);
@@ -1028,7 +1031,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

@@ -501,7 +501,7 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
             friend struct std::hash<storm::storage::BitVector>;
-            friend struct NonZeroBitVectorHash;
+            friend struct FNV1aBitVectorHash;
             
         private:
             /*!
@@ -571,8 +571,7 @@ 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 {
+        struct FNV1aBitVectorHash {
             std::size_t operator()(storm::storage::BitVector const& bv) const;
         };
         

src/storm/storage/BitVectorHashMap.cpp

@@ -5,121 +5,107 @@
 #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 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), currentSize(1), 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; } );
+
+            while (initialSize > 0) {
+                ++currentSize;
+                initialSize >>= 1;
+            }
             
             // Create the underlying containers.
-            buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator);
-            occupied = storm::storage::BitVector(*currentSizeIterator);
-            values = std::vector<ValueType>(*currentSizeIterator);
+            buckets = storm::storage::BitVector(bucketSize * (1ull << currentSize));
+            occupied = storm::storage::BitVector(1ull << currentSize);
+            values = std::vector<ValueType>(1ull << currentSize);
+
+#ifndef NDEBUG
+            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 {
-            return *currentSizeIterator;
+        template<class ValueType, class Hash>
+        std::size_t BitVectorHashMap<ValueType, Hash>::capacity() const {
+            return 1ull << currentSize;
         }
         
-        template<class ValueType, class Hash1, class Hash2>
-        void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() {
-            ++currentSizeIterator;
-            STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big.");
+        template<class ValueType, class Hash>
+        void BitVectorHashMap<ValueType, Hash>::increaseSize() {
+            ++currentSize;
+#ifndef NDEBUG
+            STORM_LOG_TRACE("Increasing size of hash map from " << (1ull << (currentSize - 1)) << " to " << (1ull << currentSize) << ". 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 " << (1ull << (currentSize - 1)) << " to " << (1ull << currentSize) << ".");
+#endif
             
             // Create new containers and swap them with the old ones.
             numberOfElements = 0;
-            storm::storage::BitVector oldBuckets(bucketSize * *currentSizeIterator);
+            storm::storage::BitVector oldBuckets(bucketSize * (1ull << currentSize));
             std::swap(oldBuckets, buckets);
-            storm::storage::BitVector oldOccupied = storm::storage::BitVector(*currentSizeIterator);
+            storm::storage::BitVector oldOccupied = storm::storage::BitVector(1ull << currentSize);
             std::swap(oldOccupied, occupied);
-            std::vector<ValueType> oldValues = std::vector<ValueType>(*currentSizeIterator);
+            std::vector<ValueType> oldValues = std::vector<ValueType>(1ull << currentSize);
             std::swap(oldValues, values);
             
             // Now iterate through the elements and reinsert them in the new storage.
             bool fail = false;
             for (auto bucketIndex : oldOccupied) {
                 fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]);
-                
-                // If we failed to insert just one element, we have to redo the procedure with a larger container size.
-                if (fail) {
-                    break;
-                }
-            }
-            
-            uint_fast64_t failCount = 0;
-            while (fail) {
-                ++failCount;
-                STORM_LOG_ASSERT(failCount < 2, "Increasing size failed too often.");
-                
-                ++currentSizeIterator;
-                STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big.");
-                
-                numberOfElements = 0;
-                buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator);
-                occupied  = storm::storage::BitVector(*currentSizeIterator);
-                values = std::vector<ValueType>(*currentSizeIterator);
-                
-                for (auto bucketIndex : oldOccupied) {
-                    fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]);
-                    
-                    // If we failed to insert just one element, we have to redo the procedure with a larger container size.
-                    if (fail) {
-                        continue;
-                    }
-                }
+                STORM_LOG_ASSERT(!fail, "Expected to be able to insert all elements.");
             }
         }
         
-        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,20 +123,20 @@ 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) {
+            if (numberOfElements >= loadFactor * (1ull << currentSize)) {
                 this->increaseSize();
             }
             
@@ -168,10 +154,10 @@ 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) {
+            if (numberOfElements >= loadFactor * (1ull << currentSize)) {
                 this->increaseSize();
             }
             
@@ -187,42 +173,55 @@ 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>
+        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) % (1ull << currentSize);
             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 += 1;
+                if (bucket == (1ull << currentSize)) {
+                    bucket = 0;
+                }
+
                 if (bucket == initialHash) {
                     return std::make_pair(false, bucket);
                 }
@@ -231,41 +230,49 @@ 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) % (1ull << currentSize);
             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 += 1;
+                if (bucket == (1ull << currentSize)) {
+                    bucket = 0;
+                }
+
                 if (bucket == initialHash) {
                     if (increaseStorage) {
                         this->increaseSize();
-                        bucket = initialHash = hasher1(key) % *currentSizeIterator;
+                        bucket = initialHash = hasher(key) % (1ull << currentSize);
                     } 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,8 @@ 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>>
+        template<typename ValueType, typename Hash = FNV1aBitVectorHash>
         class BitVectorHashMap {
         public:
             class BitVectorHashMapIterator {
@@ -57,6 +58,11 @@ namespace storm {
              */
             BitVectorHashMap(uint64_t bucketSize = 64, uint64_t initialSize = 1000, double loadFactor = 0.75);
             
+            BitVectorHashMap(BitVectorHashMap const&) = default;
+            BitVectorHashMap(BitVectorHashMap&&) = default;
+            BitVectorHashMap& operator=(BitVectorHashMap const&) = default;
+            BitVectorHashMap& operator=(BitVectorHashMap&&) = default;
+
             /*!
              * Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the
              * key is inserted with the given value.
@@ -113,6 +119,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.
@@ -210,8 +223,8 @@ namespace storm {
             // The size of one bucket.
             uint64_t bucketSize;
             
-            // The number of buckets.
-            std::size_t numberOfBuckets;
+            // The number of buckets is 2^currentSize.
+            uint64_t currentSize;
             
             // The buckets that hold the elements of the map.
             storm::storage::BitVector buckets;
@@ -225,15 +238,16 @@ namespace storm {
             // The number of elements in this map.
             std::size_t numberOfElements;
             
-            // An iterator to a value in the static sizes table.
-            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()) {
@@ -249,13 +247,7 @@ namespace storm {
                 }
             }
             
-            // Then check the formulas.
-            for (auto const& formula : this->getFormulas()) {
-                if (formula.getExpression().containsVariable(undefinedConstantVariables)) {
-                    return false;
-                }
-            }
-            
+
             // Proceed by checking each of the modules.
             for (auto const& module : this->getModules()) {
                 if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
@@ -689,7 +681,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 +775,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 +838,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 +1114,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 +1354,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 +1550,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/GmmxxHybridMdpPrctlModelCheckerTest.cpp

@@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     
@@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     

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.666666666666675, 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\"]");
 
@@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
 

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/NativeHybridMdpPrctlModelCheckerTest.cpp

@@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
     
@@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
     
@@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     
@@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     

src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = stateRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = stateAndTransitionRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(14.666658997535706, 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\"]");
 
@@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
 

src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp

@@ -19,6 +19,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) {
     
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
     ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
     
@@ -42,6 +43,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio
     
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setLowerBound(0.0);
+    solver->setUpperBound(1.0);
     
     solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true));
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
@@ -111,6 +114,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
 
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration);
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
     
 	ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
 	ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());

src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp

@@ -20,6 +20,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) {
     
     auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
 
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
     
@@ -83,7 +84,9 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
 
     auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration);
     auto solver = factory.create(A);
-    
+    solver->setLowerBound(0.0);
+    solver->setUpperBound(1.0);
+
 	ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
 	ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 

version.cmake

@@ -0,0 +1,4 @@
+set(STORM_VERSION_MAJOR 1)
+set(STORM_VERSION_MINOR 1)
+set(STORM_VERSION_PATCH 0)
+