Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicModelStateEliminator.cpp
Go to the documentation of this file.
2
6
8
9namespace storm {
10namespace solver {
11namespace stateelimination {
12
13template<typename ValueType>
16 std::vector<ValueType>& rowValues)
17 : StateEliminator<ValueType>(transitionMatrix, backwardTransitions), rowValues(rowValues) {
19 transitionMatrix.getRowCount() == backwardTransitions.getColumnCount() && transitionMatrix.getColumnCount() == backwardTransitions.getRowCount(),
20 storm::exceptions::InvalidArgumentException, "Invalid matrix dimensions of forward/backwards transition matrices.");
21 STORM_LOG_THROW(rowValues.size() == transitionMatrix.getRowCount(), storm::exceptions::InvalidArgumentException, "Invalid size of row value vector");
22 // Intentionally left empty
23}
24
25template<typename ValueType>
27 rowValues[row] = storm::utility::simplify((ValueType)(loopProbability * rowValues[row]));
28}
29
30template<typename ValueType>
33 rowValues[predecessorRow] =
34 storm::utility::simplify((ValueType)(rowValues[predecessorRow] + storm::utility::simplify((ValueType)(probability * rowValues[row]))));
35}
36
38
39#ifdef STORM_HAVE_CARL
42#endif
43} // namespace stateelimination
44} // namespace solver
45} // namespace storm
virtual void updatePredecessor(storm::storage::sparse::state_type const &predecessorRow, ValueType const &probability, storm::storage::sparse::state_type const &row) override
virtual void updateValue(storm::storage::sparse::state_type const &row, ValueType const &loopProbability) override
NondeterministicModelStateEliminator(storm::storage::FlexibleSparseMatrix< ValueType > &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > &backwardTransitions, std::vector< ValueType > &rowValues)
The flexible sparse matrix is used during state elimination.
index_type getColumnCount() const
Returns the number of columns of the matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
ValueType simplify(ValueType value)
LabParser.cpp.
Definition cli.cpp:18