Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::builder::DdPrismModelBuilder< Type, ValueType > Class Template Reference

#include <DdPrismModelBuilder.h>

Classes

struct  Options
class  GenerationInformation
struct  SystemResult

Public Member Functions

std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build (storm::prism::Program const &program, Options const &options=Options())
 Translates the given program into a symbolic model (i.e.

Static Public Member Functions

static bool canHandle (storm::prism::Program const &program)
 A quick check to detect whether the given model is not supported.

Friends

template<storm::dd::DdType TypePrime, typename ValueTypePrime>
class ModuleComposer

Detailed Description

template<storm::dd::DdType Type, typename ValueType = double>
class storm::builder::DdPrismModelBuilder< Type, ValueType >

Definition at line 40 of file DdPrismModelBuilder.h.

Member Function Documentation

◆ build()

template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > storm::builder::DdPrismModelBuilder< Type, ValueType >::build ( storm::prism::Program const & program,
Options const & options = Options() )

Translates the given program into a symbolic model (i.e.

one that stores the transition relation as a decision diagram).

Parameters
programThe program to translate.
Returns
A pointer to the resulting model.

Definition at line 1573 of file DdPrismModelBuilder.cpp.

◆ canHandle()

template<storm::dd::DdType Type, typename ValueType>
bool storm::builder::DdPrismModelBuilder< Type, ValueType >::canHandle ( storm::prism::Program const & program)
static

A quick check to detect whether the given model is not supported.

This method only over-approximates the set of models that can be handled, i.e., if this returns true, the model might still be unsupported.

Definition at line 601 of file DdPrismModelBuilder.cpp.

◆ ModuleComposer

template<storm::dd::DdType Type, typename ValueType = double>
template<storm::dd::DdType TypePrime, typename ValueTypePrime>
friend class ModuleComposer
friend

Definition at line 248 of file DdPrismModelBuilder.h.


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