Momba Models

The package momba.model contains the core data-structures for the representation of quantitative models. Essentially, a Momba model is a network of interacting stochastic hybrid automata (SHA) as per the JANI specification. At the heart of every model is a modeling context represented by a Context-object. The modeling context specifies the model type (see ModelType for an overview) and allows the definition of constants, variables, automata, and automata networks.

Individual SHAs are implemented by momba.model.Automaton. SHAs are built from a finite set of locations connected via edges. SHAs, as we understand them, are models with variables. A valuation maps variables to values. Each edge leads from a single source location via a guard and an action to a symbolic probability distribution over variable assignments and successor locations.

• Expressions

class momba.model.Context(model_type=<ModelType.SHA: 'Stochastic Hybrid Automaton'>)

Represents a modeling context.

Parameters

model_type (ModelType) – The model type to use for the context.

model_type

The type of the model, e.g., SHA, PTA or MDP.

global_scope

The scope for global variables and constants.

actions

A set of actions usable in the context.

networks

Automata networks defined in the modeling context.

properties

Properties defined in the modeling context.

property automata

The automata defined in the modeling context.

Return type

AbstractSet[Automaton]

class momba.model.Scope(ctx, parent=None)

property clock_declarations

Returns the set of declarations for clock variables.

Return type

AbstractSet[VariableDeclaration]

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

Declare a constant in the scope.

Parameters

• identifier (str) – The name of the constant to declare.

• typ (types.Type) – The type of the constant.

• value (Union[bool, int, Real, float, Literal[‘π’, ‘e’], NamedReal, Expression, None]) – The value of the constant. If none is provided, the constant becomes a parameter of the model.

• comment (Optional[str]) – An optional comment describing the constant.

Return type

None

class momba.model.ModelType(full_name)

Type of the model.

LTS = 'Labeled Transition System'

DTMC = 'Discrete-Time Markov Chain'

CTMC = 'Continuous-Time Markov Chain'

MDP = 'Markov Decision Process'

CTMDP = 'Continuous-Time Markov Decision Process'

MA = 'Markov Automaton'

TA = 'Timed Automaton'

PTA = 'Probabilistic Timed Automaton'

STA = 'Stochastic Timed Automaton'

HA = 'Hybrid Automaton'

PHA = 'Probabilistic Timed Automaton'

SHA = 'Stochastic Hybrid Automaton'

full_name: str

class momba.model.Location(name: Optional[str] = None, progress_invariant: Optional[expressions.Expression] = None, transient_values: AbstractSet[momba.model.effects.Assignment] = frozenset({}))

Represents a location of a SHA.

name

The unique name of the location.

progress_invariant

The time-progression invariant of the location. Has to be a boolean expression in the scope the location is used.

transient_values

Assignments for transient variables.

class momba.model.Automaton(ctx, *, name=None)

create_location(name=None, *, progress_invariant=None, transient_values=frozenset({}), initial=False)

Adds a location to the automaton.

Parameters

location – The Location to add.

Return type

Location

add_edge(edge)

Adds an edge to the automaton.

Return type

None

create_edge(source, destinations, *, action_pattern=None, guard=None, rate=None)

Creates a new edge with the given parameters.

See Edge for more details.

Return type

None

get_incoming_edges(location)

Returns the set of outgoing edges from the given location.

Return type

AbstractSet[Edge]

get_outgoing_edges(location)

Returns the set of incoming edges to the given location.

Return type

AbstractSet[Edge]

declare_variable(name, typ, *, is_transient=None, initial_value=None)

Declares a variable in the local scope of the automaton.

Return type

None

declare_parameter(name, typ, *, default_value=None)

Declarse a parameter for the automaton.

Return type

None

create_instance(*, parameters=(), input_enable=frozenset({}))

Creates an instance of the automaton for composition.

Return type

Instance

class momba.model.Network(ctx, *, name=None)

The core class representing a network of interacting SHAs.