diff --git a/CMakeLists.txt b/CMakeLists.txt index 73be3c249..2f564a05f 100644 --- a/CMakeLists.txt +++ b/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() diff --git a/resources/3rdparty/exprtk/exprtk.hpp b/resources/3rdparty/exprtk/exprtk.hpp index 079ee1b6f..a86c45509 100755 --- a/resources/3rdparty/exprtk/exprtk.hpp +++ b/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 ; } diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 67ece142a..da7ac1862 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -102,6 +102,24 @@ namespace storm { return static_cast(bound); } + template <> + double BoundedUntilFormula::getNonStrictUpperBound() const { + double bound = getUpperBound(); + 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(); + 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."); } diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 862871796..5dc2a3889 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -40,6 +40,9 @@ namespace storm { template ValueType getUpperBound() const; + + template + ValueType getNonStrictUpperBound() const; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 05bf0353b..36c82856c 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -64,6 +64,24 @@ namespace storm { return value; } + template <> + double CumulativeRewardFormula::getNonStrictBound() const { + double bound = getBound(); + 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(); + 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."); } diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index ad9d5e3c0..fce825271 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -35,6 +35,9 @@ namespace storm { template ValueType getBound() const; + template + ValueType getNonStrictBound() const; + private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 18deaedc1..399b0ed46 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -90,7 +90,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } @@ -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(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 4d6e9407f..1f5c9ee0d 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -67,7 +67,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } @@ -108,7 +108,7 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask 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 numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 4aef07d8d..03789fe53 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -61,7 +61,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index facf38fbe..0cfc305d0 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -76,14 +76,14 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask 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::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index c773609af..93f538987 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -95,7 +95,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template @@ -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::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ll), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5bbf6cf23..229af5a8a 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -48,7 +48,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } @@ -86,7 +86,7 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask 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 numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 2a7f6d725..55f9c1fc6 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -64,7 +64,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(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 numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 9922c77d1..1be2991d9 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -76,16 +76,16 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); - return std::make_unique>(this->getModel().getReachableStates(), numericResult); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); + return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask 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 numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); - return std::make_unique>(this->getModel().getReachableStates(), numericResult); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); + return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 1eebe4842..436a55925 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template @@ -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::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index d743d9ced..4101359d3 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -186,7 +186,7 @@ namespace storm { return std::make_shared(propertyStructure.get()); } } - storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", std::unordered_map>(), true); if(expr.isInitialized()) { assert(bound == boost::none); return std::make_shared(expr); diff --git a/src/storm/parser/JaniParser.h b/src/storm/parser/JaniParser.h index 627a056dd..2ac6c8366 100644 --- a/src/storm/parser/JaniParser.h +++ b/src/storm/parser/JaniParser.h @@ -59,8 +59,8 @@ namespace storm { */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound = boost::none); - std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); std::vector> 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 parseComposition(json const& compositionStructure); - storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); + storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>()); /** diff --git a/src/storm/parser/SpiritErrorHandler.h b/src/storm/parser/SpiritErrorHandler.h index 53a73c9e3..34280e422 100644 --- a/src/storm/parser/SpiritErrorHandler.h +++ b/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; diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index b1d3813de..4670fda66 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/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>(transitionMatrix, labelling, rewardModels); } + template + std::shared_ptr> SymbolicCtmcToSparseCtmcTransformer::translate( + storm::models::symbolic::Ctmc const& symbolicCtmc) { + storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicCtmc.getRewardModels()) { + boost::optional> stateRewards; + boost::optional> stateActionRewards; + boost::optional> 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(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>(transitionMatrix, labelling, rewardModels); + } + template class SymbolicDtmcToSparseDtmcTransformer; template class SymbolicDtmcToSparseDtmcTransformer; @@ -84,8 +114,11 @@ namespace storm { template class SymbolicMdpToSparseMdpTransformer; template class SymbolicMdpToSparseMdpTransformer; - template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; + } } diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h index eb1f973d6..5f4bed6c4 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.h +++ b/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" @@ -26,6 +27,11 @@ namespace storm { public: static std::shared_ptr> translate(storm::models::symbolic::Mdp const& symbolicMdp); }; - + + template + class SymbolicCtmcToSparseCtmcTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Ctmc const& symbolicCtmc); + }; } } diff --git a/src/storm/utility/ModelInstantiator.cpp b/src/storm/utility/ModelInstantiator.cpp index df8dc025a..7b370274d 100644 --- a/src/storm/utility/ModelInstantiator.cpp +++ b/src/storm/utility/ModelInstantiator.cpp @@ -40,16 +40,24 @@ namespace storm { storm::storage::SparseMatrixBuilder 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){ - ConstantType dummyValue = storm::utility::one(); - for(auto const& paramEntry : parametricMatrix.getRow(row)){ + true, + !parametricMatrix.hasTrivialRowGrouping(), + parametricMatrix.hasTrivialRowGrouping() ? 0 : parametricMatrix.getRowGroupCount()); + ConstantType dummyValue = storm::utility::one(); + 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); - dummyValue = storm::utility::zero(); + } + } + } + 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); + } } } } @@ -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(); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index f64d46896..ef912c14e 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -43,9 +43,9 @@ namespace storm { std::vector 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() && !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::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::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,41 +603,49 @@ namespace storm { if (useStepBound) { currentStepBound = stepStack.back(); stepStack.pop_back(); + if (currentStepBound == 0) { + continue; + } } for(typename storm::storage::SparseMatrix::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))) { - // Check whether the predecessor has at least one successor in the current state set for every - // nondeterministic choice. - bool addToStatesWithProbabilityGreater0 = true; - for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { - bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) { - hasAtLeastOneSuccessorWithProbabilityGreater0 = true; + 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; + for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { + bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) { + hasAtLeastOneSuccessorWithProbabilityGreater0 = true; + break; + } + } + + if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { + addToStatesWithProbabilityGreater0 = false; break; } } - if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { - addToStatesWithProbabilityGreater0 = false; - break; - } - } - - // If we need to add the state, then actually add it and perform further search from the state. - if (addToStatesWithProbabilityGreater0) { - // 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[predecessorEntryIt->getColumn()] = currentStepBound - 1; - stepStack.push_back(currentStepBound - 1); - - if (currentStepBound == 0) { - continue; + // If we need to add the state, then actually add it and perform further search from the state. + if (addToStatesWithProbabilityGreater0) { + // 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[predecessorEntryIt->getColumn()] = currentStepBound - 1; + stepStack.push_back(currentStepBound - 1); } + statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); } - statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + + } 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()); } } diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index 19ba70983..c2f6a97b9 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -1,3 +1,4 @@ +#include #include #include #include @@ -373,6 +374,16 @@ namespace storm { template class ShortestPathsGenerator; + + // only prints the info stored in the Path struct; + // does not traverse the actual path (see printKShortestPath for that) + template + std::ostream& operator<<(std::ostream& out, Path 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 const& p); } } } diff --git a/src/storm/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h index 359a30c5e..ad344f1aa 100644 --- a/src/storm/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -55,6 +55,9 @@ namespace storm { } }; + template + std::ostream& operator<<(std::ostream& out, Path 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