counterexamples.h File Reference

#include "storm-counterexamples/counterexamples/CounterexampleOptions.h"
#include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "storm-counterexamples/counterexamples/PathCounterexample.h"
#include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h"

Include dependency graph for counterexamples.h:

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

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::api

Functions
std::shared_ptr< storm::counterexamples::Counterexample >	storm::api::computeHighLevelCounterexampleMilp (storm::Environment const &env, storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Mdp< double > > mdp, std::shared_ptr< storm::logic::Formula const > const &formula, bool includeSchedulerCuts)
std::shared_ptr< storm::counterexamples::Counterexample >	storm::api::computeHighLevelCounterexampleMaxSmt (storm::Environment const &env, storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, storm::counterexamples::SMTMinimalLabelSetGenerator< double >::Options const &options)
std::shared_ptr< storm::counterexamples::Counterexample >	storm::api::computeKShortestPathCounterexample (std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, size_t maxK)