#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/transformer/AddUncertainty.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)

	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, TinyO2Propositional)

Function Documentation

◆ checkExplicitModelForQuantitativeResult()

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

Definition at line 77 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkModelForQualitativeResult()

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

Definition at line 125 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ checkPrismModelForQuantitativeResult()

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

Definition at line 99 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 40 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ expectThrowPrism()

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

Definition at line 59 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ getInitialStateFilter() [1/2]

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

Definition at line 22 of file RobustDtmcPrctlModelCheckerTest.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 17 of file RobustDtmcPrctlModelCheckerTest.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 33 of file RobustDtmcPrctlModelCheckerTest.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 26 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [1/11]

TEST	(	RobustDtmcModelCheckerTest	,
		BrpIntervalsMaxMin
	)

Definition at line 185 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [2/11]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMin
	)

Definition at line 177 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [3/11]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMinRewards
	)

Definition at line 194 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [4/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoOptimizationDirectionButRobust
	)

Definition at line 166 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [5/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoUncertaintyResolutionMode
	)

Definition at line 160 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [6/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01ReachMaxMinProbs
	)

Definition at line 155 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [7/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny02GloballyMaxMinProbs
	)

Definition at line 172 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [8/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03MaxMinRewards
	)

Definition at line 202 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [9/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03RewardsNoUncertaintyResolutionMode
	)

Definition at line 207 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [10/11]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny04MaxMinRewards
	)

Definition at line 212 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [11/11]

TEST	(	RobustDtmcModelCheckerTest	,
		TinyO2Propositional
	)

Definition at line 218 of file RobustDtmcPrctlModelCheckerTest.cpp.

Functions