#include "storm-config.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/exceptions/NotImplementedException.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)
std::unique_ptr< storm::modelchecker::QualitativeCheckResult >	getInitialStateFilter (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &model)
storm::RationalNumber	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
std::unique_ptr< storm::modelchecker::QualitativeCheckResult >	getInitialStateFilter (std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > 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)
storm::RationalNumber	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > 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)
void	checkModelRational (std::string const &path, std::string const &formulaString, storm::RationalNumber maxmin, storm::RationalNumber maxmax, storm::RationalNumber minmax, storm::RationalNumber minmin, bool produceScheduler)
	TEST (RobustMdpModelCheckerTest, RobotMinMaxTest)
void	makeUncertainAndCheck (std::string const &path, std::string const &formulaString, double amountOfUncertainty)
void	makeUncertainAndCheckRational (std::string const &path, std::string const &formulaString, storm::RationalNumber amountOfUncertainty)
	TEST (RobustMDPModelCheckingTest, Tiny01maxmin)
	TEST (RobustMDPModelCheckingTest, Tiny03maxmin)
	TEST (RobustMDPModelCheckingTest, BoundedTiny03maxmin)
	TEST (RobustMDPModelCheckingTest, BoundedMaxmin)
	TEST (RobustMDPModelCheckingTest, Tiny04maxmin)
	TEST (RobustMDPModelCheckingTest, Tiny05maxmin)
	TEST (RobustMDPModelCheckingTest, Tiny04maxmin_rewards)
	TEST (RobustMDPModelCheckingTest, CrowdsQuotientIMDP)
	TEST (RobustRationalMDPModelCheckingTest, Tiny01maxmin)
	TEST (RobustRationalMDPModelCheckingTest, Tiny03maxmin)
	TEST (RobustRationalMDPModelCheckingTest, BoundedTiny03maxmin)
	TEST (RobustRationalMDPModelCheckingTest, BoundedMaxmin)
	TEST (RobustRationalMDPModelCheckingTest, Tiny04maxmin)
	TEST (RobustRationalMDPModelCheckingTest, Tiny05maxmin)
	TEST (RobustMDPModelCheckingTest, AddUncertaintyCoin22max)
	TEST (RobustRationalMDPModelCheckingTest, 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 83 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ checkModelRational()

void checkModelRational	(	std::string const &	path,
		std::string const &	formulaString,
		storm::RationalNumber	maxmin,
		storm::RationalNumber	maxmax,
		storm::RationalNumber	minmax,
		storm::RationalNumber	minmin,
		bool	produceScheduler )

Definition at line 153 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 113 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ expectThrow()

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

Definition at line 68 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [1/4]

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

Definition at line 26 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [2/4]

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

Definition at line 21 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [3/4]

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

Definition at line 42 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [4/4]

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

Definition at line 30 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [1/4]

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

Definition at line 54 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [2/4]

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

Definition at line 47 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [3/4]

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

Definition at line 61 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ getQuantitativeResultAtInitialState() [4/4]

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

Definition at line 35 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ makeUncertainAndCheck()

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

Definition at line 195 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ makeUncertainAndCheckRational()

void makeUncertainAndCheckRational	(	std::string const &	path,
		std::string const &	formulaString,
		storm::RationalNumber	amountOfUncertainty )

Definition at line 229 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [1/17]

TEST	(	RobustMdpModelCheckerTest	,
		RobotMinMaxTest	)

Definition at line 185 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [2/17]

TEST	(	RobustMDPModelCheckingTest	,
		AddUncertaintyCoin22max	)

Definition at line 363 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [3/17]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedMaxmin	)

Definition at line 280 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [4/17]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedTiny03maxmin	)

Definition at line 275 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [5/17]

TEST	(	RobustMDPModelCheckingTest	,
		CrowdsQuotientIMDP	)

Definition at line 305 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [6/17]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny01maxmin	)

Definition at line 267 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [7/17]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny03maxmin	)

Definition at line 271 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [8/17]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin	)

Definition at line 293 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [9/17]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin_rewards	)

Definition at line 301 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [10/17]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny05maxmin	)

Definition at line 297 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [11/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		AddUncertaintyCoin22max	)

Definition at line 371 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [12/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		BoundedMaxmin	)

Definition at line 330 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [13/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		BoundedTiny03maxmin	)

Definition at line 323 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [14/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny01maxmin	)

Definition at line 313 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [15/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny03maxmin	)

Definition at line 318 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [16/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny04maxmin	)

Definition at line 352 of file RobustMdpPrctlModelCheckerTest.cpp.

◆ TEST() [17/17]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny05maxmin	)

Definition at line 358 of file RobustMdpPrctlModelCheckerTest.cpp.

Functions