LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: Amazon fulfillment",
   "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/Amazon-Fulfillment.txt",
   "states": [
     {
        "id": 0,
        "name": "idle",
        "initial": true
     },
     {
        "id": 1,
        "name": "loggedIn"
     },
     {
        "id": 2,
        "name": "shopping"
     },
     {
        "id": 3,
        "name": "checkout"
     },
     {
        "id": 4,
        "name": "unpaid"
     },
     {
        "id": 5,
        "name": "paid"
     },
     {
        "id": 6,
        "name": "canceled",
        "final": true
     },
     {
        "id": 7,
        "name": "startPacking"
     },
     {
        "id": 8,
        "name": "packed"
     },
     {
        "id": 9,
        "name": "startedShipping"
     },
     {
        "id": 10,
        "name": "addingTruck"
     },
     {
        "id": 11,
        "name": "truckReady"
     },
     {
        "id": 12,
        "name": "shipped",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 0,
        "name": "enterCustomerInfo",
        "guard": "((name' != StringUndef) && (phone' != StringUndef) && (addr' != StringUndef) && (billing_addr' != StringUndef))"
     },
     {
        "source": 0,
        "target": 1,
        "name": "customerLogin",
        "guard": "(cid == NULL) && (EXISTS _x _y. Customer(cid', name', phone', addr', _x, _y)) && (cid' != NULL)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "startShopping"
     },
     {
        "source": 2,
        "target": 2,
        "name": "pickItem",
        "guard": "(iid == NULL) && (EXISTS _w _x _y _z. Item(iid', _w, _x, _y, _z)) && (iid' != NULL)"
     },
     {
        "source": 2,
        "target": 2,
        "name": "addToCart",
        "guard": "(iid' == NULL)"
     },
     {
        "source": 2,
        "target": 2,
        "name": "retrieveFromCart",
        "guard": "(iid == NULL) && (iid' != NULL)"
     },
     {
        "source": 2,
        "target": 3,
        "name": "finishShopping",
        "guard": "(iid != NULL)"
     },
     {
        "source": 3,
        "target": 4,
        "name": "initPayment",
        "guard": "(card_id' == NULLcard) && (billing_addr' == StringUndef)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "verifyCardInfo",
        "guard": "(card_id == NULLcard) && (CreditCard(card_id', name, billing_addr') || ((cid != NULL) -> (EXISTS _x _y _z. Customer(cid, _x, _y, _z, billing_addr', card_id') && CreditCard(card_id', name, billing_addr'))))"
     },
     {
        "source": 4,
        "target": 6,
        "name": "cancelPayment"
     },
     {
        "source": 5,
        "target": 7,
        "name": "startPacking",
        "guard": "(pid' == NULL)"
     },
     {
        "source": 7,
        "target": 8,
        "name": "pack",
        "guard": "(EXISTS _p _x _y _z. Package(pid', _p) && (Item(iid, _x, _y, pid, _z) || Item(iid, _x, _y, _z, pid)) )"
     },
     {
        "source": 8,
        "target": 9,
        "name": "startShipping"
     },
     {
        "source": 9,
        "target": 10,
        "name": "newTruck",
        "guard": "(tid == NULL) && (tid' != NULL) && (EXISTS _w _x _y _z. Truck(tid, _w, _x, _y, _z))"
     },
     {
        "source": 10,
        "target": 10,
        "name": "addCandTruck",
        "guard": "(tid' == NULL) && (tid != NULL) && (EXISTS _w _x _y _z. Truck(tid, _w, pid, _y, _z) || Truck(tid, _w, _x, pid, _z) || Truck(tid, _w, _x, _y, pid))"
     },
     {
        "source": 10,
        "target": 11,
        "name": "retrieveTruck",
        "guard": "(tid == NULL) && (tid' != NULL) && (EXISTS _w _x _y _z. Truck(tid, _w, pid, _y, _z) || Truck(tid, _w, _x, pid, _z) || Truck(tid, _w, _x, _y, pid))"
     },
     {
        "source": 11,
        "target": 12,
        "name": "ship"
     }
   ],
   "variables": [ 
      {
         "name": "cid",
         "type": "id_type",
         "initial": "NULL"
      }, 
      {
         "name": "name",
         "type": "string",
         "initial": "StringUndef"
      },
      {
         "name": "phone",
         "type": "string",
         "initial": "StringUndef"
      },
      {
         "name": "addr",
         "type": "string",
         "initial": "StringUndef"
      },
      {
         "name": "billing_addr",
         "type": "string",
         "initial": "StringUndef"
      },
      {
         "name": "iid",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "card_id",
         "type": "card_number",
         "initial": "NULLcard"
      },
      {
         "name": "tid",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "pid",
         "type": "id_type",
         "initial": "NULL"
      }
   ],
   "relations": [
      {
         "name": "Customer",
         "domain": ["id_type", "string", "string", "string", "string", "card_number"]
      },
      {
         "name": "Package",
         "domain": ["id_type", "rat"]
      },
      {
         "name": "Item",
         "domain": ["id_type", "string", "rat", "id_type", "id_type"]
      },
      {
         "name": "CreditCard",
         "domain": ["card_number", "string", "string"]
      },
      {
         "name": "Truck",
         "domain": ["id_type", "string", "id_type", "id_type", "id_type"]
      }
   ],
   "functions": [ 
      {
         "name": "NULL",
         "domain": [],
         "range": "id_type"
      },
      {
         "name": "NULLcard",
         "domain": [],
         "range": "card_number"
      },
      {
         "name": "StringUndef",
         "domain": [],
         "range": "string"
      }
   ],
   "ltl": [
      { "property": "F ((paid) && (G ! shipped))", "result": false },
      { "property": "G ! paid", "result": true },
      { "property": "F (paid && X F canceled)", "result": false },
      { "property": "G ((tid == NULL) && (cid == NULL))", "result": false },
      { "property": "F ((billing_addr != StringUndef) && G ! shipped)", "result": true }
   ]
}

LTL_f property