LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "BPM: credit approval",
   "states": [
     {
        "id": 0,
        "name": "s0",
        "initial": true
     },
     {
        "id": 1,
        "name": "s1"
     },
     {
        "id": 2,
        "name": "s2"
     },
     {
        "id": 3,
        "name": "s3"
     },
     {
        "id": 4,
        "name": "s4"
     },
     {
        "id": 5,
        "name": "end",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "creditRequest",
        "guard": "(amount' > 0)",
        "written": ["vip", "amount"]
     },
     {
        "source": 1,
        "target": 2,
        "name": "verify",
        "written": ["ver"]
     },
     {
        "source": 2,
        "target": 3,
        "name": "simpleAssessment",
        "guard": "((ver == Verified) && (amount <= 5000) && (0.15 * amount < interest') && (interest' < 0.2 * amount))",
        "written": ["dec"]
     },
     {
        "source": 2,
        "target": 3,
        "name": "advancedAssessment",
        "guard": "((ver == Verified) && (amount > 5000) && (0.1 * amount < interest') && (interest' < 0.15 * amount))",
        "written": ["dec"]
     },
     {
        "source": 2,
        "target": 4,
        "name": "skipAssessment",
        "guard": "(ver != Verified)",
        "written": ["dec"]
     },
     {
        "source": 3,
        "target": 1,
        "name": "renegotiate"
     },
     {
        "source": 3,
        "target": 4,
        "name": "proceed"
     },
     {
        "source": 4,
        "target": 5,
        "name": "informNormalCustomer",
        "guard": "(vip != Is_vip)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "informVipCustomer",
        "guard": "(vip == Is_vip)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "openLoan",
        "guard": "((ver == Verified) && (dec == Accept))"
     }
   ],
   "variables": [ 
      {
         "name": "amount",
         "type": "rat",
         "initial": 0.0
      }, 
      {
         "name": "interest",
         "type": "rat",
         "initial": 0.0
      }, 
      {
         "name": "ver",
         "type": "type_ver",
         "initial": "Undef_verified"
      }, 
      {
         "name": "dec",
         "type": "type_dec",
         "initial": "Undef_decision"
      }, 
      {
         "name": "vip",
         "type": "type_vip",
         "initial": "Undef_vip"
      }
   ],
   "functions": [ 
      {
         "name": "Is_vip",
         "domain": [],
         "range": "type_vip"
      },
      {
         "name": "Is_no_vip",
         "domain": [],
         "range": "type_vip"
      },
      {
         "name": "Undef_vip",
         "domain": [],
         "range": "type_vip"
      },
      {
         "name": "Verified",
         "domain": [],
         "range": "type_ver"
      },
      {
         "name": "Not_verified",
         "domain": [],
         "range": "type_ver"
      },
      {
         "name": "Undef_verified",
         "domain": [],
         "range": "type_ver"
      },
      {
         "name": "Accept",
         "domain": [],
         "range": "type_dec"
      },
      {
         "name": "Reject",
         "domain": [],
         "range": "type_dec"
      },
      {
         "name": "Undef_decision",
         "domain": [],
         "range": "type_dec"
      }
    ],
    "ltl": [
       { "property": "F ((<openLoan> True) && (ver != Verified))", "result": false },
       { "property": "F ((<creditRequest> True) && G (dec != Accept))", "result": true },
       { "property": "F ((ver == Not_verified) && X F (ver == Verified))", "result": true },
       { "property": "(F ((<creditRequest> True) && G (ver != Verified))) && F (amount > 10000)", "result": true },
       { "property": "F ((amount == 10000) && (interest == 500) && F (<proceed> True))", "result": false }
    ]
}

LTL_f property