Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StateEliminator.h
Go to the documentation of this file.
1
#ifndef STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_
2
#define STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_
3
4
#include "
storm/solver/stateelimination/EliminatorBase.h
"
5
6
namespace
storm
{
7
namespace
solver {
8
namespace
stateelimination {
9
10
template
<
typename
ValueType>
11
class
StateEliminator
:
public
EliminatorBase
<ValueType, ScalingMode::DivideOneMinus> {
12
public
:
13
StateEliminator
(
storm::storage::FlexibleSparseMatrix<ValueType>
& transitionMatrix,
storm::storage::FlexibleSparseMatrix<ValueType>
& backwardTransitions);
14
15
void
eliminateState
(
storm::storage::sparse::state_type
state,
bool
removeForwardTransitions);
16
};
17
18
}
// namespace stateelimination
19
}
// namespace solver
20
}
// namespace storm
21
22
#endif
// STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_
EliminatorBase.h
storm::solver::stateelimination::EliminatorBase
Definition
EliminatorBase.h:14
storm::solver::stateelimination::StateEliminator
Definition
StateEliminator.h:11
storm::solver::stateelimination::StateEliminator::eliminateState
void eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions)
Definition
StateEliminator.cpp:27
storm::storage::FlexibleSparseMatrix
The flexible sparse matrix is used during state elimination.
Definition
FlexibleSparseMatrix.h:21
storm::storage::sparse::state_type
uint64_t state_type
Definition
StateType.h:9
storm
LabParser.cpp.
Definition
cli.cpp:18
src
storm
solver
stateelimination
StateEliminator.h
Generated by
1.9.8