UmbTest.cpp File Reference

#include <filesystem>
#include <limits>
#include <random>
#include <span>
#include <vector>
#include "storm-config.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/adapters/IntervalAdapter.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/storage/umb/export/SparseModelToUmb.h"
#include "storm/storage/umb/export/UmbExport.h"
#include "storm/storage/umb/import/SparseModelFromUmb.h"
#include "storm/storage/umb/import/UmbImport.h"
#include "storm/storage/umb/model/StringEncoding.h"
#include "storm/storage/umb/model/UmbModel.h"
#include "storm/storage/umb/model/ValueEncoding.h"
#include "storm/storage/valuations/ValuationsStorage.h"
#include "storm/utility/constants.h"
#include "test/storm_gtest.h"

Include dependency graph for UmbTest.cpp:

Go to the source code of this file.

Functions
	TEST (UmbTest, RationalEncoding)
	TEST (UmbTest, DuplicateBranches)
	UMB allows multiple branches with the same source choice and target state, whereas a sparse matrix has at most one entry per row and column.
	TEST (UmbTest, ChoiceLabelingExport)
	Choices without a label are exported with the empty action string, which always has index 0.

Function Documentation

TEST() [1/3]

TEST	(	UmbTest	,
		ChoiceLabelingExport	)

Choices without a label are exported with the empty action string, which always has index 0.

In particular, this also holds if the choice labeling does not contain any label (then there is exactly one action).

Definition at line 398 of file UmbTest.cpp.

TEST() [2/3]

TEST	(	UmbTest	,
		DuplicateBranches	)

UMB allows multiple branches with the same source choice and target state, whereas a sparse matrix has at most one entry per row and column.

Probabilities of such branches are summed up. Branch rewards of such branches must coincide.

Definition at line 286 of file UmbTest.cpp.

TEST() [3/3]

TEST	(	UmbTest	,
		RationalEncoding	)

Definition at line 229 of file UmbTest.cpp.