Model Exploration

In the previous section, we defined a formal model of a simple jump ‘n’ run game. Here, we demonstrate how to use Momba’s state space exploration engine to explore the state space of this model.

For the following examples, we have to import the model defined in Model Construction:

from momba_guide import model

The package momba.engine exposes the API for state space exploration. Momba’s state space exploration engine supports a variety of different model types including Probabilistic Timed Automata (PTAs) and Markov Decision Processes (MDPs). It is written in Rust.

We import the package and create a discrete time explorer for our MDP automaton network:

from momba import engine

explorer = engine.Explorer.new_discrete_time(model.network)

The model has one initial state which can be obtained as follows:

(state,) = explorer.initial_states

Remember that we declared two global variables, pos_x and pos_y, which hold the position of the player on the track. The values of these variables can be accessed as follows:

state.global_env

{'pos_x': Value(0), 'pos_y': Value(0)}

The global_env attributes contains a mapping from variable names to the values of these variables. As defined in the model, the player starts at the position \((0, 0)\) on the track.

Having a state, we can also ask for the outgoing transitions of this state:

for transition in state.transitions:
    assert transition.action is not None
    print(f"Move: {transition.action.action_type.label}")
    for destination in transition.destinations.support:
        print(f"  Probability: {destination.probability}")
        print(f"    Globals: {destination.state.global_env}")
        print(f"    Locals: {destination.state.get_local_env(model.environment)}")

Move: left
  Probability: 0.6
    Globals: {'pos_x': Value(1), 'pos_y': Value(-1)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(True)}
  Probability: 0.4
    Globals: {'pos_x': Value(1), 'pos_y': Value(0)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(False)}
Move: right
  Probability: 0.6
    Globals: {'pos_x': Value(1), 'pos_y': Value(1)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(False)}
  Probability: 0.4
    Globals: {'pos_x': Value(1), 'pos_y': Value(0)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(False)}
Move: stay
  Probability: 0.6
    Globals: {'pos_x': Value(1), 'pos_y': Value(0)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(False)}
  Probability: 0.4
    Globals: {'pos_x': Value(1), 'pos_y': Value(0)}
    Locals: {'has_won': Value(False), 'has_crashed': Value(False)}

As specified in the model, we can keep our current \(y\) position or move left or right. As the model is probabilistic, there are multiple destinations with different probabilities for each transition. As the player starts on a left-most position on the track, successfully moving left leads to a crash into the wall. This is also reflected in the successor state where has_crashed becomes True.

Based on this API, it is straightforward to develop a domain specific tool for interactive model exploration or test various aspects of the model. For a more elaborate example where we programmed an interactive racing game including some visualizations based on a model using Momba’s state space exploration engine, check out the Racetrack example.