Model Analysis#
To harvest the results of formal modeling, Momba exposes unified interfaces to state-of-the-art tools. Currently, Storm and the Modest Toolset are supported. As installation can sometimes be a hassle, especially for beginners, Momba also tries its best to install these tools for you. Note, that these tools are not distributed with Momba but downloaded on-demand. They are not a part of Momba and distributed under their own respective licenses. For more information, please visit the website of the respective tool and make sure your usage complies with their license.
As Momba tries to install the tools for you, it suffices to just install Momba with:
pip install momba[all]
For the following examples, we have to import the model defined in Model Construction:
from momba_guide import model
Model Checking#
Imagine you would like to know the maximal probability of winning the game assuming the player performs optimal moves. Put into a property definition, this may look as follows:
from momba.moml import expr, prop
properties = {
"goal": prop(
"min({ Pmax(F($has_won)) | initial })",
has_won=model.has_won(expr("pos_x"), model.track)
),
}
Here, we use Momba’s prop() function to define the property.
Intuitively, we aggregate over all initial states by taking the minimum over all initial states of the maximal probability of winning the game from the respective initial state.
We call has_finished as defined for our model to build an expression being true if and only if the game has been won by moving over the finishing line.
As a unified interface to model checkers, Momba provides the abstract base class Checker.
Let’s say we would like to check the property with both, Storm and the Modest Toolset.
To this end, we import both tools and obtain a Checker instance for each tool, respectively:
from momba.tools import modest, storm
modest_checker = modest.get_checker(accept_license=True)
storm_checker = storm.get_checker(accept_license=True)
We have to explicitly pass accept_license=True to the get_checker functions to indicate that we have read and accept the licenses applying to these tools which are not a part of Momba.
For Storm, Docker has to be running on the system, as Momba will use the Docker image of Storm.
Checking the defined property with both model checkers is now straightforward:
results = {
checker: checker.check(model.network, properties=properties)
for checker in [modest_checker, storm_checker]
}
for checker, values in results.items():
print(f"{checker.description}:")
for prop_name, prop_value in values.items():
print(f" Property {prop_name!r}: {float(prop_value)}")
Modest (mcsta):
Property 'goal': 0.9529825323233355
Storm in Docker (engine = sparse):
Property 'goal': 0.9529825323
There also exists a cross checker which automatically cross validates the results produced by different model checkers and raises an exception if the results do not match:
from momba.analysis import checkers
cross_checker = checkers.CrossChecker([modest_checker, storm_checker])
cross_checker.check(model.network, properties=properties)
{'goal': Fraction(8583703554923931, 9007199254740992)}
JANI Export#
Momba is centered around the JANI-model modeling formalism and interchange format. Hence, models defined with Momba can easily be exported in JANI-model format:
from momba import jani
jani.dump_model(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": [{"name": "pos_x", "type": "int", "initial-value": 0}, {"name": "pos_y", "type": "int", "initial-value": 0}], "constants": [], "actions": [{"name": "left"}, {"name": "right"}, {"name": "stay"}], "automata": [{"name": "Environment", "x-momba-anonymous": false, "variables": [{"name": "has_won", "type": "bool", "initial-value": false}, {"name": "has_crashed", "type": "bool", "initial-value": false}], "locations": [{"name": "ready", "x-momba-anonymous": false, "transient-values": []}], "edges": [{"location": "ready", "destinations": [{"location": "ready", "probability": {"exp": {"op": "-", "left": 1, "right": 0.6}}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": "pos_y", "right": 3}, "right": {"op": "<", "left": "pos_y", "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": "pos_y", "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 2}}}}}]}, {"location": "ready", "probability": {"exp": 0.6}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "pos_y", "value": {"op": "+", "left": "pos_y", "right": -1}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 3}, "right": {"op": "<", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": -1}, "right": 2}}}}}]}], "action": "left", "guard": {"exp": {"op": "∧", "left": {"op": "¬", "exp": "has_won"}, "right": {"op": "¬", "exp": "has_crashed"}}}}, {"location": "ready", "destinations": [{"location": "ready", "probability": {"exp": {"op": "-", "left": 1, "right": 0.6}}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": "pos_y", "right": 3}, "right": {"op": "<", "left": "pos_y", "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": "pos_y", "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 2}}}}}]}, {"location": "ready", "probability": {"exp": 0.6}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "pos_y", "value": {"op": "+", "left": "pos_y", "right": 1}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 3}, "right": {"op": "<", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 1}, "right": 2}}}}}]}], "action": "right", "guard": {"exp": {"op": "∧", "left": {"op": "¬", "exp": "has_won"}, "right": {"op": "¬", "exp": "has_crashed"}}}}, {"location": "ready", "destinations": [{"location": "ready", "probability": {"exp": {"op": "-", "left": 1, "right": 0.6}}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": "pos_y", "right": 3}, "right": {"op": "<", "left": "pos_y", "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": "pos_y", "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": "pos_y", "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": "pos_y", "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": "pos_y", "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": "pos_y", "right": 2}}}}}]}, {"location": "ready", "probability": {"exp": 0.6}, "assignments": [{"ref": "pos_x", "value": {"op": "+", "left": "pos_x", "right": 1}}, {"ref": "pos_y", "value": {"op": "+", "left": "pos_y", "right": 0}}, {"ref": "has_won", "value": {"op": "≥", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 34}}, {"ref": "has_crashed", "value": {"op": "∨", "left": {"op": "∨", "left": {"op": "≥", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 3}, "right": {"op": "<", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}, "right": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∨", "left": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 12}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 17}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 2}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 6}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 21}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 31}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 4}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 27}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 19}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 11}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 1}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 13}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 24}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 20}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 0}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 3}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 5}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 32}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 1}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 7}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}, "right": {"op": "∧", "left": {"op": "=", "left": {"op": "+", "left": "pos_x", "right": 1}, "right": 18}, "right": {"op": "=", "left": {"op": "+", "left": "pos_y", "right": 0}, "right": 2}}}}}]}], "action": "stay", "guard": {"exp": {"op": "∧", "left": {"op": "¬", "exp": "has_won"}, "right": {"op": "¬", "exp": "has_crashed"}}}}], "initial-locations": ["ready"]}], "properties": [], "system": {"elements": [{"automaton": "Environment"}], "syncs": [{"synchronise": ["left"], "result": "left"}, {"synchronise": ["right"], "result": "right"}, {"synchronise": ["stay"], "result": "stay"}]}, "features": ["derived-operators"]}'
The resulting JANI model can then be fed in any compatible tool for further analysis.