Merge branch 'master' of https://github.com/sjunges/storm

.github/workflows/buildtest.yml

@@ -14,7 +14,7 @@ env:
   CARL_BRANCH: "master14"
   CARL_GIT_URL: "https://github.com/smtrat/carl.git"
   STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git"
-  STORM_BRANCH: "master"
+  STORM_BRANCH: "${{ github.ref }}"
   # github runners currently have two cores
   NR_JOBS: "2"
 
@@ -45,7 +45,10 @@ jobs:
       - name: Init Docker
         run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }}
       - name: Git clone
-        run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
+        # git clone cannot clone individual commits based on a sha and some other refs
+        # this workaround fixes this and fetches only one commit
+        run: |
+          sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD"
       - name: Run cmake
         run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
       - name: Build storm
@@ -83,6 +86,8 @@ jobs:
           ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CARL_CMAKE_ARGS=${CARL_CMAKE_DEBUG}" || echo "CARL_CMAKE_ARGS=${CARL_CMAKE_RELEASE}") >> $GITHUB_ENV
 
       - name: Login into docker
+        # Only login if using master on original repo (and not for pull requests or forks)
+        if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
         run: echo "${{ secrets.STORM_CI_DOCKER_PASSWORD }}" | sudo docker login -u "${{ secrets.STORM_CI_DOCKER_USERNAME }}" --password-stdin
       - name: Init Docker
         run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO}
@@ -106,6 +111,8 @@ jobs:
       - name: Build carl
         run: sudo docker exec storm bash -c "cd /opt/carl/build; make lib_carl -j ${NR_JOBS}"
       - name: Deploy carl
+        # Only deploy if using master on original repo (and not for pull requests or forks)
+        if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
         run: |
           sudo docker commit storm movesrwth/carl:ci-${{ matrix.debugOrRelease }}
           sudo docker push movesrwth/carl:ci-${{ matrix.debugOrRelease }}
@@ -114,8 +121,17 @@ jobs:
         #####
         # Build & TEST & DEPLOY STORM
         #####
-      - name: Git clone
-        run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
+      - name: Git shallow clone
+        # Only clone shallow if not using master on original repo (and not for pull requests or forks)
+        if: ${{ !(github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master') }}
+        run: |
+          # git clone cannot clone individual commits based on a sha and some other refs
+          sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD"
+      - name: Git deep clone
+        # needed for versioning for now on deployment
+        if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
+        run: |
+          sudo docker exec storm git clone --branch master $STORM_GIT_URL /opt/storm
       - name: Run cmake
         run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
       - name: Build storm
@@ -135,8 +151,8 @@ jobs:
         run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure"
 
       - name: Deploy storm
-        # Only deploy if using master (and not for pull requests)
-        if: github.ref == 'refs/heads/master'
+        # Only deploy if using master on original repo (and not for pull requests or forks)
+        if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
         run: |
           sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }}
           sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }}
@@ -145,7 +161,8 @@ jobs:
     name: Email notification
     runs-on: ubuntu-latest
     needs: [noDeploy, deploy]
-    if: always() # set always
+    # Only run in main repo and even if previous step failed
+    if: github.repository_owner == 'moves-rwth' && always()
     steps:
       - uses: technote-space/workflow-conclusion-action@v2
       - uses: dawidd6/action-send-mail@v2

.github/workflows/doxygen.yml

@@ -21,6 +21,8 @@ jobs:
   deploy:
     name: Create documentation
     runs-on: ubuntu-latest
+    # Do not run on forks
+    if: github.repository_owner == 'moves-rwth'
     steps:
       - name: Init Docker
         run: sudo docker run -d -it --name storm --privileged ${BASE_IMG}
@@ -55,7 +57,8 @@ jobs:
     name: Email notification
     runs-on: ubuntu-latest
     needs: [deploy]
-    if: always() # set always
+    # Only run in main repo and even if previous step failed
+    if: github.repository_owner == 'moves-rwth' && always()
     steps:
       - uses: technote-space/workflow-conclusion-action@v2
       - uses: dawidd6/action-send-mail@v2

CHANGELOG.md

@@ -1,3 +1,4 @@
+
 Changelog
 ==============
 
@@ -10,6 +11,7 @@ Branch Changes
 Version 1.6.x
 -------------
 ## Version 1.6.4 (20xx/xx)
+- Added support for PRISM models that use unbounded integer variables.
 - Added an export of check results to json. Use `--exportresult` in the command line interface.
 - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface.
 - Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now.

CMakeLists.txt

@@ -47,7 +47,9 @@ set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version
 option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF)
 MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL)
 option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
+mark_as_advanced(USE_SMTRAT)
 option(USE_HYPRO "Sets whether HyPro should be included." OFF)
+mark_as_advanced(USE_HYPRO)
 option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON)
 option(FORCE_COLOR "Force color output" OFF)
 mark_as_advanced(FORCE_COLOR)

README.md

@@ -48,10 +48,12 @@ Storm has been developed at RWTH Aachen University.
 * Jip Spel
 
 ###### Contributors (lexicographical order)
+* Daniel Basgöze
 * Dimitri Bohlender
 * Alexander Bork
 * Harold Bruintjes
 * Michael Deutschen
+* Linus Heck
 * Thomas Heinemann
 * Thomas Henn
 * Tom Janson

resources/3rdparty/carl/CMakeLists.txt

@@ -7,7 +7,7 @@ option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir")
 message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}")
 
 ExternalProject_Add(carl-config
-	GIT_REPOSITORY https://github.com/smtrat/carl
+	GIT_REPOSITORY https://github.com/ths-rwth/carl
 	GIT_TAG master14
 	PREFIX here
 	SOURCE_DIR source_dir

resources/3rdparty/include_cudd.cmake

@@ -36,7 +36,7 @@ endif()
 
 set(CUDD_CXX_COMPILER "${CMAKE_CXX_COMPILER}")
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
-	if (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 12.0.0.12000032)
+	if (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER_EQUAL 12.0.0.12000032)
 		if (CMAKE_HOST_SYSTEM_VERSION VERSION_GREATER_EQUAL 20.1.0)
 			message(WARNING "There are some known issues compiling CUDD on some setups. We implemented a workaround that mostly works, but if you still have problems compiling CUDD, especially if you do not use the default compiler of your system, please contact the Storm developers.")
 			# The issue is known to occur using the Command Line Tools for XCode 12.2. Apparently, it is fixed in the beta for XCode 12.3. 

resources/examples/testfiles/mdp/unbounded.nm

@@ -0,0 +1,8 @@
+mdp
+const int N;
+module main
+	x : int;
+	[] x<=0 -> (x'=x+1);
+	[] x>0 -> (x'=N*x);
+endmodule
+

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -423,13 +423,11 @@ namespace storm {
                         
                         // Then add the constraints for bounds of the integer variables.
                         for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
-                            localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression());
-                            localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression());
+                            localSolver->add(integerVariable.getRangeExpression());
                         }
                         for (auto const& module : program.getModules()) {
                             for (auto const& integerVariable : module.getIntegerVariables()) {
-                                localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression());
-                                localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression());
+                                localSolver->add(integerVariable.getRangeExpression());
                             }
                         }
                     } else {

src/storm-dft/api/storm-dft.h

@@ -129,8 +129,8 @@ namespace storm {
          */
         template<typename ValueType>
         storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const& additionalRelevantEventNames) {
-            storm::utility::RelevantEvents events(additionalRelevantEventNames);
-            events.addNamesFromProperty(properties);
+            storm::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
+            events.insertNamesFromProperties(properties.begin(), properties.end());
             return events;
         }
 
@@ -153,7 +153,7 @@ namespace storm {
          */
         template<typename ValueType>
         typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
-        analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
+        analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
                    double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false,
                    storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput = false) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);

src/storm-dft/modelchecker/dft/DFTModelChecker.h

@@ -56,7 +56,7 @@ namespace storm {
              * @return Model checking results for the given properties..
              */
             dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
-                              storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
+                              storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
                               double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
                               bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);
 

src/storm-dft/utility/RelevantEvents.h

@@ -7,6 +7,7 @@
 
 #include "storm-dft/storage/dft/DFT.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
+#include <initializer_list>
 
 namespace storm {
     namespace utility {
@@ -15,47 +16,65 @@ namespace storm {
         public:
 
             /*!
-             * Create relevant events from given event names.
+             * Constructs empty RelevantEvents object
+             */
+            RelevantEvents() = default;
+
+            /*!
+             * Create relevant events from given event names in an initializer list.
              * If name 'all' occurs, all elements are stored as relevant.
              *
-             * @param relevantEvents List of relevant event names.
+             * Allows syntactic sugar like:
+             * RelevantEvents e = {};
+             * and
+             * RelevantEvents e{"a"};
+             *
+             * @param init The initializer list.
              */
-            RelevantEvents(std::vector<std::string> const& relevantEvents = {}) {
-                // check if the name "all" occurs
-                if (std::any_of(relevantEvents.begin(), relevantEvents.end(),
-                                [](auto const& name) { return name == "all"; })) {
-                    this->allRelevant = true;
-                } else {
-                    this->names.insert(relevantEvents.begin(), relevantEvents.end());
+            RelevantEvents(std::initializer_list<std::string> init) {
+                insert(init.begin(), init.end());
             }
+
+            /*!
+             * Create relevant events from given event names in a range.
+             * If name 'all' occurs, all elements are stored as relevant.
+             *
+             * @param first Iterator pointing to the start of a range of names.
+             * @param last Iterator pointing to the end of a range of names.
+             */
+            template <typename ForwardIt>
+            RelevantEvents(ForwardIt first, ForwardIt last) {
+                insert(first, last);
             }
 
-            bool operator==(RelevantEvents const& rhs) {
+            bool operator==(RelevantEvents const& rhs) const {
                 return this->allRelevant == rhs.allRelevant || this->names == rhs.names;
             }
 
-            bool operator!=(RelevantEvents const& rhs) {
+            bool operator!=(RelevantEvents const& rhs) const {
                 return !(*this == rhs);
             }
 
             /*!
-             * Add relevant event names required by the labels in properties.
+             * Add relevant event names required by the labels in properties of a range.
              *
-             * @param properties List of properties. All events occurring in a property are relevant.
+             * @param first Iterator pointing to the start of a std::shared_ptr<storm::logic::Formula const> range.
+             * @param last Iterator pointing to the end of a std::shared_ptr<storm::logic::Formula const> range.
              */
-            void addNamesFromProperty(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties) {
+            template <typename ForwardIt>
+            void insertNamesFromProperties(ForwardIt first, ForwardIt last) {
                 if (this->allRelevant) {
                     return;
                 }
 
                 // Get necessary labels from properties
-                std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
-                for (auto property : properties) {
+                std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels{};
+                std::for_each(first, last, [&atomicLabels](auto const& property){
                         property->gatherAtomicLabelFormulas(atomicLabels);
-                }
+                        });
 
                 // Add relevant event names from properties
-                for (auto atomic : atomicLabels) {
+                for (auto const& atomic : atomicLabels) {
                     std::string label = atomic->getLabel();
                     if (label == "failed" or label == "skipped") {
                         // Ignore as these label will always be added if necessary
@@ -63,10 +82,10 @@ namespace storm {
                         // Get name of event
                         if (boost::ends_with(label, "_failed")) {
                             // length of "_failed" = 7
-                            this->addEvent(label.substr(0, label.size() - 7));
+                            this->names.insert(label.substr(0, label.size() - 7));
                         } else if (boost::ends_with(label, "_dc")) {
                             // length of "_dc" = 3
-                            this->addEvent(label.substr(0, label.size() - 3));
+                            this->names.insert(label.substr(0, label.size() - 3));
                         } else if (label.find("_claimed_") != std::string::npos) {
                             STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming.");
                         } else {
@@ -76,6 +95,36 @@ namespace storm {
                 }
             }
 
+            /*!
+             * Add relevant event.
+             * If name 'all' occurs, all elements are stored as relevant.
+             *
+             * @param name Name of relevant event.
+             */
+            void insert(std::string const& name) {
+                if(name == "all") {
+                    setAllRelevant();
+                }
+                names.insert(name);
+            }
+
+            /*!
+             * Add relevant event names from a range.
+             * If name 'all' occurs, all elements are stored as relevant.
+             *
+             * @param first Iterator pointing to the start of a range of names.
+             * @param last Iterator pointing to the end of a range of names.
+             */
+            template <typename ForwardIt>
+            void insert(ForwardIt first, ForwardIt last) {
+                // check if the name "all" occurs
+                if (std::any_of(first, last, [](auto const& name) { return name == "all"; })) {
+                    setAllRelevant();
+                } else {
+                    this->names.insert(first, last);
+                }
+            }
+
             /*!
              * Check that the relevant names correspond to existing elements in the DFT.
              *
@@ -103,15 +152,26 @@ namespace storm {
                 }
             }
 
-        private:
-
             /*!
-             * Add relevant event.
+             * Merge the given RelevantEvents with *this
              *
-             * @param name Name of relevant event.
+             * @return A reference to *this, allowing chaining i.e. e.merge(a).merge(b)
              */
-            void addEvent(std::string const& name) {
-                names.insert(name);
+            RelevantEvents& merge(RelevantEvents const &other) {
+                if (!this->allRelevant) {
+                    if(other.allRelevant) {
+                        setAllRelevant();
+                    } else {
+                        this->names.insert(other.names.begin(), other.names.end());
+                    }
+                }
+                return *this;
+            }
+
+        private:
+            void setAllRelevant() {
+                this->allRelevant = true;
+                this->names.clear();
             }
 
             // Names of relevant events.

src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp

@@ -140,7 +140,7 @@ namespace storm {
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(env, *this->currentCheckTask);
+                result = modelChecker.check(env, *this->currentCheckTask);
                 storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                 hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));

src/storm-parsers/parser/PrismParser.cpp

@@ -151,7 +151,13 @@ namespace storm {
             booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
             booleanVariableDefinition.name("boolean variable definition");
 
-            integerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
+            boundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
+            boundedIntegerVariableDefinition.name("bounded integer variable definition");
+
+            unboundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("int")) > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, storm::expressions::Expression(), storm::expressions::Expression(), qi::_a)];
+            unboundedIntegerVariableDefinition.name("unbounded integer variable definition");
+
+            integerVariableDefinition = boundedIntegerVariableDefinition | unboundedIntegerVariableDefinition;
             integerVariableDefinition.name("integer variable definition");
 
             clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)];

src/storm-parsers/parser/PrismParser.h

@@ -243,8 +243,6 @@ namespace storm {
 
             // Rules for global variable definitions.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalVariableDefinition;
-            qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalBooleanVariableDefinition;
-            qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition;
 
             // Rules for modules definition.
             qi::rule<Iterator, std::string(), Skipper> knownModuleName;
@@ -257,6 +255,8 @@ namespace storm {
             qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition;
             qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
             qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
+            qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> boundedIntegerVariableDefinition;
+            qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> unboundedIntegerVariableDefinition;
             qi::rule<Iterator, storm::prism::ClockVariable(), qi::locals<storm::expressions::Expression>, Skipper> clockVariableDefinition;
 
             // Rules for command definitions.

src/storm/builder/DdPrismModelBuilder.cpp

@@ -541,7 +541,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         bool DdPrismModelBuilder<Type, ValueType>::canHandle(storm::prism::Program const& program) {
-            return program.getModelType() != storm::prism::Program::ModelType::PTA;
+            return !program.hasUnboundedVariables() && (program.getModelType() != storm::prism::Program::ModelType::PTA);
         }
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -1311,6 +1311,7 @@ namespace storm {
                 stream << ".";
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
             }
+            STORM_LOG_THROW(!program.hasUnboundedVariables(), storm::exceptions::InvalidArgumentException, "Program contains unbounded variables which is not supported by the DD engine.");
             
             STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl);
             

src/storm/builder/TerminalStatesGetter.cpp

@@ -26,7 +26,7 @@ namespace storm {
                 } else if (left.isAtomicLabelFormula()) {
                     terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false);
                 }
-            } else if (formula.isBoundedUntilFormula()) {
+            } else if (formula.isBoundedUntilFormula() && !formula.asBoundedUntilFormula().hasMultiDimensionalSubformulas()) {
                 storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula();
                 bool hasLowerBound = false;
                 for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) {

src/storm/generator/JaniNextStateGenerator.cpp

@@ -98,10 +98,9 @@ namespace storm {
             if (this->options.hasTerminalStates()) {
                 for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
                     if (expressionOrLabelAndBool.first.isExpression()) {
-                        this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
+                        this->terminalStates.emplace_back(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second);
                     } else {
-                        // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression
-                        // for the label so we can cut off the exploration there.
+                        // If it's a label, i.e. refers to a transient boolean variable we do some sanity checks first
                         if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") {
                             STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             
@@ -109,7 +108,7 @@ namespace storm {
                             STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             
-                            this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata), expressionOrLabelAndBool.second));
+                            this->terminalStates.emplace_back(variable.getExpressionVariable().getExpression(), expressionOrLabelAndBool.second);
                         }
                     }
                 }
@@ -550,6 +549,8 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
+            // The evaluator should have the default values of the transient variables right now.
+            
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
             
@@ -561,18 +562,22 @@ namespace storm {
             auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator);
             transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
             result.addStateRewards(evaluateRewardExpressions());
-            this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
-
 
             // If a terminal expression was set and we must not expand this state, return now.
+            // Terminal state expressions do not consider transient variables.
             if (!this->terminalStates.empty()) {
                 for (auto const& expressionBool : this->terminalStates) {
                     if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
+                        // Set back transient variables to default values so we are ready to process the next state
+                        this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
                         return result;
                     }
                 }
             }
             
+            // Set back transient variables to default values so we are ready to process the transition assignments
+            this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
+            
             // Get all choices for the state.
             result.setExpanded();
             std::vector<Choice<ValueType>> allChoices;

src/storm/generator/PrismNextStateGenerator.cpp

@@ -33,7 +33,7 @@ namespace storm {
 
             // Only after checking validity of the program, we initialize the variable information.
             this->checkValid();
-            this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet());
+            this->variableInformation = VariableInformation(program, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet());
 
             // Create a proper evalator.
             this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());

src/storm/generator/VariableInformation.cpp

@@ -34,7 +34,47 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) {
+        /*!
+         * Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range
+         * @pre If has[Lower,Upper]Bound is true, [lower,upper]Bound must be set to the corresponding bound.
+         * @post lowerBound and upperBound are set to the considered bound for this variable
+         * @param hasLowerBound shall be true iff there is a lower bound given
+         * @param lowerBound a reference to the lower bound value
+         * @param hasUpperBound shall be true iff there is an upper bound given
+         * @param upperBound a reference to the upper bound
+         * @param reservedBitsForUnboundedVariables the number of bits that shall be used to represent unbounded variables
+         * @return the number of bits required to represent the final variable range
+         */
+        uint64_t getBitWidthLowerUpperBound(bool const& hasLowerBound, int64_t& lowerBound, bool const& hasUpperBound, int64_t& upperBound, uint64_t  const& reservedBitsForUnboundedVariables) {
+            if (hasLowerBound) {
+                if (hasUpperBound) {
+                    STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound");
+                    // We do not have to set any bounds in this case.
+                    // Return the number of bits required to store all the values between lower and upper bound
+                    return static_cast<uint64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+                } else {
+                    // We only have a lower bound. Find the largest upper bound we can store with the given number of bits.
+                    upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1);
+                }
+            } else {
+                if (hasUpperBound) {
+                    // We only have an upper bound. Find the smallest lower bound we can store with the given number of bits
+                    lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1);
+                } else {
+                    // We neither have a lower nor an upper bound. Take the usual n-bit integer values for lower/upper bounds
+                    lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); // = -2^(reservedBits-1)
+                    upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; // = 2^(reservedBits-1) - 1
+                }
+            }
+            // If we reach this point, it means that the variable is unbounded.
+            // Lets check for potential overflows.
+            STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound. Has there been an integer over-/underflow?");
+            // By choice of the lower/upper bound, the number of reserved bits must coincide with the bitwidth
+            STORM_LOG_ASSERT(reservedBitsForUnboundedVariables == static_cast<uint64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))), "Unexpected bitwidth for unbounded variable.");
+            return reservedBitsForUnboundedVariables;
+        }
+        
+        VariableInformation::VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) {
             if (outOfBoundsState) {
                 outOfBoundsBit = 0;
                 ++totalBitOffset;
@@ -47,11 +87,15 @@ namespace storm {
                 ++totalBitOffset;
             }
             for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
-                int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
-                int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
-                STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound");
-                uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable());
+                int64_t lowerBound, upperBound;
+                if (integerVariable.hasLowerBoundExpression()) {
+                    lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
+                }
+                if (integerVariable.hasUpperBoundExpression()) {
+                    upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
+                }
+                uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables);
+                integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression());
                 totalBitOffset += bitwidth;
             }
             for (auto const& module : program.getModules()) {
@@ -60,11 +104,15 @@ namespace storm {
                     ++totalBitOffset;
                 }
                 for (auto const& integerVariable : module.getIntegerVariables()) {
-                    int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
-                    int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
-                    STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound");
-                    uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable());
+                    int64_t lowerBound, upperBound;
+                    if (integerVariable.hasLowerBoundExpression()) {
+                        lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
+                    }
+                    if (integerVariable.hasUpperBoundExpression()) {
+                        upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
+                    }
+                    uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables);
+                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression());
                     totalBitOffset += bitwidth;
                 }
             }
@@ -81,22 +129,6 @@ namespace storm {
             for (auto const& automaton : model.getAutomata()) {
                 STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
             }
-//            
-//            for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
-//                if (!variable.isTransient()) {
-//                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true);
-//                    ++totalBitOffset;
-//                }
-//            }
-//            for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
-//                if (!variable.isTransient()) {
-//                    int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
-//                    int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
-//                    uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-//                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true);
-//                    totalBitOffset += bitwidth;
-//                }
-//            }
 
             if (outOfBoundsState) {
                 outOfBoundsBit = 0;
@@ -181,30 +213,24 @@ namespace storm {
             }
             for (auto const& variable : variableSet.getBoundedIntegerVariables()) {
                 if (!variable.isTransient()) {
-                    int64_t lowerBound;
-                    int64_t upperBound;
+                    int64_t lowerBound, upperBound;
+                    STORM_LOG_ASSERT(variable.hasLowerBound() || variable.hasUpperBound(), "Bounded integer variable has neither a lower nor an upper bound.");
                     if (variable.hasLowerBound()) {
                         lowerBound = variable.getLowerBound().evaluateAsInt();
-                        if (variable.hasUpperBound()) {
-                            upperBound = variable.getUpperBound().evaluateAsInt();
-                        } else {
-                            upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1);
                     }
-                    } else {
-                        STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound.");
+                    if (variable.hasUpperBound()) {
                         upperBound = variable.getUpperBound().evaluateAsInt();
-                        lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1);
                     }
-                    uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+                    uint64_t bitwidth = getBitWidthLowerUpperBound(variable.hasLowerBound(), lowerBound, variable.hasUpperBound(), upperBound, reservedBitsForUnboundedVariables);
                     integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, !variable.hasLowerBound() || !variable.hasUpperBound());
                     totalBitOffset += bitwidth;
                 }
             }
             for (auto const& variable : variableSet.getUnboundedIntegerVariables()) {
                 if (!variable.isTransient()) {
-                    int64_t lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1));
-                    int64_t upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1;
-                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true, true);
+                    int64_t lowerBound, upperBound;
+                    uint64_t bitwidth = getBitWidthLowerUpperBound(false, lowerBound, false, upperBound, reservedBitsForUnboundedVariables);
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, true);
                     totalBitOffset += reservedBitsForUnboundedVariables;
                 }
             }

src/storm/generator/VariableInformation.h

@@ -98,7 +98,7 @@ namespace storm {
         
         // A structure storing information about the used variables of the program.
         struct VariableInformation {
-            VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false);
+            VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState = false);
             VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState);
             
             VariableInformation() = default;

src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp

@@ -92,7 +92,7 @@ namespace storm {
 
                 bool CostLimitClosure::containsUpwardClosure(CostLimits const& costLimits) const {
                     CostLimits infinityProjection(costLimits);
-                    for (auto const& dim : downwardDimensions) {
+                    for (auto dim : downwardDimensions) {
                         infinityProjection[dim] = CostLimit::infinity();
                     }
                     return contains(infinityProjection);
@@ -104,7 +104,7 @@ namespace storm {
                 
                 bool CostLimitClosure::full() const {
                     CostLimits p(dimension(), CostLimit(0));
-                    for (auto const& dim : downwardDimensions) {
+                    for (auto dim : downwardDimensions) {
                         p[dim] = CostLimit::infinity();
                     }
                     return contains(p);

src/storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.cpp

@@ -61,12 +61,12 @@ namespace storm {
                     STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count.");
                     STORM_LOG_ASSERT(dimensions.size() == dimensionCount, "Invalid size of given bitset.");
                     if (value) {
-                        for (auto const& d : dimensions) {
+                        for (auto d : dimensions) {
                             STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'relevant'-memory state but the dimension is assumed to have no memory.");
                             state |= (dimensionBitMask << d);
                         }
                     } else {
-                        for (auto const& d : dimensions) {
+                        for (auto d : dimensions) {
                             STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'unrelevant'-memory state but the dimension is assumed to have no memory.");
                             state &= ~(dimensionBitMask << d);
                         }

src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp

@@ -215,7 +215,7 @@ namespace storm {
             
             if (this->isResultForAllStates()) {
                 map_type newMap;
-                for (auto const& element : filterTruthValues) {
+                for (auto element : filterTruthValues) {
                     newMap.emplace(element, this->getTruthValuesVector().get(element));
                 }
                 this->truthValues = newMap;

src/storm/solver/AbstractEquationSolver.cpp

@@ -126,6 +126,21 @@ namespace storm {
             return lowerBound.get();
         }
 
+        template<typename ValueType>
+        ValueType const& AbstractEquationSolver<ValueType>::getLowerBound(uint64_t const& index) const {
+            if (lowerBounds) {
+                STORM_LOG_ASSERT(index < lowerBounds->size(), "Invalid row index " << index << " for vector of size " << lowerBounds->size());
+                if (lowerBound) {
+                    return std::max(lowerBound.get(), lowerBounds.get()[index]);
+                } else {
+                    return lowerBounds.get()[index];
+                }
+            } else {
+                STORM_LOG_ASSERT(lowerBound, "Lower bound requested but was not specified before.");
+                return lowerBound.get();
+            }
+        }
+
         template<typename ValueType>
         ValueType AbstractEquationSolver<ValueType>::getLowerBound(bool convertLocalBounds) const {
             if (lowerBound) {
@@ -142,6 +157,21 @@ namespace storm {
             return upperBound.get();
         }
 
+        template<typename ValueType>
+        ValueType const& AbstractEquationSolver<ValueType>::getUpperBound(uint64_t const& index) const {
+            if (upperBounds) {
+                STORM_LOG_ASSERT(index < upperBounds->size(), "Invalid row index " << index << " for vector of size " << upperBounds->size());
+                if (upperBound) {
+                    return std::min(upperBound.get(), upperBounds.get()[index]);
+                } else {
+                    return upperBounds.get()[index];
+                }
+            } else {
+                STORM_LOG_ASSERT(upperBound, "Upper bound requested but was not specified before.");
+                return upperBound.get();
+            }
+        }
+
         template<typename ValueType>
         ValueType AbstractEquationSolver<ValueType>::getUpperBound(bool convertLocalBounds) const {
             if (upperBound) {

src/storm/solver/AbstractEquationSolver.h

@@ -100,6 +100,13 @@ namespace storm {
              */
             ValueType const& getLowerBound() const;
             
+            /*!
+             * Retrieves the lower bound for the variable with the given index (if there is any lower bound).
+             * @pre some lower bound (local or global) has been specified
+             * @return the largest lower bound known for the given row
+             */
+            ValueType const& getLowerBound(uint64_t const& index) const;
+            
             /*!
              * Retrieves the lower bound (if there is any).
              * If the given flag is true and if there are only local bounds,
@@ -112,6 +119,13 @@ namespace storm {
              */
             ValueType const& getUpperBound() const;
             
+            /*!
+             * Retrieves the upper bound for the variable with the given index (if there is any upper bound).
+             * @pre some upper bound (local or global) has been specified
+             * @return the smallest upper bound known for the given row
+             */
+            ValueType const& getUpperBound(uint64_t const& index) const;
+            
            /*!
              * Retrieves the upper bound (if there is any).
              * If the given flag is true and if there are only local bounds,

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -3,6 +3,8 @@
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/macros.h"
+#include "storm/storage/expressions/VariableExpression.h"
+#include "storm/storage/expressions/RationalLiteralExpression.h"
 #include "storm/exceptions/InvalidEnvironmentException.h"
 #include "storm/exceptions/UnexpectedException.h"
 
@@ -31,23 +33,30 @@ namespace storm {
 
             // Set up the LP solver
             std::unique_ptr<storm::solver::LpSolver<ValueType>> solver = lpSolverFactory->create("");
-            solver->setOptimizationDirection(invert(dir));
 
             // Create a variable for each row group
-            std::vector<storm::expressions::Variable> variables;
-            variables.reserve(this->A->getRowGroupCount());
+            std::vector<storm::expressions::Expression> variableExpressions;
+            variableExpressions.reserve(this->A->getRowGroupCount());
             for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
-                if (this->lowerBound) {
-                    if (this->upperBound) {
-                        variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one<ValueType>()));
+                if (this->hasLowerBound()) {
+                    ValueType lowerBound = this->getLowerBound(rowGroup);
+                    if (this->hasUpperBound()) {
+                        ValueType upperBound = this->getUpperBound(rowGroup);
+                        if (lowerBound == upperBound) {
+                            // Some solvers (like glpk) don't support variables with bounds [x,x]. We therefore just use a constant instead. This should be more efficient anyways.
+                            variableExpressions.push_back(solver->getConstant(lowerBound));
+                        } else {
+                            STORM_LOG_ASSERT(lowerBound <= upperBound, "Lower Bound at row group " << rowGroup << " is " << lowerBound << " which exceeds the upper bound " << upperBound << ".");
+                            variableExpressions.emplace_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), lowerBound, upperBound, storm::utility::one<ValueType>()));
+                        }
                     } else {
-                        variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one<ValueType>()));
+                        variableExpressions.emplace_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), lowerBound, storm::utility::one<ValueType>()));
                     }
                 } else {
                     if (this->upperBound) {
-                        variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one<ValueType>()));
+                        variableExpressions.emplace_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->getUpperBound(rowGroup), storm::utility::one<ValueType>()));
                     } else {
-                        variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one<ValueType>()));
+                        variableExpressions.emplace_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one<ValueType>()));
                     }
                 }
             }
@@ -55,15 +64,19 @@ namespace storm {
             
             // Add a constraint for each row
             for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
-                for (uint64_t row = this->A->getRowGroupIndices()[rowGroup]; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row) {
-                    storm::expressions::Expression rowConstraint = solver->getConstant(b[row]);
-                    for (auto const& entry : this->A->getRow(row)) {
-                        rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression());
-                    }
+                for (uint64_t rowIndex = this->A->getRowGroupIndices()[rowGroup]; rowIndex < this->A->getRowGroupIndices()[rowGroup + 1]; ++rowIndex) {
+                    auto row = this->A->getRow(rowIndex);
+                    std::vector<storm::expressions::Expression> summands;
+                    summands.reserve(1+row.getNumberOfEntries());
+                    summands.push_back(solver->getConstant(b[rowIndex]));
+                    for (auto const& entry : row) {
+                        summands.push_back(solver->getConstant(entry.getValue()) * variableExpressions[entry.getColumn()]);
+                    }
+                    storm::expressions::Expression rowConstraint = storm::expressions::sum(summands);
                     if (minimize(dir)) {
-                        rowConstraint = variables[rowGroup].getExpression() <= rowConstraint;
+                        rowConstraint = variableExpressions[rowGroup] <= rowConstraint;
                     } else {
-                        rowConstraint = variables[rowGroup].getExpression() >= rowConstraint;
+                        rowConstraint = variableExpressions[rowGroup] >= rowConstraint;
                     }
                     solver->addConstraint("", rowConstraint);
                 }
@@ -76,11 +89,17 @@ namespace storm {
             STORM_LOG_THROW(solver->isOptimal(), storm::exceptions::UnexpectedException, "Unable to find optimal solution for MinMax equation system.");
             
             // write the solution into the solution vector
-            STORM_LOG_ASSERT(x.size() == variables.size(), "Dimension of x-vector does not match number of varibales.");
+            STORM_LOG_ASSERT(x.size() == variableExpressions.size(), "Dimension of x-vector does not match number of varibales.");
             auto xIt = x.begin();
-            auto vIt = variables.begin();
+            auto vIt = variableExpressions.begin();
             for (; xIt != x.end(); ++xIt, ++vIt) {
-                *xIt = solver->getContinuousValue(*vIt);
+                auto const& vBaseExpr = vIt->getBaseExpression();
+                if (vBaseExpr.isVariable()) {
+                    *xIt = solver->getContinuousValue(vBaseExpr.asVariableExpression().getVariable());
+                } else {
+                    STORM_LOG_ASSERT(vBaseExpr.isRationalLiteralExpression(), "Variable expression has unexpected type.");
+                    *xIt = storm::utility::convertNumber<ValueType>(vBaseExpr.asRationalLiteralExpression().getValue());
+                }
             }
             
             // If requested, we store the scheduler for retrieval.

src/storm/solver/TerminationCondition.cpp

@@ -69,7 +69,7 @@ namespace storm {
             
             if (useMinimum) {
                 if (this->strict) {
-                    for (auto const& pos : this->filter) {
+                    for (auto pos : this->filter) {
                         extremum = std::min(valueGetter(pos), extremum);
                         if (extremum <= this->threshold) {
                             cachedExtremumIndex = pos;
@@ -77,7 +77,7 @@ namespace storm {
                         }
                     }
                 } else {
-                    for (auto const& pos : this->filter) {
+                    for (auto pos : this->filter) {
                         extremum = std::min(valueGetter(pos), extremum);
                         if (extremum < this->threshold) {
                             cachedExtremumIndex = pos;
@@ -86,7 +86,7 @@ namespace storm {
                     }
                 }
             } else {
-                    for (auto const& pos : this->filter) {
+                    for (auto pos : this->filter) {
                     extremum = std::max(valueGetter(pos), extremum);
                 }
             }
@@ -118,12 +118,12 @@ namespace storm {
             }
             
             if (useMinimum) {
-                for (auto const& pos : this->filter) {
+                for (auto pos : this->filter) {
                     extremum = std::min(valueGetter(pos), extremum);
                 }
             } else {
                 if (this->strict) {
-                    for (auto const& pos : this->filter) {
+                    for (auto pos : this->filter) {
                         extremum = std::max(valueGetter(pos), extremum);
                         if (extremum >= this->threshold) {
                             cachedExtremumIndex = pos;
@@ -131,7 +131,7 @@ namespace storm {
                         }
                     }
                 } else {
-                    for (auto const& pos : this->filter) {
+                    for (auto pos : this->filter) {
                         extremum = std::max(valueGetter(pos), extremum);
                         if (extremum > this->threshold) {
                             cachedExtremumIndex = pos;

src/storm/storage/expressions/LinearCoefficientVisitor.cpp

@@ -42,8 +42,8 @@ namespace storm {
 
         LinearCoefficientVisitor::VariableCoefficients& LinearCoefficientVisitor::VariableCoefficients::operator/=(VariableCoefficients&& other) {
             STORM_LOG_THROW(other.variableToCoefficientMapping.size() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
-            for (auto const& otherVariableCoefficientPair : other.variableToCoefficientMapping) {
-                this->variableToCoefficientMapping[otherVariableCoefficientPair.first] /= other.constantPart;
+            for (auto& variableCoefficientPair : this->variableToCoefficientMapping) {
+                variableCoefficientPair.second /= other.constantPart;
             }
             constantPart /= other.constantPart;
             return *this;

src/storm/storage/expressions/SimpleValuation.cpp

@@ -122,7 +122,7 @@ namespace storm {
                 sstr << "[" << std::endl;
                 sstr << getManager() << std::endl;
                 if (!booleanValues.empty()) {
-                    for (auto const& element : booleanValues) {
+                    for (auto element : booleanValues) {
                         sstr << element << " ";
                     }
                     sstr << std::endl;

src/storm/storage/geometry/ReduceVertexCloud.cpp

@@ -115,7 +115,7 @@ namespace storm {
                     }
                     if (timeOut > )
 #endif
-                    if (timeOut > 0 && totalTime.getTimeInMilliseconds() > timeOut) {
+                    if (timeOut > 0 && static_cast<uint64_t>(totalTime.getTimeInMilliseconds()) > timeOut) {
                         for (uint64_t remainingPoint = pointIndex + 1; remainingPoint < input.size(); ++remainingPoint) {
                             vertices.set(remainingPoint);
                         }

src/storm/storage/jani/UnboundedIntegerVariable.cpp

@@ -19,5 +19,14 @@ namespace storm {
             return true;
         }
         
+        std::shared_ptr<UnboundedIntegerVariable> makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient) {
+            if (initValue) {
+                return std::make_shared<UnboundedIntegerVariable>(name, variable, initValue.get(), transient);
+            } else {
+                assert(!transient);
+                return std::make_shared<UnboundedIntegerVariable>(name, variable);
+            }
+        }
+        
     }
 }

src/storm/storage/jani/UnboundedIntegerVariable.h

@@ -21,5 +21,10 @@ namespace storm {
             virtual bool isUnboundedIntegerVariable() const override;
         };
         
+        /**
+        * Convenience function to call the appropriate constructor and return a shared pointer to the variable.
+        */
+        std::shared_ptr<UnboundedIntegerVariable> makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient);
+        
     }
 }

src/storm/storage/jani/VariableSet.cpp

@@ -214,7 +214,7 @@ namespace storm {
             std::shared_ptr<Variable> janiVar = std::move(vToVIt->second);
             variableToVariable.erase(vToVIt);
             
-            nameToVariable.erase(variable.getName());
+            nameToVariable.erase(janiVar->getName());
             eraseFromVariableVector(variables, variable);
             if (janiVar->isBooleanVariable()) {
                 eraseFromVariableVector(booleanVariables, variable);

src/storm/storage/prism/IntegerVariable.cpp

@@ -1,25 +1,53 @@
 #include "storm/storage/prism/IntegerVariable.h"
 
+#include "storm/storage/expressions/ExpressionManager.h"
+
 namespace storm {
     namespace prism {
         IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, observable, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
             // Intentionally left empty.
         }
         
+        bool IntegerVariable::hasLowerBoundExpression() const {
+            return this->lowerBoundExpression.isInitialized();
+        }
+        
         storm::expressions::Expression const& IntegerVariable::getLowerBoundExpression() const {
+            STORM_LOG_ASSERT(hasLowerBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from below.");
             return this->lowerBoundExpression;
         }
         
+        bool IntegerVariable::hasUpperBoundExpression() const {
+            return this->upperBoundExpression.isInitialized();
+        }
+
         storm::expressions::Expression const& IntegerVariable::getUpperBoundExpression() const {
+            STORM_LOG_ASSERT(hasUpperBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from above.");
             return this->upperBoundExpression;
         }
         
         storm::expressions::Expression IntegerVariable::getRangeExpression() const {
+            if (hasLowerBoundExpression()) {
+                if (hasUpperBoundExpression()) {
                     return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression();
+                } else {
+                    return this->getLowerBoundExpression() <= this->getExpressionVariable();
+                }
+            } else {
+                if (hasUpperBoundExpression()) {
+                    return this->getExpressionVariable() <= this->getUpperBoundExpression();
+                } else {
+                    return this->getExpressionVariable().getManager().boolean(true);
+                }
+            }
         }
         
         IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
+            return IntegerVariable(this->getExpressionVariable(),
+                                   this->hasLowerBoundExpression() ? this->getLowerBoundExpression().substitute(substitution) : storm::expressions::Expression(),
+                                   this->hasUpperBoundExpression() ? this->getUpperBoundExpression().substitute(substitution) : storm::expressions::Expression(),
+                                   this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(),
+                                   this->isObservable(), this->getFilename(), this->getLineNumber());
         }
 
         IntegerVariable IntegerVariable::substituteNonStandardPredicates() const {
@@ -28,12 +56,30 @@ namespace storm {
         
         void IntegerVariable::createMissingInitialValue() {
             if (!this->hasInitialValue()) {
+                if (this->hasLowerBoundExpression()) {
                     this->setInitialValueExpression(this->getLowerBoundExpression());
+                } else {
+                    this->setInitialValueExpression(this->getExpressionVariable().getManager().integer(0));
+                }
             }
         }
         
         std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
-            stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]";
+            stream << variable.getName() << ": ";
+            if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
+                // The syntax for the case where there is only one bound is not standardized, yet.
+                std::cout << "[";
+                if (variable.hasLowerBoundExpression()) {
+                    std::cout << variable.getLowerBoundExpression();
+                }
+                std::cout << "..";
+                if (variable.hasUpperBoundExpression()) {
+                    std::cout << variable.getUpperBoundExpression();
+                }
+                std::cout << "]";
+            } else {
+                std::cout << "int";
+            }
             if (variable.hasInitialValue()) {
                 stream << " init " << variable.getInitialValueExpression();
             }

src/storm/storage/prism/IntegerVariable.h

@@ -29,22 +29,35 @@ namespace storm {
              */
             IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
+            /*!
+             * @return true if a lower bound for this integer variable is defined
+             */
+            bool hasLowerBoundExpression() const;
+            
             /*!
              * Retrieves an expression defining the lower bound for this integer variable.
-             *
+             * @pre A lower bound for this integer variable is defined
              * @return An expression defining the lower bound for this integer variable.
              */
             storm::expressions::Expression const& getLowerBoundExpression() const;
 
+            /*!
+             * @return true if an upper bound for this integer variable is defined
+             */
+            bool hasUpperBoundExpression() const;
+
             /*!
              * Retrieves an expression defining the upper bound for this integer variable.
-             *
+             * @pre An upper bound for this integer variable is defined
              * @return An expression defining the upper bound for this integer variable.
              */
             storm::expressions::Expression const& getUpperBoundExpression() const;
 
+            
             /*!
              * Retrieves an expression characterizing the legal range of the variable.
+             * Only bounds that are defined will be considered in this expression.
+             * If neither a lower nor an upper bound is defined, this expression will be equivalent to true.
              *
              * @return An expression characterizing the legal range of the variable.
              */

src/storm/storage/prism/Module.cpp

@@ -15,6 +15,15 @@ namespace storm {
             this->createMappings();
         }
         
+        bool Module::hasUnboundedVariables() const {
+            for (auto const& integerVariable : this->integerVariables) {
+                if (!integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+
         std::size_t Module::getNumberOfBooleanVariables() const {
             return this->booleanVariables.size();
         }
@@ -74,8 +83,10 @@ namespace storm {
         std::vector<storm::expressions::Expression> Module::getAllRangeExpressions() const {
             std::vector<storm::expressions::Expression> result;
             for (auto const& integerVariable : this->integerVariables) {
+                if (integerVariable.hasLowerBoundExpression() || integerVariable.hasUpperBoundExpression()) {
                     result.push_back(integerVariable.getRangeExpression());
                 }
+            }
             return result;
         }
 
@@ -299,10 +310,10 @@ namespace storm {
                 if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
-                if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
-                if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
             }

src/storm/storage/prism/Module.h

@@ -57,6 +57,11 @@ namespace storm {
             Module(Module&& other) = default;
             Module& operator=(Module&& other) = default;
 
+            /*!
+             * @return True iff the module contains at least one variable with infinite domain
+             */
+            bool hasUnboundedVariables() const;
+            
             /*!
              * Retrieves the number of boolean variables in the module.
              *

src/storm/storage/prism/Program.cpp

@@ -225,6 +225,20 @@ namespace storm {
             return res;
         }
         
+        bool Program::hasUnboundedVariables() const {
+            for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
+                if (!globalIntegerVariable.hasLowerBoundExpression() || !globalIntegerVariable.hasUpperBoundExpression()) {
+                    return true;
+                }
+            }
+            for (auto const& module : modules) {
+                if (module.hasUnboundedVariables()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
         bool Program::hasUndefinedConstants() const {
             for (auto const& constant : this->getConstants()) {
                 if (!constant.isDefined()) {
@@ -271,10 +285,10 @@ namespace storm {
                         return false;
                     }
                 }
-                if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
-                if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
             }
@@ -454,8 +468,10 @@ namespace storm {
         std::vector<storm::expressions::Expression> Program::getAllRangeExpressions() const {
             std::vector<storm::expressions::Expression> result;
             for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
+                if (globalIntegerVariable.hasLowerBoundExpression() || globalIntegerVariable.hasUpperBoundExpression()) {
                     result.push_back(globalIntegerVariable.getRangeExpression());
                 }
+            }
 
             for (auto const& module : modules) {
                 std::vector<storm::expressions::Expression> moduleRangeExpressions = module.getAllRangeExpressions();
@@ -1157,6 +1173,7 @@ namespace storm {
             }
             for (auto const& variable : this->getGlobalIntegerVariables()) {
                 // Check that bound expressions of the range.
+                if (variable.hasLowerBoundExpression()) {
                     std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
                     std::set<storm::expressions::Variable> illegalVariables;
                     std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
@@ -1169,10 +1186,13 @@ namespace storm {
                         }
                         STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                     }
+                }
 
-                containedVariables = variable.getLowerBoundExpression().getVariables();
+                if (variable.hasUpperBoundExpression()) {
+                    std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
+                    std::set<storm::expressions::Variable> illegalVariables;
                     std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
-                isValid = illegalVariables.empty();
+                    bool isValid = illegalVariables.empty();
                     if (!isValid) {
                         std::vector<std::string> illegalVariableNames;
                         for (auto const& var : illegalVariables) {
@@ -1180,14 +1200,16 @@ namespace storm {
                         }
                         STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                     }
+                }
 
                 if (variable.hasInitialValue()) {
                     STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present.");
 
                     // Check the initial value of the variable.
-                    containedVariables = variable.getInitialValueExpression().getVariables();
+                    std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
+                    std::set<storm::expressions::Variable> illegalVariables;
                     std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
-                    isValid = illegalVariables.empty();
+                    bool isValid = illegalVariables.empty();
                     if (!isValid) {
                         std::vector<std::string> illegalVariableNames;
                         for (auto const& var : illegalVariables) {
@@ -1230,6 +1252,7 @@ namespace storm {
                 }
                 for (auto const& variable : module.getIntegerVariables()) {
                     // Check that bound expressions of the range.
+                    if (variable.hasLowerBoundExpression()) {
                         std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
                         std::set<storm::expressions::Variable> illegalVariables;
                         std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
@@ -1241,11 +1264,15 @@ namespace storm {
                             }
                             STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                         }
+                    }
+                    
+                    if (variable.hasUpperBoundExpression()) {
+                        std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
+                        std::set<storm::expressions::Variable> illegalVariables;
     
-                    containedVariables = variable.getLowerBoundExpression().getVariables();
                         illegalVariables.clear();
                         std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
-                    isValid = illegalVariables.empty();
+                        bool isValid = illegalVariables.empty();
                         if (!isValid) {
                             std::vector<std::string> illegalVariableNames;
                             for (auto const& var : illegalVariables) {
@@ -1253,15 +1280,17 @@ namespace storm {
                             }
                             STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
                         }
+                    }
 
                     if (variable.hasInitialValue()) {
                         STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present.");
 
                         // Check the initial value of the variable.
-                        containedVariables = variable.getInitialValueExpression().getVariables();
+                        std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
+                        std::set<storm::expressions::Variable> illegalVariables;
                         illegalVariables.clear();
                         std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
-                        isValid = illegalVariables.empty();
+                        bool isValid = illegalVariables.empty();
                         if (!isValid) {
                             std::vector<std::string> illegalVariableNames;
                             for (auto const& var : illegalVariables) {
@@ -1715,8 +1744,7 @@ namespace storm {
 
             // Assert the bounds of the global variables.
             for (auto const& variable : this->getGlobalIntegerVariables()) {
-                solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
-                solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
+                solver->add(variable.getRangeExpression());
             }
 
             // Make the global variables local, such that the resulting module covers all occurring variables. Note that
@@ -1734,8 +1762,7 @@ namespace storm {
                 allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
 
                 for (auto const& variable : module.getIntegerVariables()) {
-                    solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
-                    solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
+                    solver->add(variable.getRangeExpression());
                 }
 
                 if (module.hasInvariant()) {
@@ -2079,14 +2106,10 @@ namespace storm {
 
         void Program::createMissingInitialValues() {
             for (auto& variable : globalBooleanVariables) {
-                if (!variable.hasInitialValue()) {
-                    variable.setInitialValueExpression(manager->boolean(false));
-                }
+                variable.createMissingInitialValue();
             }
             for (auto& variable : globalIntegerVariables) {
-                if (!variable.hasInitialValue()) {
-                    variable.setInitialValueExpression(variable.getLowerBoundExpression());
-                }
+                variable.createMissingInitialValue();
             }
         }
 

src/storm/storage/prism/Program.h

@@ -93,6 +93,11 @@ namespace storm {
              */
             bool isPartiallyObservable() const;
 
+            /*!
+             * @return True iff the program contains at least one variable with infinite domain
+             */
+            bool hasUnboundedVariables() const;
+
             /*!
              * Retrieves whether there are undefined constants of any type in the program.
              *

src/storm/storage/prism/ToJaniConverter.cpp

@@ -129,11 +129,21 @@ namespace storm {
             
             // Add all global variables of the PRISM program to the JANI model.
             for (auto const& variable : program.getGlobalIntegerVariables()) {
-                if (variable.hasInitialValue()) {
-                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+                if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
+                    storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(),
+                                                                                                                  variable.getExpressionVariable(),
+                                                                                                                  variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
+                                                                                                                  false,
+                                                                                                                  variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none,
+                                                                                                                  variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none);
+                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newBoundedIntegerVariable);
                     variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
                 } else {
-                    storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+                    storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(),
+                                                                                                                  variable.getExpressionVariable(),
+                                                                                                                  variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
+                                                                                                                  false);
+                    storm::jani::UnboundedIntegerVariable const& createdVariable = janiModel.addVariable(newUnboundedIntegerVariable);
                     variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
                 }
             }
@@ -344,21 +354,35 @@ namespace storm {
 
                 storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix));
                 for (auto const& variable : module.getIntegerVariables()) {
-                    storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
                     auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
                     if (findRes != variablesToMakeGlobal.end()) {
                         bool makeVarGlobal = findRes->second;
-                        storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newIntegerVariable) : automaton.addVariable(newIntegerVariable);
+                        if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
+                            storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(),
+                                                                                                                          variable.getExpressionVariable(),
+                                                                                                                          variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
+                                                                                                                          false,
+                                                                                                                          variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none,
+                                                                                                                          variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none);
+                            storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBoundedIntegerVariable) : automaton.addVariable(newBoundedIntegerVariable);
+                            variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                        } else {
+                            storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(),
+                                                                                                                          variable.getExpressionVariable(),
+                                                                                                                          variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
+                                                                                                                          false);
+                            storm::jani::UnboundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newUnboundedIntegerVariable) : automaton.addVariable(newUnboundedIntegerVariable);
                             variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                        }
                     } else {
                         STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
                     }
                 }
                 for (auto const& variable : module.getBooleanVariables()) {
-                    storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
                     auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
                     if (findRes != variablesToMakeGlobal.end()) {
                         bool makeVarGlobal = findRes->second;
+                        storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
                         storm::jani::BooleanVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBooleanVariable) : automaton.addVariable(newBooleanVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
                     } else {

src/test/storm/builder/DdPrismModelBuilderTest.cpp

@@ -319,3 +319,14 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) {
     EXPECT_EQ(21ul, mdp->getNumberOfChoices());
 }
 
+TEST(UnboundedTest_Sylvan, Mdp) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
+    storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram();
+    EXPECT_FALSE(storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().canHandle(program));
+}
+
+TEST(UnboundedTest_Cudd, Mdp) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
+    storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram();
+    EXPECT_FALSE(storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().canHandle(program));
+}

src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp

@@ -94,6 +94,12 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
     model = storm::builder::ExplicitModelBuilder<double>(program).build();
     EXPECT_EQ(37ul, model->getNumberOfStates());
     EXPECT_EQ(59ul, model->getNumberOfTransitions());
+    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
+    program = modelDescription.preprocess("N=-7").asPrismProgram();
+    model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(9ul, model->getNumberOfStates());
+    EXPECT_EQ(9ul, model->getNumberOfTransitions());
 }
 
 TEST(ExplicitPrismModelBuilderTest, Ma) {
@@ -125,3 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, FailComposition) {
 
     STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);
 }
+
+TEST(ExplicitPrismModelBuilderTest, FailUnbounded) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
+    storm::prism::Program program = modelDescription.preprocess("N=7").asPrismProgram();
+    STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);
+}

src/test/storm/parser/PrismParserTest.cpp

@@ -28,6 +28,7 @@ TEST(PrismParser, SimpleTest) {
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
     EXPECT_EQ(1ul, result.getNumberOfModules());
     EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
+    EXPECT_FALSE(result.hasUnboundedVariables());
     
     testInput =
     R"(mdp
@@ -44,6 +45,7 @@ TEST(PrismParser, SimpleTest) {
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
     EXPECT_EQ(1ul, result.getNumberOfModules());
     EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
+    EXPECT_FALSE(result.hasUnboundedVariables());
 }
 
 TEST(PrismParser, ComplexTest) {
@@ -97,8 +99,23 @@ TEST(PrismParser, ComplexTest) {
     EXPECT_EQ(3ul, result.getNumberOfModules());
     EXPECT_EQ(2ul, result.getNumberOfRewardModels());
     EXPECT_EQ(1ul, result.getNumberOfLabels());
+    EXPECT_FALSE(result.hasUnboundedVariables());
 }
 
+TEST(PrismParser, UnboundedTest) {
+    std::string testInput =
+    R"(mdp
+    module main
+        b : int;
+        [a] true -> 1: (b'=b+1);
+    endmodule)";
+    
+    storm::prism::Program result;
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
+    EXPECT_EQ(1ul, result.getNumberOfModules());
+    EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
+    EXPECT_TRUE(result.hasUnboundedVariables());
+}
 
 TEST(PrismParser, POMDPInputTest) {
     std::string testInput =

src/test/storm/storage/PrismProgramTest.cpp

@@ -1,5 +1,5 @@
-#include "test/storm_gtest.h"
 #include "storm-config.h"
+#include "test/storm_gtest.h"
 #include "storm-parsers/parser/PrismParser.h"
 
 #include "storm/utility/solver.h"
@@ -163,4 +163,7 @@ TEST(PrismProgramTest, ConvertToJani) {
 
     ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"));
     ASSERT_NO_THROW(janiModel = prismProgram.toJani());
+
+    ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"));
+    ASSERT_NO_THROW(janiModel = prismProgram.toJani());
 }