#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::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)
storm::ExtendedRationalNumber	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::ExtendedRationalNumber min, storm::ExtendedRationalNumber 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, Tiny03CumulativeRewards)
	TEST (RobustDtmcModelCheckerTest, Tiny04CumulativeRewards)
	TEST (RobustDtmcModelCheckerTest, Tiny03CumulativeRewardsNoUncertaintyResolutionMode)
	TEST (RobustDtmcModelCheckerTest, Tiny03CumulativeRewardsRobust)
	TEST (RobustDtmcModelCheckerTest, ReachabilityTimes)
	TEST (RobustDtmcModelCheckerTest, ReachabilityTimesAndRewardsTargetStateBeforeMaybeStates)
	TEST (RobustDtmcModelCheckerTest, GraphPreservationRequired)
	TEST (RobustDtmcModelCheckerTest, GraphPreservationAfterTightening)
	TEST (RobustDtmcModelCheckerTest, ReachabilityTimesNoUncertaintyResolutionMode)
	TEST (RobustDtmcModelCheckerTest, ReachabilityTimesRobust)
	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, Tiny03CumulativeRewards)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny04CumulativeRewards)
	TEST (RobustRationalDtmcModelCheckerTest, Tiny03CumulativeRewardsNoUncertaintyResolutionMode)
	TEST (RobustRationalDtmcModelCheckerTest, ReachabilityTimes)
	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::ExtendedRationalNumber	min,
		storm::ExtendedRationalNumber	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::ExtendedRationalNumber 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::ExtendedRationalNumber 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/39]

TEST	(	RobustDtmcModelCheckerTest	,
		BoundedMaxmin	)

Definition at line 428 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [2/39]

TEST	(	RobustDtmcModelCheckerTest	,
		BrpIntervalsMaxMin	)

Definition at line 315 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [3/39]

TEST	(	RobustDtmcModelCheckerTest	,
		CrowdsQuotientIDTMC	)

Definition at line 402 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [4/39]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMin	)

Definition at line 307 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [5/39]

TEST	(	RobustDtmcModelCheckerTest	,
		DieIntervalsMaxMinRewards	)

Definition at line 324 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [6/39]

TEST	(	RobustDtmcModelCheckerTest	,
		GraphPreservationAfterTightening	)

Definition at line 389 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [7/39]

TEST	(	RobustDtmcModelCheckerTest	,
		GraphPreservationRequired	)

Definition at line 382 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [8/39]

TEST	(	RobustDtmcModelCheckerTest	,
		ReachabilityTimes	)

Definition at line 370 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [9/39]

TEST	(	RobustDtmcModelCheckerTest	,
		ReachabilityTimesAndRewardsTargetStateBeforeMaybeStates	)

Definition at line 376 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [10/39]

TEST	(	RobustDtmcModelCheckerTest	,
		ReachabilityTimesNoUncertaintyResolutionMode	)

Definition at line 394 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [11/39]

TEST	(	RobustDtmcModelCheckerTest	,
		ReachabilityTimesRobust	)

Definition at line 398 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [12/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoOptimizationDirectionButRobust	)

Definition at line 296 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [13/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoUncertaintyResolutionMode	)

Definition at line 290 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [14/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny01ReachMaxMinProbs	)

Definition at line 285 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [15/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny02GloballyMaxMinProbs	)

Definition at line 302 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [16/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03CumulativeRewards	)

Definition at line 348 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [17/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03CumulativeRewardsNoUncertaintyResolutionMode	)

Definition at line 362 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [18/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03CumulativeRewardsRobust	)

Definition at line 366 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [19/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03MaxMinRewards	)

Definition at line 332 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [20/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny03RewardsNoUncertaintyResolutionMode	)

Definition at line 337 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [21/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny04CumulativeRewards	)

Definition at line 356 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [22/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny04MaxMinRewards	)

Definition at line 342 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [23/39]

TEST	(	RobustDtmcModelCheckerTest	,
		Tiny05StepBounded	)

Definition at line 421 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [24/39]

TEST	(	RobustDtmcModelCheckerTest	,
		TinyO2Propositional	)

Definition at line 408 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [25/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		AddUncertaintyBrpMax	)

Definition at line 539 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [26/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		BrpIntervalsMaxMin	)

Definition at line 473 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [27/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		DieIntervalsMaxMin	)

Definition at line 465 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [28/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		DieIntervalsMaxMinRewards	)

Definition at line 494 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [29/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		ReachabilityTimes	)

Definition at line 533 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [30/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoOptimizationDirectionButRobust	)

Definition at line 456 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [31/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01MaxReachProbNoUncertaintyResolutionMode	)

Definition at line 451 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [32/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny01ReachMaxMinProbs	)

Definition at line 446 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [33/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny02GloballyMaxMinProbs	)

Definition at line 461 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [34/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03CumulativeRewards	)

Definition at line 517 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [35/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03CumulativeRewardsNoUncertaintyResolutionMode	)

Definition at line 529 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [36/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03MaxMinRewards	)

Definition at line 502 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [37/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny03RewardsNoUncertaintyResolutionMode	)

Definition at line 507 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [38/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny04CumulativeRewards	)

Definition at line 524 of file RobustDtmcPrctlModelCheckerTest.cpp.

◆ TEST() [39/39]

TEST	(	RobustRationalDtmcModelCheckerTest	,
		Tiny04MaxMinRewards	)

Definition at line 511 of file RobustDtmcPrctlModelCheckerTest.cpp.

Functions