From b7170b3c3b29962198d56f8cd5df4f6eda6ed7ca Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 Mar 2017 15:01:48 +0100 Subject: [PATCH 1/8] fixed two issues pointed out by Joachim Klein: spirit error message (superfluous tab) and wrong treatment of strict upper bounds in bounded until and cumulative reward properties --- src/storm/logic/BoundedUntilFormula.cpp | 18 ++++++++++++++++++ src/storm/logic/BoundedUntilFormula.h | 3 +++ src/storm/logic/CumulativeRewardFormula.cpp | 18 ++++++++++++++++++ src/storm/logic/CumulativeRewardFormula.h | 3 +++ .../csl/HybridCtmcCslModelChecker.cpp | 4 ++-- .../csl/SparseCtmcCslModelChecker.cpp | 4 ++-- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 4 ++-- .../prctl/HybridMdpPrctlModelChecker.cpp | 4 ++-- .../prctl/SparseDtmcPrctlModelChecker.cpp | 4 ++-- .../prctl/SparseMdpPrctlModelChecker.cpp | 4 ++-- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 4 ++-- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 4 ++-- src/storm/parser/SpiritErrorHandler.h | 2 +- 14 files changed, 60 insertions(+), 18 deletions(-) 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 fc221147b..f59273480 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -77,7 +77,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } @@ -98,7 +98,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 1936e60bd..ebbb34e99 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 d42de45dd..ff1785db4 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 c52307315..b7d163f62 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.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(); - 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); + 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)); } @@ -84,7 +84,7 @@ namespace storm { 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); + 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)); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 2ac26509a..e077fbb26 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/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; From ad3e99f55868831678403e294d310aab9527ca7a Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Mar 2017 10:51:35 +0100 Subject: [PATCH 2/8] Fixes in step bounded DFS implementations: A state should be reexplored whenever it is reached with a shorter path. Previously, it was not possible to explore a state multiple times. --- src/storm/utility/graph.cpp | 95 ++++++++++++++++++++----------------- 1 file changed, 52 insertions(+), 43 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 592167496..e5a873322 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()); } } From 95527421bf62775756b88924b1174da67401a8ba Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 17 Mar 2017 18:10:39 +0100 Subject: [PATCH 3/8] added missing parenthesis --- src/storm/utility/graph.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index e5a873322..8cdc78cd2 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -68,7 +68,7 @@ namespace storm { 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 (!storm::utility::isZero(successor.getValue()) && !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())) { From 82cc5867180c5ed92682e9e817ac84a463f0f8b8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 21 Mar 2017 17:35:52 +0100 Subject: [PATCH 4/8] fixed some issues related to assigning an initializer list to an unordered_map which causes problems on older platforms --- CMakeLists.txt | 2 +- src/storm/parser/JaniParser.cpp | 2 +- src/storm/parser/JaniParser.h | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 57e94b8b8..2f4aa6536 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -295,7 +295,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/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>()); /** From acd486f0f25f78b4999b4f641bccada948d37c81 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 21 Mar 2017 20:30:02 +0100 Subject: [PATCH 5/8] reverted a change in ExprTk: dots are no longer recognized as letters --- resources/3rdparty/exprtk/exprtk.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ; } From 44ab16d126f917f5fc9785e19d579dd0089ee466 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 24 Mar 2017 11:58:20 +0100 Subject: [PATCH 6/8] Added symbolicToSparse transformers for DTMCs and CTMCs --- .../SymbolicToSparseTransformer.cpp | 67 ++++++++++++++++++- .../transformer/SymbolicToSparseTransformer.h | 16 +++++ 2 files changed, 81 insertions(+), 2 deletions(-) diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index 5dfbd2b4a..9dcd7f1ea 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -5,12 +5,42 @@ #include "storm/storage/dd/Bdd.h" #include "storm/models/symbolic/StandardRewardModel.h" - #include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace transformer { + template + std::shared_ptr> SymbolicDtmcToSparseDtmcTransformer::translate( + storm::models::symbolic::Dtmc const& symbolicDtmc) { + storm::dd::Odd odd = symbolicDtmc.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicDtmc.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", symbolicDtmc.getInitialStates().toVector(odd)); + labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(odd)); + for(auto const& label : symbolicDtmc.getLabels()) { + labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(odd)); + } + return std::make_shared>(transitionMatrix, labelling, rewardModels); + } + template std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate( storm::models::symbolic::Mdp const& symbolicMdp) { @@ -40,11 +70,44 @@ namespace storm { labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd)); } 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; template class SymbolicMdpToSparseMdpTransformer; template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; } -} \ No newline at end of file +} diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h index 7ea46fff4..414d4454b 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.h +++ b/src/storm/transformer/SymbolicToSparseTransformer.h @@ -1,15 +1,31 @@ #pragma once +#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" namespace storm { namespace transformer { + template + class SymbolicDtmcToSparseDtmcTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Dtmc const& symbolicDtmc); + }; + template class SymbolicMdpToSparseMdpTransformer { 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); + }; } } From 457943351d31e315853a8e7dcabb762d9dbab750 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 30 Mar 2017 16:17:50 +0200 Subject: [PATCH 7/8] fixed matrix building in ModelInstantiator for deterministic models. Previously, a non-trivial row grouping was introduced. --- src/storm/utility/ModelInstantiator.cpp | 27 ++++++++++++++++--------- 1 file changed, 17 insertions(+), 10 deletions(-) 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(); } From ee510df4ec30b2c2e3f8b7fb22aa7abed7148216 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Fri, 17 Mar 2017 16:57:52 +0100 Subject: [PATCH 8/8] add Path stream print for debug / Python __str__ --- src/storm/utility/shortestPaths.cpp | 11 +++++++++++ src/storm/utility/shortestPaths.h | 3 +++ 2 files changed, 14 insertions(+) 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