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 = -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)[source]#

A reach-avoid objective.

Represents a reach-avoid objective of the form $\mathrm{\neg }\varphi \mathbf{U}\psi$, i.e., $\mathrm{\neg }\varphi$ has to be true until the goal $\psi$ is reached. Used in conjunction with Rewards to provide rewards.

dead_predicate#

A boolean expression for $\varphi$.

goal_predicate#

A boolean expression for $\psi$.