Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::jani::InformationObject Struct Reference

#include <InformationCollector.h>

Public Member Functions

 InformationObject ()
 

Public Attributes

storm::jani::ModelType modelType
 
uint64_t nrVariables
 The type of the model.
 
uint64_t nrAutomata
 The number of non-transient variables in the model.
 
uint64_t nrEdges
 The number of automata in the model.
 
uint64_t nrLocations
 The number of edges in the model.
 
uint64_t stateDomainSize
 The numer of all locations of all automata of the model.
 
double avgVarDomainSize
 The size of the domain of the states (i.e., the product of the range of all variables times the number of locations).
 

Detailed Description

Definition at line 13 of file InformationCollector.h.

Constructor & Destructor Documentation

◆ InformationObject()

storm::jani::InformationObject::InformationObject ( )

Definition at line 77 of file InformationCollector.cpp.

Member Data Documentation

◆ avgVarDomainSize

double storm::jani::InformationObject::avgVarDomainSize

The size of the domain of the states (i.e., the product of the range of all variables times the number of locations).

Here, 0 means that the state domain size is unknown.

Definition at line 22 of file InformationCollector.h.

◆ modelType

storm::jani::ModelType storm::jani::InformationObject::modelType

Definition at line 15 of file InformationCollector.h.

◆ nrAutomata

uint64_t storm::jani::InformationObject::nrAutomata

The number of non-transient variables in the model.

Definition at line 17 of file InformationCollector.h.

◆ nrEdges

uint64_t storm::jani::InformationObject::nrEdges

The number of automata in the model.

Definition at line 18 of file InformationCollector.h.

◆ nrLocations

uint64_t storm::jani::InformationObject::nrLocations

The number of edges in the model.

Definition at line 19 of file InformationCollector.h.

◆ nrVariables

uint64_t storm::jani::InformationObject::nrVariables

The type of the model.

Definition at line 16 of file InformationCollector.h.

◆ stateDomainSize

uint64_t storm::jani::InformationObject::stateDomainSize

The numer of all locations of all automata of the model.

Definition at line 20 of file InformationCollector.h.


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