Generic Explorer

Versatile implementation of Explorer.

class momba.gym.generic.Actions(value)[source]

Specifies how edges of the controlled automaton are chosen.

EDGE_BY_INDEX = 1

The edge is chosen based on its index.

EDGE_BY_LABEL = 2

The edge is chosen based on its label.

class momba.gym.generic.Observations(value)[source]

Specifies what is observable by the agent.

GLOBAL_ONLY = 1

Only global variables are observable.

LOCAL_AND_GLOBAL = 2

Local and global variables are observable.

OMNISCIENT = 3

All (non-transient) variables are observable.

class momba.gym.generic.Rewards(goal_reached=100, dead_end=- 100, step_taken=0, invalid_action=- 100)[source]

Specifies the rewards for a reachability objective.

dead_end: float = -100

The reward when a dead end or bad state is reached.

goal_reached: float = 100

The reward when a goal state is reached.

invalid_action: float = -100

The reward when an invalid decision has been taken.

step_taken: float = 0

The reward when a valid decision has been taken.

class momba.gym.generic.Objective(goal_predicate, dead_predicate)[source]

A reachability objective.

Represents a reachability objective of the form \(\lnot\phi\mathbin{\mathbf{U}}\psi\), i.e., \(\lnot\phi\) has to be true until the goal \(\psi\) is reached. Used in conjunction with Rewards to provide rewards.

dead_predicate: momba.model.expressions.Expression

A boolean expression for \(\phi\).

goal_predicate: momba.model.expressions.Expression

A boolean expression for \(\psi\).