#include <queue>
#include <utility>
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/models/sparse/Model.h"
#include "storm/storage/sparse/PrismChoiceOrigins.h"

Include dependency graph for GuaranteedLabelSet.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.

namespace	storm::counterexamples

Functions
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.

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.

Namespaces

Functions