#include "storm-config.h"
#include "storm/adapters/IntervalForward.h"
#include "storm/adapters/RationalNumberForward.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/transformer/AddUncertainty.h"
#include "storm/utility/constants.h"

Include dependency graph for RobustDtmcPrctlModelCheckerTest.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, std::optional< storm::UncertaintyResolutionMode > uncertaintyResolutionMode=std::nullopt)
void	expectThrowPrism (std::string const &path, std::string const &formulaString)
void	checkExplicitModelForQuantitativeResult (std::string const &path, std::string const &formulaString, double min, double max)
void	checkPrismModelForQuantitativeResult (std::string const &path, std::string const &formulaString, double min, double max)
void	checkModelForQualitativeResult (std::string const &path, std::string const &formulaString, std::vector< storm::storage::BitVector > expectedResultVector)
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)
storm::RationalNumber	getQuantitativeResultAtInitialState (std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
void	expectThrowRational (std::string const &path, std::string const &formulaString, std::optional< storm::UncertaintyResolutionMode > uncertaintyResolutionMode=std::nullopt)
void	checkExplicitModelForQuantitativeResultRational (std::string const &path, std::string const &formulaString, storm::RationalNumber min, storm::RationalNumber max)
void	checkPrismModelForQuantitativeResultRational (std::string const &path, std::string const &formulaString, storm::RationalNumber min, storm::RationalNumber max)
void	makeUncertainAndCheckRational (std::string const &path, std::string const &formulaString, storm::RationalNumber amountOfUncertainty)
	TEST (RobustDtmcModelCheckerTest, Tiny01ReachMaxMinProbs)
	TEST (RobustDtmcModelCheckerTest, Tiny01MaxReachProbNoUncertaintyResolutionMode)
	TEST (RobustDtmcModelCheckerTest, Tiny01MaxReachProbNoOptimizationDirectionButRobust)
	TEST (RobustDtmcModelCheckerTest, Tiny02GloballyMaxMinProbs)
	TEST (RobustDtmcModelCheckerTest, DieIntervalsMaxMin)
	TEST (RobustDtmcModelCheckerTest, BrpIntervalsMaxMin)
	TEST (RobustDtmcModelCheckerTest, DieIntervalsMaxMinRewards)
	TEST (RobustDtmcModelCheckerTest, Tiny03MaxMinRewards)
	TEST (RobustDtmcModelCheckerTest, Tiny03RewardsNoUncertaintyResolutionMode)
	TEST (RobustDtmcModelCheckerTest, Tiny04MaxMinRewards)
	TEST (RobustDtmcModelCheckerTest, CrowdsQuotientIDTMC)
	TEST (RobustDtmcModelCheckerTest, TinyO2Propositional)
	TEST (RobustDtmcModelCheckerTest, Tiny05StepBounded)
	TEST (RobustDtmcModelCheckerTest, BoundedMaxmin)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny01ReachMaxMinProbs)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny01MaxReachProbNoUncertaintyResolutionMode)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny01MaxReachProbNoOptimizationDirectionButRobust)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny02GloballyMaxMinProbs)
	TEST (RobustRationalDtmcModelCheckerTest, DieIntervalsMaxMin)
	TEST (RobustRationalDtmcModelCheckerTest, BrpIntervalsMaxMin)
	TEST (RobustRationalDtmcModelCheckerTest, DieIntervalsMaxMinRewards)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny03MaxMinRewards)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny03RewardsNoUncertaintyResolutionMode)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny04MaxMinRewards)
	TEST (RobustRationalDtmcModelCheckerTest, AddUncertaintyBrpMax)

Function Documentation

◆ checkExplicitModelForQuantitativeResult()

void checkExplicitModelForQuantitativeResult	(	std::string const &	path,
		std::string const &	formulaString,
		double	min,
		double	max )

Definition at line 80 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkExplicitModelForQuantitativeResultRational()

void checkExplicitModelForQuantitativeResultRational	(	std::string const &	path,
		std::string const &	formulaString,
		storm::RationalNumber	min,
		storm::RationalNumber	max )

Definition at line 202 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkModelForQualitativeResult()

void checkModelForQualitativeResult	(	std::string const &	path,
		std::string const &	formulaString,
		std::vector< storm::storage::BitVector >	expectedResultVector )

Definition at line 128 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkPrismModelForQuantitativeResult()

void checkPrismModelForQuantitativeResult	(	std::string const &	path,
		std::string const &	formulaString,
		double	min,
		double	max )

Definition at line 102 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkPrismModelForQuantitativeResultRational()

void checkPrismModelForQuantitativeResultRational	(	std::string const &	path,
		std::string const &	formulaString,
		storm::RationalNumber	min,
		storm::RationalNumber	max )

Definition at line 225 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ expectThrow()

void expectThrow	(	std::string const &	path,
		std::string const &	formulaString,
		std::optional< storm::UncertaintyResolutionMode >	uncertaintyResolutionMode = std::nullopt )

Definition at line 43 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ expectThrowPrism()

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

Definition at line 62 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ expectThrowRational()

void expectThrowRational	(	std::string const &	path,
		std::string const &	formulaString,
		std::optional< storm::UncertaintyResolutionMode >	uncertaintyResolutionMode = std::nullopt )

Definition at line 182 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [1/4]

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

Definition at line 25 of file RobustDtmcPrctlModelCheckerTest.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 20 of file RobustDtmcPrctlModelCheckerTest.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 170 of file RobustDtmcPrctlModelCheckerTest.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 158 of file RobustDtmcPrctlModelCheckerTest.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 36 of file RobustDtmcPrctlModelCheckerTest.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 29 of file RobustDtmcPrctlModelCheckerTest.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 175 of file RobustDtmcPrctlModelCheckerTest.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 163 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ makeUncertainAndCheckRational()

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

Definition at line 252 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [1/25]

TEST	(	RobustDtmcModelCheckerTest	,
		BoundedMaxmin	)

Definition at line 374 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [2/25]

TEST	(	RobustDtmcModelCheckerTest	,
		BrpIntervalsMaxMin	)

Definition at line 315 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [3/25]

TEST	(	RobustDtmcModelCheckerTest	,
		CrowdsQuotientIDTMC	)

Definition at line 348 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [4/25]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMin	)

Definition at line 307 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [5/25]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMinRewards	)

Definition at line 324 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [6/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoOptimizationDirectionButRobust	)

Definition at line 296 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [7/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoUncertaintyResolutionMode	)

Definition at line 290 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [8/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01ReachMaxMinProbs	)

Definition at line 285 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [9/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny02GloballyMaxMinProbs	)

Definition at line 302 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [10/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03MaxMinRewards	)

Definition at line 332 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [11/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03RewardsNoUncertaintyResolutionMode	)

Definition at line 337 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [12/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny04MaxMinRewards	)

Definition at line 342 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [13/25]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny05StepBounded	)

Definition at line 367 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [14/25]

TEST	(	RobustDtmcModelCheckerTest	,
		TinyO2Propositional	)

Definition at line 354 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [15/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		AddUncertaintyBrpMax	)

Definition at line 462 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [16/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		BrpIntervalsMaxMin	)

Definition at line 419 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [17/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		DieIntervalsMaxMin	)

Definition at line 411 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [18/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		DieIntervalsMaxMinRewards	)

Definition at line 440 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [19/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoOptimizationDirectionButRobust	)

Definition at line 402 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [20/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoUncertaintyResolutionMode	)

Definition at line 397 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [21/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01ReachMaxMinProbs	)

Definition at line 392 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [22/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny02GloballyMaxMinProbs	)

Definition at line 407 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [23/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03MaxMinRewards	)

Definition at line 448 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [24/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03RewardsNoUncertaintyResolutionMode	)

Definition at line 453 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [25/25]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny04MaxMinRewards	)

Definition at line 457 of file RobustDtmcPrctlModelCheckerTest.cpp.

Functions