Crate momba_explore

State space exploration engine for PTAs and MDPs augmented with variables.

This crate provides the necessary functionality for efficiently exploring the state space of Probabilistic Timed Automata (PTAs) and Markov Decision Processes (MDPs) augmented with variables.

Momba Explore uses its own model representation defined in the module model leveraging Serde. Hence, models can be loaded from any format supported by Serde. JANI models can be loaded by first translating them using Momba.

Modules

• external
  Data structures for communicating with external tools.
• model
  Data structures for representing automaton networks.
• simulate
  Convenience functions for simulating random runs.
• time
  Algorithms and data structures for representing time.

Structs

• Destination
  A destination of a transition.
• Explorer
  A state space explorer for a particular automaton network.
• LabeledAction
  Label and arguments associated with a labeled action.
• State
  A state of an automaton network.
• Transition
  A transition of an automaton network.

Enums

• Action
  An action which is either silent or labeled.

Type Aliases

• MDPExplorer
  A specialization of Explorer for MDPs using NoClocks.