Ada

Model

{
    "name": "B4",
    "states": [
        {
            "id": 0,
            "name": "s0",
            "initial": true
        },
        {
            "id": 1,
            "name": "s1"
        },
        {
            "id": 2,
            "name": "s2",
            "final": true
        }
    ],
    "transitions": [
        {
            "source": 0,
            "target": 0,
            "name": "write a",
            "guard": "(a' > 0)"
        },
        {
            "source": 0,
            "target": 1,
            "name": "set s to a",
            "guard": "(s' == a)"
        },
        {
            "source": 1,
            "target": 1,
            "name": "write b",
            "guard": "(b' > 0)"
        },
        {
            "source": 1,
            "target": 2,
            "name": "add b to s",
            "guard": "(s' == s + b)"
        },
        {
            "source": 2,
            "target": 0,
            "name": "reset",
            "guard": "(s' == 0)"
        }
    ],
    "variables": [
        {
            "name": "a",
            "type": "int",
            "initial": 0
        },
        {
            "name": "b",
            "type": "int",
            "initial": 0
        },
        {
            "name": "s",
            "type": "int",
            "initial": 0
        }
    ]
}

LTLf property

Ada - the arithmetic DDS analyzer