#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/DirectEncodingParser.h"
#include "storm/adapters/IntervalAdapter.h"
#include "storm/api/builder.h"
#include "storm/api/properties.h"
#include "storm/api/verification.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/transformer/AddUncertainty.h"

Include dependency graph for RobustMdpPrctlModelCheckerTest.cpp:

Functions
std::unique_ptr< storm::modelchecker::QualitativeCheckResult >	getInitialStateFilter (std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)

std::unique_ptr< storm::modelchecker::QualitativeCheckResult >	getInitialStateFilter (std::shared_ptr< storm::models::sparse::Model< double > > const &model)

double	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)

double	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< double > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)

void	expectThrow (std::string const &path, std::string const &formulaString)

void	checkModel (std::string const &path, std::string const &formulaString, double maxmin, double maxmax, double minmax, double minmin, bool produceScheduler)

void	checkPrismModelForQuantitativeResult (std::string const &path, std::string const &formulaString, double minmin, double minmax, double maxmin, double maxmax, std::string constantsString)

	TEST (RobustMdpModelCheckerTest, RobotMinMaxTest)

void	makeUncertainAndCheck (std::string const &path, std::string const &formulaString, double amountOfUncertainty)

	TEST (RobustMDPModelCheckingTest, Tiny01maxmin)

	TEST (RobustMDPModelCheckingTest, Tiny03maxmin)

	TEST (RobustMDPModelCheckingTest, BoundedTiny03maxmin)

	TEST (RobustMDPModelCheckingTest, Tiny04maxmin)

	TEST (RobustMDPModelCheckingTest, Tiny05maxmin)

	TEST (RobustMDPModelCheckingTest, Tiny04maxmin_rewards)

	TEST (RobustMDPModelCheckingTest, AddUncertaintyCoin22max)

Function Documentation

◆ checkModel()

void checkModel	(	std::string const &	path,
		std::string const &	formulaString,
		double	maxmin,
		double	maxmax,
		double	minmax,
		double	minmin,
		bool	produceScheduler
	)

Definition at line 57 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ checkPrismModelForQuantitativeResult()

void checkPrismModelForQuantitativeResult	(	std::string const &	path,
		std::string const &	formulaString,
		double	minmin,
		double	minmax,
		double	maxmin,
		double	maxmax,
		std::string	constantsString
	)

Definition at line 87 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ expectThrow()

void expectThrow	(	std::string const &	path,
		std::string const &	formulaString
	)

Definition at line 42 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [1/2]

std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter ( std::shared_ptr< storm::models::sparse::Model< double > > const & model )

Definition at line 24 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [2/2]

std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter ( std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const & model )

Definition at line 19 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [1/2]

double getQuantitativeResultAtInitialState	(	std::shared_ptr< storm::models::sparse::Model< double > > const &	model,
		std::unique_ptr< storm::modelchecker::CheckResult > &	result
	)

Definition at line 35 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [2/2]

double getQuantitativeResultAtInitialState	(	std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &	model,
		std::unique_ptr< storm::modelchecker::CheckResult > &	result
	)

Definition at line 28 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ makeUncertainAndCheck()

void makeUncertainAndCheck	(	std::string const &	path,
		std::string const &	formulaString,
		double	amountOfUncertainty
	)

Definition at line 137 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [1/8]

TEST	(	RobustMdpModelCheckerTest	,
		RobotMinMaxTest
	)

Definition at line 127 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [2/8]

TEST	(	RobustMDPModelCheckingTest	,
		AddUncertaintyCoin22max
	)

Definition at line 195 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [3/8]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedTiny03maxmin
	)

Definition at line 179 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [4/8]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny01maxmin
	)

Definition at line 171 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [5/8]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny03maxmin
	)

Definition at line 175 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [6/8]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin
	)

Definition at line 183 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [7/8]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin_rewards
	)

Definition at line 191 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [8/8]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny05maxmin
	)

Definition at line 187 of file RobustMdpPrctlModelCheckerTest.cpp.

Functions