#include "storm-config.h"
#include "test/storm_gtest.h"
#include <filesystem>
#include <fstream>
#include <random>
#include <sstream>
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/adapters/JsonAdapter.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/api/builder.h"
#include "storm/api/export.h"
#include "storm/api/properties.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/ExtendedNumber.h"
#include "storm/utility/constants.h"

Include dependency graph for ExportCheckResultTest.cpp:

Functions
template<typename ValueType>
void	runNegativeInfinityExportTest ()
	No model checker hands out a negative infinity today, so this builds the check result directly.
	TEST (ExportCheckResultTest, NegativeInfinityDouble)
	TEST (ExportCheckResultTest, NegativeInfinityExact)
	TEST (ExportCheckResultTest, PrintsTheApproximationOfAnExactValue)
	A check result holds its values in the extended value type, so the test that decides whether to print the decimal approximation of an exact value has to recognise that type too.
	TEST (ExportCheckResultTest, PrintsNoApproximationOfAnInexactValue)
	The counterpart: a value type that is already decimal has nothing to approximate.
	TEST (ExportCheckResultTest, RangeOutputShowsBounds)
	A result with ten or more values is written as the range of its values, which then also has to show the bounds.
	TEST (ExportCheckResultTest, ExactSolutionIsAnnouncedInsteadOfItsBounds)
	Bounds that coincide with the values leave nothing to report but the fact that they do.
	TEST (ExportCheckResultTest, RangeOutputAnnouncesAnExactSolution)
	TEST (ExportCheckResultTest, InfiniteRewardDouble)
	TEST (ExportCheckResultTest, InfiniteRewardExact)

Function Documentation

◆ runNegativeInfinityExportTest()

template<typename ValueType>

void runNegativeInfinityExportTest ( )

No model checker hands out a negative infinity today, so this builds the check result directly.

The export must not fall back to the finite payload of an infinite value, which is a zero that means nothing.

Definition at line 131 of file ExportCheckResultTest.cpp.

◆ TEST() [1/9]

TEST	(	ExportCheckResultTest	,
		ExactSolutionIsAnnouncedInsteadOfItsBounds	)

Bounds that coincide with the values leave nothing to report but the fact that they do.

Definition at line 204 of file ExportCheckResultTest.cpp.

◆ TEST() [2/9]

TEST	(	ExportCheckResultTest	,
		InfiniteRewardDouble	)

Definition at line 224 of file ExportCheckResultTest.cpp.

◆ TEST() [3/9]

TEST	(	ExportCheckResultTest	,
		InfiniteRewardExact	)

Definition at line 229 of file ExportCheckResultTest.cpp.

◆ TEST() [4/9]

TEST	(	ExportCheckResultTest	,
		NegativeInfinityDouble	)

Definition at line 150 of file ExportCheckResultTest.cpp.

◆ TEST() [5/9]

TEST	(	ExportCheckResultTest	,
		NegativeInfinityExact	)

Definition at line 154 of file ExportCheckResultTest.cpp.

◆ TEST() [6/9]

TEST	(	ExportCheckResultTest	,
		PrintsNoApproximationOfAnInexactValue	)

The counterpart: a value type that is already decimal has nothing to approximate.

Definition at line 177 of file ExportCheckResultTest.cpp.

◆ TEST() [7/9]

TEST	(	ExportCheckResultTest	,
		PrintsTheApproximationOfAnExactValue	)

A check result holds its values in the extended value type, so the test that decides whether to print the decimal approximation of an exact value has to recognise that type too.

It recognised only the plain one for a while, which silently dropped the approximation from every exact result.

Definition at line 163 of file ExportCheckResultTest.cpp.

◆ TEST() [8/9]

TEST	(	ExportCheckResultTest	,
		RangeOutputAnnouncesAnExactSolution	)

Definition at line 213 of file ExportCheckResultTest.cpp.

◆ TEST() [9/9]

TEST	(	ExportCheckResultTest	,
		RangeOutputShowsBounds	)

A result with ten or more values is written as the range of its values, which then also has to show the bounds.

Definition at line 188 of file ExportCheckResultTest.cpp.

Functions