LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: mortgage",
  "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/Morgage-Approval.txt",
  "states": [
    {
       "id": 0,
       "name": "Start",
       "initial": true
    },
    {
     "id": 1,
     "name": "NotInterested"
    },
    {
     "id": 2,
     "name": "SevenDays"
    },
    {
     "id": 3,
     "name": "FillApplication"
    },
    {
     "id": 4,
     "name": "Archived",
     "final": true
    },
    {
     "id": 5,
     "name": "CompletedApplication"
    },
    {
     "id": 6,
     "name": "OpeningAssessment"
    },
    {
     "id": 7,
     "name": "Offer"
    },
    {
     "id": 8,
     "name": "Rejected"
    },
    {
     "id": 9,
     "name": "OfferMade",
     "final": true
    },
    {
     "id": 10,
     "name": "RejectSent",
     "final": true
    }
  ],
  "transitions": [
    {
       "source": 0,
       "target": 1,
       "name": "SendOutApplication",
       "guard": "(customer_id' != undef_customer_id) && ((app_type' == VIP) || (app_type' == Normal))"
    },
    {
       "source": 0,
       "target": 2,
       "name": "SendOutApplication",
       "guard": "(customer_id' != undef_customer_id) && ((app_type' == VIP) || (app_type' == Normal))"
    },
    {
       "source": 0,
       "target": 3,
       "name": "SendOutApplication",
       "guard": "(customer_id' != undef_customer_id) && ((app_type' == VIP) || (app_type' == Normal))"
    },
    {
       "source": 2,
       "target": 2,
       "name": "SendReminder"
    },
    {
       "source": 2,
       "target": 1,
       "name": "SendReminder"
    },
    {
       "source": 2,
       "target": 3,
       "name": "SendReminder"
    },
    {
       "source": 1,
       "target": 4,
       "name": "ArchiveDetails",
       "guard": "(archived' == customer_id)"
    },
    {
       "source": 3,
       "target": 5,
       "name": "CompleteApplication",
       "guard": "((length' > 0) && (amount' > 0) && (mortgage_id' != undef_mortgage_id))"
    },
    {
       "source": 5,
       "target": 6,
       "name": "openAssessment"
    },
    {
       "source": 6,
       "target": 7,
       "name": "MakeAssessment1",
       "guard": "(max_amount' == MortgageAmount(customer_id)) && (max_length' == MortgageLength(customer_id)) && Record(customer_id, Good) && BankAccount(customer_id, bank_amount') && (CustomerIncome(customer_id) == income') && ((income' + bank_amount') > amount) && (amount < max_amount') && (length < max_length')"
    },
    {
       "source": 6,
       "target": 8,
       "name": "MakeAssessment2",
       "guard": "(max_amount' == MortgageAmount(customer_id)) && (max_length' == MortgageLength(customer_id))"
    },
    {
       "source": 7,
       "target": 9,
       "name": "OfferMortgage"
    },
    {
       "source": 8,
       "target": 10,
       "name": "SendReject"
    }
  ],
  "variables": [ 
     {
        "name": "customer_id",
        "type": "customer_id_type",
        "initial": "undef_customer_id"
     },
     {
        "name": "archived",
        "type": "customer_id_type",
        "initial": "undef_customer_id"
     },
     {
        "name": "mortgage_id",
        "type": "mortgage_id_type",
        "initial": "undef_mortgage_id"
     },
     {
        "name": "length",
        "type": "rat",
        "initial": "-1"
     },
     {
        "name": "amount",
        "type": "rat",
        "initial": "-1"
     },
     {
        "name": "app_type",
        "type": "string",
        "initial": "undef_string"
     },
      {
        "name": "bank_amount",
        "type": "rat",
        "initial": "-1"
     },
      {
        "name": "income",
        "type": "rat",
        "initial": "-1"
     },
      {
        "name": "max_amount",
        "type": "rat",
        "initial": "-1"
     },
     {
        "name": "max_length",
        "type": "rat",
        "initial": "-1"
     }
  ],
  "relations": [
     {
        "name": "BankAccount",
        "domain": ["customer_id_type", "rat"]
     },
     {
        "name": "Record",
        "domain": ["customer_id_type", "string"]
     }
  ],
  "functions": [ 
      {
        "name": "MortgageName",
        "domain": ["mortgage_id_type"],
        "range": "string"
     },
      {
        "name": "MortgageAmount",
        "domain": ["mortgage_id_type"],
        "range": "rat"
     },
     {
        "name": "MortgageLength",
        "domain": ["mortgage_id_type"],
        "range": "rat"
     },
     {
        "name": "MortgageInterest",
        "domain": ["mortgage_id_type"],
        "range": "rat"
     },
     {
        "name": "CustomerName",
        "domain": ["customer_id_type"],
        "range": "string"
     },
     {
       "name": "CustomerIncome",
       "domain": ["customer_id_type"],
       "range": "rat"
     },
     {
        "name": "undef_customer_id",
        "domain": [],
        "range": "customer_id_type"
     },
     {
        "name": "undef_mortgage_id",
        "domain": [],
        "range": "mortgage_id_type"
     },
     {
        "name": "undef_string",
        "domain": [],
        "range": "string"
     },
     {
        "name": "VIP",
        "domain": [],
        "range": "string"
     },
     {
        "name": "Normal",
        "domain": [],
        "range": "string"
     },
     {
        "name": "Good",
        "domain": [],
        "range": "string"
     }
  ],
  "facts":"distinct(VIP, Normal)",
  "ltl": [
     { "property": "F OfferMade", "result": true },
     { "property": "F (SevenDays && G ! OfferMade)", "result": true },
     { "property": "F ((app_type == VIP) && G ((income + bank_amount) <= amount))", "result": true },
     { "property": "F OfferMade && F RejectSent", "result": false },
     { "property": "F (OfferMade && (length > max_length))", "result": false }
  ]
}

LTL_f property