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 0x7fb860900d60>

class momba.model.Context(model_type)

Represents a modeling context.

model_type

The ModelType of the modeling context.

global_scope

The global Scope of the 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.

update_metadata(metadata)

Updates the metadata with the provided mapping.

get_automaton_by_name(name)

Retrieves an automaton by its name.

Raises NotFoundError if no such automaton exists.

get_network_by_name(name)

Retrives a network by its name.

Raises NotFoundError if no such network exists.

get_property_definition_by_name(name)

Retrieves a property definition by its name.

Raises NotFoundError if no such property definition exists.

get_action_type_by_name(name)

Retrives an action type by its name.

Raises NotFoundError if no such action type exists.

create_action_type(name, *, parameters=())

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)

Creates an automaton with the given optional name and returns it.

create_network(*, name=None)

Creates a network with the given optional name and returns it.

define_property(name, expression)

Defines a property on the modeling context.

The different model types are represented by an enum:

class momba.model.ModelType(value)

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, and MDP.

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)

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.

create_child_scope()

Creates a child scope.

get_type(expr)

Returns the (inferred) type of the given expression in the scope.

get_function(name)

Retrieves a FunctionDefinition by its name.

Raises NotFoundError if no such definition exists.

is_local(identifier)

Checks whether the identifier is locally declared in the scope.

is_declared(identifier)

Checks whether the identifier is declared in the scope.

get_scope(identifier)

Retrieves the scope in which the given identifier is declared.

Raises NotFoundError if no such identifier is declared.

lookup(identifier)

Retrieves the declaration for the given identifier.

Raises NotFoundError if no such identifier is declared.

add_declaration(declaration, *, validate=True)

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)

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 using ensure_expr().

Raises ModelingError in case the identifier has already been declared.

declare_constant(identifier, typ, *, value=None, comment=None)

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 using ensure_expr().

Raises ModelingError in case the identifier has already been declared.

define_function(name, parameters, returns, body)

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)

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)

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)

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)

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)

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)

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.

class momba.model.PropertyDefinition(name, expression, comment=None)

Represents a property definition.

name

The name of the property.

expression

An Expression defining the property.

comment

An optional comment describing the property.