Model Construction
Contents
Model Construction¶
Momba provides append-only APIs for incremental model construction, i.e., one can define a model incrementally but one cannot change already defined parts of a model. For instance, it is possible to add a location to an already defined automaton but it is not possible to remove a location from the automaton. Thereby, the provided APIs ensure that the model is valid at all times.
Here, we construct a model of a simple jump ‘n’ run game where the player has to avoid obstacles while moving forward at a constant speed. To avoid obstacles the player can move left or right. The goal is to reach the end of the track without crashing into an obstacle.
With the help of a little ASCII art, a track may be represented as follows:
TRACK = (
" x xxxxx x ",
" xxx x xx ",
" xxxxxxx xx ",
)
Every x represents an obstacle and the player starts on the left and moves forward to the right.
The player wins, if and only if it moves beyond the finishing line, i.e., reaches the end of the track.
Now, given such a track, we would like to create a model of the game.
Note that this goes beyond what is possible with mere parametrization of a model.
First, we create a more formal representation of the scenario to be modeled.
To this end, we define a class Track holding all the information of the track:
import dataclasses as d
import typing as t
@d.dataclass(frozen=True)
class Cell:
x: int
y: int
@d.dataclass(frozen=True)
class Track:
width: int
height: int
obstacles: t.Set[Cell]
@classmethod
def from_ascii(cls, ascii: t.Tuple[str, ...]) -> "Track":
width = len(ascii[0])
height = len(ascii)
obstacles = set()
for y, line in enumerate(ascii):
for x, symbol in enumerate(line):
if symbol == "x":
obstacles.add(Cell(x, y))
return cls(width, height, obstacles)
track = Track.from_ascii(TRACK)
track
Track(width=34, height=3, obstacles={Cell(x=12, y=1), Cell(x=17, y=0), Cell(x=19, y=0), Cell(x=2, y=2), Cell(x=6, y=2), Cell(x=21, y=0), Cell(x=31, y=1), Cell(x=4, y=2), Cell(x=27, y=0), Cell(x=19, y=2), Cell(x=11, y=1), Cell(x=1, y=2), Cell(x=13, y=1), Cell(x=24, y=1), Cell(x=7, y=0), Cell(x=18, y=0), Cell(x=20, y=0), Cell(x=3, y=2), Cell(x=5, y=2), Cell(x=32, y=1), Cell(x=7, y=2), Cell(x=18, y=2)})
With this in place, we are now ready to construct the model.
Modeling with Momba¶
The package momba.model provides the core modeling API for model construction.
At the heart of every model is a modeling context (Context) of a specific model type (ModelType).
Every modeling context can hold several automata and automata networks comprised of these automata.
Also, global variables, constants, functions, and properties are declared on the modeling context.
To construct a model, we first have to create a modeling context of the respective type:
from momba import model
# creates a *Markov Decision Process* (MDP) modeling context
ctx = model.Context(model.ModelType.MDP)
ctx
<Context model_type=ModelType.MDP at 0x7fdeff6c1b70>
In our case, the model will be a Markov Decision Process (MDP).
To represent the position of the car, we define two global variables, pos_x and pos_y:
ctx.global_scope.declare_variable("pos_x", typ=model.types.INT, initial_value=0)
ctx.global_scope.declare_variable("pos_y", typ=model.types.INT, initial_value=0)
To control the game, we create three action types:
left_action = ctx.create_action_type("left")
right_action = ctx.create_action_type("right")
stay_action = ctx.create_action_type("stay")
Each of these action types corresponds to a distance moved on the \(y\)-axis:
moves = {left_action: -1, right_action: 1, stay_action: 0}
Next, we define an automaton modeling the environment:
environment_automaton = ctx.create_automaton(name="Environment")
This automaton will have one location:
ready_location = environment_automaton.create_location("ready", initial=True)
To keep track of whether the player reached the goal or crashed into an obstacle or a wall, we declare two local variables has_won and has_crashed for the environment automaton:
environment_automaton.scope.declare_variable(
"has_won", typ=model.types.BOOL, initial_value=False
)
environment_automaton.scope.declare_variable(
"has_crashed", typ=model.types.BOOL, initial_value=False
)
With the help of Momba’s syntax-aware macros we now define two functions computing whether the player has crashed or has finished depending on the position:
from momba.moml import expr
def has_finished(x: model.Expression, track: Track) -> model.Expression:
return expr("$x >= $width", x=x, width=track.width)
def has_crashed(
x: model.Expression, y: model.Expression, track: Track
) -> model.Expression:
out_of_bounds = expr("$y >= $height or $y < 0", y=y, height=track.height)
on_obstacle = model.expressions.logic_any(
*(
expr(
"$x == $obstacle_x and $y == $obstacle_y",
x=x,
y=y,
obstacle_x=obstacle.x,
obstacle_y=obstacle.y,
)
for obstacle in track.obstacles
)
)
return model.expressions.logic_or(out_of_bounds, on_obstacle)
Momba makes it easy to define functions operating on JANI-model expressions.
In particular, the function expr() can be used to build expressions with a succinct and intuitive syntax.
We use the same approach to define an expression indicating whether a move can be performed:
can_move = expr("not has_won and not has_crashed")
Now, with these definitions in place, we create the edges of the automaton:
for action_type, delta in moves.items():
new_pos_x = expr("pos_x + 1")
new_pos_y = expr("pos_y + $delta", delta=delta)
environment_automaton.create_edge(
ready_location,
destinations={
model.create_destination(
ready_location,
probability=expr("0.6"),
assignments={
"pos_x": new_pos_x,
"pos_y": new_pos_y,
"has_won": has_finished(new_pos_x, track),
"has_crashed": has_crashed(new_pos_x, new_pos_y, track),
},
),
model.create_destination(
ready_location,
probability=expr("1 - 0.6"),
assignments={
"pos_x": new_pos_x,
"has_won": has_finished(new_pos_x, track),
"has_crashed": has_crashed(new_pos_x, expr("pos_y"), track),
},
),
},
action_pattern=action_type.create_pattern(),
guard=can_move,
)
For each of the previously defined action types, an edge is created. In this case, the model introduces probabilistic noise and a move might fail, i.e., not change the \(y\) coordinate, with a probability of \(0.4\). When taking an edge, the variables get updated accordingly.
Finally, we create an instance of the automaton:
environment = environment_automaton.create_instance()
The instance is then added to an automaton network and a synchronization link for each action type is created which allows the resulting composition to perform the respective action:
network = ctx.create_network()
network.add_instance(environment)
for action_type in moves.keys():
network.create_link(
{environment: action_type.create_pattern()},
result=action_type.create_pattern(),
)
You can find the full source code of this example here.