Context
Contents
Context¶
At the heart of every model is a modeling context of a specific model type. Every modeling context can hold several automata and automata networks comprised of these automata.
A modeling context is created as follows proving a model type:
from momba import model
# creates a *Probabilistic Timed Automata* (PTA) modeling context
ctx = model.Context(model.ModelType.PTA)
ctx
<Context model_type=ModelType.PTA at 0x7ff05820b2e0>
- class momba.model.Context(model_type)[source]¶
Represents a modeling context.
- property automata¶
The set of automata defined on the modeling context.
- property networks¶
The set of networks defined on the modeling context.
- property metadata¶
Additional metadata associated with the modeling context (e.g., author information).
- property action_types¶
The action types defined on the modeling context.
- property properties¶
The properties defined on the modeling context.
- get_automaton_by_name(name)[source]¶
Retrieves an automaton by its name.
Raises
NotFoundError
if no such automaton exists.
- get_network_by_name(name)[source]¶
Retrives a network by its name.
Raises
NotFoundError
if no such network exists.
- get_property_definition_by_name(name)[source]¶
Retrieves a property definition by its name.
Raises
NotFoundError
if no such property definition exists.
- get_action_type_by_name(name)[source]¶
Retrives an action type by its name.
Raises
NotFoundError
if no such action type exists.
- create_action_type(name, *, parameters=())[source]¶
Creates a new action type with the given name and parameters.
Raises
ModelingError
if an identically named action type already exists.
- create_automaton(*, name=None)[source]¶
Creates an automaton with the given optional name and returns it.
The different model types are represented by an enum:
- class momba.model.ModelType(value)[source]¶
An enum representing different model types.
- full_name¶
The full human-readable name of the model type.
- CTMC = 'Continuous-Time Markov Chain'¶
Continuous-Time Markov Chain
- CTMDP = 'Continuous-Time Markov Decision Process'¶
Continuous-Time Markov Decision Process
- DTMC = 'Discrete-Time Markov Chain'¶
Discrete-Time Markov Chain
- HA = 'Hybrid Automaton'¶
Hybrid Automaton
- LTS = 'Labeled Transition System'¶
Labeled Transition System
- MA = 'Markov Automaton'¶
Markov Automaton
- MDP = 'Markov Decision Process'¶
Markov Decision Process
- PHA = 'Probabilistic Hybrid Automaton'¶
Probabilistic Hybrid Automaton
- PTA = 'Probabilistic Timed Automaton'¶
Probabilistic Timed Automaton
- SHA = 'Stochastic Hybrid Automaton'¶
Stochastic Hybrid Automaton
- STA = 'Stochastic Timed Automaton'¶
Stochastic Timed Automaton
- TA = 'Timed Automaton'¶
Timed Automaton
- property is_untimed¶
Returns
True
if and only if the model type is not timed.Untimed model types are
LTS
,DTMC
, andMDP
.
- property uses_clocks¶
Returns
True
if and only if the respective models use real-value clocks.
Scope¶
Variables and constants are declared in a scope.
There is one global scope associated with each modeling context (see attribute global_scope
).
In addition, each automaton has its own local scope.
Scopes can be nested enabling access to identifies declared in a parent scope within a child scope.
For instance, the local scopes of automata defined on a modeling context are children of the global scope of the respective context enabling access to both local and global variables and constants.
- class momba.model.Scope(ctx, parent=None)[source]¶
Represents a scope.
- ctx¶
The modeling context associated with the scope.
- parent¶
The parent scope if it exists (
None
if there is no parent).
- property declarations¶
Variable and constant declarations of the scope.
- property variable_declarations¶
Variable declarations of the scope.
- property constant_declarations¶
Constant declarations of the scope.
- property clock_declarations¶
Variable declarations of clock variables of the scope.
- get_function(name)[source]¶
Retrieves a
FunctionDefinition
by its name.Raises
NotFoundError
if no such definition exists.
- get_scope(identifier)[source]¶
Retrieves the scope in which the given identifier is declared.
Raises
NotFoundError
if no such identifier is declared.
- lookup(identifier)[source]¶
Retrieves the declaration for the given identifier.
Raises
NotFoundError
if no such identifier is declared.
- add_declaration(declaration, *, validate=True)[source]¶
Adds an identifier declaration to the scope.
The flag validate specifies whether the declaration should be validated within the scope before adding it. In case validation fails, a
ModelingError
is raised.Raises
ModelingError
in case the identifier has already been declared.
- declare_variable(identifier, typ, *, is_transient=None, initial_value=None, comment=None)[source]¶
Declares a variable within the scope.
The parameters are passed to
VariableDeclaration
with the exception of initial_value. When provided with a value which is not an expressions, this function implicitly converts the provided value into an expression usingensure_expr()
.Raises
ModelingError
in case the identifier has already been declared.
- declare_constant(identifier, typ, *, value=None, comment=None)[source]¶
Declares a constant within the scope.
The parameters are passed to
ConstantDeclaration
with the exception of value. When provided with a value which is not an expressions, this function implicitly converts the provided value into an expression usingensure_expr()
.Raises
ModelingError
in case the identifier has already been declared.
- define_function(name, parameters, returns, body)[source]¶
Defines a function within the scope.
The parameters are passed to
FunctionDefinition
.Raises
ModelingError
in case an identically named function already exists.
Declarations¶
There are two kinds of identifier declarations, variable declarations and constant declarations.
Every identifier declaration declares a particular identifier with a specified Type
.
- class momba.model.IdentifierDeclaration(identifier, typ, comment=None)[source]¶
Represents a declaration of an identifier.
- identifier¶
The declared identifier.
- typ¶
The type of the identifier.
- comment¶
An additional optional comment for the declaration.
- validate(scope)[source]¶
Validates that the declaration is valid in the given scope.
Raises
ModelingError
if the declaration is invalid.
- class momba.model.VariableDeclaration(identifier, typ, comment=None, is_transient=None, initial_value=None)[source]¶
Represents a variable declaration.
- is_transient¶
Optional boolean flag indicating whether the variable is transient.
- initial_value¶
Optional
Expression
providing an initial value for the variable.
- validate(scope)[source]¶
Validates that the declaration is valid in the given scope.
Raises
ModelingError
if the declaration is invalid.
- class momba.model.ConstantDeclaration(identifier, typ, comment=None, value=None)[source]¶
Represents a constant declaration.
- value¶
Optional
Expression
specifying the value of the constant.
- property is_parameter¶
Returns
True
if and only if the constant is a parameter.Parameters are constants without a
value
.
- validate(scope)[source]¶
Validates that the declaration is valid in the given scope.
Raises
ModelingError
if the declaration is invalid.
Properties¶
Every modeling context may have several property definitions attached to it.