[−][src]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
| model | Data structures for representing automaton networks. |
| 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 |
Type Definitions
| MDPExplorer |