storm::counterexamples Namespace Reference

Classes
class	Counterexample
class	HighLevelCounterexample
class	MILPMinimalLabelSetGenerator
	This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels. More...
class	PathCounterexample
class	SMTMinimalLabelSetGenerator
	This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels. More...

Functions
std::ostream &	operator<< (std::ostream &out, Counterexample const &counterexample)
template<typename T >
std::vector< storm::storage::FlatSet< uint_fast64_t > >	getGuaranteedLabelSets (storm::models::sparse::Model< T > const &model, std::vector< storm::storage::FlatSet< uint_fast64_t > > const &labelSets, storm::storage::BitVector const &psiStates, storm::storage::FlatSet< uint_fast64_t > const &relevantLabels)
	Computes a set of labels that is executed along all paths from any state to a target state.
template<typename T >
storm::storage::FlatSet< uint_fast64_t >	getGuaranteedLabelSet (storm::models::sparse::Model< T > const &model, std::vector< storm::storage::FlatSet< uint_fast64_t > > const &labelSets, storm::storage::BitVector const &psiStates, storm::storage::FlatSet< uint_fast64_t > const &relevantLabels)
	Computes a set of labels that is executed along all paths from an initial state to a target state.
size_t	nrCommands (storm::storage::SymbolicModelDescription const &descr)
	Helper to avoid case disticinot between prism and jani Returns the number of edges/commands in a symbolic model description.

Function Documentation

getGuaranteedLabelSet()

template<typename T >

storm::storage::FlatSet< uint_fast64_t > storm::counterexamples::getGuaranteedLabelSet	(	storm::models::sparse::Model< T > const &	model,
		std::vector< storm::storage::FlatSet< uint_fast64_t > > const &	labelSets,
		storm::storage::BitVector const &	psiStates,
		storm::storage::FlatSet< uint_fast64_t > const &	relevantLabels
	)

Computes a set of labels that is executed along all paths from an initial state to a target state.

Parameters

labelSet

the considered label sets (a label set is assigned to each choice)

Returns

The set of labels that is executed on all paths from an initial state to a target state.

Definition at line 118 of file GuaranteedLabelSet.h.

getGuaranteedLabelSets()

template<typename T >

std::vector< storm::storage::FlatSet< uint_fast64_t > > storm::counterexamples::getGuaranteedLabelSets	(	storm::models::sparse::Model< T > const &	model,
		std::vector< storm::storage::FlatSet< uint_fast64_t > > const &	labelSets,
		storm::storage::BitVector const &	psiStates,
		storm::storage::FlatSet< uint_fast64_t > const &	relevantLabels
	)

Computes a set of labels that is executed along all paths from any state to a target state.

Parameters

labelSet

the considered label sets (a label set is assigned to each choice)

Returns

The set of labels that is visited on all paths from any state to a target state.

Definition at line 21 of file GuaranteedLabelSet.h.

nrCommands()

size_t storm::counterexamples::nrCommands ( storm::storage::SymbolicModelDescription const &  descr )

inline

Helper to avoid case disticinot between prism and jani Returns the number of edges/commands in a symbolic model description.

Definition at line 36 of file SMTMinimalLabelSetGenerator.h.

operator<<()

std::ostream & storm::counterexamples::operator<<	(	std::ostream &	out,
		Counterexample const &	counterexample
	)

Definition at line 6 of file Counterexample.cpp.