diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index eed303311..4e4befb1e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -193,7 +193,7 @@ namespace storm { } // Build a single CTMC - STORM_LOG_DEBUG("Building Model..."); + STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 28b7d29d0..0ae6db850 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -335,14 +335,14 @@ namespace storm { STORM_LOG_ASSERT(mElements[rewrites[1]]->parents().front()->isGate(), "Rewritten element has no parent gate."); DFTGatePointer originalParent = std::static_pointer_cast>(mElements[rewrites[1]]->parents().front()); std::string newParentName = builder.getUniqueName(originalParent->name()); - + // Accumulate children names std::vector childrenNames; for (size_t i = 1; i < rewrites.size(); ++i) { - STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have the same father"); + STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have not the same father for rewrite " << mElements[rewrites[i]]->name()); childrenNames.push_back(mElements[rewrites[i]]->name()); } - + // Add element inbetween parent and children switch (originalParent->type()) { case DFTElementType::AND: @@ -809,6 +809,7 @@ namespace storm { for(size_t isdElemId : ISD) { if(isdElemId == child->id()) continue; if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; } ) != children.end()) { + // element in subtree is also child rewrite.push_back(isdElemId); } } diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index d084a42e4..89a2c9e03 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -155,6 +155,22 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::vector SparseCtmcCslModelChecker::computeAllTransientProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded or reward-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::NotImplementedException, "Computation needs upper limit for time bound."); + double upperBound = pathFormula.getNonStrictUpperBound(); + + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), upperBound); + return result; + } + // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker>; diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 5bf4735d0..d7f432f53 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -35,6 +35,11 @@ namespace storm { virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + /*! + * Compute transient probabilities for all states. + */ + std::vector computeAllTransientProbabilities(Environment const& env, CheckTask const& checkTask); + private: template::SupportsExponential, int>::type = 0> bool canHandleImplementation(CheckTask const& checkTask) const; diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index a6bee0577..ed87a9e1a 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -208,7 +208,12 @@ namespace storm { std::vector SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) { return SparseDtmcPrctlHelper::computeUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative); } - + + template + std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), initialStates, phiStates, psiStates); + } + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates) { return SparseDtmcPrctlHelper::computeNextProbabilities(env, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates); @@ -648,6 +653,76 @@ namespace storm { return result; } + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound) { + + // Compute transient probabilities going from initial state + // Instead of y=Px we now compute y=xP <=> y^T=P^Tx^T via transposition + uint_fast64_t numberOfStates = rateMatrix.getRowCount(); + + // Create the result vector. + std::vector result = std::vector(numberOfStates, storm::utility::zero()); + + storm::storage::SparseMatrix transposedMatrix(rateMatrix); + transposedMatrix.makeRowsAbsorbing(psiStates); + std::vector newRates = exitRates; + for (auto const& state : psiStates) { + newRates[state] = storm::utility::one(); + } + + // Identify all maybe states which have a probability greater than 0 to be reached from the initial state. + //storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(transposedMatrix, phiStates, initialStates); + //STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " states with probability greater 0."); + + //storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & ~initialStates;//phiStates | psiStates; + storm::storage::BitVector relevantStates(numberOfStates, true); + STORM_LOG_DEBUG(relevantStates.getNumberOfSetBits() << " relevant states."); + + if (!relevantStates.empty()) { + // Find the maximal rate of all relevant states to take it as the uniformization rate. + ValueType uniformizationRate = 0; + for (auto const& state : relevantStates) { + uniformizationRate = std::max(uniformizationRate, newRates[state]); + } + uniformizationRate *= 1.02; + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + transposedMatrix = transposedMatrix.transpose(); + + // Compute the uniformized matrix. + storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(transposedMatrix, relevantStates, uniformizationRate, newRates); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + /*std::vector b = transposedMatrix.getConstrainedRowSumVector(relevantStates, initialStates); + for (auto& element : b) { + element /= uniformizationRate; + std::cout << element << std::endl; + }*/ + + std::vector values(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Set initial states + size_t i = 0; + ValueType initDist = storm::utility::one() / initialStates.getNumberOfSetBits(); + for (auto const& state : relevantStates) { + if (initialStates.get(state)) { + values[i] = initDist; + } + ++i; + } + // Finally compute the transient probabilities. + std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, nullptr, timeBound, uniformizationRate, values); + + storm::utility::vector::setVectorValues(result, relevantStates, subresult); + } + + return result; + } + + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const&, storm::storage::SparseMatrix const&, storm::storage::BitVector const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector const&, double) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + template ::SupportsExponential, int>::type> storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates) { STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); @@ -786,6 +861,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); @@ -801,6 +878,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); + + template std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); @@ -813,6 +892,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); @@ -840,6 +922,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); + template std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + template std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index b6e7b508c..4fb01d5ff 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -27,6 +27,9 @@ namespace storm { template static std::vector computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); @@ -60,6 +63,11 @@ namespace storm { template static std::vector computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative); + template ::SupportsExponential, int>::type = 0> + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + template ::SupportsExponential, int>::type = 0> + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + /*! * Computes the matrix representing the transitions of the uniformized CTMC. * diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index ff7cb5c98..a03914c8c 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -175,7 +175,7 @@ namespace storm { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // We need to identify the maybe states (states which have a probability for satisfying the until formula - // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1. + // that is strictly between 0 and 1) and the states that satisfy the formula with probability 1. storm::storage::BitVector maybeStates, statesWithProbability1; if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { @@ -215,7 +215,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); } else { if (!maybeStates.empty()) { - // In this case we have have to compute the probabilities. + // In this case we have to compute the probabilities. // Check whether we need to convert the input to equation system format. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; @@ -255,7 +255,67 @@ namespace storm { } return result; } - + + template + std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + std::vector result(numberOfStates, storm::utility::zero()); + + // All states are relevant + storm::storage::BitVector relevantStates(numberOfStates, true); + + // Compute exact probabilities for some states. + if (!relevantStates.empty()) { + // Check whether we need to convert the input to equation system format. + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + + storm::storage::SparseMatrix submatrix(transitionMatrix); + submatrix.makeRowsAbsorbing(phiStates); + submatrix.makeRowsAbsorbing(psiStates); + //submatrix.deleteDiagonalEntries(psiStates); + //storm::storage::BitVector failState(numberOfStates, false); + //failState.set(0, true); + submatrix.deleteDiagonalEntries(); + submatrix = submatrix.transpose(); + submatrix = submatrix.getSubmatrix(true, relevantStates, relevantStates, convertToEquationSystem); + + if (convertToEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } + + // Initialize the x vector with 0.5 for each element. + // This is the initial guess for the iterative solvers. It should be safe as for all + // 'maybe' states we know that the probability is strictly larger than 0. + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); + + // Prepare the right-hand side of the equation system. + std::vector b(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Set initial states + size_t i = 0; + ValueType initDist = storm::utility::one() / storm::utility::convertNumber(initialStates.getNumberOfSetBits()); + for (auto const& state : relevantStates) { + if (initialStates.get(state)) { + b[i] = initDist; + } + ++i; + } + + // Now solve the created system of linear equations. + goal.restrictRelevantValues(relevantStates); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + solver->solveEquations(env, x, b); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, relevantStates, x); + } + return result; + } + template std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative) { goal.oneMinus(); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 16702ffed..e22e4bfc4 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -36,6 +36,8 @@ namespace storm { static std::vector computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative); static std::vector computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound); diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 69ad4a909..3b8dcfade 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -385,7 +385,7 @@ namespace storm { for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) { ArgumentBase& argument = option->getArgument(i); bool conversionOk = argument.setFromStringValue(argumentCache[i]); - STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument '" << argument.getName() << "' of option " << option->getModuleName() << ":" << option->getLongName() << "."); + STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument <" << argument.getName() << "> of option:\n" << *option); } // In case there are optional arguments that were not set, we set them to their default value. diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index fc906da6c..fcb8b53df 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -16,6 +16,7 @@ #include "storm/models/symbolic/Ctmc.h" #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -458,4 +459,23 @@ namespace { } } + + TEST(CtmcCslModelCheckerTest, TransientProbabilities) { + // Example from lecture + storm::storage::SparseMatrixBuilder matrixBuilder; + matrixBuilder.addNextValue(0, 1, 3.0); + matrixBuilder.addNextValue(1, 0, 2.0); + storm::storage::SparseMatrix matrix = matrixBuilder.build(); + + std::vector exitRates = {3, 2}; + storm::storage::BitVector initialStates(2); + initialStates.set(0); + storm::storage::BitVector phiStates(2); + storm::storage::BitVector psiStates(2); + storm::Environment env; + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, matrix, initialStates, phiStates, psiStates, exitRates, 1); + + EXPECT_NEAR(0.404043, result[0], 1e-6); + EXPECT_NEAR(0.595957, result[1], 1e-6); + } } diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index ff0e4630d..6c5f08c86 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -17,6 +17,7 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -644,5 +645,57 @@ namespace { EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) { + std::string formulasString = "P=? [F \"one\"]"; + formulasString += "; P=? [F \"two\"]"; + formulasString += "; P=? [F \"three\"]"; + + storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + std::vector> tasks; + for (auto const& f : formulas) { + tasks.emplace_back(*f); + } + auto model = storm::api::buildSparseModel(program, formulas)->template as>(); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + storm::storage::SparseMatrix matrix = model->getTransitionMatrix(); + storm::storage::BitVector initialStates(13); + initialStates.set(0); + storm::storage::BitVector phiStates(13); + storm::storage::BitVector psiStates(13); + psiStates.set(7); + psiStates.set(8); + psiStates.set(9); + psiStates.set(10); + psiStates.set(11); + psiStates.set(12); + storm::Environment env; + storm::solver::SolveGoal goal(*model, tasks[0]); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); + + EXPECT_NEAR(1.0/6, result[7], 1e-6); + EXPECT_NEAR(1.0/6, result[8], 1e-6); + EXPECT_NEAR(1.0/6, result[9], 1e-6); + EXPECT_NEAR(1.0/6, result[10], 1e-6); + EXPECT_NEAR(1.0/6, result[11], 1e-6); + EXPECT_NEAR(1.0/6, result[12], 1e-6); + + phiStates.set(6); + psiStates.set(1); + result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); + + EXPECT_NEAR(1, result[0], 1e-6); + EXPECT_NEAR(0.5, result[1], 1e-6); + EXPECT_NEAR(0.5, result[2], 1e-6); + EXPECT_NEAR(0.25, result[5], 1e-6); + EXPECT_NEAR(0, result[7], 1e-6); + EXPECT_NEAR(0, result[8], 1e-6); + EXPECT_NEAR(0, result[9], 1e-6); + EXPECT_NEAR(0.125, result[10], 1e-6); + EXPECT_NEAR(0.125, result[11], 1e-6); + EXPECT_NEAR(0, result[12], 1e-6); + } }