Exploration Engine

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

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 0x7faedcfc71c0>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faedcfc7d30>.
Action: snd_idle21
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faedcfc7bb0>.
  With p=0.5 to <momba.engine.explore.Destination object at 0x7faedcfc7820>.

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.

Paramaters#

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#

Paramaters#

Time Representations#