LinDMT: LTLf Model Checking Modulo Theories

input system

{
  "name": "BPM: road fine management (mined)",
  "comment": "Adapted from Fig. 12.7. in F. Mannhardt: Multi-perspective Process Mining. Ph.D. thesis, Technical University of Eindhoven, 2018 (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", "amount", "totalPaymentAmount", "points"]
    },
    {
      "source": 1,
      "target": 1,
      "name": "Payment",
      "written": ["totalPaymentAmount"],
      "guard": "(totalPaymentAmount <= 18)"
    },
    {
      "source": 1,
      "target": 3,
      "name": "Inv2"
    },
    {
      "source": 1,
      "target": 2,
      "name": "Insert Fine Notification"
    },
    {
      "source": 2,
      "target": 3,
      "name": "Inv3"
    },
    {
      "source": 2,
      "target": 3,
      "name": "Send for Credit Collection"
    },
    {
      "source": 2,
      "target": 4,
      "name": "Appeal to Judge",
      "written": ["dismissal"]
    },
    {
      "source": 2,
      "target": 2,
      "name": "Add penalty",
      "written": ["amount"]
    },
    {
      "source": 2,
      "target": 5,
      "name": "Insert Date Appeal to Prefecture"
    },
    {
      "source": 2,
      "target": 2,
      "name": "Payment",
      "written": ["totalPaymentAmount"],
      "guard": "(totalPaymentAmount <= 18)"
    },
    {
      "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": "(expenses > 15.6)"
    },
    {
      "source": 6,
      "target": 3,
      "name": "Inv6",
      "guard": "(expenses <= 15.6)"
    },
    {
      "source": 7,
      "target": 2,
      "name": "Notify"
    },
    {
      "source": 8,
      "target": 3,
      "name": "Inv1",
      "guard": "totalPaymentAmount > 18"
    },
    {
      "source": 8,
      "target": 8,
      "name": "Payment",
      "written": ["totalPaymentAmount"],
      "guard": "(totalPaymentAmount <= 18)"
    },
    {
      "source": 8,
      "target": 1,
      "name": "Send Fine",
      "guard": "(totalPaymentAmount <= 18)"
    }
  ],
  "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": false },
     { "property": "F ((<CreateFine> True) && G (totalPaymentAmount <= 0))", "result": true }
  ]
}

LTL_f property