LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: property and casuality",
   "comment": "This example was adopted from the VERIFAS problem set. Updates of relations were omitted.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/Property-and-Casualty-Insurance-Claim-Processing.txt",
   "states": [
     {
        "id": 0,
        "name": "Start",
        "initial": true
     },
     {
      "id": 1,
      "name": "NewCase"
     },
     {
      "id": 5,
      "name": "CaseEnded",
      "final": true
     },
     {
        "id": 6,
        "name": "OpeningNotExceedDeductible"
     },
     {
        "id": 7,
        "name": "LocationFound"
     },
     {
        "id": 8,
        "name": "Notified"
     },
     {
        "id": 9,
        "name": "OpeningExceedDeductible"
     },
     {
        "id": 10,
        "name": "Paid"
     },
     {
        "id": 11,
        "name": "Approved"
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "Init",
        "guard": "(case_id' != undef_case_id)"
     },
     {
        "source": 1,
        "target": 6,
        "name": "OpenNotExceedDeductible",
        "guard": "CaseType(case_id) == NotExceedDeductible"
     },
     {
        "source": 6,
        "target": 7,
        "name": "SuggestRepairLocations",
        "guard": "(repair_loc' != undef_string)"
     },
     {
        "source": 7,
        "target": 8,
        "name": "RepairerNotify",
        "guard": "(repair_loc != undef_string)"
     },
     {
        "source": 8,
        "target": 5,
        "name": "PerformRepair"
     },
     {
        "source": 1,
        "target": 9,
        "name": "OpenExceedDeductible",
        "guard": "CaseType(case_id) == ExceedDeductible"
     },
     {
        "source": 9,
        "target": 5,
        "name": "Unrecoverable"
     },
     {
        "source": 9,
        "target": 10,
        "name": "CustomerPays"
     },
     {
        "source": 10,
        "target": 11,
        "name": "AdjusterApproves"
     },
     {
        "source": 11,
        "target": 5,
        "name": "RepairComplete"
     }
   ],
   "variables": [ 
      {
         "name": "case_id",
         "type": "case_id_type",
         "initial": "undef_case_id"
      },
      {
         "name": "repair_loc",
         "type": "string",
         "initial": "undef_string"
      }
   ],
   "relations": [
      {
         "name": "Customer",
         "domain": ["string", "string", "string"]
      },
      {
         "name": "Claim",
         "domain": ["rat", "string", "case_id_type"]
      }
   ],
   "functions": [ 
      {
         "name": "CaseCustomer",
         "domain": ["case_id_type"],
         "range": "customer_id"
      },
      {
        "name": "CaseType",
        "domain": ["case_id_type"],
        "range": "string"
      },
      {
        "name": "CaseEstimate",
        "domain": ["case_id_type"],
        "range": "rat"
      },
      {
        "name": "CaseDeductible",
        "domain": ["case_id_type"],
        "range": "rat"
      },
      {
         "name": "undef_case_id",
         "domain": [],
         "range": "case_id_type"
      },
      {
         "name": "customer_id_undef",
         "domain": [],
         "range": "customer_id"
      },
      {
         "name": "undef_string",
         "domain": [],
         "range": "string"
      },
      {
         "name": "NotExceedDeductible",
         "domain": [],
         "range": "string"
      },
      {
         "name": "ExceedDeductible",
         "domain": [],
         "range": "string"
      }
   ],
   "facts":"distinct(NotExceedDeductible, ExceedDeductible)",
   "ltl": [
      { "property": "F CaseEnded", "result": true },
      { "property": "F (OpeningExceedDeductible && G ! CaseEnded)", "result": false },
      { "property": "F (OpeningNotExceedDeductible && G ! CaseEnded)", "result": false },
      { "property": "F ((repair_loc != undef_string) && F (CaseType(case_id) == ExceedDeductible))", "result": false },
      { "property": "G ! Paid", "result": true }
   ]
}

LTL_f property