diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 428584385..413f34ac8 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -1,19 +1,9 @@ #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" -#include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" -#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" - -#include "src/storage/dd/CuddOdd.h" -#include "src/utility/macros.h" -#include "src/utility/graph.h" +#include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" +#include "src/modelchecker/csl/helper/HybridCtmcCslHelper.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" - -#include "src/exceptions/InvalidStateException.h" -#include "src/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { @@ -31,12 +21,7 @@ namespace storm { bool HybridCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); } - - template - storm::dd::Add HybridCtmcCslModelChecker::computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { - return rateMatrix / exitRateVector; - } - + template std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -44,14 +29,15 @@ namespace storm { SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), HybridDtmcPrctlModelChecker::computeNextProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), subResult.getTruthValuesVector()))); + + return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); } template @@ -60,34 +46,11 @@ namespace storm { } template - storm::dd::Add HybridCtmcCslModelChecker::computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { - STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); - STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows."); - - // Cut all non-maybe rows/columns from the transition matrix. - storm::dd::Add uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); - - // Now perform the uniformization. - uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate); - storm::dd::Add diagonal = model.getRowColumnIdentity() * maybeStates.toAdd(); - storm::dd::Add diagonalOffset = diagonal; - diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate)); - uniformizedMatrix += diagonalOffset; - - return uniformizedMatrix; - } - - template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - boost::optional> modifiedStateRewardVector; - if (this->getModel().hasStateRewards()) { - modifiedStateRewardVector = this->getModel().getStateRewardVector() / this->getModel().getExitRateVector(); - } - - return HybridDtmcPrctlModelChecker::computeReachabilityRewardsHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); } template @@ -106,255 +69,17 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - return this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound); - } - - template - std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Add const& exitRates, bool qualitative, double lowerBound, double upperBound) const { - // If the time bounds are [0, inf], we rather call untimed reachability. - storm::utility::ConstantsComparator comparator; - if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { - return HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), phiStates, psiStates, qualitative, *this->linearEquationSolverFactory); - } - - // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0 - // or t' != inf. - - // If we identify the states that have probability 0 of reaching the target states, we can exclude them from the - // further computations. - storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix().notZero(), phiStates, psiStates); - STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0."); - storm::dd::Bdd statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 && !psiStates; - STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); - - if (!statesWithProbabilityGreater0NonPsi.isZero()) { - if (comparator.isZero(upperBound)) { - // In this case, the interval is of the form [0, 0]. - return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), psiStates.toAdd())); - } else { - if (comparator.isZero(lowerBound)) { - // In this case, the interval is of the form [0, t]. - // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. - - // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. - ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRates).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate); - - // Compute the vector that is to be added as a compensation for removing the absorbing states. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * this->getModel().getTransitionMatrix() * psiStates.swapVariables(this->getModel().getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(this->getModel().getColumnVariables()) / this->getModel().getManager().getConstant(uniformizationRate); - - // Create an ODD for the translation to an explicit representation. - storm::dd::Odd odd(statesWithProbabilityGreater0NonPsi); - - // Convert the symbolic parts to their explicit representation. - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - std::vector explicitB = b.template toVector(odd); - - // Finally compute the transient probabilities. - std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subresult = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, *this->linearEquationSolverFactory); - - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), - (psiStates || !statesWithProbabilityGreater0) && this->getModel().getReachableStates(), - psiStates.toAdd(), - statesWithProbabilityGreater0NonPsi, - odd, subresult)); - } else if (comparator.isInfinity(upperBound)) { - // In this case, the interval is of the form [t, inf] with t != 0. - - // Start by computing the (unbounded) reachability probabilities of reaching psi states while - // staying in phi states. - std::unique_ptr unboundedResult = HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), phiStates, psiStates, qualitative, *this->linearEquationSolverFactory); - - // Compute the set of relevant states. - storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; - - // Filter the unbounded result such that it only contains values for the relevant states. - unboundedResult->filter(SymbolicQualitativeCheckResult(this->getModel().getReachableStates(), relevantStates)); - - // Build an ODD for the relevant states. - storm::dd::Odd odd(relevantStates); - - std::vector result; - if (unboundedResult->isHybridQuantitativeCheckResult()) { - std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); - result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult().getValueVector()); - } else { - STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type."); - result = unboundedResult->asSymbolicQuantitativeCheckResult().getValueVector().template toVector(odd); - } - - // Determine the uniformization rate for the transient probability computation. - ValueType uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRates).getMax(); - - // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, relevantStates, uniformizationRate); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - - // Compute the transient probabilities. - result = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, *this->linearEquationSolverFactory); - - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, result)); - } else { - // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. - - if (lowerBound != upperBound) { - // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'. - - // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. - ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRates).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the (first) uniformized matrix. - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate); - - // Create the one-step vector. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * this->getModel().getTransitionMatrix() * psiStates.swapVariables(this->getModel().getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(this->getModel().getColumnVariables()) / this->getModel().getManager().getConstant(uniformizationRate); - - // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. - storm::dd::Odd odd = storm::dd::Odd(statesWithProbabilityGreater0NonPsi); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - std::vector explicitB = b.template toVector(odd); - - // Compute the transient probabilities. - std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subResult = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory); - - // Transform the explicit result to a hybrid check result, so we can easily convert it to - // a symbolic qualitative format. - HybridQuantitativeCheckResult hybridResult(this->getModel().getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && this->getModel().getReachableStates()), - psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult); - - // Compute the set of relevant states. - storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; - - // Filter the unbounded result such that it only contains values for the relevant states. - hybridResult.filter(SymbolicQualitativeCheckResult(this->getModel().getReachableStates(), relevantStates)); - - // Build an ODD for the relevant states. - odd = storm::dd::Odd(relevantStates); - - std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); - std::vector newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().getValueVector()); - - // Then compute the transient probabilities of being in such a state after t time units. For this, - // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. - uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRates).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // If the lower and upper bounds coincide, we have only determined the relevant states at this - // point, but we still need to construct the starting vector. - if (lowerBound == upperBound) { - odd = storm::dd::Odd(relevantStates); - newSubresult = psiStates.toAdd().template toVector(odd); - } - - // Finally, we compute the second set of transient probabilities. - uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, relevantStates, uniformizationRate); - explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - - newSubresult = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); - - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, newSubresult)); - } else { - // In this case, the interval is of the form [t, t] with t != 0, t != inf. - - // Build an ODD for the relevant states. - storm::dd::Odd odd = storm::dd::Odd(statesWithProbabilityGreater0); - - std::vector newSubresult = psiStates.toAdd().template toVector(odd); - - // Then compute the transient probabilities of being in such a state after t time units. For this, - // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. - ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.toAdd() * exitRates).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Finally, we compute the second set of transient probabilities. - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0, uniformizationRate); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - - newSubresult = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); - - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), !statesWithProbabilityGreater0 && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), statesWithProbabilityGreater0, odd, newSubresult)); - } - } - } - } else { - return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), psiStates.toAdd())); - } + return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, lowerBound, upperBound, *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - return this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound()); - } - - template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewardsHelper(double timeBound) const { - // Only compute the result if the model has a state-based reward this->getModel(). - STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - - // Create ODD for the translation. - storm::dd::Odd odd(this->getModel().getReachableStates()); - - // Initialize result to state rewards of the this->getModel(). - std::vector result = this->getModel().getStateRewardVector().template toVector(odd); - - // If the time-bound is not zero, we need to perform a transient analysis. - if (timeBound > 0) { - ValueType uniformizationRate = 1.02 * this->getModel().getExitRateVector().getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), this->getModel().getReachableStates(), uniformizationRate); - - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - result = SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, *this->linearEquationSolverFactory); - } - - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), odd, result)); + std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - return this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound()); - } - - template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewardsHelper(double timeBound) const { - // Only compute the result if the model has a state-based reward this->getModel(). - STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - - // If the time bound is zero, the result is the constant zero vector. - if (timeBound == 0) { - return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getAddZero())); - } - - // Otherwise, we need to perform some computations. - - // Start with the uniformization. - ValueType uniformizationRate = 1.02 * this->getModel().getExitRateVector().getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Create ODD for the translation. - storm::dd::Odd odd(this->getModel().getReachableStates()); - - // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), this->getModel().getReachableStates(), uniformizationRate); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - - // Then compute the state reward vector to use in the computation. - storm::dd::Add totalRewardVector = this->getModel().hasStateRewards() ? this->getModel().getStateRewardVector() : this->getModel().getManager().getAddZero(); - if (this->getModel().hasTransitionRewards()) { - totalRewardVector += (this->getModel().getTransitionMatrix() * this->getModel().getTransitionRewardMatrix()).sumAbstract(this->getModel().getColumnVariables()); - } - std::vector explicitTotalRewardVector = totalRewardVector.template toVector(odd); - - // Finally, compute the transient probabilities. - std::vector result = SparseCtmcCslHelper::template computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, *this->linearEquationSolverFactory); - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); + std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template @@ -362,16 +87,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add probabilityMatrix = this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - - // Create ODD for the translation. - storm::dd::Odd odd(this->getModel().getReachableStates()); - - storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); - std::vector explicitExitRateVector = this->getModel().getExitRateVector().template toVector(odd); - - std::vector result = SparseCtmcCslHelper::computeLongRunAverage(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), &explicitExitRateVector, qualitative, *this->linearEquationSolverFactory); - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverage(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); } // Explicitly instantiate the model checker. diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index b2a94d51e..a1f9cb6d4 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -2,9 +2,10 @@ #define STORM_MODELCHECKER_HYBRIDCTMCCSLMODELCHECKER_H_ #include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" + #include "src/models/symbolic/Ctmc.h" + #include "src/utility/solver.h" -#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -20,42 +21,15 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Ctmc const& getModel() const override; private: - /*! - * Converts the given rate-matrix into a time-abstract probability matrix. - * - * @param model The symbolic model. - * @param rateMatrix The rate matrix. - * @param exitRateVector The exit rate vector of the model. - * @return The probability matrix. - */ - static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); - - /*! - * Computes the matrix representing the transitions of the uniformized CTMC. - * - * @param model The symbolic model. - * @param transitionMatrix The matrix to uniformize. - * @param exitRateVector The exit rate vector. - * @param maybeStates The states that need to be considered. - * @param uniformizationRate The rate to be used for uniformization. - * @return The uniformized matrix. - */ - static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); - - // The methods that perform the actual checking. - std::unique_ptr computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Add const& exitRates, bool qualitative, double lowerBound, double upperBound) const; - std::unique_ptr computeInstantaneousRewardsHelper(double timeBound) const; - std::unique_ptr computeCumulativeRewardsHelper(double timeBound) const; - // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolverFactory; }; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 99c92ee85..fa7fb98b0 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -1,208 +1,46 @@ #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include -#include +#include "src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" -#include "src/storage/StronglyConnectedComponentDecomposition.h" - -#include "src/utility/constants.h" #include "src/utility/macros.h" -#include "src/utility/vector.h" -#include "src/utility/graph.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/solver/LpSolver.h" - #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" namespace storm { namespace modelchecker { - template - SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory) : model(model), MinMaxLinearEquationSolverFactory(std::move(MinMaxLinearEquationSolverFactory)) { + template + SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model, std::unique_ptr>&& minMaxLinearEquationSolverFactory) : SparsePropositionalModelChecker(model), minMaxLinearEquationSolverFactory(std::move(minMaxLinearEquationSolverFactory)) { // Intentionally left empty. } - template - SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model) : model(model), MinMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory()) { + template + SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model) : SparsePropositionalModelChecker(model), minMaxLinearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory()) { // Intentionally left empty. } - template - bool SparseMarkovAutomatonCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + template + bool SparseMarkovAutomatonCslModelChecker::canHandle(storm::logic::Formula const& formula) const { return formula.isCslStateFormula() || formula.isCslPathFormula() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula()); } - - template - void SparseMarkovAutomatonCslModelChecker::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory) { - // Start by computing four sparse matrices: - // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. - // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states. - // * a matrix aProbabilistic with all (non-discretized) transitions from probabilistic non-goal states to other probabilistic non-goal states. - // * a matrix aProbabilisticToMarkovian with all (non-discretized) transitions from probabilistic non-goal states to all Markovian non-goal states. - typename storm::storage::SparseMatrix aMarkovian = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, markovianNonGoalStates, true); - typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, probabilisticNonGoalStates); - typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates); - typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, markovianNonGoalStates); - - // The matrices with transitions from Markovian states need to be digitized. - // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. - uint_fast64_t rowIndex = 0; - for (auto state : markovianNonGoalStates) { - for (auto& element : aMarkovian.getRow(rowIndex)) { - ValueType eTerm = std::exp(-exitRates[state] * delta); - if (element.getColumn() == rowIndex) { - element.setValue((storm::utility::one() - eTerm) * element.getValue() + eTerm); - } else { - element.setValue((storm::utility::one() - eTerm) * element.getValue()); - } - } - ++rowIndex; - } - - // Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors. - rowIndex = 0; - for (auto state : markovianNonGoalStates) { - for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) { - element.setValue((1 - std::exp(-exitRates[state] * delta)) * element.getValue()); - } - ++rowIndex; - } - - // Initialize the two vectors that hold the variable one-step probabilities to all target states for probabilistic and Markovian (non-goal) states. - std::vector bProbabilistic(aProbabilistic.getRowCount()); - std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); - - // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); - std::vector bMarkovianFixed; - bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); - for (auto state : markovianNonGoalStates) { - bMarkovianFixed.push_back(storm::utility::zero()); - - for (auto& element : transitionMatrix.getRowGroup(state)) { - if (goalStates.get(element.getColumn())) { - bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); - } - } - } - - std::unique_ptr> solver = MinMaxLinearEquationSolverFactory.create(aProbabilistic); - - // Perform the actual value iteration - // * loop until the step bound has been reached - // * in the loop: - // * perform value iteration using A_PSwG, v_PS and the vector b where b = (A * 1_G)|PS + A_PStoMS * v_MS - // and 1_G being the characteristic vector for all goal states. - // * perform one timed-step using v_MS := A_MSwG * v_MS + A_MStoPS * v_PS + (A * 1_G)|MS - std::vector markovianNonGoalValuesSwap(markovianNonGoalValues); - std::vector multiplicationResultScratchMemory(aProbabilistic.getRowCount()); - std::vector aProbabilisticScratchMemory(probabilisticNonGoalValues.size()); - for (uint_fast64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { - // Start by (re-)computing bProbabilistic = bProbabilisticFixed + aProbabilisticToMarkovian * vMarkovian. - aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); - storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); - - // Now perform the inner value iteration for probabilistic states. - solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); - - // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. - aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); - storm::utility::vector::addVectors(bMarkovian, bMarkovianFixed, bMarkovian); - aMarkovian.multiplyWithVector(markovianNonGoalValues, markovianNonGoalValuesSwap); - std::swap(markovianNonGoalValues, markovianNonGoalValuesSwap); - storm::utility::vector::addVectors(markovianNonGoalValues, bMarkovian, markovianNonGoalValues); - } - - // After the loop, perform one more step of the value iteration for PS states. - aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); - storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); - solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); - } - template - std::vector SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) const { - // 'Unpack' the bounds to make them more easily accessible. - double lowerBound = boundsPair.first; - double upperBound = boundsPair.second; - - // Get some data fields for convenient access. - typename storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& exitRates = model.getExitRates(); - storm::storage::BitVector const& markovianStates = model.getMarkovianStates(); - - // (1) Compute the accuracy we need to achieve the required error bound. - ValueType maxExitRate = model.getMaximalExitRate(); - ValueType delta = (2 * storm::settings::generalSettings().getPrecision()) / (upperBound * maxExitRate * maxExitRate); - - // (2) Compute the number of steps we need to make for the interval. - uint_fast64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); - STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [" << lowerBound << ", " << upperBound << "]." << std::endl); - - // (3) Compute the non-goal states and initialize two vectors - // * vProbabilistic holds the probability values of probabilistic non-goal states. - // * vMarkovian holds the probability values of Markovian non-goal states. - storm::storage::BitVector const& markovianNonGoalStates = markovianStates & ~psiStates; - storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates; - std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); - std::vector vMarkovian(markovianNonGoalStates.getNumberOfSetBits()); - - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, *MinMaxLinearEquationSolverFactory); - - // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. - if (lowerBound != storm::utility::zero()) { - std::vector vAllProbabilistic((~markovianStates).getNumberOfSetBits()); - std::vector vAllMarkovian(markovianStates.getNumberOfSetBits()); - - // Create the starting value vectors for the next value iteration based on the results of the previous one. - storm::utility::vector::setVectorValues(vAllProbabilistic, psiStates % ~markovianStates, storm::utility::one()); - storm::utility::vector::setVectorValues(vAllProbabilistic, ~psiStates % ~markovianStates, vProbabilistic); - storm::utility::vector::setVectorValues(vAllMarkovian, psiStates % markovianStates, storm::utility::one()); - storm::utility::vector::setVectorValues(vAllMarkovian, ~psiStates % markovianStates, vMarkovian); - - // Compute the number of steps to reach the target interval. - numberOfSteps = static_cast(std::ceil(lowerBound / delta)); - STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); - - // Compute the bounded reachability for interval [0, b-a]. - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRates, markovianStates, storm::storage::BitVector(model.getNumberOfStates()), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, *MinMaxLinearEquationSolverFactory); - - // Create the result vector out of vAllProbabilistic and vAllMarkovian and return it. - std::vector result(model.getNumberOfStates()); - storm::utility::vector::setVectorValues(result, ~markovianStates, vAllProbabilistic); - storm::utility::vector::setVectorValues(result, markovianStates, vAllMarkovian); - - return result; - } else { - // Create the result vector out of 1_G, vProbabilistic and vMarkovian and return it. - std::vector result(model.getNumberOfStates()); - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - storm::utility::vector::setVectorValues(result, probabilisticNonGoalStates, vProbabilistic); - storm::utility::vector::setVectorValues(result, markovianNonGoalStates, vMarkovian); - return result; - } - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + 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(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "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(); + return storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds()); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds()))); return result; } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { - return storm::modelchecker::SparseMdpPrctlModelChecker::computeUntilProbabilitiesHelper(minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, *MinMaxLinearEquationSolverFactory, qualitative); - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + + 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."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -210,366 +48,34 @@ namespace storm { ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative))); } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { - std::vector totalRewardVector; - if (model.hasTransitionRewards()) { - totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix()); - if (model.hasStateRewards()) { - storm::utility::vector::addVectors(totalRewardVector, model.getStateRewardVector(), totalRewardVector); - } - } else { - totalRewardVector = std::vector(model.getStateRewardVector()); - } - - return this->computeExpectedRewards(minimize, psiStates, totalRewardVector); - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, 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(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { - // If there are no goal states, we avoid the computation and directly return zero. - if (psiStates.empty()) { - return std::vector(model.getNumberOfStates(), storm::utility::zero()); - } - - // Likewise, if all bits are set, we can avoid the computation and set. - if ((~psiStates).empty()) { - return std::vector(model.getNumberOfStates(), storm::utility::one()); - } - - // Start by decomposing the Markov automaton into its MECs. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(model); - - // Get some data members for convenience. - typename storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - - // Now start with compute the long-run average for all end components in isolation. - std::vector lraValuesForEndComponents; - - // While doing so, we already gather some information for the following steps. - std::vector stateToMecIndexMap(model.getNumberOfStates()); - storm::storage::BitVector statesInMecs(model.getNumberOfStates()); - - for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { - storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; - - // Gather information for later use. - for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; - - statesInMecs.set(state); - stateToMecIndexMap[state] = currentMecIndex; - } - - // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(minimize, transitionMatrix, nondeterministicChoiceIndices, model.getMarkovianStates(), model.getExitRates(), psiStates, mec, currentMecIndex)); - } - - // For fast transition rewriting, we build some auxiliary data structures. - storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; - uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); - uint_fast64_t lastStateNotInMecs = 0; - uint_fast64_t numberOfStatesNotInMecs = 0; - std::vector statesNotInMecsBeforeIndex; - statesNotInMecsBeforeIndex.reserve(model.getNumberOfStates()); - for (auto state : statesNotContainedInAnyMec) { - while (lastStateNotInMecs <= state) { - statesNotInMecsBeforeIndex.push_back(numberOfStatesNotInMecs); - ++lastStateNotInMecs; - } - ++numberOfStatesNotInMecs; - } - - // Finally, we are ready to create the SSP matrix and right-hand side of the SSP. - std::vector b; - typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); - - // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). - uint_fast64_t currentChoice = 0; - for (auto state : statesNotContainedInAnyMec) { - sspMatrixBuilder.newRowGroup(currentChoice); - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { - std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); - b.push_back(storm::utility::zero()); - - for (auto element : transitionMatrix.getRow(choice)) { - if (statesNotContainedInAnyMec.get(element.getColumn())) { - // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); - } else { - // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector - // so that we are able to write the cumulative probability to the MEC into the matrix. - auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); - } - } - - // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { - if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { - sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); - } - } - } - } - - // Now we are ready to construct the choices for the auxiliary states. - for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { - storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex]; - sspMatrixBuilder.newRowGroup(currentChoice); - - for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; - boost::container::flat_set const& choicesInMec = stateChoicesPair.second; - - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { - std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); - - // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. - if (choicesInMec.find(choice) == choicesInMec.end()) { - b.push_back(storm::utility::zero()); - - for (auto element : transitionMatrix.getRow(choice)) { - if (statesNotContainedInAnyMec.get(element.getColumn())) { - // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); - } else { - // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector - // so that we are able to write the cumulative probability to the MEC into the matrix. - auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); - } - } - - // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { - if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { - sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); - } - } - - ++currentChoice; - } - } - } - - // For each auxiliary state, there is the option to achieve the reward value of the LRA associated with the MEC. - ++currentChoice; - b.push_back(lraValuesForEndComponents[mecIndex]); - } - - // Finalize the matrix and solve the corresponding system of equations. - storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice); - - std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); - std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(sspMatrix); - solver->solveEquationSystem(minimize, x, b); - - // Prepare result vector. - std::vector result(model.getNumberOfStates()); - - // Set the values for states not contained in MECs. - storm::utility::vector::setVectorValues(result, statesNotContainedInAnyMec, x); - - // Set the values for all states in MECs. - for (auto state : statesInMecs) { - result[state] = x[firstAuxiliaryStateIndex + stateToMecIndexMap[state]]; - } - - return result; - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + 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(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { - std::vector rewardValues(model.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(rewardValues, model.getMarkovianStates(), storm::utility::one()); - return this->computeExpectedRewards(minimize, psiStates, rewardValues); - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + + 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(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeExpectedTimesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { - if (stateFormula.isTrueFormula()) { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); - } else { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); - } - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { - STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); - } - template - ValueType SparseMarkovAutomatonCslModelChecker::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex) { - std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); - std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); - solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); - - // First, we need to create the variables for the problem. - std::map stateToVariableMap; - for (auto const& stateChoicesPair : mec) { - std::string variableName = "x" + std::to_string(stateChoicesPair.first); - stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); - } - storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", 1); - solver->update(); - - // Now we encode the problem as constraints. - for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; - - // Now, based on the type of the state, create a suitable constraint. - if (markovianStates.get(state)) { - storm::expressions::Expression constraint = stateToVariableMap.at(state); - - for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { - constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); - } - - constraint = constraint + solver->getConstant(storm::utility::one() / exitRates[state]) * k; - storm::expressions::Expression rightHandSide = psiStates.get(state) ? solver->getConstant(storm::utility::one() / exitRates[state]) : solver->getConstant(0); - if (minimize) { - constraint = constraint <= rightHandSide; - } else { - constraint = constraint >= rightHandSide; - } - solver->addConstraint("state" + std::to_string(state), constraint); - } else { - // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action - // and the sum ranges over all states s'. - for (auto choice : stateChoicesPair.second) { - storm::expressions::Expression constraint = stateToVariableMap.at(state); - - for (auto element : transitionMatrix.getRow(choice)) { - constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); - } - - storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::zero()); - if (minimize) { - constraint = constraint <= rightHandSide; - } else { - constraint = constraint >= rightHandSide; - } - solver->addConstraint("state" + std::to_string(state), constraint); - } - } - } - - solver->optimize(); - return solver->getContinuousValue(k); - } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeExpectedRewards(bool minimize, storm::storage::BitVector const& goalStates, std::vector const& stateRewards) const { - // First, we need to check which states have infinite expected time (by definition). - storm::storage::BitVector infinityStates; - if (minimize) { - // If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers, - // reach a bottom SCC without a goal state. - - // So we start by computing all bottom SCCs without goal states. - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(model, ~goalStates, true, true); - - // Now form the union of all these SCCs. - storm::storage::BitVector unionOfNonGoalBSccs(model.getNumberOfStates()); - for (auto const& scc : sccDecomposition) { - for (auto state : scc) { - unionOfNonGoalBSccs.set(state); - } - } - - // Finally, if this union is non-empty, compute the states such that all schedulers reach some state of the union. - if (!unionOfNonGoalBSccs.empty()) { - infinityStates = storm::utility::graph::performProbGreater0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), storm::storage::BitVector(model.getNumberOfStates(), true), unionOfNonGoalBSccs); - } else { - // Otherwise, we have no infinity states. - infinityStates = storm::storage::BitVector(model.getNumberOfStates()); - } - } else { - // If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable. - - // So we start by computing all MECs that have no goal state. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(model, ~goalStates); - - // Now we form the union of all states in these end components. - storm::storage::BitVector unionOfNonGoalMaximalEndComponents(model.getNumberOfStates()); - for (auto const& mec : mecDecomposition) { - for (auto const& stateActionPair : mec) { - unionOfNonGoalMaximalEndComponents.set(stateActionPair.first); - } - } - - if (!unionOfNonGoalMaximalEndComponents.empty()) { - // Now we need to check for which states there exists a scheduler that reaches one of the previously computed states. - infinityStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), storm::storage::BitVector(model.getNumberOfStates(), true), unionOfNonGoalMaximalEndComponents); - } else { - // Otherwise, we have no infinity states. - infinityStates = storm::storage::BitVector(model.getNumberOfStates()); - } - } - - // Now we identify the states for which values need to be computed. - storm::storage::BitVector maybeStates = ~(goalStates | infinityStates); - - // Then, we can eliminate the rows and columns for all states whose values are already known to be 0. - std::vector x(maybeStates.getNumberOfSetBits()); - storm::storage::SparseMatrix submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates); - - // Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system. - std::vector rewardValues(stateRewards); - for (auto state : model.getMarkovianStates()) { - rewardValues[state] = rewardValues[state] / model.getExitRates()[state]; - } - - // Finally, prepare the actual right-hand side. - std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, model.getNondeterministicChoiceIndices(), rewardValues); - - // Solve the corresponding system of equations. - std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(submatrix); - solver->solveEquationSystem(minimize, x, b); - - // Create resulting vector. - std::vector result(model.getNumberOfStates()); - - // Set values of resulting vector according to previous result and return the result. - storm::utility::vector::setVectorValues(result, maybeStates, x); - storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero()); - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); - - return result; - } - template class SparseMarkovAutomatonCslModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index cd51608eb..26e47bd92 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -1,73 +1,35 @@ #ifndef STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ #define STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ -#include "src/modelchecker/AbstractModelChecker.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" + #include "src/models/sparse/MarkovAutomaton.h" -#include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/solver/MinMaxLinearEquationSolver.h" + #include "src/utility/solver.h" namespace storm { namespace modelchecker { - template - class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker { + template + class SparseMarkovAutomatonCslModelChecker : public SparsePropositionalModelChecker { public: - explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model, std::unique_ptr>&& MinMaxLinearEquationSolver); - explicit SparseMarkovAutomatonCslModelChecker(storm::models::sparse::MarkovAutomaton const& model); + typedef typename SparseMarkovAutomatonModelType::ValueType ValueType; + typedef typename SparseMarkovAutomatonModelType::RewardModelType RewardModelType; + + explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model, std::unique_ptr>&& minMaxLinearEquationSolver); + explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; private: - // The methods that perform the actual checking. - std::vector computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) const; - static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory); - std::vector computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; - std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; - std::vector computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; - std::vector computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; - - /*! - * Computes the long-run average value for the given maximal end component of a Markov automaton. - * - * @param minimize Sets whether the long-run average is to be minimized or maximized. - * @param transitionMatrix The transition matrix of the underlying Markov automaton. - * @param nondeterministicChoiceIndices A vector indicating at which row the choice of a given state begins. - * @param markovianStates A bit vector storing all markovian states. - * @param exitRates A vector with exit rates for all states. Exit rates of probabilistic states are assumed to be zero. - * @param goalStates A bit vector indicating which states are to be considered as goal states. - * @param mec The maximal end component to consider for computing the long-run average. - * @param mecIndex The index of the MEC. - * @return The long-run average of being in a goal state for the given MEC. - */ - static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex = 0); - - /*! - * Computes the expected reward that is gained from each state before entering any of the goal states. - * - * @param minimize Indicates whether minimal or maximal rewards are to be computed. - * @param goalStates The goal states that define until which point rewards are gained. - * @param stateRewards A vector that defines the reward gained in each state. For probabilistic states, this is an instantaneous reward - * that is fully gained and for Markovian states the actually gained reward is dependent on the expected time to stay in the - * state, i.e. it is gouverned by the exit rate of the state. - * @return A vector that contains the expected reward for each state of the model. - */ - std::vector computeExpectedRewards(bool minimize, storm::storage::BitVector const& goalStates, std::vector const& stateRewards) const; - - // The model this model checker is supposed to analyze. - storm::models::sparse::MarkovAutomaton const& model; - // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. - std::unique_ptr> MinMaxLinearEquationSolverFactory; + std::unique_ptr> minMaxLinearEquationSolverFactory; }; } } diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index e69de29bb..ba43b4060 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -0,0 +1,325 @@ +#include "src/modelchecker/csl/helper/HybridCtmcCslHelper.h" + +#include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" +#include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" + +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddOdd.h" + +#include "src/utility/macros.h" +#include "src/utility/graph.h" + +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + boost::optional> modifiedStateRewardVector; + if (stateRewardVector) { + modifiedStateRewardVector = stateRewardVector.get() / exitRateVector; + } + + return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), modifiedStateRewardVector, transitionRewardMatrix, targetStates, qualitative, linearEquationSolverFactory); + } + + template + std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { + return HybridDtmcPrctlHelper::computeNextProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), nextStates); + } + + template + std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); + } + + template + std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + // If the time bounds are [0, inf], we rather call untimed reachability. + storm::utility::ConstantsComparator comparator; + if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { + return computeUntilProbabilities(model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative, linearEquationSolverFactory); + } + + // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0 + // or t' != inf. + + // If we identify the states that have probability 0 of reaching the target states, we can exclude them from the + // further computations. + storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, rateMatrix.notZero(), phiStates, psiStates); + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0."); + storm::dd::Bdd statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 && !psiStates; + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); + + if (!statesWithProbabilityGreater0NonPsi.isZero()) { + if (comparator.isZero(upperBound)) { + // In this case, the interval is of the form [0, 0]. + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.toAdd())); + } else { + if (comparator.isZero(lowerBound)) { + // In this case, the interval is of the form [0, t]. + // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. + + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + + // Create an ODD for the translation to an explicit representation. + storm::dd::Odd odd(statesWithProbabilityGreater0NonPsi); + + // Convert the symbolic parts to their explicit representation. + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.template toVector(odd); + + // Finally compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), + (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(), + psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subresult)); + } else if (comparator.isInfinity(upperBound)) { + // In this case, the interval is of the form [t, inf] with t != 0. + + // Start by computing the (unbounded) reachability probabilities of reaching psi states while + // staying in phi states. + std::unique_ptr unboundedResult = computeUntilProbabilities(model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative, linearEquationSolverFactory); + + // Compute the set of relevant states. + storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; + + // Filter the unbounded result such that it only contains values for the relevant states. + unboundedResult->filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); + + // Build an ODD for the relevant states. + storm::dd::Odd odd(relevantStates); + + std::vector result; + if (unboundedResult->isHybridQuantitativeCheckResult()) { + std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); + result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult().getValueVector()); + } else { + STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type."); + result = unboundedResult->asSymbolicQuantitativeCheckResult().getValueVector().template toVector(odd); + } + + // Determine the uniformization rate for the transient probability computation. + ValueType uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRateVector).getMax(); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + // Compute the transient probabilities. + result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().getAddZero(), relevantStates, odd, result)); + } else { + // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. + + if (lowerBound != upperBound) { + // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'. + + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the (first) uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Create the one-step vector. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + + // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. + storm::dd::Odd odd = storm::dd::Odd(statesWithProbabilityGreater0NonPsi); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.template toVector(odd); + + // Compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, linearEquationSolverFactory); + + // Transform the explicit result to a hybrid check result, so we can easily convert it to + // a symbolic qualitative format. + HybridQuantitativeCheckResult hybridResult(model.getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && model.getReachableStates()), + psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult); + + // Compute the set of relevant states. + storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; + + // Filter the unbounded result such that it only contains values for the relevant states. + hybridResult.filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); + + // Build an ODD for the relevant states. + odd = storm::dd::Odd(relevantStates); + + std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); + std::vector newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().getValueVector()); + + // Then compute the transient probabilities of being in such a state after t time units. For this, + // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. + uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // If the lower and upper bounds coincide, we have only determined the relevant states at this + // point, but we still need to construct the starting vector. + if (lowerBound == upperBound) { + odd = storm::dd::Odd(relevantStates); + newSubresult = psiStates.toAdd().template toVector(odd); + } + + // Finally, we compute the second set of transient probabilities. + uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().getAddZero(), relevantStates, odd, newSubresult)); + } else { + // In this case, the interval is of the form [t, t] with t != 0, t != inf. + + // Build an ODD for the relevant states. + storm::dd::Odd odd = storm::dd::Odd(statesWithProbabilityGreater0); + + std::vector newSubresult = psiStates.toAdd().template toVector(odd); + + // Then compute the transient probabilities of being in such a state after t time units. For this, + // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Finally, we compute the second set of transient probabilities. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().getAddZero(), statesWithProbabilityGreater0, odd, newSubresult)); + } + } + } + } else { + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.toAdd())); + } + } + + template + std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + // Only compute the result if the model has a state-based reward model. + STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + // Create ODD for the translation. + storm::dd::Odd odd(model.getReachableStates()); + + // Initialize result to state rewards of the model. + std::vector result = model.getStateRewardVector().template toVector(odd); + + // If the time-bound is not zero, we need to perform a transient analysis. + if (timeBound > 0) { + ValueType uniformizationRate = 1.02 * exitRateVector.getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); + } + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, result)); + } + + template + std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Only compute the result if the model has a state-based reward model. + STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + // If the time bound is zero, the result is the constant zero vector. + if (timeBound == 0) { + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), model.getManager().getAddZero())); + } + + // Otherwise, we need to perform some computations. + + // Start with the uniformization. + ValueType uniformizationRate = 1.02 * exitRateVector.getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Create ODD for the translation. + storm::dd::Odd odd(model.getReachableStates()); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + // Then compute the state reward vector to use in the computation. + storm::dd::Add totalRewardVector = model.hasStateRewards() ? model.getStateRewardVector() : model.getManager().getAddZero(); + if (model.hasTransitionRewards()) { + totalRewardVector += (rateMatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables()); + } + std::vector explicitTotalRewardVector = totalRewardVector.template toVector(odd); + + // Finally, compute the transient probabilities. + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::template computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, linearEquationSolverFactory); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + + template + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverage(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); + + // Create ODD for the translation. + storm::dd::Odd odd(model.getReachableStates()); + + storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); + std::vector explicitExitRateVector = exitRateVector.template toVector(odd); + + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + + template + storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { + STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); + STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows."); + + // Cut all non-maybe rows/columns from the transition matrix. + storm::dd::Add uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); + + // Now perform the uniformization. + uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate); + storm::dd::Add diagonal = model.getRowColumnIdentity() * maybeStates.toAdd(); + storm::dd::Add diagonalOffset = diagonal; + diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate)); + uniformizedMatrix += diagonalOffset; + + return uniformizedMatrix; + } + + template + storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { + return rateMatrix / exitRateVector; + } + + template class HybridCtmcCslHelper; + + } + } +} \ No newline at end of file diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h index e69de29bb..b768ea103 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -0,0 +1,60 @@ +#ifndef STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_ +#define STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_ + +#include + +#include "src/models/symbolic/Ctmc.h" + +#include "src/modelchecker/results/CheckResult.h" + +#include "src/utility/solver.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + class HybridCtmcCslHelper { + public: + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeLongRunAverage(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + + /*! + * Converts the given rate-matrix into a time-abstract probability matrix. + * + * @param model The symbolic model. + * @param rateMatrix The rate matrix. + * @param exitRateVector The exit rate vector of the model. + * @return The probability matrix. + */ + static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + + /*! + * Computes the matrix representing the transitions of the uniformized CTMC. + * + * @param model The symbolic model. + * @param transitionMatrix The matrix to uniformize. + * @param exitRateVector The exit rate vector. + * @param maybeStates The states that need to be considered. + * @param uniformizationRate The rate to be used for uniformization. + * @return The uniformized matrix. + */ + static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_ */ \ No newline at end of file diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp new file mode 100644 index 000000000..089a39c8a --- /dev/null +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -0,0 +1,494 @@ +#include "src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" + +#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" + +#include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/storage/MaximalEndComponentDecomposition.h" + +#include "src/utility/macros.h" +#include "src/utility/vector.h" +#include "src/utility/graph.h" + +#include "src/utility/numerical.h" + +#include "src/solver/LpSolver.h" + +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + template + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Start by computing four sparse matrices: + // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. + // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states. + // * a matrix aProbabilistic with all (non-discretized) transitions from probabilistic non-goal states to other probabilistic non-goal states. + // * a matrix aProbabilisticToMarkovian with all (non-discretized) transitions from probabilistic non-goal states to all Markovian non-goal states. + typename storm::storage::SparseMatrix aMarkovian = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, markovianNonGoalStates, true); + typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, probabilisticNonGoalStates); + typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates); + typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, markovianNonGoalStates); + + // The matrices with transitions from Markovian states need to be digitized. + // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. + uint_fast64_t rowIndex = 0; + for (auto state : markovianNonGoalStates) { + for (auto& element : aMarkovian.getRow(rowIndex)) { + ValueType eTerm = std::exp(-exitRates[state] * delta); + if (element.getColumn() == rowIndex) { + element.setValue((storm::utility::one() - eTerm) * element.getValue() + eTerm); + } else { + element.setValue((storm::utility::one() - eTerm) * element.getValue()); + } + } + ++rowIndex; + } + + // Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors. + rowIndex = 0; + for (auto state : markovianNonGoalStates) { + for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) { + element.setValue((1 - std::exp(-exitRates[state] * delta)) * element.getValue()); + } + ++rowIndex; + } + + // Initialize the two vectors that hold the variable one-step probabilities to all target states for probabilistic and Markovian (non-goal) states. + std::vector bProbabilistic(aProbabilistic.getRowCount()); + std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); + + // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); + std::vector bMarkovianFixed; + bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); + for (auto state : markovianNonGoalStates) { + bMarkovianFixed.push_back(storm::utility::zero()); + + for (auto& element : transitionMatrix.getRowGroup(state)) { + if (goalStates.get(element.getColumn())) { + bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); + } + } + } + + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + + // Perform the actual value iteration + // * loop until the step bound has been reached + // * in the loop: + // * perform value iteration using A_PSwG, v_PS and the vector b where b = (A * 1_G)|PS + A_PStoMS * v_MS + // and 1_G being the characteristic vector for all goal states. + // * perform one timed-step using v_MS := A_MSwG * v_MS + A_MStoPS * v_PS + (A * 1_G)|MS + std::vector markovianNonGoalValuesSwap(markovianNonGoalValues); + std::vector multiplicationResultScratchMemory(aProbabilistic.getRowCount()); + std::vector aProbabilisticScratchMemory(probabilisticNonGoalValues.size()); + for (uint_fast64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { + // Start by (re-)computing bProbabilistic = bProbabilisticFixed + aProbabilisticToMarkovian * vMarkovian. + aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); + storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); + + // Now perform the inner value iteration for probabilistic states. + solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + + // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. + aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); + storm::utility::vector::addVectors(bMarkovian, bMarkovianFixed, bMarkovian); + aMarkovian.multiplyWithVector(markovianNonGoalValues, markovianNonGoalValuesSwap); + std::swap(markovianNonGoalValues, markovianNonGoalValuesSwap); + storm::utility::vector::addVectors(markovianNonGoalValues, bMarkovian, markovianNonGoalValues); + } + + // After the loop, perform one more step of the value iteration for PS states. + aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); + storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); + solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + + // 'Unpack' the bounds to make them more easily accessible. + double lowerBound = boundsPair.first; + double upperBound = boundsPair.second; + + // (1) Compute the accuracy we need to achieve the required error bound. + ValueType maxExitRate = 0; + for (auto value : exitRateVector) { + maxExitRate = std::max(maxExitRate, value); + } + ValueType delta = (2 * storm::settings::generalSettings().getPrecision()) / (upperBound * maxExitRate * maxExitRate); + + // (2) Compute the number of steps we need to make for the interval. + uint_fast64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); + STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [" << lowerBound << ", " << upperBound << "]." << std::endl); + + // (3) Compute the non-goal states and initialize two vectors + // * vProbabilistic holds the probability values of probabilistic non-goal states. + // * vMarkovian holds the probability values of Markovian non-goal states. + storm::storage::BitVector const& markovianNonGoalStates = markovianStates & ~psiStates; + storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates; + std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); + std::vector vMarkovian(markovianNonGoalStates.getNumberOfSetBits()); + + computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRateVector, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + + // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. + if (lowerBound != storm::utility::zero()) { + std::vector vAllProbabilistic((~markovianStates).getNumberOfSetBits()); + std::vector vAllMarkovian(markovianStates.getNumberOfSetBits()); + + // Create the starting value vectors for the next value iteration based on the results of the previous one. + storm::utility::vector::setVectorValues(vAllProbabilistic, psiStates % ~markovianStates, storm::utility::one()); + storm::utility::vector::setVectorValues(vAllProbabilistic, ~psiStates % ~markovianStates, vProbabilistic); + storm::utility::vector::setVectorValues(vAllMarkovian, psiStates % markovianStates, storm::utility::one()); + storm::utility::vector::setVectorValues(vAllMarkovian, ~psiStates % markovianStates, vMarkovian); + + // Compute the number of steps to reach the target interval. + numberOfSteps = static_cast(std::ceil(lowerBound / delta)); + STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); + + // Compute the bounded reachability for interval [0, b-a]. + computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRateVector, markovianStates, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + + // Create the result vector out of vAllProbabilistic and vAllMarkovian and return it. + std::vector result(numberOfStates, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, ~markovianStates, vAllProbabilistic); + storm::utility::vector::setVectorValues(result, markovianStates, vAllMarkovian); + + return result; + } else { + // Create the result vector out of 1_G, vProbabilistic and vMarkovian and return it. + std::vector result(numberOfStates); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + storm::utility::vector::setVectorValues(result, probabilisticNonGoalStates, vProbabilistic); + storm::utility::vector::setVectorValues(result, markovianNonGoalStates, vMarkovian); + return result; + } + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); + return computeExpectedRewards(minimize, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + + // If there are no goal states, we avoid the computation and directly return zero. + if (psiStates.empty()) { + return std::vector(numberOfStates, storm::utility::zero()); + } + + // Likewise, if all bits are set, we can avoid the computation and set. + if ((~psiStates).empty()) { + return std::vector(numberOfStates, storm::utility::one()); + } + + // Start by decomposing the Markov automaton into its MECs. + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); + + // Get some data members for convenience. + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + + // Now start with compute the long-run average for all end components in isolation. + std::vector lraValuesForEndComponents; + + // While doing so, we already gather some information for the following steps. + std::vector stateToMecIndexMap(numberOfStates); + storm::storage::BitVector statesInMecs(numberOfStates); + + for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { + storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; + + // Gather information for later use. + for (auto const& stateChoicesPair : mec) { + uint_fast64_t state = stateChoicesPair.first; + + statesInMecs.set(state); + stateToMecIndexMap[state] = currentMecIndex; + } + + // Compute the LRA value for the current MEC. + lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(minimize, transitionMatrix, exitRateVector, markovianStates, psiStates, mec)); + } + + // For fast transition rewriting, we build some auxiliary data structures. + storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; + uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); + uint_fast64_t lastStateNotInMecs = 0; + uint_fast64_t numberOfStatesNotInMecs = 0; + std::vector statesNotInMecsBeforeIndex; + statesNotInMecsBeforeIndex.reserve(numberOfStates); + for (auto state : statesNotContainedInAnyMec) { + while (lastStateNotInMecs <= state) { + statesNotInMecsBeforeIndex.push_back(numberOfStatesNotInMecs); + ++lastStateNotInMecs; + } + ++numberOfStatesNotInMecs; + } + + // Finally, we are ready to create the SSP matrix and right-hand side of the SSP. + std::vector b; + typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); + + // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). + uint_fast64_t currentChoice = 0; + for (auto state : statesNotContainedInAnyMec) { + sspMatrixBuilder.newRowGroup(currentChoice); + + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { + std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); + b.push_back(storm::utility::zero()); + + for (auto element : transitionMatrix.getRow(choice)) { + if (statesNotContainedInAnyMec.get(element.getColumn())) { + // If the target state is not contained in an MEC, we can copy over the entry. + sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); + } else { + // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector + // so that we are able to write the cumulative probability to the MEC into the matrix. + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); + } + } + + // Now insert all (cumulative) probability values that target an MEC. + for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { + if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { + sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); + } + } + } + } + + // Now we are ready to construct the choices for the auxiliary states. + for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { + storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex]; + sspMatrixBuilder.newRowGroup(currentChoice); + + for (auto const& stateChoicesPair : mec) { + uint_fast64_t state = stateChoicesPair.first; + boost::container::flat_set const& choicesInMec = stateChoicesPair.second; + + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); + + // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. + if (choicesInMec.find(choice) == choicesInMec.end()) { + b.push_back(storm::utility::zero()); + + for (auto element : transitionMatrix.getRow(choice)) { + if (statesNotContainedInAnyMec.get(element.getColumn())) { + // If the target state is not contained in an MEC, we can copy over the entry. + sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); + } else { + // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector + // so that we are able to write the cumulative probability to the MEC into the matrix. + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); + } + } + + // Now insert all (cumulative) probability values that target an MEC. + for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { + if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { + sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); + } + } + + ++currentChoice; + } + } + } + + // For each auxiliary state, there is the option to achieve the reward value of the LRA associated with the MEC. + ++currentChoice; + b.push_back(lraValuesForEndComponents[mecIndex]); + } + + // Finalize the matrix and solve the corresponding system of equations. + storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice); + + std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->solveEquationSystem(minimize, x, b); + + // Prepare result vector. + std::vector result(numberOfStates); + + // Set the values for states not contained in MECs. + storm::utility::vector::setVectorValues(result, statesNotContainedInAnyMec, x); + + // Set the values for all states in MECs. + for (auto state : statesInMecs) { + result[state] = x[firstAuxiliaryStateIndex + stateToMecIndexMap[state]]; + } + + return result; + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeExpectedTimes(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + std::vector rewardValues(numberOfStates, storm::utility::zero()); + storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one()); + return computeExpectedRewards(minimize, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, rewardValues, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + + // First, we need to check which states have infinite expected time (by definition). + storm::storage::BitVector infinityStates; + if (minimize) { + // If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers, + // reach a bottom SCC without a goal state. + + // So we start by computing all bottom SCCs without goal states. + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, ~goalStates, true, true); + + // Now form the union of all these SCCs. + storm::storage::BitVector unionOfNonGoalBSccs(numberOfStates); + for (auto const& scc : sccDecomposition) { + for (auto state : scc) { + unionOfNonGoalBSccs.set(state); + } + } + + // Finally, if this union is non-empty, compute the states such that all schedulers reach some state of the union. + if (!unionOfNonGoalBSccs.empty()) { + infinityStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalBSccs); + } else { + // Otherwise, we have no infinity states. + infinityStates = storm::storage::BitVector(numberOfStates); + } + } else { + // If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable. + + // So we start by computing all MECs that have no goal state. + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, ~goalStates); + + // Now we form the union of all states in these end components. + storm::storage::BitVector unionOfNonGoalMaximalEndComponents(numberOfStates); + for (auto const& mec : mecDecomposition) { + for (auto const& stateActionPair : mec) { + unionOfNonGoalMaximalEndComponents.set(stateActionPair.first); + } + } + + if (!unionOfNonGoalMaximalEndComponents.empty()) { + // Now we need to check for which states there exists a scheduler that reaches one of the previously computed states. + infinityStates = storm::utility::graph::performProbGreater0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalMaximalEndComponents); + } else { + // Otherwise, we have no infinity states. + infinityStates = storm::storage::BitVector(numberOfStates); + } + } + + // Now we identify the states for which values need to be computed. + storm::storage::BitVector maybeStates = ~(goalStates | infinityStates); + + // Then, we can eliminate the rows and columns for all states whose values are already known to be 0. + std::vector x(maybeStates.getNumberOfSetBits()); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates); + + // Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system. + std::vector rewardValues(stateRewards); + for (auto state : markovianStates) { + rewardValues[state] = rewardValues[state] / exitRateVector[state]; + } + + // Finally, prepare the actual right-hand side. + std::vector b(submatrix.getRowCount()); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues); + + // Solve the corresponding system of equations. + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); + solver->solveEquationSystem(minimize, x, b); + + // Create resulting vector. + std::vector result(numberOfStates); + + // Set values of resulting vector according to previous result and return the result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); + + return result; + } + + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); + std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); + solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); + + // First, we need to create the variables for the problem. + std::map stateToVariableMap; + for (auto const& stateChoicesPair : mec) { + std::string variableName = "x" + std::to_string(stateChoicesPair.first); + stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); + } + storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", 1); + solver->update(); + + // Now we encode the problem as constraints. + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + for (auto const& stateChoicesPair : mec) { + uint_fast64_t state = stateChoicesPair.first; + + // Now, based on the type of the state, create a suitable constraint. + if (markovianStates.get(state)) { + storm::expressions::Expression constraint = stateToVariableMap.at(state); + + for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); + } + + constraint = constraint + solver->getConstant(storm::utility::one() / exitRateVector[state]) * k; + storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::one() / exitRateVector[state]) : solver->getConstant(0); + if (minimize) { + constraint = constraint <= rightHandSide; + } else { + constraint = constraint >= rightHandSide; + } + solver->addConstraint("state" + std::to_string(state), constraint); + } else { + // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action + // and the sum ranges over all states s'. + for (auto choice : stateChoicesPair.second) { + storm::expressions::Expression constraint = stateToVariableMap.at(state); + + for (auto element : transitionMatrix.getRow(choice)) { + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); + } + + storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::zero()); + if (minimize) { + constraint = constraint <= rightHandSide; + } else { + constraint = constraint >= rightHandSide; + } + solver->addConstraint("state" + std::to_string(state), constraint); + } + } + } + + solver->optimize(); + return solver->getContinuousValue(k); + } + + template class SparseMarkovAutomatonCslHelper; + + } + } +} \ No newline at end of file diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h new file mode 100644 index 000000000..ec70e97ce --- /dev/null +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -0,0 +1,68 @@ +#ifndef STORM_MODELCHECKER_SPARSE_MARKOVAUTOMATON_CSL_MODELCHECKER_HELPER_H_ +#define STORM_MODELCHECKER_SPARSE_MARKOVAUTOMATON_CSL_MODELCHECKER_HELPER_H_ + +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/storage/BitVector.h" +#include "src/storage/MaximalEndComponent.h" + +#include "src/utility/solver.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template > + class SparseMarkovAutomatonCslHelper { + public: + static std::vector computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeExpectedTimes(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + private: + static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + /*! + * Computes the long-run average value for the given maximal end component of a Markov automaton. + * + * @param minimize Sets whether the long-run average is to be minimized or maximized. + * @param transitionMatrix The transition matrix of the underlying Markov automaton. + * @param markovianStates A bit vector storing all markovian states. + * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are + * assumed to be zero. + * @param goalStates A bit vector indicating which states are to be considered as goal states. + * @param mec The maximal end component to consider for computing the long-run average. + * @return The long-run average of being in a goal state for the given MEC. + */ + static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + + /*! + * Computes the expected reward that is gained from each state before entering any of the goal states. + * + * @param minimize Indicates whether minimal or maximal rewards are to be computed. + * @param transitionMatrix The transition matrix of the underlying Markov automaton. + * @param backwardTransitions The reversed transition relation of the underlying Markov automaton. + * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are + * assumed to be zero. + * @param markovianStates A bit vector storing all markovian states. + * @param goalStates The goal states that define until which point rewards are gained. + * @param stateRewards A vector that defines the reward gained in each state. For probabilistic states, + * this is an instantaneous reward that is fully gained and for Markovian states the actually gained + * reward is dependent on the expected time to stay in the state, i.e. it is gouverned by the exit rate + * of the state. + * @return A vector that contains the expected reward for each state of the model. + */ + static std::vector computeExpectedRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_SPARSE_MARKOVAUTOMATON_CSL_MODELCHECKER_HELPER_H_ */ diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index cc809e03f..7a8c53cda 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -22,6 +22,11 @@ namespace storm { performMaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); } + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem) { + performMaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, subsystem); + } + template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& subsystem) { performMaximalEndComponentDecomposition(model.getTransitionMatrix(), model.getBackwardTransitions(), subsystem); diff --git a/src/storage/MaximalEndComponentDecomposition.h b/src/storage/MaximalEndComponentDecomposition.h index 672163e52..9708bd65a 100644 --- a/src/storage/MaximalEndComponentDecomposition.h +++ b/src/storage/MaximalEndComponentDecomposition.h @@ -33,6 +33,15 @@ namespace storm { * @param backwardTransition The reversed transition relation. */ MaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + + /* + * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix). + * + * @param transitionMatrix The transition relation of model to decompose into MECs. + * @param backwardTransition The reversed transition relation. + * @param subsystem The subsystem to decompose. + */ + MaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem); /*! * Creates an MEC decomposition of the given subsystem in the given model.