Expand description
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.
- Labeled
Action - Label and arguments associated with a labeled action.
- State
- A state of an automaton network.
- Transition
- A transition of an automaton network.
Enums§
Type Aliases§
- MDPExplorer
- A specialization of Explorer for MDPs using NoClocks.