LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: hardware retailer",
   "comment": "This example models an order process of a hardware retailer, it was adopted from the VERIFAS problem set. The carrier and retailer relations were dropped since they are not used. The second and third argument of hardware was removed as it is not used in constraints.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/Ship-Process-of-a-Hardware-Retailer.txt",
   "states": [
     {
        "id": 0,
        "name": "start",
        "initial": true
     },
     {
        "id": 1,
        "name": "analyzeRequest"
     },
     {
        "id": 2,
        "name": "directPickup"
     },
     {
        "id": 3,
        "name": "shippingRequired"
     },
     {
        "id": 4,
        "name": "carrierShipping"
     },
     {
        "id": 5,
        "name": "ready"
     },
     {
        "id": 6,
        "name": "normalShipping"
     },
     {
        "id": 7,
        "name": "insuranceChecked"
     },
     {
        "id": 8,
        "name": "shipped",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "receiveShippingRequest1",
        "guard": "(rid' != retailer_undef) && (h1' != hardware_undef) && (caid' == carrier_undef) && (cuid' != customer_undef) && (employee' != customer_undef) && (location' != string_undef)"
     },
     {
        "source": 0,
        "target": 1,
        "name": "receiveShippingRequest2",
        "guard": "(rid' != retailer_undef) && (h2' != hardware_undef) && (caid' == carrier_undef) && (cuid' != customer_undef) && (employee' != customer_undef) && (location' != string_undef)"
     },
     {
        "source": 0,
        "target": 1,
        "name": "receiveShippingRequest3",
        "guard": "(rid' != retailer_undef) && (h3' != hardware_undef) && (caid' == carrier_undef) && (cuid' != customer_undef) && (employee' != customer_undef) && (location' != string_undef)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "analyzeShippingRequest1",
        "guard": "customer(cuid, dummy', true, location)"
     },
     {
        "source": 1,
        "target": 3,
        "name": "analyzeShippingRequest2",
        "guard": "customer(cuid, dummy', false, location) && (price' >= 0) && (hardware(h1, normal) || hardware(h1, fragile)) && (hardware(h2, normal) || hardware(h2, fragile)) && (hardware(h3, normal) || hardware(h3, fragile))"
     },
     {
        "source": 2,
        "target": 8,
        "name": "pickup",
        "guard": "true"
     },
     {
        "source": 4,
        "target": 5,
        "name": "requestQuotes",
        "guard": "quote' > 0"
     },
     {
        "source": 6,
        "target": 7,
        "name": "checkInsurance",
        "guard": "insurance_fee' > 0"
     },
     {
        "source": 3,
        "target": 4,
        "name": "shippingDecision1",
        "guard": "(hardware(h1, fragile) || hardware(h2, fragile) || hardware(h3, fragile)) && (caid' != carrier_undef)"
     },
     {
        "source": 3,
        "target": 6,
        "name": "shippingDecision2",
        "guard": "hardware(h1, normal) && hardware(h2, normal) && hardware(h3, normal) "
     },
     {
        "source": 5,
        "target": 8,
        "name": "shipping",
        "guard": "true"
     },
     {
        "source": 7,
        "target": 8,
        "name": "estimateFee",
        "guard": "(handling_fee' > 0) && (fee' == insurance_fee + handling_fee)"
     }
   ],
   "variables": [ 
      {
         "name": "rid",
         "type": "retailerid",
         "initial": "retailer_undef"
      },
      {
         "name": "h1",
         "type": "hardwareid",
         "initial": "hardware_undef"
      },
      {
         "name": "h2",
         "type": "hardwareid",
         "initial": "hardware_undef"
      },
      {
         "name": "h3",
         "type": "hardwareid",
         "initial": "hardware_undef"
      },
      {
         "name": "caid",
         "type": "carrierid",
         "initial": "carrier_undef"
      },
      {
         "name": "cuid",
         "type": "customerid",
         "initial": "customer_undef"
      },
      {
         "name": "employee",
         "type": "customerid",
         "initial": "customer_undef"
      },
      {
         "name": "location",
         "type": "string",
         "initial": "string_undef"
      },
      {
         "name": "dummy",
         "type": "string",
         "initial": "string_undef"
      },
      {
         "name": "price",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "quote",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "insurance_fee",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "handling_fee",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "fee",
         "type": "rat",
         "initial": 0
      }
   ],
   "relations": [
      {
         "name": "hardware",
         "domain": ["hardwareid", "hardware_type"]
      },
      {
         "name": "customer",
         "domain": ["customerid", "string", "bool", "string"]
      }
   ],
   "functions": [ 
      {
         "name": "retailer_undef",
         "domain": [],
         "range": "retailerid"
      },
      {
         "name": "hardware_undef",
         "domain": [],
         "range": "hardwareid"
      },
      {
         "name": "string_undef",
         "domain": [],
         "range": "string"
      },
      {
         "name": "carrier_undef",
         "domain": [],
         "range": "carrierid"
      },
      {
         "name": "customer_undef",
         "domain": [],
         "range": "customerid"
      },
      {
         "name": "normal",
         "domain": [],
         "range": "hardware_type"
      },
      {
         "name": "fragile",
         "domain": [],
         "range": "hardware_type"
      }
   ],
   "ltl": [
      { "property": "(F normalShipping) && (G (fee <= 0))", "result": false },
      { "property": "F (shipped && (fee < (insurance_fee + handling_fee)))", "result": true },
      { "property": "(F normalShipping) && (G ((insurance_fee == 0) && (handling_fee == 0)))", "result": false },
      { "property": "G ! shipped", "result": false },
      { "property": "F (<requestQuotes> (quote == 0))", "result": false }
   ]
}

LTL_f property