Namespaces
namespace	bisimulation
namespace	geometry
namespace	expressions
namespace	sparse

Classes
class	DFT
class	SparseMatrix
	A class that holds a possibly non-square matrix in the compressed row storage format. More...
class	ParameterRegion
class	FlexibleSparseMatrix
	The flexible sparse matrix is used during state elimination. More...
class	BeliefManager
class	PomdpMemory
class	PomdpMemoryBuilder
class	Scheduler
	This class defines which action is chosen in a particular state of a non-deterministic model. More...
class	MaximalEndComponentDecomposition
	This class represents the decomposition of a nondeterministic model into its maximal end components. More...
class	BisimulationDecomposition
	This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. More...
class	DeterministicModelBisimulationDecomposition
	This class represents the decomposition of a deterministic model into its bisimulation quotient. More...
class	NondeterministicModelBisimulationDecomposition
	This class represents the decomposition of a nondeterministic model into its bisimulation quotient. More...
class	BitVector
	A bit vector that is internally represented as a vector of 64-bit values. More...
struct	FNV1aBitVectorHash
struct	Murmur3BitVectorHash
class	BitVectorHashMap
	This class represents a hash-map whose keys are bit vectors. More...
class	ConsecutiveUint64DynamicPriorityQueue
class	MatrixEntry
class	Decomposition
	This class represents the decomposition of a model into blocks which are of the template type. More...
class	DeterministicTransition
class	Distribution
class	DistributionWithReward
class	DynamicPriorityQueue
class	ExplicitGameStrategy
class	ExplicitGameStrategyPair
class	IntegerInterval
class	MaximalEndComponent
	This class represents a maximal end-component of a nondeterministic model. More...
class	SparseModelMemoryProduct
	This class builds the product of the given sparse model and the given memory structure. More...
class	MemoryStructure
	This class represents a (deterministic) memory structure that can be used to encode certain events (such as reaching a set of goal states) into the state space of the model. More...
class	MemoryStructureBuilder
class	NondeterministicMemoryStructure
class	NondeterministicMemoryStructureBuilder
class	SparseModelMemoryProductReverseData
	Data to restore memory incorporation applied with SparseModelMemoryProduct. More...
class	SparseModelNondeterministicMemoryProduct
struct	ModelFormulasPair
class	QvbsBenchmark
	This class provides easy access to a benchmark of the Quantitative Verification Benchmark Set http://qcomp.org/benchmarks/. More...
class	RobustMaximalEndComponentDecomposition
	This class represents the decomposition of a nondeterministic model into its maximal end components. More...
class	SchedulerChoice
class	SchedulerClass
class	SparseMatrixBuilder
	A class that can be used to build a sparse matrix by adding value by value. More...
class	StateActionPair
struct	StateActionTarget
class	StateBlock
class	StronglyConnectedComponent
	This class represents a strongly connected component, i.e., a set of states such that every state can reach every other state. More...
struct	StronglyConnectedComponentDecompositionOptions
struct	SccDecompositionMemoryCache
	Holds temporary computation data used during the SCC decomposition algorithm. More...
struct	SccDecompositionResult
	Holds the result data of the implemented SCC decomposition algorithm. More...
class	StronglyConnectedComponentDecomposition
	This class represents the decomposition of a graph-like structure into its strongly connected components. More...
class	SymbolicModelDescription

Typedefs
template<typename Key>
using	FlatSet = boost::container::flat_set<Key, std::less<Key>, boost::container::new_allocator<Key>>
	Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
typedef uint_fast64_t	StateId
typedef uint64_t	PlayerIndex
typedef storm::storage::sparse::state_type	SparseMatrixIndexType
typedef storm::storage::FlatSet< sparse::state_type >	FlatSetStateContainer

Enumerations
enum class	PomdpMemoryPattern { Trivial , FixedCounter , SelectiveCounter , FixedRing , SelectiveRing , SettableBits , Full }
enum class	BisimulationType { Strong , Weak }
enum class	BisimulationTypeChoice { Strong , Weak , FromSettings }
enum class	NondeterministicMemoryStructurePattern { Trivial , FixedCounter , SelectiveCounter , FixedRing , SelectiveRing , SettableBits , Full }

Functions
template<typename ParametricType>
std::ostream &	operator<< (std::ostream &out, ParameterRegion< ParametricType > const &region)
template std::ostream &	operator<< (std::ostream &out, ParameterRegion< storm::RationalFunction > const &region)
std::string	toString (PomdpMemoryPattern const &pattern)
BisimulationType	resolveBisimulationTypeChoice (BisimulationTypeChoice c)
std::ostream &	operator<< (std::ostream &out, BitVector const &bitvector)
	__attribute__ ((always_inline)) uint32_t fmix32(uint32_t h)
uint32_t	rotl32 (uint32_t x, int8_t r)
uint64_t	rotl64 (uint64_t x, int8_t r)
template<typename ValueType>
std::string	toString (FlatSet< ValueType > const &set)
	Output vector as string.
template<typename BlockType>
std::ostream &	operator<< (std::ostream &out, Decomposition< BlockType > const &decomposition)
template std::ostream &	operator<< (std::ostream &out, Decomposition< StateBlock > const &decomposition)
template std::ostream &	operator<< (std::ostream &out, Decomposition< StronglyConnectedComponent > const &decomposition)
template std::ostream &	operator<< (std::ostream &out, Decomposition< MaximalEndComponent > const &decomposition)
template<typename ValueType, typename StateType>
std::ostream &	operator<< (std::ostream &out, Distribution< ValueType, StateType > const &distribution)
template<typename ValueType, typename StateType>
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, StateType >::type	sample (boost::container::flat_map< StateType, ValueType > const &distr, ValueType const &quantile)
template<typename ValueType, typename StateType>
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, StateType >::type	sample (boost::container::flat_map< StateType, storm::RationalFunction > const &distr, storm::RationalFunction const &quantile)
template std::ostream &	operator<< (std::ostream &out, Distribution< double > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< double, uint_fast64_t > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalNumber > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalNumber, uint_fast64_t > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalFunction > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalFunction, uint64_t > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::Interval > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::Interval, uint64_t > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalInterval > const &distribution)
template std::ostream &	operator<< (std::ostream &out, Distribution< storm::RationalInterval, uint64_t > const &distribution)
std::ostream &	operator<< (std::ostream &out, ExplicitGameStrategy const &strategy)
std::ostream &	operator<< (std::ostream &out, ExplicitGameStrategyPair const &strategyPair)
template<typename ValueType>
std::ostream &	operator<< (std::ostream &out, FlexibleSparseMatrix< ValueType > const &matrix)
template std::ostream &	operator<< (std::ostream &out, FlexibleSparseMatrix< double > const &matrix)
template std::ostream &	operator<< (std::ostream &out, FlexibleSparseMatrix< storm::RationalNumber > const &matrix)
template std::ostream &	operator<< (std::ostream &out, FlexibleSparseMatrix< storm::RationalFunction > const &matrix)
IntegerInterval	parseIntegerInterval (std::string const &stringRepr)
std::ostream &	operator<< (std::ostream &os, IntegerInterval const &i)
std::ostream &	operator<< (std::ostream &out, storm::storage::FlatSet< uint_fast64_t > const &block)
std::ostream &	operator<< (std::ostream &out, MaximalEndComponent const &component)
void	getFlatSccDecomposition (SccDecompositionResult const &sccDecRes, std::vector< uint64_t > &sccStates, std::vector< uint64_t > &sccIndications)
	Compute a mapping from SCC index to the set of states in that SCC.
std::string	toString (NondeterministicMemoryStructurePattern const &pattern)
storm::json< storm::RationalNumber >	readQvbsJsonFile (std::string const &filePath)
std::string	getString (storm::json< storm::RationalNumber > const &structure, std::string const &errorInfo="")
std::string	findModelPath (std::string const &modelName)
template<typename ValueType>
std::ostream &	operator<< (std::ostream &out, SchedulerChoice< ValueType > const &schedulerChoice)
template std::ostream &	operator<< (std::ostream &out, SchedulerChoice< double > const &schedulerChoice)
template std::ostream &	operator<< (std::ostream &out, SchedulerChoice< storm::RationalNumber > const &schedulerChoice)
template std::ostream &	operator<< (std::ostream &out, SchedulerChoice< storm::RationalFunction > const &schedulerChoice)
template std::ostream &	operator<< (std::ostream &out, SchedulerChoice< storm::Interval > const &schedulerChoice)
template std::ostream &	operator<< (std::ostream &out, SchedulerChoice< storm::RationalInterval > const &schedulerChoice)
template<typename IndexTypePrime, typename ValueTypePrime>
std::ostream &	operator<< (std::ostream &out, MatrixEntry< IndexTypePrime, ValueTypePrime > const &entry)
template<typename ValueType>
void	print (std::vector< typename SparseMatrix< ValueType >::index_type > const &rowGroupIndices, std::vector< MatrixEntry< typename SparseMatrix< ValueType >::index_type, typename SparseMatrix< ValueType >::value_type > > const &columnsAndValues, std::vector< typename SparseMatrix< ValueType >::index_type > const &rowIndications)
template<typename ValueType>
std::ostream &	operator<< (std::ostream &out, SparseMatrix< ValueType > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< double >::index_type, double > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< double > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< uint32_t, double > const &entry)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< int >::index_type, int > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< int > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< storm::storage::sparse::state_type >::index_type, storm::storage::sparse::state_type > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< storm::storage::sparse::state_type > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< RationalFunction >::index_type, RationalFunction > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< RationalFunction > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< Interval >::index_type, Interval > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< Interval > const &matrix)
template std::ostream &	operator<< (std::ostream &out, MatrixEntry< typename SparseMatrix< RationalInterval >::index_type, RationalInterval > const &entry)
template std::ostream &	operator<< (std::ostream &out, SparseMatrix< RationalInterval > const &matrix)
template<typename IndexType, typename ValueType>
std::size_t	hash_value (MatrixEntry< IndexType, ValueType > const &matrixEntry)
	Computes the hash value of a matrix entry.
std::set< storm::RationalFunctionVariable >	getVariables (SparseMatrix< storm::RationalFunction > const &matrix)
std::string	to_string (StateActionTarget const &sat)
bool	operator== (StateActionTarget const &sat1, StateActionTarget const &sat2)
std::ostream &	operator<< (std::ostream &out, FlatSetStateContainer const &block)
std::ostream &	operator<< (std::ostream &out, StateBlock const &block)
	Writes a string representation of the state block to the given output stream.
template<typename ValueType>
void	performSccDecompositionGCM (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::OptionalRef< storm::storage::BitVector const > subsystem, storm::OptionalRef< storm::storage::BitVector const > choices, bool, uint64_t startState, uint64_t &currentIndex, SccDecompositionResult &result, SccDecompositionMemoryCache &cache)
	Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to compute a mapping of states to their SCCs.
template<typename ValueType>
void	performSccDecomposition (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, StronglyConnectedComponentDecompositionOptions const &options, SccDecompositionResult &result)
	Computes an SCC decomposition for the given matrix and options.
template<typename ValueType>
void	performSccDecomposition (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, StronglyConnectedComponentDecompositionOptions const &options, SccDecompositionResult &result, SccDecompositionMemoryCache &cache)
	Computes an SCC decomposition for the given matrix and options.
std::ostream &	operator<< (std::ostream &out, SymbolicModelDescription const &model)
std::ostream &	operator<< (std::ostream &out, SymbolicModelDescription::ModelType const &type)

Variables
int	i
PlayerIndex const	INVALID_PLAYER_INDEX = std::numeric_limits<PlayerIndex>::max()

Typedef Documentation

◆ FlatSet

template<typename Key>

using storm::storage::FlatSet = boost::container::flat_set<Key, std::less<Key>, boost::container::new_allocator<Key>>

Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.

Definition at line 13 of file BoostTypes.h.

◆ FlatSetStateContainer

typedef storm::storage::FlatSet<sparse::state_type> storm::storage::FlatSetStateContainer

Definition at line 15 of file StateBlock.h.

◆ PlayerIndex

typedef uint64_t storm::storage::PlayerIndex

Definition at line 7 of file PlayerIndex.h.

◆ SparseMatrixIndexType

typedef storm::storage::sparse::state_type storm::storage::SparseMatrixIndexType

Definition at line 37 of file SparseMatrix.h.

◆ StateId

typedef uint_fast64_t storm::storage::StateId

Definition at line 12 of file DeterministicTransition.h.

Enumeration Type Documentation

◆ BisimulationType

enum class storm::storage::BisimulationType

strong

Enumerator
Strong
Weak

Definition at line 6 of file BisimulationType.h.

◆ BisimulationTypeChoice

enum class storm::storage::BisimulationTypeChoice

strong

Enumerator
Strong
Weak
FromSettings

Definition at line 7 of file BisimulationType.h.

◆ NondeterministicMemoryStructurePattern

enum class storm::storage::NondeterministicMemoryStructurePattern

strong

Enumerator
Trivial
FixedCounter
SelectiveCounter
FixedRing
SelectiveRing
SettableBits
Full

Definition at line 8 of file NondeterministicMemoryStructureBuilder.h.

◆ PomdpMemoryPattern

enum class storm::storage::PomdpMemoryPattern

strong

Enumerator
Trivial
FixedCounter
SelectiveCounter
FixedRing
SelectiveRing
SettableBits
Full

Definition at line 25 of file PomdpMemory.h.

Function Documentation

◆ attribute()

storm::storage::__attribute__ ( (always_inline) )

inline

Definition at line 1195 of file BitVector.cpp.

◆ findModelPath()

std::string storm::storage::findModelPath ( std::string const & modelName )

Definition at line 42 of file Qvbs.cpp.

◆ getFlatSccDecomposition()

void storm::storage::getFlatSccDecomposition	(	SccDecompositionResult const &	sccDecRes,
		std::vector< uint64_t > &	sccStates,
		std::vector< uint64_t > &	sccIndications )

Compute a mapping from SCC index to the set of states in that SCC.

Parameters

sccDecRes	The result of the SCC decomposition.
sccStates	flattened vector that contains all states of the different SCCs
sccIndications	vector that contains the index of the first state of each SCC in the sccStates vector plus one last entry pointing to the end of the sccStates vector That means that SCC i has its states in the range [sccIndications[i], sccIndications[i+1])

Definition at line 117 of file MaximalEndComponentDecomposition.cpp.

◆ getString()

std::string storm::storage::getString	(	storm::json< storm::RationalNumber > const &	structure,
		std::string const &	errorInfo = "" )

Definition at line 27 of file Qvbs.cpp.

◆ getVariables()

std::set< storm::RationalFunctionVariable > storm::storage::getVariables ( SparseMatrix< storm::RationalFunction > const & matrix )

Definition at line 6 of file SparseMatrixOperations.cpp.

◆ hash_value()

template<typename IndexType, typename ValueType>

std::size_t storm::storage::hash_value ( MatrixEntry< IndexType, ValueType > const & matrixEntry )

Computes the hash value of a matrix entry.

Definition at line 123 of file SparseMatrix.h.

◆ operator<<() [1/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	os,
		IntegerInterval const &	i )

◆ operator<<() [2/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		BitVector const &	bitvector )

Definition at line 1149 of file BitVector.cpp.

◆ operator<<() [3/52]

template<typename BlockType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Decomposition< BlockType > const &	decomposition )

Definition at line 131 of file Decomposition.cpp.

◆ operator<<() [4/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Decomposition< MaximalEndComponent > const &	decomposition )

◆ operator<<() [5/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Decomposition< StateBlock > const &	decomposition )

◆ operator<<() [6/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Decomposition< StronglyConnectedComponent > const &	decomposition )

◆ operator<<() [7/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< double > const &	distribution )

◆ operator<<() [8/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< double, uint_fast64_t > const &	distribution )

◆ operator<<() [9/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::Interval > const &	distribution )

◆ operator<<() [10/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::Interval, uint64_t > const &	distribution )

◆ operator<<() [11/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalFunction > const &	distribution )

◆ operator<<() [12/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalFunction, uint64_t > const &	distribution )

◆ operator<<() [13/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalInterval > const &	distribution )

◆ operator<<() [14/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalInterval, uint64_t > const &	distribution )

◆ operator<<() [15/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalNumber > const &	distribution )

◆ operator<<() [16/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< storm::RationalNumber, uint_fast64_t > const &	distribution )

◆ operator<<() [17/52]

template<typename ValueType, typename StateType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		Distribution< ValueType, StateType > const &	distribution )

Definition at line 134 of file Distribution.cpp.

◆ operator<<() [18/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		ExplicitGameStrategy const &	strategy )

Definition at line 45 of file ExplicitGameStrategy.cpp.

◆ operator<<() [19/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		ExplicitGameStrategyPair const &	strategyPair )

Definition at line 40 of file ExplicitGameStrategyPair.cpp.

◆ operator<<() [20/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		FlatSetStateContainer const &	block )

Definition at line 49 of file StateBlock.cpp.

◆ operator<<() [21/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		FlexibleSparseMatrix< double > const &	matrix )

◆ operator<<() [22/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		FlexibleSparseMatrix< storm::RationalFunction > const &	matrix )

◆ operator<<() [23/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		FlexibleSparseMatrix< storm::RationalNumber > const &	matrix )

◆ operator<<() [24/52]

template<typename ValueType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		FlexibleSparseMatrix< ValueType > const &	matrix )

Definition at line 312 of file FlexibleSparseMatrix.cpp.

◆ operator<<() [25/52]

template<typename IndexTypePrime, typename ValueTypePrime>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< IndexTypePrime, ValueTypePrime > const &	entry )

Definition at line 75 of file SparseMatrix.cpp.

◆ operator<<() [26/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< double >::index_type, double > const &	entry )

◆ operator<<() [27/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< int >::index_type, int > const &	entry )

◆ operator<<() [28/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< Interval >::index_type, Interval > const &	entry )

◆ operator<<() [29/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< RationalFunction >::index_type, RationalFunction > const &	entry )

◆ operator<<() [30/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< RationalInterval >::index_type, RationalInterval > const &	entry )

◆ operator<<() [31/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< typename SparseMatrix< storm::storage::sparse::state_type >::index_type, storm::storage::sparse::state_type > const &	entry )

◆ operator<<() [32/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MatrixEntry< uint32_t, double > const &	entry )

◆ operator<<() [33/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		MaximalEndComponent const &	component )

Definition at line 125 of file MaximalEndComponent.cpp.

◆ operator<<() [34/52]

template<typename ParametricType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		ParameterRegion< ParametricType > const &	region )

Definition at line 336 of file ParameterRegion.cpp.

◆ operator<<() [35/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		ParameterRegion< storm::RationalFunction > const &	region )

◆ operator<<() [36/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< double > const &	schedulerChoice )

◆ operator<<() [37/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< storm::Interval > const &	schedulerChoice )

◆ operator<<() [38/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< storm::RationalFunction > const &	schedulerChoice )

◆ operator<<() [39/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< storm::RationalInterval > const &	schedulerChoice )

◆ operator<<() [40/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< storm::RationalNumber > const &	schedulerChoice )

◆ operator<<() [41/52]

template<typename ValueType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SchedulerChoice< ValueType > const &	schedulerChoice )

Definition at line 57 of file SchedulerChoice.cpp.

◆ operator<<() [42/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< double > const &	matrix )

◆ operator<<() [43/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< int > const &	matrix )

◆ operator<<() [44/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< Interval > const &	matrix )

◆ operator<<() [45/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< RationalFunction > const &	matrix )

◆ operator<<() [46/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< RationalInterval > const &	matrix )

◆ operator<<() [47/52]

template std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< storm::storage::sparse::state_type > const &	matrix )

◆ operator<<() [48/52]

template<typename ValueType>

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SparseMatrix< ValueType > const &	matrix )

Definition at line 2405 of file SparseMatrix.cpp.

◆ operator<<() [49/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		StateBlock const &	block )

Writes a string representation of the state block to the given output stream.

Parameters

out	The output stream to write to.
block	The block to print to the stream.

Returns: The given output stream.

Definition at line 58 of file StateBlock.cpp.

◆ operator<<() [50/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		storm::storage::FlatSet< uint_fast64_t > const &	block )

◆ operator<<() [51/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SymbolicModelDescription const &	model )

Definition at line 222 of file SymbolicModelDescription.cpp.

◆ operator<<() [52/52]

std::ostream & storm::storage::operator<<	(	std::ostream &	out,
		SymbolicModelDescription::ModelType const &	type )

Definition at line 233 of file SymbolicModelDescription.cpp.

◆ operator==()

bool storm::storage::operator==	(	StateActionTarget const &	sat1,
		StateActionTarget const &	sat2 )

inline

Definition at line 19 of file StateActionTargetTuple.h.

◆ parseIntegerInterval()

IntegerInterval storm::storage::parseIntegerInterval ( std::string const & stringRepr )

Definition at line 15 of file IntegerInterval.cpp.

◆ performSccDecomposition() [1/2]

template<typename ValueType>

void storm::storage::performSccDecomposition	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		StronglyConnectedComponentDecompositionOptions const &	options,
		SccDecompositionResult &	result )

Computes an SCC decomposition for the given matrix and options.

Note: This method does initialize the given result data. This means that if multiple SCC decompositions (e.g. with different options) are computed, the result memory can be re-used to avoid expensive reallocations.

Parameters

transitionMatrix	transition matrix of the model
options	options for the decomposition
result	The resulting information will be stored into this struct.

Definition at line 272 of file StronglyConnectedComponentDecomposition.cpp.

◆ performSccDecomposition() [2/2]

template<typename ValueType>

void storm::storage::performSccDecomposition	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		StronglyConnectedComponentDecompositionOptions const &	options,
		SccDecompositionResult &	result,
		SccDecompositionMemoryCache &	cache )

Computes an SCC decomposition for the given matrix and options.

Note: This method does initialize the given result and cache data. This means that if multiple SCC decompositions (e.g. with different options) are computed, the result and cache memory can be re-used to avoid expensive reallocations.

Parameters

transitionMatrix	transition matrix of the model
options	options for the decomposition
result	The resulting information will be stored into this struct.
cache	memory used by the underlying algorithm

Definition at line 279 of file StronglyConnectedComponentDecomposition.cpp.

◆ performSccDecompositionGCM()

template<typename ValueType>

void storm::storage::performSccDecompositionGCM	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::OptionalRef< storm::storage::BitVector const >	subsystem,
		storm::OptionalRef< storm::storage::BitVector const >	choices,
		bool	,
		uint64_t	startState,
		uint64_t &	currentIndex,
		SccDecompositionResult &	result,
		SccDecompositionMemoryCache &	cache )

Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to compute a mapping of states to their SCCs.

All arguments given by (non-const) reference are modified by the function as a side-effect.

Parameters

transitionMatrix	The transition matrix of the system to decompose.
startState	The starting state for the search of Tarjan's algorithm.
nonTrivialStates	A bit vector where entries for non-trivial states (states that either have a selfloop or whose SCC is not a singleton) will be set to true
subsystem	An optional bit vector indicating which subsystem to consider.
choices	An optional bit vector indicating which choices belong to the subsystem.
currentIndex	The next free index that can be assigned to states.
hasPreorderNumber	A bit that is used to keep track of the states that already have a preorder number.
preorderNumbers	A vector storing the preorder number for each state.
recursionStateStack	memory used for the recursion stack.
s	The stack S used by the algorithm.
p	The stack S used by the algorithm.
stateHasScc	A bit vector containing all states that have already been assigned to an SCC.
stateToSccMapping	A mapping from states to the SCC indices they belong to. As a side effect of this function this mapping is filled (for all states reachable from the starting state).
sccCount	The number of SCCs that have been computed. As a side effect of this function, this count is increased.

Definition at line 135 of file StronglyConnectedComponentDecomposition.cpp.

◆ print()

template<typename ValueType>

void storm::storage::print	(	std::vector< typename SparseMatrix< ValueType >::index_type > const &	rowGroupIndices,
		std::vector< MatrixEntry< typename SparseMatrix< ValueType >::index_type, typename SparseMatrix< ValueType >::value_type > > const &	columnsAndValues,
		std::vector< typename SparseMatrix< ValueType >::index_type > const &	rowIndications )

Definition at line 374 of file SparseMatrix.cpp.

◆ readQvbsJsonFile()

storm::json< storm::RationalNumber > storm::storage::readQvbsJsonFile ( std::string const & filePath )

Definition at line 17 of file Qvbs.cpp.

◆ resolveBisimulationTypeChoice()

BisimulationType storm::storage::resolveBisimulationTypeChoice ( BisimulationTypeChoice c )

inline

Definition at line 21 of file BisimulationDecomposition.h.

◆ rotl32()

uint32_t storm::storage::rotl32	(	uint32_t	x,
		int8_t	r )

inline

Definition at line 1215 of file BitVector.cpp.

◆ rotl64()

uint64_t storm::storage::rotl64	(	uint64_t	x,
		int8_t	r )

inline

Definition at line 1219 of file BitVector.cpp.

◆ sample() [1/2]

template<typename ValueType, typename StateType>

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, StateType >::type storm::storage::sample	(	boost::container::flat_map< StateType, storm::RationalFunction > const &	distr,
		storm::RationalFunction const &	quantile )

Definition at line 203 of file Distribution.cpp.

◆ sample() [2/2]

template<typename ValueType, typename StateType>

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, StateType >::type storm::storage::sample	(	boost::container::flat_map< StateType, ValueType > const &	distr,
		ValueType const &	quantile )

Definition at line 189 of file Distribution.cpp.

◆ to_string()

std::string storm::storage::to_string ( StateActionTarget const & sat )

inline

Definition at line 15 of file StateActionTargetTuple.h.

◆ toString() [1/3]

template<typename ValueType>

std::string storm::storage::toString ( FlatSet< ValueType > const & set )

Output vector as string.

Parameters

vector Vector to output.

Returns: String containing the representation of the vector.

Definition at line 22 of file BoostTypes.h.

◆ toString() [2/3]

std::string storm::storage::toString ( NondeterministicMemoryStructurePattern const & pattern )

Definition at line 10 of file NondeterministicMemoryStructureBuilder.cpp.

◆ toString() [3/3]

std::string storm::storage::toString ( PomdpMemoryPattern const & pattern )

Definition at line 79 of file PomdpMemory.cpp.

Variable Documentation

◆ i

int storm::storage::i

Initial value:

{

return p[i]

storm::storage::i

int i

Definition BitVector.cpp:1223

Definition at line 1223 of file BitVector.cpp.

◆ INVALID_PLAYER_INDEX

PlayerIndex const storm::storage::INVALID_PLAYER_INDEX = std::numeric_limits<PlayerIndex>::max()

Definition at line 8 of file PlayerIndex.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ FlatSet

◆ FlatSetStateContainer

◆ PlayerIndex

◆ SparseMatrixIndexType

◆ StateId

Enumeration Type Documentation

◆ BisimulationType

◆ BisimulationTypeChoice

◆ NondeterministicMemoryStructurePattern

◆ PomdpMemoryPattern

Function Documentation

◆ __attribute__()

◆ findModelPath()

◆ getFlatSccDecomposition()

◆ getString()

◆ getVariables()

◆ hash_value()

◆ operator<<() [1/52]

◆ operator<<() [2/52]

◆ operator<<() [3/52]

◆ operator<<() [4/52]

◆ operator<<() [5/52]

◆ operator<<() [6/52]

◆ operator<<() [7/52]

◆ operator<<() [8/52]

◆ operator<<() [9/52]

◆ operator<<() [10/52]

◆ operator<<() [11/52]

◆ operator<<() [12/52]

◆ operator<<() [13/52]

◆ operator<<() [14/52]

◆ operator<<() [15/52]

◆ operator<<() [16/52]

◆ operator<<() [17/52]

◆ operator<<() [18/52]

◆ operator<<() [19/52]

◆ operator<<() [20/52]

◆ operator<<() [21/52]

◆ operator<<() [22/52]

◆ operator<<() [23/52]

◆ operator<<() [24/52]

◆ operator<<() [25/52]

◆ operator<<() [26/52]

◆ operator<<() [27/52]

◆ operator<<() [28/52]

◆ operator<<() [29/52]

◆ operator<<() [30/52]

◆ operator<<() [31/52]

◆ operator<<() [32/52]

◆ operator<<() [33/52]

◆ operator<<() [34/52]

◆ operator<<() [35/52]

◆ operator<<() [36/52]

◆ operator<<() [37/52]

◆ operator<<() [38/52]

◆ operator<<() [39/52]

◆ operator<<() [40/52]

◆ operator<<() [41/52]

◆ operator<<() [42/52]

◆ operator<<() [43/52]

◆ operator<<() [44/52]

◆ operator<<() [45/52]

◆ operator<<() [46/52]

◆ operator<<() [47/52]

◆ operator<<() [48/52]

◆ operator<<() [49/52]

◆ operator<<() [50/52]

◆ operator<<() [51/52]

◆ operator<<() [52/52]

◆ operator==()

◆ parseIntegerInterval()

◆ performSccDecomposition() [1/2]

◆ performSccDecomposition() [2/2]

◆ attribute()