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.

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

Represents a modeling context.


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


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


The scope for global variables and constants.


A set of actions usable in the context.


Automata networks defined in the modeling context.


Properties defined in the modeling context.

property automata

The automata defined in the modeling context.

Return type


class momba.model.Scope(ctx, parent=None)[source]
property clock_declarations

Returns the set of declarations for clock variables.

Return type


declare_constant(identifier, typ, *, value=None, comment=None)[source]

Declare a constant in the scope.

  • 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


class momba.model.ModelType(full_name)[source]

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({}))[source]

Represents a location of a SHA.


The unique name of the location.


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


Assignments for transient variables.

class momba.model.Automaton(ctx, *, name=None)[source]
create_location(name=None, *, progress_invariant=None, transient_values=frozenset({}), initial=False)[source]

Adds a location to the automaton.


location – The Location to add.

Return type



Adds an edge to the automaton.

Return type


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

Creates a new edge with the given parameters.

See Edge for more details.

Return type



Returns the set of outgoing edges from the given location.

Return type



Returns the set of incoming edges to the given location.

Return type


declare_variable(name, typ, *, is_transient=None, initial_value=None)[source]

Declares a variable in the local scope of the automaton.

Return type


declare_parameter(name, typ, *, default_value=None)[source]

Declarse a parameter for the automaton.

Return type


create_instance(*, parameters=(), input_enable=frozenset({}))[source]

Creates an instance of the automaton for composition.

Return type


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

The core class representing a network of interacting SHAs.