Momba Models

The package momba.model contains the core data structures for the representation of quantitative models. Momba’s internal model representation closely follows the JANI specification. A model is represented as a network of interacting automata. At the heart of every model is a modeling context represented by a Context object. A modeling context specifies a model type (MDP, PTA, et cetera) and contains declarations for global variables. A modeling context allows creating automata (Automaton) of the respective model type as well as composing those automata to networks (Network).


The data structures are append only, i.e., one can define a model incrementally but one cannot change already defined parts of a model. For instance, it is possible to add a location to an already defined automaton but it is not possible to remove a location from the automaton. Thereby, the provided API ensures that the model is valid at all times.