Momba Gym

Momba Gym enables (a) the usage of JANI models as training environments for Reinforcement Learning and (b) the rigorous assessment of trained decision agents based on Deep Statistical Model Checking.

momba.gym.create_generic_env(network, controlled_instance, property_name, *, parameters=None, rewards=Rewards(goal_reached=100, dead_end=- 100, step_taken=0, invalid_action=- 100), actions=Actions.EDGE_BY_INDEX, observations=Observations.GLOBAL_ONLY, renderer=None)[source]

Convenience function for constructing a generic environment from a model.

class momba.gym.env.MombaEnv(explorer, *, renderer=None)[source]

Implementation of an OpenAI Gym environment.

fork()[source]

Forks the environment.

render(mode='human')[source]

Renders the environment assuming a render has been supplied.

reset()[source]

Resets the environment to an initial state and returns an initial observation.

step(action)[source]

Takes a decision in response to the last observation.

Deep Statistical Model Checking

momba.gym.checker.check_oracle(network, instance, oracle, *, parameters={}, toolset=Toolset(executable='modest', environment=None), options=ModesOptions(max_run_length_as_end=True), actions=Actions.EDGE_BY_INDEX, observations=Observations.GLOBAL_ONLY)[source]
momba.gym.checker.check_nn(network, instance, nn, *, parameters={}, toolset=Toolset(executable='modest', environment=None), options=ModesOptions(max_run_length_as_end=True), actions=Actions.EDGE_BY_INDEX, observations=Observations.GLOBAL_ONLY)[source]

Checks a PyTorch neural network.