#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/graph.h"
#include "storm/utility/shortestPaths.h"

Include dependency graph for KSPTest.cpp:

Classes
class	KSPTest

Functions
std::shared_ptr< storm::models::sparse::Model< double > >	buildExampleModel ()
	TEST_F (KSPTest, dijkstra)
	TEST_F (KSPTest, singleTarget)
	TEST_F (KSPTest, reentry)
	TEST_F (KSPTest, groupTarget)
	TEST_F (KSPTest, kTooLargeException)
	TEST_F (KSPTest, kspStateSet)
	TEST_F (KSPTest, kspPathAsList)

Variables
const storm::utility::ksp::state_t	testState = 296
const storm::utility::ksp::state_t	stateWithOnlyOnePath = 1

Function Documentation

◆ buildExampleModel()

std::shared_ptr< storm::models::sparse::Model< double > > buildExampleModel ( )

Definition at line 25 of file KSPTest.cpp.

◆ TEST_F() [1/7]

TEST_F	(	KSPTest	,
		dijkstra	)

Definition at line 38 of file KSPTest.cpp.

◆ TEST_F() [2/7]

TEST_F	(	KSPTest	,
		groupTarget	)

Definition at line 66 of file KSPTest.cpp.

◆ TEST_F() [3/7]

TEST_F	(	KSPTest	,
		kspPathAsList	)

Definition at line 105 of file KSPTest.cpp.

◆ TEST_F() [4/7]

TEST_F	(	KSPTest	,
		kspStateSet	)

Definition at line 88 of file KSPTest.cpp.

◆ TEST_F() [5/7]

TEST_F	(	KSPTest	,
		kTooLargeException	)

Definition at line 81 of file KSPTest.cpp.

◆ TEST_F() [6/7]

TEST_F	(	KSPTest	,
		reentry	)

Definition at line 54 of file KSPTest.cpp.

◆ TEST_F() [7/7]

TEST_F	(	KSPTest	,
		singleTarget	)

Definition at line 46 of file KSPTest.cpp.

Variable Documentation

◆ stateWithOnlyOnePath

const storm::utility::ksp::state_t stateWithOnlyOnePath = 1

Definition at line 36 of file KSPTest.cpp.

◆ testState

const storm::utility::ksp::state_t testState = 296

Definition at line 35 of file KSPTest.cpp.

Classes

Functions

Variables