#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm-parsers/parser/JaniParser.h"
#include "storm/api/storm.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/environment/Environment.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.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 dependency graph for JaniLocalEliminatorTests.cpp:

Classes
class	JaniLocalElimination
class	JaniLocalEliminator

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 23 of file JaniLocalEliminatorTests.cpp.

◆ DtmcModelChecker

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

Definition at line 25 of file JaniLocalEliminatorTests.cpp.

◆ Mdp

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

Definition at line 24 of file JaniLocalEliminatorTests.cpp.

◆ MdpModelChecker

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

Definition at line 26 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 55 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [1/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultipleEdges	)

Definition at line 472 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [2/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultiplicityTest	)

Definition at line 492 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [3/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewGuardTest	)

Definition at line 412 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [4/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewProbabilityTest	)

Definition at line 431 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [5/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewUpdatesTest	)

Definition at line 451 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [6/19]

TEST_F	(	JaniLocalElimination	,
		FlatteningTest	)

Definition at line 132 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [7/19]

TEST_F	(	JaniLocalElimination	,
		IsEliminableDetection	)

Definition at line 291 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [8/19]

TEST_F	(	JaniLocalElimination	,
		IsInitialDetection	)

Definition at line 233 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [9/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropComputation	)

Definition at line 188 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [10/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropPropagationUnfolding	)

Definition at line 403 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [11/19]

TEST_F	(	JaniLocalElimination	,
		IsVariablePartOfProperty	)

Definition at line 316 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [12/19]

TEST_F	(	JaniLocalElimination	,
		LoopDetection	)

Definition at line 164 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [13/19]

TEST_F	(	JaniLocalElimination	,
		MissingGuardCompletion	)

Definition at line 147 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [14/19]

TEST_F	(	JaniLocalElimination	,
		NoPropertiesTest	)

Definition at line 123 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [15/19]

TEST_F	(	JaniLocalElimination	,
		PropertyTypeTest	)

Definition at line 83 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [16/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoolean	)

Definition at line 359 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [17/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoundedInteger	)

Definition at line 342 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [18/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingTwice	)

Definition at line 376 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [19/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingWithSink	)

Definition at line 391 of file JaniLocalEliminatorTests.cpp.

Classes

Typedefs

Functions