storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType > Class Template Reference

#include <ExplicitModelBuilder.h>

Classes
struct	Options

Public Member Functions
	ExplicitModelBuilder (std::shared_ptr< storm::generator::NextStateGenerator< ValueType, StateType > > const &generator, Options const &options=Options())
	Creates an explicit model builder that uses the provided generator.
	ExplicitModelBuilder (storm::prism::Program const &program, storm::generator::NextStateGeneratorOptions const &generatorOptions=storm::generator::NextStateGeneratorOptions(), Options const &builderOptions=Options())
	Creates an explicit model builder for the given PRISM program.
	ExplicitModelBuilder (storm::jani::Model const &model, storm::generator::NextStateGeneratorOptions const &generatorOptions=storm::generator::NextStateGeneratorOptions(), Options const &builderOptions=Options())
	Creates an explicit model builder for the given JANI model.
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	build ()
	Convert the program given at construction time to an abstract model.
ExplicitStateLookup< StateType >	exportExplicitStateLookup () const
	Export a wrapper that contains (a copy of) the internal information that maps states to ids.

Detailed Description

template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >

Definition at line 69 of file ExplicitModelBuilder.h.

Constructor & Destructor Documentation

ExplicitModelBuilder() [1/3]

template<typename ValueType , typename RewardModelType , typename StateType >

storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::ExplicitModelBuilder	(	std::shared_ptr< storm::generator::NextStateGenerator< ValueType, StateType > > const &	generator,
		Options const &	options = Options()
	)

Creates an explicit model builder that uses the provided generator.

Parameters

generator

The generator to use.

Definition at line 68 of file ExplicitModelBuilder.cpp.

ExplicitModelBuilder() [2/3]

template<typename ValueType , typename RewardModelType , typename StateType >

storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::ExplicitModelBuilder	(	storm::prism::Program const &	program,
		storm::generator::NextStateGeneratorOptions const &	generatorOptions = storm::generator::NextStateGeneratorOptions(),
		Options const &	builderOptions = Options()
	)

Creates an explicit model builder for the given PRISM program.

Parameters

program

The program for which to build the model.

Definition at line 75 of file ExplicitModelBuilder.cpp.

ExplicitModelBuilder() [3/3]

template<typename ValueType , typename RewardModelType , typename StateType >

storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::ExplicitModelBuilder	(	storm::jani::Model const &	model,
		storm::generator::NextStateGeneratorOptions const &	generatorOptions = storm::generator::NextStateGeneratorOptions(),
		Options const &	builderOptions = Options()
	)

Creates an explicit model builder for the given JANI model.

Parameters

model

The JANI model for which to build the model.

Definition at line 83 of file ExplicitModelBuilder.cpp.

Member Function Documentation

build()

template<typename ValueType , typename RewardModelType , typename StateType >

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::build

(

)

Convert the program given at construction time to an abstract model.

The type of the model is the one specified in the program. The given reward model name selects the rewards that the model will contain.

Returns

The explicit model that was given by the probabilistic program as well as additional information (if requested).

Definition at line 91 of file ExplicitModelBuilder.cpp.

exportExplicitStateLookup()

template<typename ValueType , typename RewardModelType , typename StateType >

ExplicitStateLookup< StateType > storm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::exportExplicitStateLookup

(

)

const

Export a wrapper that contains (a copy of) the internal information that maps states to ids.

This wrapper can be helpful to find states in later stages.

Returns

Definition at line 140 of file ExplicitModelBuilder.cpp.

---

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

• src/storm/builder/ExplicitModelBuilder.h
• src/storm/builder/ExplicitModelBuilder.cpp