Toggle navigation

.md .pdf

repository open issue

Contents

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.7)", "x-momba-release": "0.6.7", "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": 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}}}}}]}, {"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}}}}}]}], "action": "left", "guard": {"exp": {"op": "∧", "left": {"op": "¬", "exp": "has_won"}, "right": {"op": "¬", "exp": "has_crashed"}}}}, {"location": "ready", "destinations": [{"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}}}}}]}, {"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}}}}}]}], "action": "right", "guard": {"exp": {"op": "∧", "left": {"op": "¬", "exp": "has_won"}, "right": {"op": "¬", "exp": "has_crashed"}}}}, {"location": "ready", "destinations": [{"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}}}}}]}, {"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}}}}}]}], "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.

previous

Model Exploration

next

Examples