SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp File Reference

#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm-parsers/api/storm-parsers.h"
#include "storm/api/storm.h"
#include "storm/environment/Environment.h"
#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/modelchecker/multiobjective/MultiObjectiveModelChecking.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/geometry/Hyperrectangle.h"
#include "storm/storage/geometry/Polytope.h"
#include "storm/storage/jani/Property.h"

Include dependency graph for SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp:

Go to the source code of this file.

Classes
class	SparseMdpPcaaMultiObjectiveModelCheckerTest

Functions
template<typename ValueType>
bool	expectPointConained (std::vector< std::vector< ValueType > > const &pointset, std::vector< ValueType > const &point, ValueType precision)
template<typename ValueType>
bool	expectSubset (std::vector< std::vector< ValueType > > const &lhs, std::vector< std::vector< ValueType > > const &rhs, ValueType precision)
template<typename ValueType>
std::vector< std::vector< ValueType > >	convertPointset (std::vector< std::vector< std::string > > const &in)
template<typename ValueType>
void	evaluateScheduler (storm::Environment const &env, storm::models::sparse::Mdp< ValueType > const &mdp, storm::storage::Scheduler< ValueType > const &scheduler, storm::logic::MultiObjectiveFormula const &formula, std::vector< ValueType > &result)
template<typename ValueType>
void	assertParetoResult (storm::Environment const &env, storm::models::sparse::Mdp< ValueType > const &mdp, storm::logic::MultiObjectiveFormula const &formula, storm::modelchecker::CheckResult const &result, std::vector< std::vector< std::string > > const &expectedPoints, bool expectSchedulers)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_memory)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, tiny_rewards_negative)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, resource_gathering)
	TEST_F (SparseMdpPcaaMultiObjectiveModelCheckerTest, uav)

Function Documentation

assertParetoResult()

template<typename ValueType>

void assertParetoResult	(	storm::Environment const &	env,
		storm::models::sparse::Mdp< ValueType > const &	mdp,
		storm::logic::MultiObjectiveFormula const &	formula,
		storm::modelchecker::CheckResult const &	result,
		std::vector< std::vector< std::string > > const &	expectedPoints,
		bool	expectSchedulers )

Definition at line 116 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

convertPointset()

template<typename ValueType>

std::vector< std::vector< ValueType > > convertPointset

(

std::vector< std::vector< std::string > > const &

in

)

Definition at line 83 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

evaluateScheduler()

template<typename ValueType>

void evaluateScheduler	(	storm::Environment const &	env,
		storm::models::sparse::Mdp< ValueType > const &	mdp,
		storm::storage::Scheduler< ValueType > const &	scheduler,
		storm::logic::MultiObjectiveFormula const &	formula,
		std::vector< ValueType > &	result )

Definition at line 95 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

expectPointConained()

template<typename ValueType>

bool expectPointConained	(	std::vector< std::vector< ValueType > > const &	pointset,
		std::vector< ValueType > const &	point,
		ValueType	precision )

Definition at line 21 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

expectSubset()

template<typename ValueType>

bool expectSubset	(	std::vector< std::vector< ValueType > > const &	lhs,
		std::vector< std::vector< ValueType > > const &	rhs,
		ValueType	precision )

Definition at line 73 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [1/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		consensus	)

Definition at line 211 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [2/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		dpm	)

Definition at line 329 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [3/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		resource_gathering	)

Definition at line 435 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [4/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		scheduler	)

Definition at line 309 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [5/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		simple_lra	)

Definition at line 351 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [6/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		simple_memory	)

Definition at line 148 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [7/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		team3with3objectives	)

Definition at line 266 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [8/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		tiny_rewards_negative	)

Definition at line 289 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [9/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		uav	)

Definition at line 529 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.

TEST_F() [10/10]

TEST_F	(	SparseMdpPcaaMultiObjectiveModelCheckerTest	,
		zeroconf	)

Definition at line 243 of file SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp.