SparseStepBoundedHorizonHelper.cpp File Reference

#include "storm/modelchecker/helper/finitehorizon/SparseStepBoundedHorizonHelper.h"
#include "storm/adapters/IntervalAdapter.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/solver/multiplier/Multiplier.h"
#include "storm/utility/SignalHandler.h"

Include dependency graph for SparseStepBoundedHorizonHelper.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::modelchecker
namespace	storm::modelchecker::helper
namespace	storm::modelchecker::helper::detail

Functions
template<typename ValueType, typename SolutionType>
storm::storage::BitVector	storm::modelchecker::helper::detail::computeProbGreater0States (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, uint64_t const upperBound, ModelCheckerHint const &hint)