Generic Explorer

Versatile implementation of Explorer.

class momba.gym.generic.Actions(value)

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)

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)

Specifies the rewards for a reachability objective.

dead_end = -100

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

goal_reached = 100

The reward when a goal state is reached.

invalid_action = -100

The reward when an invalid decision has been taken.

step_taken = 0

The reward when a valid decision has been taken.

class momba.gym.generic.Objective(goal_predicate, dead_predicate)

A reach-avoid objective.

Represents a reach-avoid 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

A boolean expression for \(\phi\).

goal_predicate

A boolean expression for \(\psi\).