storm::transformer::TimeTravelling Class Reference

#include <TimeTravelling.h>

Public Member Functions
	TimeTravelling ()=default
	This class re-orders parameteric transitions of a pMC so bounds computed by Parameter Lifting will eventually be better.
models::sparse::Dtmc< RationalFunction >	timeTravel (models::sparse::Dtmc< RationalFunction > const &model, modelchecker::CheckTask< logic::Formula, RationalFunction > const &checkTask)
	Perform time-travelling on the given model and the given checkTask.

Detailed Description

Definition at line 15 of file TimeTravelling.h.

Constructor & Destructor Documentation

TimeTravelling()

storm::transformer::TimeTravelling::TimeTravelling ( )

default

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.

Member Function Documentation

timeTravel()

models::sparse::Dtmc< RationalFunction > TimeTravelling::timeTravel	(	models::sparse::Dtmc< RationalFunction > const &	model,
		modelchecker::CheckTask< logic::Formula, RationalFunction > const &	checkTask
	)

Perform time-travelling on the given model and the given checkTask.

Parameters

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

Returns

models::sparse::Dtmc<RationalFunction> The time-travelled pMC.

Definition at line 37 of file TimeTravelling.cpp.

---

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

• src/storm-pars/transformer/TimeTravelling.h
• src/storm-pars/transformer/TimeTravelling.cpp