LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "paper examples: webshop",
   "comment": "This example models the webshop system given in the introduction of the paper.",
   "states": [
     {
        "id": 1,
        "name": "b1",
        "initial": true
     },
     {
        "id": 2,
        "name": "b2"
     },
     {
        "id": 3,
        "name": "b3"
     },
     {
        "id": 4,
        "name": "b4"
     },
     {
        "id": 5,
        "name": "b5"
     },
     {
        "id": 6,
        "name": "shipped",
        "final": true
     },
     {
        "id": 7,
        "name": "b7",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 1,
        "target": 2,
        "name": "login",
        "guard": "cust(xcst', xbank', xvip')"
     },
     {
        "source": 2,
        "target": 3,
        "name": "select",
        "guard": "itmid(xitm1') && itmid(xitm2') && itmid(xitm3') && itmid(xitm4') && itmid(xitm5') "
     },
     {
        "source": 3,
        "target": 4,
        "name": "sumup",
        "guard": "(xtotal' == price(xitm1) + price(xitm2) + price(xitm3) + price(xitm4) + price(xitm5))"
     },
     {
        "source": 4,
        "target": 5,
        "name": "discount",
        "guard": "( (xvip == 1) && (xtotal' == xtotal - 0.2 * xtotal))"
     },
     {
        "source": 4,
        "target": 5,
        "name": "nodiscount",
        "guard": "(xvip == 0)"
     },
     {
        "source": 5,
        "target": 6,
        "name": "ship",
        "guard": "(xtotal <= xbank)"
     },
     {
        "source": 5,
        "target": 7,
        "name": "reject",
        "guard": "(xtotal > xbank)"
     },
     {
        "source": 7,
        "target": 2,
        "name": "restart",
        "guard": "((xitm1 == itemid_undef) && (xitm2 == itemid_undef))"
     }
   ],
   "variables": [ 
      {
         "name": "xcst",
         "type": "customerid",
         "initial": "customerid_undef"
      },
      {
         "name": "xbank",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "xvip",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "xitm1",
         "type": "itemid",
         "initial": "itemid_undef"
      },
      {
         "name": "xitm2",
         "type": "itemid",
         "initial": "itemid_undef"
      },
      {
         "name": "xitm3",
         "type": "itemid",
         "initial": "itemid_undef"
      },
      {
         "name": "xitm4",
         "type": "itemid",
         "initial": "itemid_undef"
      },
      {
         "name": "xitm5",
         "type": "itemid",
         "initial": "itemid_undef"
      },
      {
         "name": "xtotal",
         "type": "rat",
         "initial": 0
      }
   ],
   "relations": [ 
      {
         "name": "cust",
         "domain": ["customerid", "rat", "rat"]
      },
      {
         "name": "itmid",
         "domain": ["itemid"]
      }
   ],
   "functions": [ 
      {
         "name": "price",
         "domain": ["itemid"],
         "range": "rat"
      },
      {
         "name": "itemid_undef",
         "domain": [],
         "range": "itemid"
      },
      {
         "name": "customerid_undef",
         "domain": [],
         "range": "customerid"
      }
   ],
   "ltl": [
      { "property": "F (shipped && ((price(xitm1) + (price(xitm2) + (price(xitm3) + (price(xitm4) + price(xitm5))))) > xbank)))", "result": true },
      { "property": "F ((<sumup> True) && G (! shipped))", "result": true },
      { "property": "F (shipped && (xtotal > xbank))", "result": false },
      { "property": "G (<sumup> True) && G (! shipped)", "result": false },
      { "property": "F ((xtotal > xbank) && X (F shipped))", "result": true },
      { "property": "(! shipped) U shipped", "result": true }
   ]
}

LTL_f property