SparseMarkovAutomatonCslHelper.cpp File Reference

#include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/LpSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/multiplier/Multiplier.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/SchedulerChoice.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/SignalHandler.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"

Include dependency graph for SparseMarkovAutomatonCslHelper.cpp:

Go to the source code of this file.

Classes
class	storm::modelchecker::helper::UnifPlusHelper< ValueType >

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

Functions
template<typename ValueType>
std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType > >	storm::modelchecker::helper::setUpProbabilisticStatesSolver (storm::Environment &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitions)
template<typename ValueType>
void	storm::modelchecker::helper::computeBoundedReachabilityProbabilitiesImca (Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &exitRates, storm::storage::BitVector const &goalStates, storm::storage::BitVector const &markovianNonGoalStates, storm::storage::BitVector const &probabilisticNonGoalStates, std::vector< ValueType > &markovianNonGoalValues, std::vector< ValueType > &probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps)
template<typename ValueType>
std::vector< ValueType >	storm::modelchecker::helper::computeBoundedUntilProbabilitiesImca (Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &exitRateVector, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const &psiStates, std::pair< double, double > const &boundsPair)