Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Classes | Public Member Functions | Static Public Member Functions | Friends | List of all members
storm::builder::DdPrismModelBuilder< Type, ValueType > Class Template Reference

#include <DdPrismModelBuilder.h>

Classes

class  GenerationInformation
 
struct  Options
 
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 1576 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 604 of file DdPrismModelBuilder.cpp.

Friends And Related Symbol Documentation

◆ 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: