#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/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 22 of file JaniLocalEliminatorTests.cpp.

◆ DtmcModelChecker

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

Definition at line 24 of file JaniLocalEliminatorTests.cpp.

◆ Mdp

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

Definition at line 23 of file JaniLocalEliminatorTests.cpp.

◆ MdpModelChecker

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

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

◆ TEST_F() [1/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultipleEdges	)

Definition at line 471 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [2/19]

TEST_F	(	JaniLocalElimination	,
		EliminationMultiplicityTest	)

Definition at line 491 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [3/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewGuardTest	)

Definition at line 411 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [4/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewProbabilityTest	)

Definition at line 430 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [5/19]

TEST_F	(	JaniLocalElimination	,
		EliminationNewUpdatesTest	)

Definition at line 450 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [6/19]

TEST_F	(	JaniLocalElimination	,
		FlatteningTest	)

Definition at line 131 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [7/19]

TEST_F	(	JaniLocalElimination	,
		IsEliminableDetection	)

Definition at line 290 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [8/19]

TEST_F	(	JaniLocalElimination	,
		IsInitialDetection	)

Definition at line 232 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [9/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropComputation	)

Definition at line 187 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [10/19]

TEST_F	(	JaniLocalElimination	,
		IsPartOfPropPropagationUnfolding	)

Definition at line 402 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [11/19]

TEST_F	(	JaniLocalElimination	,
		IsVariablePartOfProperty	)

Definition at line 315 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [12/19]

TEST_F	(	JaniLocalElimination	,
		LoopDetection	)

Definition at line 163 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [13/19]

TEST_F	(	JaniLocalElimination	,
		MissingGuardCompletion	)

Definition at line 146 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [14/19]

TEST_F	(	JaniLocalElimination	,
		NoPropertiesTest	)

Definition at line 122 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [15/19]

TEST_F	(	JaniLocalElimination	,
		PropertyTypeTest	)

Definition at line 82 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [16/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoolean	)

Definition at line 358 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [17/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingBoundedInteger	)

Definition at line 341 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [18/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingTwice	)

Definition at line 375 of file JaniLocalEliminatorTests.cpp.

◆ TEST_F() [19/19]

TEST_F	(	JaniLocalElimination	,
		UnfoldingWithSink	)

Definition at line 390 of file JaniLocalEliminatorTests.cpp.

Classes

Typedefs

Functions