JaniLocalEliminatorTests.cpp File Reference

#include <storm-parsers/parser/FormulaParser.h>
#include <storm-parsers/parser/JaniParser.h>
#include <storm/api/storm.h>
#include <storm/builder/ExplicitModelBuilder.h>
#include <storm/modelchecker/results/ExplicitQuantitativeCheckResult.h>
#include <storm/settings/modules/GeneralSettings.h>
#include "storm-parsers/api/model_descriptions.h"
#include "storm/environment/Environment.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/ModelFeatures.h"
#include "storm/storage/jani/Property.h"
#include "storm/storage/jani/localeliminator/EliminateAction.h"
#include "storm/storage/jani/localeliminator/JaniLocalEliminator.h"
#include "storm/storage/jani/localeliminator/RebuildWithoutUnreachableAction.h"
#include "storm/storage/jani/localeliminator/UnfoldAction.h"
#include "test/storm_gtest.h"

Include dependency graph for JaniLocalEliminatorTests.cpp:

Go to the source code of this file.

Classes
class	JaniLocalElimination

Typedefs
typedef storm::models::sparse::Dtmc< double >	Dtmc
typedef storm::models::sparse::Mdp< double >	Mdp
typedef storm::modelchecker::SparseDtmcPrctlModelChecker< Dtmc >	DtmcModelChecker
typedef storm::modelchecker::SparseMdpPrctlModelChecker< Dtmc >	MdpModelChecker

Functions
void	checkModel (storm::jani::Model model, std::vector< storm::jani::Property > properties, std::map< storm::expressions::Variable, storm::expressions::Expression > consts, double expectedValue)
	TEST_F (JaniLocalElimination, PropertyTypeTest)
	TEST_F (JaniLocalElimination, NoPropertiesTest)
	TEST_F (JaniLocalElimination, FlatteningTest)
	TEST_F (JaniLocalElimination, MissingGuardCompletion)
	TEST_F (JaniLocalElimination, LoopDetection)
	TEST_F (JaniLocalElimination, IsPartOfPropComputation)
	TEST_F (JaniLocalElimination, IsInitialDetection)
	TEST_F (JaniLocalElimination, IsEliminableDetection)
	TEST_F (JaniLocalElimination, IsVariablePartOfProperty)
	TEST_F (JaniLocalElimination, UnfoldingBoundedInteger)
	TEST_F (JaniLocalElimination, UnfoldingBoolean)
	TEST_F (JaniLocalElimination, UnfoldingTwice)
	TEST_F (JaniLocalElimination, UnfoldingWithSink)
	TEST_F (JaniLocalElimination, IsPartOfPropPropagationUnfolding)
	TEST_F (JaniLocalElimination, EliminationNewGuardTest)
	TEST_F (JaniLocalElimination, EliminationNewProbabilityTest)
	TEST_F (JaniLocalElimination, EliminationNewUpdatesTest)
	TEST_F (JaniLocalElimination, EliminationMultipleEdges)
	TEST_F (JaniLocalElimination, EliminationMultiplicityTest)

Typedef Documentation

Dtmc

typedef storm::models::sparse::Dtmc<double> Dtmc

Definition at line 20 of file JaniLocalEliminatorTests.cpp.

DtmcModelChecker

typedef storm::modelchecker::SparseDtmcPrctlModelChecker<Dtmc> DtmcModelChecker

Definition at line 22 of file JaniLocalEliminatorTests.cpp.

Mdp

typedef storm::models::sparse::Mdp<double> Mdp

Definition at line 21 of file JaniLocalEliminatorTests.cpp.

MdpModelChecker

typedef storm::modelchecker::SparseMdpPrctlModelChecker<Dtmc> MdpModelChecker

Definition at line 23 of file JaniLocalEliminatorTests.cpp.

Function Documentation

checkModel()

void checkModel	(	storm::jani::Model	model,
		std::vector< storm::jani::Property >	properties,
		std::map< storm::expressions::Variable, storm::expressions::Expression >	consts,
		double	expectedValue
	)

Definition at line 52 of file JaniLocalEliminatorTests.cpp.

TEST_F() [1/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultipleEdges
	)

Definition at line 469 of file JaniLocalEliminatorTests.cpp.

TEST_F() [2/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultiplicityTest
	)

Definition at line 489 of file JaniLocalEliminatorTests.cpp.

TEST_F() [3/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewGuardTest
	)

Definition at line 409 of file JaniLocalEliminatorTests.cpp.

TEST_F() [4/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewProbabilityTest
	)

Definition at line 428 of file JaniLocalEliminatorTests.cpp.

TEST_F() [5/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewUpdatesTest
	)

Definition at line 448 of file JaniLocalEliminatorTests.cpp.

TEST_F() [6/19]

TEST_F	(	JaniLocalElimination	,
		FlatteningTest
	)

Definition at line 129 of file JaniLocalEliminatorTests.cpp.

TEST_F() [7/19]

TEST_F	(	JaniLocalElimination	,
		IsEliminableDetection
	)

Definition at line 288 of file JaniLocalEliminatorTests.cpp.

TEST_F() [8/19]

TEST_F	(	JaniLocalElimination	,
		IsInitialDetection
	)

Definition at line 230 of file JaniLocalEliminatorTests.cpp.

TEST_F() [9/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropComputation
	)

Definition at line 185 of file JaniLocalEliminatorTests.cpp.

TEST_F() [10/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropPropagationUnfolding
	)

Definition at line 400 of file JaniLocalEliminatorTests.cpp.

TEST_F() [11/19]

TEST_F	(	JaniLocalElimination	,
		IsVariablePartOfProperty
	)

Definition at line 313 of file JaniLocalEliminatorTests.cpp.

TEST_F() [12/19]

TEST_F	(	JaniLocalElimination	,
		LoopDetection
	)

Definition at line 161 of file JaniLocalEliminatorTests.cpp.

TEST_F() [13/19]

TEST_F	(	JaniLocalElimination	,
		MissingGuardCompletion
	)

Definition at line 144 of file JaniLocalEliminatorTests.cpp.

TEST_F() [14/19]

TEST_F	(	JaniLocalElimination	,
		NoPropertiesTest
	)

Definition at line 120 of file JaniLocalEliminatorTests.cpp.

TEST_F() [15/19]

TEST_F	(	JaniLocalElimination	,
		PropertyTypeTest
	)

Definition at line 80 of file JaniLocalEliminatorTests.cpp.

TEST_F() [16/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoolean
	)

Definition at line 356 of file JaniLocalEliminatorTests.cpp.

TEST_F() [17/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoundedInteger
	)

Definition at line 339 of file JaniLocalEliminatorTests.cpp.

TEST_F() [18/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingTwice
	)

Definition at line 373 of file JaniLocalEliminatorTests.cpp.

TEST_F() [19/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingWithSink
	)

Definition at line 388 of file JaniLocalEliminatorTests.cpp.