RobustMdpPrctlModelCheckerTest.cpp File Reference

#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:

Go to the source code of this file.

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::ExtendedRationalNumber	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::ExtendedRationalNumber	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
void	expectSolutionBoundsSound (std::unique_ptr< storm::modelchecker::CheckResult > const &result, double expected)
void	expectSolutionBoundsSound (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::RationalNumber const &expected)
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, Tiny04MinRewards)
	TEST (RobustMDPModelCheckingTest, RewardsTargetTransitionInterval)
	TEST (RobustMDPModelCheckingTest, RewardsTargetStateBeforeMaybeStates)
	TEST (RobustMDPModelCheckingTest, ReachabilityTimes)
	TEST (RobustMDPModelCheckingTest, ReachabilityTimesSingleAction)
	TEST (RobustMDPModelCheckingTest, GraphPreservationRequired)
	TEST (RobustMDPModelCheckingTest, GraphPreservationAfterTightening)
	TEST (RobustMDPModelCheckingTest, MinRewardsUniqueSolution)
	TEST (RobustMDPModelCheckingTest, MinRewardsNonUniqueSolution)
	TEST (RobustMDPModelCheckingTest, CumulativeRewards)
	TEST (RobustMDPModelCheckingTest, CumulativeRewardsNoUncertaintyResolutionMode)
	TEST (RobustMDPModelCheckingTest, CrowdsQuotientIMDP)
	TEST (RobustRationalMDPModelCheckingTest, CumulativeRewards)
	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 105 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 180 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 140 of file RobustMdpPrctlModelCheckerTest.cpp.

expectSolutionBoundsSound() [1/2]

void expectSolutionBoundsSound	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		double	expected )

Definition at line 68 of file RobustMdpPrctlModelCheckerTest.cpp.

expectSolutionBoundsSound() [2/2]

void expectSolutionBoundsSound	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::RationalNumber const &	expected )

Definition at line 79 of file RobustMdpPrctlModelCheckerTest.cpp.

expectThrow()

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

Definition at line 90 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::ExtendedRationalNumber 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::ExtendedRationalNumber 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 226 of file RobustMdpPrctlModelCheckerTest.cpp.

makeUncertainAndCheckRational()

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

Definition at line 260 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [1/28]

TEST	(	RobustMdpModelCheckerTest	,
		RobotMinMaxTest	)

Definition at line 216 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [2/28]

TEST	(	RobustMDPModelCheckingTest	,
		AddUncertaintyCoin22max	)

Definition at line 489 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [3/28]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedMaxmin	)

Definition at line 311 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [4/28]

TEST	(	RobustMDPModelCheckingTest	,
		BoundedTiny03maxmin	)

Definition at line 306 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [5/28]

TEST	(	RobustMDPModelCheckingTest	,
		CrowdsQuotientIMDP	)

Definition at line 424 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [6/28]

TEST	(	RobustMDPModelCheckingTest	,
		CumulativeRewards	)

Definition at line 403 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [7/28]

TEST	(	RobustMDPModelCheckingTest	,
		CumulativeRewardsNoUncertaintyResolutionMode	)

Definition at line 411 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [8/28]

TEST	(	RobustMDPModelCheckingTest	,
		GraphPreservationAfterTightening	)

Definition at line 381 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [9/28]

TEST	(	RobustMDPModelCheckingTest	,
		GraphPreservationRequired	)

Definition at line 363 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [10/28]

TEST	(	RobustMDPModelCheckingTest	,
		MinRewardsNonUniqueSolution	)

Definition at line 397 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [11/28]

TEST	(	RobustMDPModelCheckingTest	,
		MinRewardsUniqueSolution	)

Definition at line 390 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [12/28]

TEST	(	RobustMDPModelCheckingTest	,
		ReachabilityTimes	)

Definition at line 352 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [13/28]

TEST	(	RobustMDPModelCheckingTest	,
		ReachabilityTimesSingleAction	)

Definition at line 358 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [14/28]

TEST	(	RobustMDPModelCheckingTest	,
		RewardsTargetStateBeforeMaybeStates	)

Definition at line 346 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [15/28]

TEST	(	RobustMDPModelCheckingTest	,
		RewardsTargetTransitionInterval	)

Definition at line 339 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [16/28]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny01maxmin	)

Definition at line 298 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [17/28]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny03maxmin	)

Definition at line 302 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [18/28]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04maxmin	)

Definition at line 324 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [19/28]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny04MinRewards	)

Definition at line 332 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [20/28]

TEST	(	RobustMDPModelCheckingTest	,
		Tiny05maxmin	)

Definition at line 328 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [21/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		AddUncertaintyCoin22max	)

Definition at line 497 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [22/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		BoundedMaxmin	)

Definition at line 456 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [23/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		BoundedTiny03maxmin	)

Definition at line 449 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [24/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		CumulativeRewards	)

Definition at line 432 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [25/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny01maxmin	)

Definition at line 439 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [26/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny03maxmin	)

Definition at line 444 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [27/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny04maxmin	)

Definition at line 478 of file RobustMdpPrctlModelCheckerTest.cpp.

TEST() [28/28]

TEST	(	RobustRationalMDPModelCheckingTest	,
		Tiny05maxmin	)

Definition at line 484 of file RobustMdpPrctlModelCheckerTest.cpp.