Shorthand for std::unordered_map<T, uint64_t>. More...

#include <BigStep.h>

Public Member Functions
	BigStep ()
	This class re-orders parameteric transitions of a pMC so bounds computed by Parameter Lifting will eventually be better.

RationalFunction	uniPolyToRationalFunction (UniPoly poly)

std::pair< models::sparse::Dtmc< RationalFunction >, std::map< UniPoly, Annotation > >	bigStep (models::sparse::Dtmc< RationalFunction > const &model, modelchecker::CheckTask< logic::Formula, RationalFunction > const &checkTask)
	Perform big-step on the given model and the given checkTask.

Static Public Attributes
static std::unordered_map< RationalFunction, Annotation >	lastSavedAnnotations

Detailed Description

Shorthand for std::unordered_map<T, uint64_t>.

Counts elements (which elements, how many of them).

Template Parameters

T

Definition at line 176 of file BigStep.h.

Constructor & Destructor Documentation

storm::transformer::BigStep::BigStep ( )

inline

This class re-orders parameteric transitions of a pMC so bounds computed by Parameter Lifting will eventually be better.

The parametric reachability probability for the given check task will be the same in the time-travelled and in the original model.

Definition at line 182 of file BigStep.h.

std::pair< models::sparse::Dtmc< RationalFunction >, std::map< UniPoly, Annotation > > BigStep::bigStep	(	models::sparse::Dtmc< RationalFunction > const &	model,
		modelchecker::CheckTask< logic::Formula, RationalFunction > const &	checkTask
	)

Perform big-step on the given model and the given checkTask.

Parameters

model	A pMC.
checkTask	A property (probability or reward) on the pMC.

Definition at line 393 of file BigStep.cpp.

RationalFunction BigStep::uniPolyToRationalFunction ( UniPoly poly )

Definition at line 47 of file BigStep.cpp.

std::unordered_map< storm::RationalFunction, storm::transformer::Annotation > BigStep::lastSavedAnnotations

static

Definition at line 198 of file BigStep.h.

The documentation for this class was generated from the following files: