SMTMinimalLabelSetGenerator.h File Reference

#include <algorithm>
#include <chrono>
#include <iterator>
#include <memory>
#include <queue>
#include <set>
#include <sstream>
#include <utility>
#include "storm-counterexamples/counterexamples/CounterexampleOptions.h"
#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h"
#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/MissingLibraryException.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/models/ModelType.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Model.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/JaniChoiceOrigins.h"
#include "storm/storage/sparse/PrismChoiceOrigins.h"
#include "storm/utility/graph.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
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.