storm::test::bisimulation Namespace Reference

Shared helpers for the bisimulation tests, cf. More...

Classes
struct	PrismInput
	The model built from the given PRISM file together with the formulas that the minimization has to preserve. More...
struct	BuildOptions
	What to build from a PRISM program in addition to what the formulas require. More...

Typedefs
using	Options = storm::bisimulation::Options
using	StateLabelPreservation = storm::bisimulation::StateLabelPreservation

Functions
Options	strongOptions ()
Options	weakOptions ()
template<typename ModelType, typename ValueType = typename ModelType::ValueType>
std::shared_ptr< ModelType >	buildModel (storm::storage::SparseMatrix< ValueType > matrix, std::map< std::string, std::vector< uint64_t > > const &labels, std::vector< ValueType > const &stateRewards={}, std::vector< ValueType > const &stateActionRewards={})
	Builds a deterministic model with the given (probability or rate) matrix.
template<typename ValueType = double>
std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > >	buildMarkovAutomaton (storm::storage::SparseMatrix< ValueType > matrix, storm::storage::BitVector markovianStates, std::map< std::string, std::vector< uint64_t > > const &labels)
	Builds a Markov automaton.
template<typename ValueType>
ValueType	checkFormula (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::shared_ptr< storm::logic::Formula const > const &formula)
template<typename ValueType>
ValueType	checkFormula (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &formulaString)
template<typename ValueType>
PrismInput< ValueType >	buildFromPrism (std::string const &prismFile, std::string const &formulaString, BuildOptions const &buildOptions={})

Detailed Description

Shared helpers for the bisimulation tests, cf.

StrongBisimulationTest.cpp and WeakBisimulationTest.cpp.

Typedef Documentation

Options

using storm::test::bisimulation::Options = storm::bisimulation::Options

Definition at line 37 of file BisimulationTestHelper.h.

StateLabelPreservation

using storm::test::bisimulation::StateLabelPreservation = storm::bisimulation::StateLabelPreservation

Definition at line 38 of file BisimulationTestHelper.h.

Function Documentation

buildFromPrism()

template<typename ValueType>

PrismInput< ValueType > storm::test::bisimulation::buildFromPrism	(	std::string const &	prismFile,
		std::string const &	formulaString,
		BuildOptions const &	buildOptions = {} )

Definition at line 148 of file BisimulationTestHelper.h.

buildMarkovAutomaton()

template<typename ValueType = double>

std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > storm::test::bisimulation::buildMarkovAutomaton	(	storm::storage::SparseMatrix< ValueType >	matrix,
		storm::storage::BitVector	markovianStates,
		std::map< std::string, std::vector< uint64_t > > const &	labels )

Builds a Markov automaton.

The rows of matrix that belong to a state in markovianStates hold the transition rates, all other rows hold probabilities. Every entry of labels names a label and lists the states carrying it.

Definition at line 89 of file BisimulationTestHelper.h.

buildModel()

template<typename ModelType, typename ValueType = typename ModelType::ValueType>

std::shared_ptr< ModelType > storm::test::bisimulation::buildModel	(	storm::storage::SparseMatrix< ValueType >	matrix,
		std::map< std::string, std::vector< uint64_t > > const &	labels,
		std::vector< ValueType > const &	stateRewards = {},
		std::vector< ValueType > const &	stateActionRewards = {} )

Builds a deterministic model with the given (probability or rate) matrix.

Every entry of labels names a label and lists the states carrying it. stateRewards and stateActionRewards, if non-empty, are added as a reward model named "rew".

Definition at line 60 of file BisimulationTestHelper.h.

checkFormula() [1/2]

template<typename ValueType>

ValueType storm::test::bisimulation::checkFormula	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::shared_ptr< storm::logic::Formula const > const &	formula )

Returns

the value of the given formula in the (unique) initial state of the given model.

Definition at line 112 of file BisimulationTestHelper.h.

checkFormula() [2/2]

template<typename ValueType>

ValueType storm::test::bisimulation::checkFormula	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	formulaString )

Returns

the value of the given formula in the (unique) initial state of the given model.

Note

the formula is parsed without a model description, so it must not contain atomic expressions.

Definition at line 122 of file BisimulationTestHelper.h.

strongOptions()

Options storm::test::bisimulation::strongOptions ( )

inline

Definition at line 40 of file BisimulationTestHelper.h.

weakOptions()

Options storm::test::bisimulation::weakOptions ( )

inline

Definition at line 47 of file BisimulationTestHelper.h.