LinDMT: LTLf Model Checking Modulo Theories

input system

{
  "name": "BPM: road fine management (normative)",
  "comment": "Adapted from F. Mannhardt, M. de Leoni, H. Reijers, W. van der Aalst: Balanced multi-perspective checking of process conformance. Computing 98(4), 2016 (representing strings as constants instead of integers)", 
  "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": "pl12",
      "initial": false,
      "final": false
    }
  ],
  "transitions": [
    {
      "source": 0,
      "target": 8,
      "name": "CreateFine",
      "written": ["dismissal"],
      "guard": "((amount' >= 0) && (totalPaymentAmount' >= 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",
      "written": ["dismissal"],
      "guard": "((delayJudge' < 1440) && (delayJudge' >= 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 == G)"
    },
    {
      "source": 4,
      "target": 2,
      "name": "Inv5",
      "guard": "(dismissal == NIL)"
    },
    {
      "source": 5,
      "target": 6,
      "name": "Send Appeal to Prefecture",
      "written": ["dismissal"]
    },
    {
      "source": 6,
      "target": 7,
      "name": "Receive Result Appeal from Prefecture",
      "guard": "(dismissal == NIL)"
    },
    {
      "source": 6,
      "target": 3,
      "name": "Inv6",
      "guard": "(dismissal == Hash)"
    },
    {
      "source": 7,
      "target": 2,
      "name": "Notify"
    },
    {
      "source": 8,
      "target": 3,
      "name": "Inv1",
      "guard": "((dismissal != NIL) || ((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": "int"
    },
    {
      "name": "delayPrefecture",
      "initial": 0,
      "type": "int"
    },
    {
      "name": "totalPaymentAmount",
      "initial": 0,
      "type": "rat"
    },
    {
      "name": "points",
      "initial": 0,
      "type": "int"
    },
    {
      "name": "dismissal",
      "initial": "NIL",
      "type": "dismissal_type"
    },
    {
      "name": "delaySend",
      "initial": 0,
      "type": "int"
    },
    {
      "name": "expenses",
      "initial": 0,
      "type": "rat"
    }
  ],
  "functions": [
    {
       "name": "NIL",
       "domain": [],
       "range": "dismissal_type"
    },
    {
       "name": "G",
       "domain": [],
       "range": "dismissal_type"
    },
    {
       "name": "Hash",
       "domain": [],
       "range": "dismissal_type"
    }
  ],
  "facts": "distinct(NIL, G, Hash)",
  "ltl": [
    { "property": "G (totalPaymentAmount == 0)", "result": true },
    { "property": "F (<Notify> True && G (dismissal != NIL))", "result": false },
    { "property": "F (<Payment> <Payment> True)", "result": true },
    { "property": "F ((totalPaymentAmount > 18) && (<Payment> True))", "result": true },
    { "property": "F ((<CreateFine> True) && G (totalPaymentAmount <= 0))", "result": true }
  ],
  "sound": false
}

LTL_f property