|
Storm 1.11.1.1
A Modern Probabilistic Model Checker
|
#include <queue>#include <utility>#include "storm/exceptions/InvalidArgumentException.h"#include "storm/models/sparse/Model.h"#include "storm/storage/sparse/PrismChoiceOrigins.h"

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