#include "storm-config.h"
#include "test/storm_gtest.h"
#include <limits>
#include <memory>
#include <optional>
#include <set>
#include <string>
#include <utility>
#include <vector>
#include <boost/optional.hpp>
#include "storm-pomdp/analysis/FormulaInformation.h"
#include "storm-pomdp/transformer/RewardBoundUnfolder.h"
#include "storm-pomdp/transformer/ToStateBasedObservationTransformer.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/api/storm.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/logic/AtomicLabelFormula.h"
#include "storm/logic/BooleanLiteralFormula.h"
#include "storm/logic/BoundedUntilFormula.h"
#include "storm/logic/ProbabilityOperatorFormula.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/utility/ExtendedNumber.h"

Include dependency graph for RewardBoundUnfolderTest.cpp:

Functions
	TEST (RewardBoundUnfolder, FullyUnfoldedDtmcPreservesRewardBoundedProbability)
	TEST (RewardBoundUnfolder, FullyUnfoldedMdpPreservesChoicesAndOptimalProbabilities)
	TEST (RewardBoundUnfolder, FullyUnfoldedPomdpPreservesObservationsAndActiveBound)
	TEST (RewardBoundUnfolder, LevelAbstractionPreservesPomdpSpecificComponents)
	TEST (RewardBoundUnfolder, RejectsLevelWidthOutsideSignedRange)
	TEST (RewardBoundUnfolder, AcceptsLargestSignedLevelWidth)
	TEST (RewardBoundUnfolder, TrivialLowerBoundCanBeFollowedByRewardAwareObservationTransformation)
	TEST (RewardBoundUnfolder, LevelAbstractionTurnsNonStrictLowerBoundIntoStrictBound)
	TEST (RewardBoundUnfolder, DropsTriviallySatisfiedLowerBoundForDtmc)
	TEST (RewardBoundUnfolder, RejectsDimensionSpecificStateSubformulas)

Function Documentation

◆ TEST() [1/10]

TEST	(	RewardBoundUnfolder	,
		AcceptsLargestSignedLevelWidth	)

Definition at line 213 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [2/10]

TEST	(	RewardBoundUnfolder	,
		DropsTriviallySatisfiedLowerBoundForDtmc	)

Definition at line 270 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [3/10]

TEST	(	RewardBoundUnfolder	,
		FullyUnfoldedDtmcPreservesRewardBoundedProbability	)

Definition at line 131 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [4/10]

TEST	(	RewardBoundUnfolder	,
		FullyUnfoldedMdpPreservesChoicesAndOptimalProbabilities	)

Definition at line 143 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [5/10]

TEST	(	RewardBoundUnfolder	,
		FullyUnfoldedPomdpPreservesObservationsAndActiveBound	)

Definition at line 160 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [6/10]

TEST	(	RewardBoundUnfolder	,
		LevelAbstractionPreservesPomdpSpecificComponents	)

Definition at line 185 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [7/10]

TEST	(	RewardBoundUnfolder	,
		LevelAbstractionTurnsNonStrictLowerBoundIntoStrictBound	)

Definition at line 249 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [8/10]

TEST	(	RewardBoundUnfolder	,
		RejectsDimensionSpecificStateSubformulas	)

Definition at line 281 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [9/10]

TEST	(	RewardBoundUnfolder	,
		RejectsLevelWidthOutsideSignedRange	)

Definition at line 203 of file RewardBoundUnfolderTest.cpp.

◆ TEST() [10/10]

TEST	(	RewardBoundUnfolder	,
		TrivialLowerBoundCanBeFollowedByRewardAwareObservationTransformation	)

Definition at line 223 of file RewardBoundUnfolderTest.cpp.

Functions