lexicographicModelChecking.cpp File Reference

#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/environment/Environment.h"
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/SchedulerChoice.h"
#include "storm/utility/macros.h"
#include "storm/modelchecker/lexicographic/lexicographicModelChecking.h"
#include "storm/exceptions/InvalidArgumentException.h"

Include dependency graph for lexicographicModelChecking.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::modelchecker
namespace	storm::modelchecker::lexicographic

Functions
template<typename SparseModelType , typename ValueType >
helper::MDPSparseModelCheckingHelperReturnType< ValueType >	storm::modelchecker::lexicographic::check (Environment const &env, SparseModelType const &model, CheckTask< storm::logic::MultiObjectiveFormula, ValueType > const &checkTask, CheckFormulaCallback const &formulaChecker)
	check a lexicographic LTL-formula
template helper::MDPSparseModelCheckingHelperReturnType< double >	storm::modelchecker::lexicographic::check< storm::models::sparse::Mdp< double >, double > (Environment const &env, storm::models::sparse::Mdp< double > const &model, CheckTask< storm::logic::MultiObjectiveFormula, double > const &checkTask, CheckFormulaCallback const &formulaChecker)