LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: LaserTec production process",
   "comment": "This example was adopted from the VERIFAS problem set. Relations order and customer were dropped since they do not occur in constraints.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/LaserTec-Production-Process.txt",
   "states": [
     {
        "id": 0,
        "name": "start",
        "initial": true
     },
     {
        "id": 1,
        "name": "orderInitialized"
     },
     {
        "id": 2,
        "name": "orderPlaced"
     },
     {
        "id": 3,
        "name": "partsAssembled",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "initializeOrder",
        "guard": "(oid' != orderid_undef) && ((c1' == componentid_undef) || component(c1', c1price')) && ((c2' == componentid_undef) || component(c2', c2price')) && ((c3' == componentid_undef) || component(c3', c3price'))  && (totalPrice' == c1price' + (c2price' + c3price')) && (install' != string_undef) && (cid' != customerid_undef)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "orderConfirm",
        "guard": "totalPrice > 0"
     },
     {
        "source": 2,
        "target": 3,
        "name": "orderLaserParts",
        "guard": "(c1 != componentid_undef) && (c2 != componentid_undef) && (c3 != componentid_undef)"
     },
     {
        "source": 1,
        "target": 0,
        "name": "restart1"
     },
     {
        "source": 2,
        "target": 0,
        "name": "restart2"
     }
   ],
   "variables": [ 
      {
         "name": "oid",
         "type": "orderid",
         "initial": "orderid_undef"
      },
      {
         "name": "totalPrice",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "cid",
         "type": "customerid",
         "initial": "customerid_undef"
      },
      {
         "name": "c1",
         "type": "componentid",
         "initial": "componentid_undef"
      },
      {
         "name": "c2",
         "type": "componentid",
         "initial": "componentid_undef"
      },
      {
         "name": "c3",
         "type": "componentid",
         "initial": "componentid_undef"
      },
      {
         "name": "install",
         "type": "string",
         "initial": "string_undef"
      },
      {
         "name": "c1price",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "c2price",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "c3price",
         "type": "rat",
         "initial": 0
      }
   ],
   "relations": [
      {
         "name": "component",
         "domain": ["componentid", "rat"]
      }
   ],
   "functions": [ 
      {
         "name": "orderid_undef",
         "domain": [],
         "range": "orderid"
      },
      {
         "name": "componentid_undef",
         "domain": [],
         "range": "componentid"
      },
      {
         "name": "customerid_undef",
         "domain": [],
         "range": "customerid"
      },
      {
         "name": "string_undef",
         "domain": [],
         "range": "string"
      }
   ],
   "ltl": [
      { "property": "X F partsAssembled", "result": true },
      { "property": "G ! partsAssembled", "result": false },
      { "property": "(oid == orderid_undef) U (totalPrice > 0)", "result": true },
      { "property":"F (orderPlaced && (c1 == componentid_undef) && (c2 == componentid_undef) && (c3 == componentid_undef))", "result": true },
      { "property": "F (orderPlaced && X G ! partsAssembled)", "result": false }
   ]
}

LTL_f property