#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/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	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 56 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ expectThrow()

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

Definition at line 41 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 23 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 18 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 34 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 27 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ makeUncertainAndCheck()

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

Definition at line 84 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [1/7]

TEST	(	RobustMDPModelCheckingTest	,
		AddUncertaintyCoin22max
	)

Definition at line 142 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [2/7]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedTiny03maxmin
	)

Definition at line 126 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [3/7]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny01maxmin
	)

Definition at line 118 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [4/7]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny03maxmin
	)

Definition at line 122 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [5/7]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin
	)

Definition at line 130 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [6/7]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin_rewards
	)

Definition at line 138 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [7/7]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny05maxmin
	)

Definition at line 134 of file RobustMdpPrctlModelCheckerTest.cpp.

Functions