Automata

Automata are a core concept of the JANI modeling formalism. An automaton is defined by a set of locations connected via edges. Creating an automaton requires a Context. We recommend constructing automata via the method create_automaton() of the respective modeling context:

from momba import model

# creates a *Probabilistic Timed Automata* (PTA) modeling context
ctx = model.Context(model.ModelType.PTA)
# let's create an automaton named *environment*
environment = ctx.create_automaton(name="environment")
environment

<Automaton name='environment' at 0x7f10fcae3f70>

Warning

Automata in Momba support parameters. This feature, however, is not part of the official JANI specification. In case you want your model to work with a broad variety of tools do not add any parameters to your automata.

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

Represents an automaton.

ctx

The Context associated with the automaton.

scope

The local Scope of the automaton.

name

The optional name of the automaton.

property locations

The set of locations of the automaton.

property initial_locations

The set of initial locations of the automaton.

property edges

The set of edges of the automaton.

property initial_restriction

An optional restriction to be satisfied by initial states.

This property can be set only once per automaton. The expression has to be boolean.

Raises ModelingError when set twice or to a non-boolean expression.

property parameters

The sequence of parameters of the automaton.

add_location(location, *, initial=False)

Adds a location to the automaton.

The flag initial specifies whether the location is an initial location.

Raises ModelingError when the location cannot be added to the automaton. See the method Location.validate() for details.

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

Creates a location with the given name and adds it to the automaton.

The optional expression progress_invariant specifies the invariant subject to which the time may progress in the location. As per the JANI specification, the invariant is only allowed for models using real-valued clocks (see ModelType).

The parameter transient_values should be a set of assignments for transient variables. These assignments define the values of the transient variables when in the location.

The flag initial specifies whether the location is an initial location.

Raises the same exceptions as add_location().

add_edge(edge)

Adds an edge to the automaton.

Raises ModelingError when the edge cannot be added to the automaton. See the method Edge.validate() for details.

create_edge(source, destinations, *, action_pattern=None, guard=None, rate=None, annotation=None, observations=frozenset({}))

Creates an edge and adds it to the automaton.

The parameters are passed to Edge.

Raises the same exceptions as add_edge().

get_incoming_edges(location)

Returns the set of outgoing edges from the given location.

get_outgoing_edges(location)

Returns the set of incoming edges to the given location.

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

Declares a variable in the local scope of the automaton.

Passes the parameters to Scope.declare_variable().

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

Declarse a parameter of the automaton.

Passes the parameters to Scope.declare_constant() where value is default_value.

create_instance(*, arguments=(), input_enable=frozenset({}), comment=None)

Creates an instance of the automaton for composition.

Passes the parameters to Instance.

Locations

class momba.model.Location(name=None, progress_invariant=None, transient_values=frozenset({}))

Represents a location of an automaton.

name

The optional name of the location.

progress_invariant

An optional expression progress_invariant specifies the invariant subject to which the time may progress in the location. As per the JANI specification, the invariant is only allowed for models using real-valued clocks (see ModelType).

transient_values

A set of assignments for transient variables. These assignments define the values of the transient variables when in the location.

validate(automaton)

Validates the location for the given automaton.

Raises ModelingError if the location is invalid to add to the automaton according to the JANI specification. For instance, if the location has a progress_invariant but the model type does not support clocks.

Edges

class momba.model.Edge(location, destinations, action_pattern=None, guard=None, rate=None, annotation=None, observation=frozenset({}))

Represents an edge of an automaton.

location

The source location of the edge.

destinations

The destinations of the edge.

action_pattern

The optional action pattern of the edge.

guard

The optional guard of the edge.

rate

The optional rate of the edge.

annotation

An optional annotation of the edge.

create_edge_scope(parent)

Creates an edge scope with the given parent scope.

Warning

Used for value passing an experimental Momba feature. Value passing is not part of the official JANI specification.

validate(automaton)

Validates the edge for the given automaton.

Raises ModelingError if the edge is invalid to add to the automaton according to the JANI specification. For instance, if source location is not a location of the automaton.

class momba.model.Destination(location, probability=None, assignments=())

Represents a destination of an edge.

location

The target location of the destination.

probability

An optional expression for the probability of the destination.

assignments

A set of assignments to be executed when going to the destination.

momba.model.create_destination(location, *, probability=None, assignments=())

Creates a destination with the given target location.

This is a convenience function for creating destinations where assignments can be provied as a mapping. We recommend using it instead of creating Destination objects directly.

class momba.model.Assignment(target, value, index=0)

Represents an assignment.

target

The target of the assignment.

value

The value to assign.

index

The index of the assignment.

validate(scope)

Validates the assignment in the given scope.

Raises ModelingError if the target is not assignable from the value type.

momba.model.automata.are_compatible(assignments)

Checks whether the given assignments are compatible according to the JANI specification.

Instances

class momba.model.Instance(automaton, arguments=(), input_enable=frozenset({}), comment=None)

Represents an automaton instance.

automaton

The instaniated automaton.

arguments

The arguments passed to the parameters of the automaton.

input_enabled

The set of action types for which the instance is input enabled.

comment

An optional comment describing the instance.