LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: new car sales",
   "comment": "This example was adopted from the VERIFAS problem set.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/New-Car-Sales.txt",
   "states": [
     {
        "id": 0,
        "name": "start",
        "initial": true
     },
     {
        "id": 1,
        "name": "orderEntered"
     },
     {
        "id": 2,
        "name": "requestSubmitted"
     },
     {
        "id": 3,
        "name": "closedAndDelivered",
        "final": true
     },
     {
        "id": 4,
        "name": "financingFailed",
        "final": true
     },
     {
        "id": 5,
        "name": "financingReady"
     },
     {
        "id": 6,
        "name": "carAvailable"
     },
     {
        "id": 7,
        "name": "carUnavailable"
     },
     {
        "id": 8,
        "name": "customerAccept"
     },
     {
        "id": 9,
        "name": "customerDecline"
     },
     {
        "id": 10,
        "name": "customerAcceptAlternative"
     },
     {
        "id": 12,
        "name": "deliveryReady"
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "enterOrder1",
        "guard": "(cid == carmodel_undef) && (cid' != carmodel_undef) && (sid' == special_undef) && (orderfromfactory' == true)"
     },
     {
        "source": 0,
        "target": 1,
        "name": "enterOrder2",
        "guard": "(cid == carmodel_undef) && (cid' != carmodel_undef) && special(sid',cid',discount') && (orderfromfactory' == true)"
     },
     {
        "source": 0,
        "target": 1,
        "name": "enterOrder3",
        "guard": "(cid == carmodel_undef) && (cid' != carmodel_undef) && special(sid',cid',discount') && (orderfromfactory' == false) && carModel(cid', name', true, true, price')"
     },
     {
        "source": 0,
        "target": 1,
        "name": "enterOrder4",
        "guard": "(cid == carmodel_undef) && (cid' != carmodel_undef) && (sid' == special_undef) && (orderfromfactory' == false) && carModel(cid', name', true, true, price')"
     },
     {
        "source": 1,
        "target": 6,
        "name": "placeFactoryOrder",
        "guard": "orderfromfactory == true"
     },
     {
        "source": 1,
        "target": 7,
        "name": "placeFactoryOrder",
        "guard": "orderfromfactory == true"
     },
     {
        "source": 6,
        "target": 8,
        "name": "notifyPromisedDate",
        "guard": "deliverydate' != string_undef"
     },
     {
        "source": 6,
        "target": 9,
        "name": "notifyPromisedDate",
        "guard": "deliverydate' != string_undef"
     },
     {
        "source": 8,
        "target": 12,
        "name": "prepareDelivery"
     },
     {
        "source": 9,
        "target": 10,
        "name": "offerAlternative1",
        "guard": "carModel(cid, name, true, true, price) && carModel(cid', name', true, true, price') && (price' <= price * 1.1)"
     },
     {
        "source": 7,
        "target": 10,
        "name": "offerAlternative1",
        "guard": "carModel(cid, name, true, true, price) && carModel(cid', name', true, true, price') && (price' <= price * 1.1)"
     },
     {
        "source": 12,
        "target": 2,
        "name": "completeApplication1",
        "guard": "(sid != special_undef) && special(sid, cid, discount') && loan(lid', length', maxamount', interest') && carModel(cid, name, true, true, price) && (amount' == price - discount') && (maxamount' >= amount') && (interest' >= 0) && (price' >= 0) && (amount' >= 0)"
     },
     {
        "source": 12,
        "target": 2,
        "name": "completeApplication2",
        "guard": "(sid == special_undef) && loan(lid', length', maxamount', interest') && carModel(cid, name, true, true, price) && (amount' == price) && (maxamount' >= amount') && (interest' >= 0) && (price' >= 0) && (amount' >= 0)"
     },
     {
        "source": 2,
        "target": 4,
        "guard": "financed' == false",
        "name": "requestFinancingFails"
     },
     {
        "source": 2,
        "target": 5,
        "guard": "financed' == true",
        "name": "requestFinancingSucceeds"
     },
     {
        "source": 5,
        "target": 3,
        "name": "closeFinancing"
     }
   ],
   "variables": [ 
      {
         "name": "cid",
         "type": "carid",
         "initial": "carmodel_undef"
      },
      {
         "name": "sid",
         "type": "specialid",
         "initial": "special_undef"
      },
      {
         "name": "orderfromfactory",
         "type": "bool",
         "initial": false
      },
      {
         "name": "financed",
         "type": "bool",
         "initial": false
      },
      {
         "name": "name",
         "type": "string",
         "initial": "string_undef"
      },
      {
         "name": "amount",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "amountfinanced",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "length",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "interest",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "price",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "discount",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "maxamount",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "lid",
         "type": "loanid",
         "initial": "loan_undef"
      },
      {
         "name": "deliverydate",
         "type": "string",
         "initial": "string_undef"
      }
   ],
   "relations": [ 
      {
         "name": "loan",
         "domain": ["loanid", "rat", "rat", "rat"]
      },
      {
         "name": "special",
         "domain": ["specialid", "carid", "rat"]
      },
      {
         "name": "carModel",
         "domain": ["carid", "string", "bool", "bool", "rat"]
      }
   ],
   "functions": [ 
      {
         "name": "carmodel_undef",
         "domain": [],
         "range": "carid"
      },
      {
         "name": "special_undef",
         "domain": [],
         "range": "specialid"
      },
      {
         "name": "string_undef",
         "domain": [],
         "range": "string"
      },
      {
         "name": "loan_undef",
         "domain": [],
         "range": "loanid"
      }
   ],
   "ltl": [
      { "property": "F closedAndDelivered", "result": true },
      { "property": "F (orderEntered && G ! closedAndDelivered)", "result": true },
      { "property": "F (closedAndDelivered && (maxamount < amount))", "result": false },
      { "property": "F (deliveryReady && (maxamount >= amount) && G ! closedAndDelivered)", "result": true },
      { "property": "! closedAndDelivered U (financed == True))", "result": true }
   ]
}

LTL_f property