Storm
A Modern Probabilistic Model Checker
|
#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). | |
Definition at line 13 of file InformationCollector.h.
storm::jani::InformationObject::InformationObject | ( | ) |
Definition at line 77 of file InformationCollector.cpp.
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.
storm::jani::ModelType storm::jani::InformationObject::modelType |
Definition at line 15 of file InformationCollector.h.
uint64_t storm::jani::InformationObject::nrAutomata |
The number of non-transient variables in the model.
Definition at line 17 of file InformationCollector.h.
uint64_t storm::jani::InformationObject::nrEdges |
The number of automata in the model.
Definition at line 18 of file InformationCollector.h.
uint64_t storm::jani::InformationObject::nrLocations |
The number of edges in the model.
Definition at line 19 of file InformationCollector.h.
uint64_t storm::jani::InformationObject::nrVariables |
The type of the model.
Definition at line 16 of file InformationCollector.h.
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.