Browse Source

Merge branch 'master' into deterministicScheds

main
TimQu 6 years ago
parent
commit
c5a583a0d1
  1. 2
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  2. 7
      src/storm-dft/storage/dft/DFT.cpp
  3. 16
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  4. 5
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
  5. 87
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  6. 8
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h
  7. 66
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  8. 2
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  9. 2
      src/storm/settings/SettingsManager.cpp
  10. 20
      src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
  11. 53
      src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp

2
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<ValueType> builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();

7
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<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
std::string newParentName = builder.getUniqueName(originalParent->name());
// Accumulate children names
std::vector<std::string> 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<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; } ) != children.end()) {
// element in subtree is also child
rewrite.push_back(isdElemId);
}
}

16
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@ -155,6 +155,22 @@ namespace storm {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::vector<typename SparseCtmcModelType::ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeAllTransientProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<double>();
std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();;
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> 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<storm::models::sparse::Ctmc<double>>;

5
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h

@ -35,6 +35,11 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask) override;
/*!
* Compute transient probabilities for all states.
*/
std::vector<ValueType> computeAllTransientProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask);
private:
template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;

87
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -208,7 +208,12 @@ namespace storm {
std::vector<ValueType> SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) {
return SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative);
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
return SparseDtmcPrctlHelper<ValueType>::computeAllUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), initialStates, phiStates, psiStates);
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates) {
return SparseDtmcPrctlHelper<ValueType>::computeNextProbabilities(env, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates);
@ -648,6 +653,76 @@ namespace storm {
return result;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> 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<ValueType> result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
storm::storage::SparseMatrix<ValueType> transposedMatrix(rateMatrix);
transposedMatrix.makeRowsAbsorbing(psiStates);
std::vector<ValueType> newRates = exitRates;
for (auto const& state : psiStates) {
newRates[state] = storm::utility::one<ValueType>();
}
// 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<ValueType> uniformizedMatrix = computeUniformizedMatrix(transposedMatrix, relevantStates, uniformizationRate, newRates);
// Compute the vector that is to be added as a compensation for removing the absorbing states.
/*std::vector<ValueType> b = transposedMatrix.getConstrainedRowSumVector(relevantStates, initialStates);
for (auto& element : b) {
element /= uniformizationRate;
std::cout << element << std::endl;
}*/
std::vector<ValueType> values(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
// Set initial states
size_t i = 0;
ValueType initDist = storm::utility::one<ValueType>() / initialStates.getNumberOfSetBits();
for (auto const& state : relevantStates) {
if (initialStates.get(state)) {
values[i] = initDist;
}
++i;
}
// Finally compute the transient probabilities.
std::vector<ValueType> subresult = computeTransientProbabilities<ValueType>(env, uniformizedMatrix, nullptr, timeBound, uniformizationRate, values);
storm::utility::vector::setVectorValues(result, relevantStates, subresult);
}
return result;
}
template <typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const&, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector<ValueType> const&, double) {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type.");
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
storm::storage::SparseMatrix<ValueType> SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector<ValueType> const& exitRates) {
STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << ".");
@ -786,6 +861,8 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template std::vector<double> SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<double> SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::storage::BitVector const& nextStates);
template std::vector<double> SparseCtmcCslHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound);
@ -801,6 +878,8 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& probabilityMatrix, std::vector<double> const& stateRewardVector, std::vector<double> const* exitRateVector);
template std::vector<double> SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound);
template std::vector<double> SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<double> const& exitRates, double timeBound);
template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector<double> const& exitRates);
@ -813,6 +892,9 @@ namespace storm {
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<storm::RationalNumber>&& goal, storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<storm::RationalFunction>&& goal, storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<storm::RationalNumber>&& goal, storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<storm::RationalFunction>&& goal, storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& nextStates);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& nextStates);
@ -840,6 +922,9 @@ namespace storm {
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<storm::RationalNumber>&& goal, storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<storm::RationalFunction>&& goal, storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const& exitRates, double timeBound);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const& exitRates, double timeBound);
template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRates);
template storm::storage::SparseMatrix<storm::RationalNumber> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRates);
template storm::storage::SparseMatrix<storm::RationalFunction> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRates);

8
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h

@ -27,6 +27,9 @@ namespace storm {
template <typename ValueType>
static std::vector<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template <typename ValueType>
static std::vector<ValueType> computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template <typename ValueType>
static std::vector<ValueType> computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates);
@ -60,6 +63,11 @@ namespace storm {
template <typename ValueType>
static std::vector<ValueType> computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative);
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
static std::vector<ValueType> computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, double timeBound);
template <typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
static std::vector<ValueType> computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, double timeBound);
/*!
* Computes the matrix representing the transitions of the uniformized CTMC.
*

66
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@ -175,7 +175,7 @@ namespace storm {
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
// 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<ValueType>().getComputeOnlyMaybeStates()) {
@ -215,7 +215,7 @@ namespace storm {
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::convertNumber<ValueType>(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<ValueType> linearEquationSolverFactory;
@ -255,7 +255,67 @@ namespace storm {
}
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> 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<ValueType> result(numberOfStates, storm::utility::zero<ValueType>());
// 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<ValueType> linearEquationSolverFactory;
bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> 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<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber<ValueType>(0.5));
// Prepare the right-hand side of the equation system.
std::vector<ValueType> b(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
// Set initial states
size_t i = 0;
ValueType initDist = storm::utility::one<ValueType>() / storm::utility::convertNumber<ValueType>(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<storm::solver::LinearEquationSolver<ValueType>> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix));
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->solveEquations(env, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, relevantStates, x);
}
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative) {
goal.oneMinus();

2
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

@ -36,6 +36,8 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint());
static std::vector<ValueType> computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
static std::vector<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative);
static std::vector<ValueType> computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound);

2
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.

20
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<double> matrixBuilder;
matrixBuilder.addNextValue(0, 1, 3.0);
matrixBuilder.addNextValue(1, 0, 2.0);
storm::storage::SparseMatrix<double> matrix = matrixBuilder.build();
std::vector<double> 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<double> 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);
}
}

53
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<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
for (auto const& f : formulas) {
tasks.emplace_back(*f);
}
auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
storm::storage::SparseMatrix<double> 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<double> goal(*model, tasks[0]);
std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::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<double>::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);
}
}
Loading…
Cancel
Save