LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "Web service: Loan application",
   "comment": "Adapted from A, Deutsch, L, Sui, V, Vianu, D, Zhou: Verification of communicating data-driven web services, PODS 2006",
   "states": [
     {
        "id": 0,
        "name": "b0",
        "initial": true
     },
     {
        "id": 1,
        "name": "application"
     },
     {
        "id": 2,
        "name": "rating_obtained"
     },
     {
        "id": 3,
        "name": "history_check"
     },
     {
        "id": 4,
        "name": "await_manager"
     },
     {
        "id": 5,
        "name": "decided"
     },
     {
        "id": 6,
        "name": "completed",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "apply",
        "written": ["id"],
        "guard": "(loan' > 0)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "getRating",
        "guard": "(EXISTS _ssn _name . Customer(id, _ssn, _name)) && (rat' == Rating(id)) && (rat' != Rating_undef)"
     },
     {
        "source": 2,
        "target": 3,
        "name": "requestHistory"
     },
     {
        "source": 3,
        "target": 4,
        "name": "getHistory",
        "written": ["rec"]
     },
     {
        "source": 2,
        "target": 4,
        "name": "approve",
        "guard": "(rat == Excellent) && (rec == Accept)"
     },
     {
        "source": 2,
        "target": 4,
        "name": "deny",
        "guard": "(rat == Poor) && (rec == Reject)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "managerDecide",
        "written": ["dec"]
     },
     {
        "source": 5,
        "target": 6,
        "name": "writeLetter"
     }
   ],
   "variables": [ 
      {
         "name": "rat",
         "type": "type_rating",
         "initial": "Rating_undef"
      },
      {
         "name": "rec",
         "type": "type_decision",
         "initial": "Reject"
      },
      {
         "name": "id",
         "type": "type_id",
         "initial": "Id_undef"
      },
      {
         "name": "dec",
         "type": "type_decision",
         "initial": "Reject"
      },
      {
         "name": "loan",
         "type": "int",
         "initial": 0
      }
   ],
   "relations": [ 
      {
         "name": "Customer",
         "domain": ["type_id", "int", "string"]
      }
   ],
   "functions": [ 
      {
         "name": "Rating_undef",
         "domain": [],
         "range": "type_rating"
      },
      {
         "name": "Excellent",
         "domain": [],
         "range": "type_rating"
      },
      {
         "name": "Poor",
         "domain": [],
         "range": "type_rating"
      },
      {
         "name": "Id_undef",
         "domain": [],
         "range": "type_id"
      },
      {
         "name": "Id0",
         "domain": [],
         "range": "type_id"
      },
      {
         "name": "Accept",
         "domain": [],
         "range": "type_decision"
      },
      {
         "name": "Reject",
         "domain": [],
         "range": "type_decision"
      },
      {
         "name": "Rating",
         "domain": ["type_id"],
         "range": "type_rating"
      }
   ],
   "facts":"distinct(Poor, Excellent, Rating_undef)",
   "ltl": [
      { "property": "(F ((rating_obtained && (rat != Poor) && (rat != Excellent))) && (G (! history_check)))", "result": false },
      { "property": "G ((rating_obtained && (rat != Poor) && (rat != Excellent)) -> (F history_check))", "result": true },
      { "property": "F ((rat == Excellent) && X F (rat == Poor))", "result": false },
      { "property": "F ((rat == Excellent) && G (! completed))", "result": false },
      { "property": "F (rating_obtained && X(! history_check) && (rat != Poor) && (rat != Excellent))", "result": false }
   ]
}

LTL_f property