Ada

Model

{
    "name": "online auction",
    "states": [
        {
            "id": 0,
            "name": "start",
            "initial": true
        },
        {
            "id": 1,
            "name": "main"
        },
        {
            "id": 2,
            "name": "change"
        },
        {
            "id": 3,
            "name": "end"
        },
        {
            "id": 4,
            "name": "sold",
            "final": true
        }
    ],
    "transitions": [
        {
            "source": 0,
            "target": 1,
            "name": "init",
            "guard": "(d' > 0) && (t' > 0)"
        },
        {
            "source": 1,
            "target": 2,
            "name": "check",
            "guard": "(d > 0)"
        },
        {
            "source": 2,
            "target": 1,
            "name": "bid",
            "guard": "((o' > o) && (0 < b'))"
        },
        {
            "source": 2,
            "target": 1,
            "name": "dec",
            "guard": "(d - d' >= 1)"
        },
        {
            "source": 1,
            "target": 3,
            "name": "exp",
            "guard": "((d <= 0) && (o > 0))"
        },
        {
            "source": 1,
            "target": 3,
            "name": "sell now",
            "guard": "(o > t)"
        },
        {
            "source": 3,
            "target": 4,
            "name": "fee",
            "guard": "(s' == o + 10)"
        }
    ],
    "variables": [
        {
            "name": "d",
            "type": "int",
            "initial": 0
        },
        {
            "name": "o",
            "type": "real",
            "initial": 0
        },
        {
            "name": "b",
            "type": "int",
            "initial": 0
        },
        {
            "name": "s",
            "type": "real",
            "initial": 0
        },
        {
            "name": "t",
            "type": "real",
            "initial": 0
        }
    ]
}

LTLf property

Ada - the arithmetic DDS analyzer