Exploration Engine

Momba comes with its own state space exploration engine. To use this engine, you have to install the optional dependency momba_engine (or install Momba with the all feature flag). The API of the package momba_engine itself is private. Here, we document the public API exposed as part of Momba.

Example

First, an Explorer has to be created for the network:

import pathlib

from momba import engine, jani

# let's load a model from the QVBS
path = pathlib.Path("tests/resources/QVBS2019/benchmarks/mdp/firewire/firewire.true.jani")
network = jani.load_model(path.read_text("utf-8"))

# create a discrete time explorer for the loaded network
explorer = engine.Explorer.new_discrete_time(
    network,
    parameters={
        "delay": 3,
        "deadline": 200,
    }
)
explorer
<momba.engine.explore.Explorer at 0x7faa3069b3a0>

We can then use the created explorer to explore the state space of the model.

Let us start by querying the initial states of the model:

initial_states = explorer.initial_states
len(initial_states)
1

There is just one initial state, let’s have a closer look at it:

(initial_state,) = initial_states

We can easily inspect the global environment

initial_state.global_env
{'w12': Value(0),
 'y1': Value(0),
 'y2': Value(0),
 'x1': Value(0),
 's1': Value(0),
 'w21': Value(0),
 'z1': Value(0),
 'z2': Value(0),
 'x2': Value(0),
 's2': Value(0),
 't': Value(0)}

the locations the different automata instances are in

for instance, location in initial_state.locations.items():
    print(f"{instance.automaton.name}: {location.name}")
node1: l
wire12: l
wire21: l
node2: l
timer: l

and also the local environment of each instance (in this case there are no local variables):

for instance in network.instances:
    print(instance.automaton.name)
    print(initial_state.get_local_env(instance))
node1
{}
wire12
{}
wire21
{}
node2
{}
timer
{}

So, let’s explore the successors of the initial state initial_state. To this end, we query the outgoing transitions of the initial state and their respective destinations:

for transition in initial_state.transitions:
    if transition.action is None:
        # the action of the transition is internal
        print("Action: τ")
    else:
        print(f"Action: {transition.action.action_type.label}")
    for destination in transition.destinations.support:
        print(f"  With p={destination.probability} to {destination}.")
Action: snd_idle21
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faa20fdf5b0>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faa20fdf640>.
Action: snd_idle12
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faa20fdfa30>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faa20fdfa90>.

Let’s chose a transition uniformly and then pick a successor state at random:

import random

transition = random.choice(initial_state.transitions)
print(f"Action: {transition.action.action_type.label}")

successor = transition.destinations.pick().state

successor.global_env
Action: snd_idle21
{'w12': Value(0),
 'y1': Value(0),
 'y2': Value(0),
 'x1': Value(0),
 's1': Value(0),
 'w21': Value(5),
 'z1': Value(0),
 'z2': Value(0),
 'x2': Value(0),
 's2': Value(2),
 't': Value(0)}

Reference

class momba.engine.Value(_value)[source]

Represents a value.

property as_array

Asserts that the value is an array and returns a tuple of values.

property as_bool

Asserts that the value is a boolean and returns the boolean.

property as_float

Asserts that the value is a float and returns the float.

property as_int

Asserts that the value is an integer and returns the integer.

property is_array

Returns True if the value is an array.

property is_bool

Returns True if the value is a boolean.

property is_float

Returns True if the value is a float.

property is_int

Returns True if the value is an integer.

class momba.engine.Explorer(network, time_type, *, parameters=None)[source]

Main interface to the state space exploration engine.

Warning

A network must not be modified once an explorer has been created for it. Modifying the network nonetheless may lead to all kinds of unspecified behavior.

network

The Network the explorer has been created for.

time_type

The TimeType of the explorer.

property initial_states

The initial states of the network.

static new_discrete_time(network, *, parameters=None)[source]

Creates a new discrete time explorer.

class momba.engine.State(explorer, _state)[source]

Represents a state of an automaton network.

explorer

The Explorer associated with the state.

get_local_env(instance)[source]

Returns the local environment of the provided automaton instance.

property global_env

The global environment, i.e., a mapping from global variables to values.

property locations

The locations of the respective automata instances.

A mapping from instances to locations.

property transitions

Outgoing transitions of the state.

class momba.engine.Transition(explorer, source, _state, _transition)[source]

Represents a joint transition of an automaton network.

explorer

The Explorer associated with the transition.

instances

The automaton instances participating in the transition.

action

The action associated with the transition.

action_vector

The actions with which the respective instances participate.

Is a mapping from instances to actions.

edge_vector

The edges with which the respective instances participate.

Is a mapping from instances to edges.

destinations

The destinations of the transition.

class momba.engine.Action(action_type, arguments)[source]

Represents an action.

The arguments of an action are usually empty. They are used for the experimental value-passing feature of Momba which has not been stabilized yet.

action_type

The ActionType of the action.

arguments

The arguments of the action (a tuple of values).

class momba.engine.Destination(explorer, _state, _transition, _destination)[source]

Represents a destination of a transition.

explorer

The Explorer associated with the destination.

property probability

The probability associated with the destination.

property state

The target State associated with the destination.

Time Representations

The state space exploration engines supports different time representations. For discrete time models (MDP, DTMC, and LTS) DiscreteTime should be used. Creating an explorer with new_discrete_time() will use DiscreteTime. For continuous-time models (TA and PTA) different time representations are available.

class momba.engine.TimeType[source]

Base class for time representations.

class momba.engine.DiscreteTime[source]

A representation of time without continuous-time clocks.