Merge remote-tracking branch 'origin/master' into symbolic_state_elimination

CMakeLists.txt

@@ -296,7 +296,7 @@ SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
 ##
 #############################################################
 if ("${CMAKE_GENERATOR}" STREQUAL "Xcode")
-	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++11")
+	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++14")
 	set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++")
 endif()
 

resources/3rdparty/exprtk/exprtk.hpp

@@ -99,7 +99,7 @@ namespace exprtk
             return (('a' <= c) && (c <= 'z')) ||
             (('A' <= c) && (c <= 'Z'))
 #ifdef MODIFICATION
-            || ('.' == c) || ('_' == c)
+            || ('_' == c)
 #endif
             ;
         }

src/storm/logic/BoundedUntilFormula.cpp

@@ -102,6 +102,24 @@ namespace storm {
             return static_cast<uint64_t>(bound);
         }
         
+        template <>
+        double BoundedUntilFormula::getNonStrictUpperBound() const {
+            double bound = getUpperBound<double>();
+            STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+            return bound;
+        }
+
+        template <>
+        uint64_t BoundedUntilFormula::getNonStrictUpperBound() const {
+            int_fast64_t bound = getUpperBound<uint64_t>();
+            if (isUpperBoundStrict()) {
+                STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+                return bound - 1;
+            } else {
+                return bound;
+            }
+        }
+        
         void BoundedUntilFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }

src/storm/logic/BoundedUntilFormula.h

@@ -41,6 +41,9 @@ namespace storm {
             template <typename ValueType>
             ValueType getUpperBound() const;
             
+            template <typename ValueType>
+            ValueType getNonStrictUpperBound() const;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/storm/logic/CumulativeRewardFormula.cpp

@@ -64,6 +64,24 @@ namespace storm {
             return value;
         }
         
+        template <>
+        double CumulativeRewardFormula::getNonStrictBound() const {
+            double bound = getBound<double>();
+            STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+            return bound;
+        }
+        
+        template <>
+        uint64_t CumulativeRewardFormula::getNonStrictBound() const {
+            int_fast64_t bound = getBound<uint64_t>();
+            if (isBoundStrict()) {
+                STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+                return bound - 1;
+            } else {
+                return bound;
+            }
+        }
+        
         void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }

src/storm/logic/CumulativeRewardFormula.h

@@ -35,6 +35,9 @@ namespace storm {
             template <typename ValueType>
             ValueType getBound() const;
             
+            template <typename ValueType>
+            ValueType getNonStrictBound() const;
+            
         private:
             static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
 

src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp

@@ -90,7 +90,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }
@@ -111,7 +111,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
 
             STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
-            return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards<DdType, ValueType>(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<double>(), *linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards<DdType, ValueType>(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<double>(), *linearEquationSolverFactory);
         }
         
         template<typename ModelType>

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -67,7 +67,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }
@@ -108,7 +108,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<double>(), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<double>(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
                 

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -61,7 +61,7 @@ namespace storm {
                 lowerBound = pathFormula.getLowerBound<double>();
             }
             if (pathFormula.hasUpperBound()) {
-                upperBound = pathFormula.getUpperBound<double>();
+                upperBound = pathFormula.getNonStrictUpperBound<double>();
             } else {
                 upperBound = storm::utility::infinity<double>();
             }

src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -76,14 +76,14 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>
         std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>

src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -95,7 +95,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>
@@ -103,7 +103,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ll), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -48,7 +48,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *linearEquationSolverFactory);
             std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             return result;
         }
@@ -86,7 +86,7 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -64,7 +64,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
@@ -125,7 +125,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         

src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -76,16 +76,16 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
-            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType, ValueType>>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(this->getModel().getReachableStates(), numericResult));
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
-            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType, ValueType>>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(this->getModel().getReachableStates(), numericResult));
         }
         
         template<typename ModelType>

src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp

@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>
@@ -84,7 +84,7 @@ namespace storm {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>

src/storm/parser/JaniParser.cpp

@@ -186,7 +186,7 @@ namespace storm {
                     return std::make_shared<storm::logic::AtomicLabelFormula>(propertyStructure.get<std::string>());
                 }
             }
-            storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true);
+            storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), true);
             if(expr.isInitialized()) {
                 assert(bound == boost::none);
                 return std::make_shared<storm::logic::AtomicExpressionFormula>(expr);

src/storm/parser/JaniParser.h

@@ -59,8 +59,8 @@ namespace storm {
              */
             void parseActions(json const& actionStructure, storm::jani::Model& parentModel);
             std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none);
-            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
-            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
+            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
+            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
 
             std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext,  std::string const& opstring, std::string const& context);
             std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context);
@@ -68,7 +68,7 @@ namespace storm {
                 
             
             std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
-            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
+            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>());
 
             
             /**

src/storm/parser/SpiritErrorHandler.h

@@ -19,7 +19,7 @@ namespace storm {
                 
                 std::stringstream stream;
                 stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl;
-                stream << "\t" << line << std::endl << "\t";
+                stream << "\t" << line << std::endl;
                 auto caretColumn = boost::spirit::get_column(lineStart, where);
                 stream << "\t" << std::string(caretColumn - 1, ' ') << "^" << std::endl;
                 

src/storm/transformer/SymbolicToSparseTransformer.cpp

@@ -5,7 +5,6 @@
 #include "storm/storage/dd/Bdd.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
-
 #include "storm/models/sparse/StandardRewardModel.h"
 
 namespace storm {
@@ -76,6 +75,37 @@ namespace storm {
             return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc) {
+            storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicCtmc.getRewardModels()) {
+                boost::optional<std::vector<ValueType>> stateRewards;
+                boost::optional<std::vector<ValueType>> stateActionRewards;
+                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
+                if (rewardModelNameAndModel.second.hasStateRewards()) {
+                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
+                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
+                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
+
+            labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicCtmc.getLabels()) {
+                labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
+        }
+
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
         
@@ -84,8 +114,11 @@ namespace storm {
         
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
-
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
 
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+
     }
 }

src/storm/transformer/SymbolicToSparseTransformer.h

@@ -2,9 +2,10 @@
 
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/symbolic/Dtmc.h"
-
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/symbolic/Ctmc.h"
 
 #include "storm/storage/dd/Odd.h"
 
@@ -27,5 +28,10 @@ namespace storm {
             static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
         };
         
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicCtmcToSparseCtmcTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc);
+        };
     }
 }

src/storm/utility/ModelInstantiator.cpp

@@ -40,16 +40,24 @@ namespace storm {
                 storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(parametricMatrix.getRowCount(),
                                                                                 parametricMatrix.getColumnCount(),
                                                                                 parametricMatrix.getEntryCount(),
-                                                                                true, // no force dimensions
-                                                                                true, //Custom row grouping
-                                                                                parametricMatrix.getRowGroupCount());
-                for(std::size_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){
-                    matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]);
-                    for(std::size_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row){
+                                                                                true,
+                                                                                !parametricMatrix.hasTrivialRowGrouping(),
+                                                                                parametricMatrix.hasTrivialRowGrouping() ? 0 : parametricMatrix.getRowGroupCount());
                 ConstantType dummyValue = storm::utility::one<ConstantType>();
+                if (parametricMatrix.hasTrivialRowGrouping()) {
+                    for (uint_fast64_t row = 0; row < parametricMatrix.getRowCount(); ++row) {
+                        for (auto const& paramEntry : parametricMatrix.getRow(row)) {
+                            matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue);
+                        }
+                    }
+                }
+                else {
+                    for(uint_fast64_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){
+                        matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]);
+                        for (uint_fast64_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row) {
                             for(auto const& paramEntry : parametricMatrix.getRow(row)){
                                 matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue);
-                            dummyValue = storm::utility::zero<ConstantType>();
+                            }
                         }
                     }
                 }
@@ -103,7 +111,6 @@ namespace storm {
                     ++parametricEntryIt;
                 }
                 STORM_LOG_ASSERT(constantEntryIt == constantMatrix.end(), "Parametric matrix seems to have more or less entries then the constant matrix");
-                //TODO: is this necessary?
                 constantMatrix.updateNonzeroEntryCount();
             }
             

src/storm/utility/graph.cpp

@@ -43,9 +43,9 @@ namespace storm {
                 std::vector<uint_fast64_t> remainingSteps;
                 if (useStepBound) {
                     stepStack.reserve(numberOfStates);
-                    stepStack.insert(stepStack.begin(), targetStates.getNumberOfSetBits(), maximalSteps);
+                    stepStack.insert(stepStack.begin(), initialStates.getNumberOfSetBits(), maximalSteps);
                     remainingSteps.resize(numberOfStates);
-                    for (auto state : targetStates) {
+                    for (auto state : initialStates) {
                         remainingSteps[state] = maximalSteps;
                     }
                 }
@@ -59,12 +59,16 @@ namespace storm {
                     if (useStepBound) {
                         currentStepBound = stepStack.back();
                         stepStack.pop_back();
+                        
+                        if (currentStepBound == 0) {
+                            continue;
+                        }
                     }
                 
                     for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
                         // Only explore the state if the transition was actually there and the successor has not yet
                         // been visited.
-                        if (successor.getValue() != storm::utility::zero<T>() && !reachableStates.get(successor.getColumn()) && (!useStepBound || remainingSteps[successor.getColumn()] < currentStepBound - 1)) {
+                        if (!storm::utility::isZero(successor.getValue()) && (!reachableStates.get(successor.getColumn()) || (useStepBound && remainingSteps[successor.getColumn()] < currentStepBound - 1))) {
                             // If the successor is one of the target states, we need to include it, but must not explore
                             // it further.
                             if (targetStates.get(successor.getColumn())) {
@@ -72,12 +76,9 @@ namespace storm {
                             } else if (constraintStates.get(successor.getColumn())) {
                                 // However, if the state is in the constrained set of states, we potentially need to follow it.
                                 if (useStepBound) {
+                                    // As there is at least one more step to go, we need to push the state and the new number of steps.
                                     remainingSteps[successor.getColumn()] = currentStepBound - 1;
                                     stepStack.push_back(currentStepBound - 1);
-                                    
-                                    if (currentStepBound == 0) {
-                                        continue;
-                                    }
                                 }
                                 reachableStates.set(successor.getColumn());
                                 stack.push_back(successor.getColumn());
@@ -168,20 +169,21 @@ namespace storm {
                     if (useStepBound) {
                         currentStepBound = stepStack.back();
                         stepStack.pop_back();
+                        if(currentStepBound == 0) {
+                            continue;
+                        }
+                        
                     }
                     
                     for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
-                        if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound))) {
+                        if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
                             statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
 
                             // If we don't have a bound on the number of steps to take, just add the state to the stack.
                             if (useStepBound) {
-                                // If there is at least one more step to go, we need to push the state and the new number of steps.
+                                // As there is at least one more step to go, we need to push the state and the new number of steps.
                                 remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
                                 stepStack.push_back(currentStepBound - 1);
-                                if (currentStepBound == 0) {
-                                    continue;
-                                }
                             }
                             stack.push_back(entryIt->getColumn());
                         }
@@ -458,19 +460,18 @@ namespace storm {
                     if (useStepBound) {
                         currentStepBound = stepStack.back();
                         stepStack.pop_back();
+                        if (currentStepBound == 0) {
+                            continue;
+                        }
                     }
                     
                     for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
-                        if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound))) {
+                        if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
                             // If we don't have a bound on the number of steps to take, just add the state to the stack.
                             if (useStepBound) {
                                 // If there is at least one more step to go, we need to push the state and the new number of steps.
                                 remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
                                 stepStack.push_back(currentStepBound - 1);
-                                
-                                if (currentStepBound == 0) {
-                                    continue;
-                                }
                             }
                             statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
                             stack.push_back(entryIt->getColumn());
@@ -602,10 +603,15 @@ namespace storm {
                     if (useStepBound) {
                         currentStepBound = stepStack.back();
                         stepStack.pop_back();
+                        if (currentStepBound == 0) {
+                            continue;
+                        }
                     }
                     
                     for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
-                        if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) && (!useStepBound || remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound))) {
+                        if (phiStates.get(predecessorEntryIt->getColumn())) {
+                            if (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn())) {
+                                
                                 // Check whether the predecessor has at least one successor in the current state set for every
                                 // nondeterministic choice.
                                 bool addToStatesWithProbabilityGreater0 = true;
@@ -631,14 +637,17 @@ namespace storm {
                                         // If there is at least one more step to go, we need to push the state and the new number of steps.
                                         remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1;
                                         stepStack.push_back(currentStepBound - 1);
-                                    
-                                    if (currentStepBound == 0) {
-                                        continue;
-                                    }
                                     }
                                     statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
                                     stack.push_back(predecessorEntryIt->getColumn());
                                 }
+                                
+                            } else if (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1) {
+                                // We have found a shorter path to the predecessor. Hence, we need to explore it again
+                                remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1;
+                                stepStack.push_back(currentStepBound - 1);
+                                stack.push_back(predecessorEntryIt->getColumn());
+                            }
                         }
                     }
                 }

src/storm/utility/shortestPaths.cpp

@@ -1,3 +1,4 @@
+#include <ostream>
 #include <queue>
 #include <set>
 #include <string>
@@ -373,6 +374,16 @@ namespace storm {
 
 
             template class ShortestPathsGenerator<double>;
+
+            // only prints the info stored in the Path struct;
+            // does not traverse the actual path (see printKShortestPath for that)
+            template <typename T>
+            std::ostream& operator<<(std::ostream& out, Path<T> const& p) {
+                out << "Path with predecessorNode: " << ((p.predecessorNode) ? std::to_string(p.predecessorNode.get()) : "None");
+                out << " predecessorK: " << p.predecessorK << " distance: " << p.distance;
+                return out;
+            }
+            template std::ostream& operator<<(std::ostream& out, Path<double> const& p);
         }
     }
 }

src/storm/utility/shortestPaths.h

@@ -55,6 +55,9 @@ namespace storm {
                 }
             };
 
+            template <typename T>
+            std::ostream& operator<<(std::ostream& out, Path<T> const& p);
+
             // when using the raw matrix/vector invocation, this enum parameter
             // forces the caller to declare whether the matrix has the evil I-P
             // format, which requires back-conversion of the entries