JANI Models

Momba exposes two main functions to work with JANI-model files, dump_model() and load_model(). As the names suggest, dump_model() exports a Momba automaton Network to JANI-model while the function load_model() imports an automaton Network from a JANI-model file.

Momba supports the full JANI core specification and furthermore has support for the following JANI extensions: arrays, derived-operators, functions, nondet-selection, state-exit-rewards, and trigonometric-functions.

Examples

Loading a JANI-Model

import pathlib

from momba import jani

path = pathlib.Path("tests/resources/QVBS2019/benchmarks/mdp/firewire/firewire.true.jani")
jani.load_model(path.read_text("utf-8"))

<momba.model.networks.Network at 0x7f3d88f8d6a0>

Exporting a JANI-Model

from momba import jani, model

ctx = model.Context(model.ModelType.MDP)
network = ctx.create_network()

# ... build the automaton network

jani.dump_model(network)

'{"jani-version": 1, "x-generator": "Momba (v0.6.12)", "x-momba-release": "0.6.12", "name": "A Momba Model", "x-momba-anonymous": true, "metadata": {}, "x-momba-metadata": {}, "type": "mdp", "variables": [], "constants": [], "actions": [], "automata": [], "properties": [], "system": {"elements": [], "syncs": []}, "features": []}'

Reference

momba.jani.load_model(source, *, ignore_properties=False)

Constructs a Momba automaton Network based on the provided JANI model string.

The flag ignore_properties indicates whether the properties of the model should be ignored or added to the returned network’s modeling Context.

Throws a JANIError in case the JANI file cannot be loaded.

momba.jani.dump_model(network, *, indent=None, allow_momba_operators=False, properties=None)

Takes a Momba automaton Network and returns a JANI string representing the network.

The indent parameter controls the indentation of the resulting JANI string. None means no indentation. Set indent to an integer, e.g., 2, to enable pretty formatting.

Momba supports some non-standard operators which can either be preserved or desugared into standard JANI. This behavior is controlled via the flag allow_momba_operators. If the flag is set to True, then the x-momba-operators JANI model feature is enabled and the non-standard operators will be preserved in the output. Otherwise, if it is set to False (the default case), non-standard operators are desugared into standard JANI.

The properties parameter allows to provide an mapping from str to Expression. The provided expressions will be put as additional properties into the JANI-model output.

class momba.jani.ModelFeature(value)

An enum representing optional JANI model features.

ARRAYS = 'arrays'

Support for arrays.

DATATYPES = 'datatypes'

Support for datatypes.

DERIVED_OPERATORS = 'derived-operators'

Support for derived operators.

EDGE_PRIORITIES = 'edge-priorities'

Support for edge priorities.

FUNCTIONS = 'functions'

Support for functions.

HYPERBOLIC_FUNCTIONS = 'hyperbolic-functions'

Support for hyperbolic functions.

NAMED_EXPRESSIONS = 'named-expressions'

Support for named expressions.

NONDET_SELECTION = 'nondet-selection'

Suport for non-deterministic selection expressions.

STATE_EXIT_REWARDS = 'state-exit-rewards'

Support for state exit rewards.

TRADEOFF_PROPERTIES = 'tradeoff-properties'

Support for tradeoff properties.

TRIGONOMETRIC_FUNCTIONS = 'trigonometric-functions'

Support for trigonometric functions.

X_MOMBA_OPERATORS = 'x-momba-operators'

Support for Momba non-standard operators.

X_MOMBA_VALUE_PASSING = 'x-momba-value-passing'

Support for Momba non-standard value passing.

Exceptions

class momba.jani.JANIError

Indicates an error while loading a JANI string.

Usually either InvalidJANIError or UnsupportedJANIError gets thrown.

class momba.jani.InvalidJANIError

String is not valid JANI.

class momba.jani.UnsupportedJANIError(unsupported_features)

Model contains unsupported JANI features.

unsupported_features

Used model features not supported by Momba.