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.
- 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)[source]¶ -
property
clock_declarations
¶ Returns the set of declarations for clock variables.
- Return type
AbstractSet
[VariableDeclaration
]
-
declare_constant
(identifier, typ, *, value=None, comment=None)[source]¶ 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
-
property
-
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.
-
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)[source]¶ -
create_location
(name=None, *, progress_invariant=None, transient_values=frozenset({}), initial=False)[source]¶ Adds a location to the automaton.
-
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
None
-
get_incoming_edges
(location)[source]¶ Returns the set of outgoing edges from the given location.
- Return type
AbstractSet
[Edge
]
-
get_outgoing_edges
(location)[source]¶ Returns the set of incoming edges to the given location.
- Return type
AbstractSet
[Edge
]
-
declare_variable
(name, typ, *, is_transient=None, initial_value=None)[source]¶ Declares a variable in the local scope of the automaton.
- Return type
None
-