Ada

Model

{
    "name": "road fine management",
    "states": [
        {
            "id": 0,
            "name": "pl1",
            "initial": true,
            "final": false
        },
        {
            "id": 1,
            "name": "pl6",
            "initial": false,
            "final": false
        },
        {
            "id": 2,
            "name": "pl7",
            "initial": false,
            "final": false
        },
        {
            "id": 3,
            "name": "End",
            "initial": false,
            "final": true
        },
        {
            "id": 4,
            "name": "pl10",
            "initial": false,
            "final": false
        },
        {
            "id": 5,
            "name": "pl13",
            "initial": false,
            "final": false
        },
        {
            "id": 6,
            "name": "pl14",
            "initial": false,
            "final": false
        },
        {
            "id": 7,
            "name": "pl15",
            "initial": false,
            "final": false
        },
        {
            "id": 8,
            "name": "end",
            "initial": false,
            "final": false
        }
    ],
    "transitions": [
        {
            "source": 0,
            "target": 8,
            "name": "Create Fine",
            "guard": "((amount' >= 0) && (totalPaymentAmount' >= 0) && (dismissal' >= 0) && (points' >= 0))"
        },
        {
            "source": 1,
            "target": 1,
            "name": "Payment",
            "guard": "(totalPaymentAmount' >= 0)"
        },
        {
            "source": 1,
            "target": 3,
            "name": "Inv2",
            "guard": "(totalPaymentAmount >= (amount + expenses))"
        },
        {
            "source": 1,
            "target": 2,
            "name": "Insert Fine Notification"
        },
        {
            "source": 2,
            "target": 3,
            "name": "Inv3",
            "guard": "(totalPaymentAmount >= (amount + expenses))"
        },
        {
            "source": 2,
            "target": 3,
            "name": "Send for Credit Collection",
            "guard": "(totalPaymentAmount < (amount + expenses))"
        },
        {
            "source": 2,
            "target": 4,
            "name": "Appeal to Judge",
            "guard": "(((delayJudge' < 1440) && (delayJudge' >= 0)) && (dismissal' >= 0))"
        },
        {
            "source": 2,
            "target": 2,
            "name": "Add penalty",
            "guard": "(amount' >= 0)"
        },
        {
            "source": 2,
            "target": 5,
            "name": "Insert Date Appeal to Prefecture",
            "guard": "((delayPrefecture' < 1440) && (delayPrefecture' >= 0))"
        },
        {
            "source": 2,
            "target": 2,
            "name": "Payment",
            "guard": "(totalPaymentAmount' >= 0)"
        },
        {
            "source": 4,
            "target": 3,
            "name": "Inv4",
            "guard": "(dismissal == 2)"
        },
        {
            "source": 4,
            "target": 2,
            "name": "Inv5",
            "guard": "(dismissal == 0)"
        },
        {
            "source": 5,
            "target": 6,
            "name": "Send Appeal to Prefecture",
            "guard": "(dismissal' >= 0)"
        },
        {
            "source": 6,
            "target": 7,
            "name": "Receive Result Appeal from Prefecture",
            "guard": "(dismissal == 0)"
        },
        {
            "source": 6,
            "target": 3,
            "name": "Inv6",
            "guard": "(dismissal == 1)"
        },
        {
            "source": 7,
            "target": 2,
            "name": "Notify"
        },
        {
            "source": 8,
            "target": 3,
            "name": "Inv1",
            "guard": "((dismissal != 0) || ((points == 0) && (totalPaymentAmount >= amount)))"
        },
        {
            "source": 8,
            "target": 8,
            "name": "Payment",
            "guard": "(totalPaymentAmount' >= 0)"
        },
        {
            "source": 8,
            "target": 1,
            "name": "Send Fine",
            "guard": "((delaySend' < 2160) && (delaySend' >= 0) && (expenses' >= 0))"
        }
    ],
    "variables": [
        {
            "name": "amount",
            "initial": 0,
            "type": "rat"
        },
        {
            "name": "delayJudge",
            "initial": 0,
            "type": "rat"
        },
        {
            "name": "delayPrefecture",
            "initial": 0,
            "type": "rat"
        },
        {
            "name": "totalPaymentAmount",
            "initial": 0,
            "type": "rat"
        },
        {
            "name": "points",
            "initial": 0,
            "type": "int"
        },
        {
            "name": "dismissal",
            "initial": 0,
            "type": "int"
        },
        {
            "name": "delaySend",
            "initial": 0,
            "type": "rat"
        },
        {
            "name": "expenses",
            "initial": 0,
            "type": "rat"
        }
    ]
}

LTLf property

Ada - the arithmetic DDS analyzer