SMTMinimalLabelSetGenerator.h File Reference

#include <chrono>
#include <queue>
#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h"
#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/solver/Z3SmtSolver.h"
#include "storm/storage/BoostTypes.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/sparse/PrismChoiceOrigins.h"
#include "storm/utility/cli.h"
#include "storm/utility/macros.h"

Include dependency graph for SMTMinimalLabelSetGenerator.h:

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

Go to the source code of this file.

Classes
class	storm::counterexamples::SMTMinimalLabelSetGenerator< T >
	This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels. More...
struct	storm::counterexamples::SMTMinimalLabelSetGenerator< T >::Options
struct	storm::counterexamples::SMTMinimalLabelSetGenerator< T >::GeneratorStats
struct	storm::counterexamples::SMTMinimalLabelSetGenerator< T >::CexInput

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::counterexamples

Functions
size_t	storm::counterexamples::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.