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 0x7f394f6d6b30>

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)

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}")

wire12: l
node1: 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))

wire12
{}
node1
{}
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_idle12
  With p=0.5 to <momba.engine.explore.Destination object at 0x7f394f6fb010>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7f394f6fafe0>.
Action: snd_idle21
  With p=0.5 to <momba.engine.explore.Destination object at 0x7f3944ed8100>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7f3944ed84c0>.

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_idle12

{'w12': Value(5),
 'y1': Value(0),
 'y2': Value(0),
 'x1': Value(0),
 's1': Value(3),
 'w21': Value(0),
 'z1': Value(0),
 'z2': Value(0),
 'x2': Value(0),
 's2': Value(0),
 '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 probability distribution over destinations.

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.

class momba.utils.distribution.Distribution(mapping)[source]¶

A probability distribution.

pick()[source]¶: Picks an element at random according to the distribution.

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.

Exploration Engine

Contents

Exploration Engine¶

Example¶

Reference¶

Time Representations¶