Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ConditionalHelper.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
5
6namespace storm {
7class Environment;
8
9namespace storage {
10class BitVector;
11template<typename ValueType>
12class SparseMatrix;
13} // namespace storage
14
15namespace modelchecker {
16class CheckResult;
17
18namespace utility {
19template<typename ValueType>
21}
22
23template<typename ValueType, typename SolutionType = ValueType>
25 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
26 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
27 storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates);
28
29} // namespace modelchecker
30} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
std::unique_ptr< CheckResult > computeConditionalProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
storage::BitVector BitVector
LabParser.cpp.
Definition cli.cpp:18