LinDMT: LTLf Model Checking Modulo Theories

input system

{
  "name": "BPM: hospital billing",
  "comment": "Adapted from F. Mannhardt: Multi-perspective Process Mining. Ph.D. thesis",
  "states": [
    {
      "id": 0,
      "name": "src",
      "initial": true,
      "final": false
    },
    {
      "id": 1,
      "name": "p1",
      "initial": false,
      "final": false
    },
    {
      "id": 2,
      "name": "p10p25",
      "initial": false,
      "final": false
    },
    {
      "id": 3,
      "name": "p2p25",
      "initial": false,
      "final": false
    },
    {
      "id": 4,
      "name": "p10p28",
      "initial": false,
      "final": false
    },
    {
      "id": 5,
      "name": "p2p28",
      "initial": false,
      "final": false
    },
    {
      "id": 6,
      "name": "p42",
      "initial": false,
      "final": false
    },
    {
      "id": 7,
      "name": "p40",
      "initial": false,
      "final": false
    },
    {
      "id": 8,
      "name": "end",
      "initial": false,
      "final": true
    },
    {
      "id": 9,
      "name": "p15",
      "initial": false,
      "final": false
    },
    {
      "id": 10,
      "name": "p5",
      "initial": false,
      "final": false
    },
    {
      "id": 11,
      "name": "p3",
      "initial": false,
      "final": false
    },
    {
      "id": 12,
      "name": "p27",
      "initial": false,
      "final": false
    },
    {
      "id": 13,
      "name": "p11",
      "initial": false,
      "final": false
    },
    {
      "id": 14,
      "name": "p26",
      "initial": false,
      "final": false
    },
    {
      "id": 15,
      "name": "p12",
      "initial": false,
      "final": false
    },
    {
      "id": 16,
      "name": "p18",
      "initial": false,
      "final": false
    }
  ],
  "transitions": [
    {
      "source": 0,
      "target": 1,
      "name": "NEW",
      "written": [
        "caseType",
        "speciality",
        "isClosed"
      ]
    },
    {
      "source": 1,
      "target": 2,
      "name": "t1",
      "written": []
    },
    {
      "source": 2,
      "target": 3,
      "name": "ChangeDiagn",
      "guard": "(caseType == B)",
      "written": []
    },
    {
      "source": 2,
      "target": 3,
      "name": "t4",
      "guard": "(caseType != B)",
      "written": []
    },
    {
      "source": 2,
      "target": 4,
      "name": "CHANGE END",
      "written": []
    },
    {
      "source": 2,
      "target": 4,
      "name": "t25",
      "written": []
    },
    {
      "source": 3,
      "target": 5,
      "name": "CHANGE END",
      "written": []
    },
    {
      "source": 3,
      "target": 5,
      "name": "t25",
      "written": []
    },
    {
      "source": 4,
      "target": 5,
      "name": "ChangeDiagn",
      "guard": "(caseType == B)",
      "written": []
    },
    {
      "source": 4,
      "target": 5,
      "name": "t4",
      "guard": "(caseType != B)",
      "written": []
    },
    {
      "source": 5,
      "target": 6,
      "name": "t10",
      "written": []
    },
    {
      "source": 6,
      "target": 7,
      "name": "FIN",
      "guard": "speciality != K",
      "written": [
        "closeCode"
      ]
    },
    {
      "source": 6,
      "target": 8,
      "name": "DELETE",
      "written": []
    },
    {
      "source": 6,
      "target": 8,
      "name": "t12",
      "guard": "(speciality == K)",
      "written": []
    },
    {
      "source": 7,
      "target": 9,
      "name": "DELETE",
      "written": []
    },
    {
      "source": 7,
      "target": 10,
      "name": "RELEASE",
      "written": []
    },
    {
      "source": 7,
      "target": 9,
      "name": "REOPEN",
      "guard": "(closeCode != H)",
      "written": []
    },
    {
      "source": 7,
      "target": 8,
      "name": "skipRelease",
      "guard": "(closeCode == H)",
      "written": []
    },
    {
      "source": 9,
      "target": 6,
      "name": "tLoop",
      "guard": "(isClosed == true)",
      "written": []
    },
    {
      "source": 9,
      "target": 8,
      "name": "t18",
      "written": []
    },
    {
      "source": 9,
      "target": 8,
      "name": "DELETE",
      "guard": "(isClosed != true)",
      "written": []
    },
    {
      "source": 9,
      "target": 8,
      "name": "EMPTY",
      "written": []
    },
    {
      "source": 10,
      "target": 11,
      "name": "CODE OK",
      "written": []
    },
    {
      "source": 10,
      "target": 11,
      "name": "t8",
      "guard": "((caseType == F) || (((caseType != F) && (caseType != C)) && (closeCode != A)))",
      "written": []
    },
    {
      "source": 10,
      "target": 11,
      "name": "CODE NOK",
      "guard": "(((caseType != F) && (caseType == C)) || (((caseType != F) && (caseType != C)) && (closeCode == A)))",
      "written": []
    },
    {
      "source": 11,
      "target": 12,
      "name": "SET STATUS",
      "written": []
    },
    {
      "source": 11,
      "target": 12,
      "name": "t30",
      "written": []
    },
    {
      "source": 12,
      "target": 8,
      "name": "t39",
      "written": []
    },
    {
      "source": 12,
      "target": 13,
      "name": "BILLED",
      "written": []
    },
    {
      "source": 12,
      "target": 9,
      "name": "REOPEN",
      "guard": "((caseType == B) || ((caseType != B) && (closeCode != A)))",
      "written": []
    },
    {
      "source": 12,
      "target": 9,
      "name": "t15",
      "guard": "((caseType != B) && (closeCode == A))",
      "written": []
    },
    {
      "source": 13,
      "target": 14,
      "name": "STORNO",
      "guard": "(((isClosed == true) && (closeCode != A)) || (isClosed != true))",
      "written": []
    },
    {
      "source": 13,
      "target": 15,
      "name": "t31",
      "written": []
    },
    {
      "source": 13,
      "target": 15,
      "name": "STORNO",
      "guard": "((isClosed == true) && (closeCode == A))",
      "written": []
    },
    {
      "source": 14,
      "target": 15,
      "name": "REJECT",
      "written": []
    },
    {
      "source": 15,
      "target": 16,
      "name": "BILLED",
      "guard": "(isClosed == true)",
      "written": []
    },
    {
      "source": 15,
      "target": 16,
      "name": "REOPEN",
      "guard": "(isClosed != true)",
      "written": []
    },
    {
      "source": 15,
      "target": 16,
      "name": "t9",
      "written": []
    },
    {
      "source": 16,
      "target": 13,
      "name": "t7",
      "written": []
    },
    {
      "source": 16,
      "target": 9,
      "name": "t29",
      "written": []
    }
  ],
  "variables": [
    {
      "name": "caseType",
      "initial": "B",
      "type": "type_case"
    },
    {
      "name": "closeCode",
      "initial": "A",
      "type": "type_code"
    },
    {
      "name": "speciality",
      "initial": "L",
      "type": "type_specialty"
    },
    {
      "name": "isClosed",
      "initial": false,
      "type": "bool"
    }
  ],
  "functions": [ 
     {
        "name": "B",
        "domain": [],
        "range": "type_case"
     },
     {
        "name": "C",
        "domain": [],
        "range": "type_case"
     },
     {
        "name": "F",
        "domain": [],
        "range": "type_case"
     },
     {
        "name": "A",
        "domain": [],
        "range": "type_code"
     },
     {
        "name": "H",
        "domain": [],
        "range": "type_code"
     },
     {
        "name": "K",
        "domain": [],
        "range": "type_specialty"
     },
     {
        "name": "L",
        "domain": [],
        "range": "type_specialty"
     }
    ],
    "ltl": [
       { "property": "F end", "result": true },
       { "property": "F (p15 && G ! end)", "result": false },
       { "property": "F (<BILLED> True && F (<ChangeDiagn> True))", "result": false },
       { "property": "F (<ChangeDiagn> True && X F (<ChangeDiagn> True))", "result": false },
       { "property": "G ! p18", "result": true }
    ]
}

LTL_f property