From 5beb33e3d8f85050fc8ea011756597e770abb214 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 17 Aug 2015 19:58:43 +0200 Subject: [PATCH] merged a bit more Former-commit-id: e42dc212338e40fd63e7b6d5b25fba65cb8c749b --- .../csl/HybridCtmcCslModelChecker.cpp | 3 +++ .../SparseMarkovAutomatonCslModelChecker.cpp | 18 +++++++++--------- .../csl/helper/HybridCtmcCslHelper.cpp | 1 + .../csl/helper/SparseCtmcCslHelper.cpp | 3 +++ .../helper/SparseMarkovAutomatonCslHelper.cpp | 3 +++ .../prctl/helper/HybridDtmcPrctlHelper.cpp | 5 +++++ .../prctl/helper/HybridMdpPrctlHelper.cpp | 5 +++++ .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 1 + src/models/sparse/Model.cpp | 7 +++++-- 9 files changed, 35 insertions(+), 11 deletions(-) diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 413f34ac8..fa9865707 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -5,6 +5,9 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace modelchecker { template diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 4b47fd18f..0a7a95475 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -32,9 +32,9 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); - STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); @@ -43,7 +43,7 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -54,8 +54,8 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute reachability rewards in non-closed Markov automaton."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); @@ -64,8 +64,8 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverage(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); @@ -74,8 +74,8 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index ba43b4060..91088d214 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -3,6 +3,7 @@ #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddOdd.h" diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 013df87b4..8c90dd905 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -2,6 +2,9 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/utility/macros.h" diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 089a39c8a..54ccc5be0 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -5,6 +5,9 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/storage/MaximalEndComponentDecomposition.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 189a20006..8c80d83ae 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -1,5 +1,10 @@ #include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddOdd.h" + #include "src/utility/graph.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index c9e0ae290..b9425fa48 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -1,5 +1,10 @@ #include "src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddOdd.h" + #include "src/utility/graph.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 66c523331..b76056297 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h" #include "src/storage/dd/DdType.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddOdd.h" diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index f8d04654d..6f2da7268 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -1,9 +1,12 @@ #include "src/models/sparse/Model.h" +#include + #include "src/utility/vector.h" #include "src/adapters/CarlAdapter.h" #include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/IllegalFunctionCallException.h" namespace storm { namespace models { @@ -17,7 +20,7 @@ namespace storm { : ModelBase(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), choiceLabeling(optionalChoiceLabeling) { for (auto const& rewardModel : this->getRewardModels()) { - STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); } } @@ -30,7 +33,7 @@ namespace storm { : ModelBase(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), choiceLabeling(std::move(optionalChoiceLabeling)) { for (auto const& rewardModel : this->getRewardModels()) { - STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); } }