LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: acquisition following RFQ",
   "comment": "This example was adopted from the VERIFAS problem set. Updates of Candidates and Log relations were omitted.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/Acquisition-following-RFQ.txt",
   "states": [
     {
        "id": 0,
        "name": "start",
        "initial": true
     },
     {
        "id": 1,
        "name": "gotRequest"
     },
     {
        "id": 2,
        "name": "selectingSupplier"
     },
     {
        "id": 3,
        "name": "supplierSelected"
     },
     {
        "id": 4,
        "name": "noticeSent",
        "final": true
     },
     {
        "id": 5,
        "name": "resultSent"
     },
     {
        "id": 6,
        "name": "acquired",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "receiveRequest",
        "written": ["hasSupplier"],
        "guard": "((g1' != NULL) || (g2' != NULL) || (g3' != NULL)) && (cid' != NULL) && (sid' == NULL)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "analyzeAcquisitionRequest",
        "guard": "(EXISTS _x. Customer(cid, _x, Good_record))"
     },
     {
        "source": 2,
        "target": 2,
        "name": "addSupplier",
        "guard": "(sid' != NULL)"
     },
     {
        "source": 2,
        "target": 3,
        "name": "chooseSupplier",
        "guard": "((g1 != NULL) -> (EXISTS _n1 _q1. Supplier(sid, _n1, g1, _q1))) && ((g2 != NULL) -> (EXISTS _n2 _q2. Supplier(sid, _n2, g2, _q2))) && ((g3 != NULL) -> (EXISTS _n3 _q3. Supplier(sid, _n3, g3, _q3)))"
     },
     {
        "source": 2,
        "target": 3,
        "name": "chooseOptimalSupplier",
        "guard": "(sid != NULL)"
     },
     {
        "source": 2,
        "target": 3,
        "name": "chooseNoSupplier",
        "guard": "(sid != NULL)"
     },
     {
        "source": 3,
        "target": 4,
        "name": "sendNoSuppliersNotice",
        "guard": "(sid == NULL) || (supplierResponse == No)"
     },
     {
        "source": 3,
        "target": 5,
        "name": "submitResultToSupplier",
        "guard": "(sid != NULL) && ((supplierResponse' == No) || (supplierResponse' == Yes))"
     },
     {
        "source": 5,
        "target": 6,
        "name": "acquireDeliverGood",
        "guard": "(supplierResponse == Yes)"
     }
   ],
   "variables": [ 
      {
         "name": "cid",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "g1",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "g2",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "g3",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "sid",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "hasSupplier",
         "type": "string",
         "initial": "String_undef"
      },
      {
         "name": "supplierResponse",
         "type": "string",
         "initial": "String_undef"
      }
   ],
   "relations": [
      {
         "name": "Supplier",
         "domain": ["id_type", "string", "id_type", "int"]
      },
      {
         "name": "Customer",
         "domain": ["id_type", "string", "string"]
      },
      {
         "name": "Goods",
         "domain": ["id_type", "string"]
      }
   ],
   "functions": [ 
      {
         "name": "NULL",
         "domain": [],
         "range": "id_type"
      },
      {
         "name": "String_undef",
         "domain": [],
         "range": "string"
      },
      {
         "name": "Good_record",
         "domain": [],
         "range": "string"
      },
      {
         "name": "No",
         "domain": [],
         "range": "string"
      },
      {
         "name": "Yes",
         "domain": [],
         "range": "string"
      }
   ],
   "facts": "Yes != No",
   "ltl": [
      { "property": "(F acquired) || (F noticeSent)", "result": true },
      { "property": "F (gotRequest && (G ! acquired))", "result": true },
      { "property": "F ((cid != NULL) && (G ! acquired))", "result": true },
      { "property": "! acquired U (supplierResponse == Yes))", "result": true },
      { "property": "(G (supplierResponse != Yes)) && ((supplierResponse != Yes) U acquired)", "result": false }
   ]
}

LTL_f property