LinDMT: LTLf Model Checking Modulo Theories

input system

{
  "name": "BPM: package handling",
  "comment": "Felli, P., de Leoni, M., Montali, M.: Integrating BPMN and DMN: Modeling and Analysis, JODS 10, 165-80, 2021, Fig. 1",
  "states": [
    {
      "id": 0,
      "name": "p0",
      "initial": true,
      "final": false
    },
    {
      "id": 1,
      "name": "p1",
      "initial": false,
      "final": false
    },
    {
      "id": 2,
      "name": "p2",
      "initial": false,
      "final": false
    },
    {
      "id": 3,
      "name": "p3",
      "initial": false,
      "final": false
    },
    {
      "id": 4,
      "name": "p4",
      "initial": false,
      "final": false
    },
    {
      "id": 5,
      "name": "p5",
      "initial": false,
      "final": false
    },
    {
      "id": 6,
      "name": "p6",
      "initial": false,
      "final": false
    },
    {
      "id": 7,
      "name": "p7",
      "initial": false,
      "final": false
    },
    {
      "id": 8,
      "name": "p8",
      "initial": false,
      "final": false
    },
    {
      "id": 9,
      "name": "p9",
      "initial": false,
      "final": false
    },
    {
      "id": 10,
      "name": "p10",
      "initial": false,
      "final": false
    },
    {
      "id": 11,
      "name": "p11",
      "initial": false,
      "final": false
    },
    {
      "id": 12,
      "name": "declared",
      "initial": false,
      "final": false
    },
    {
      "id": 13,
      "name": "p13",
      "initial": false,
      "final": false
    },
    {
      "id": 14,
      "name": "p14",
      "initial": false,
      "final": false
    },
    {
      "id": 15,
      "name": "end",
      "initial": false,
      "final": true
    }
  ],
  "transitions": [
    {
      "source": 0,
      "target": 1,
      "name": "init",
      "guard": "(pType' != sizeUndef)",
      "written": [
        "pType"
      ]
    },
    {
      "source": 1,
      "target": 2,
      "name": "getlength1",
      "guard": "((pType == std) && (pL' == 0.5))",
      "written": [
        "pL"
      ]
    },
    {
      "source": 1,
      "target": 2,
      "name": "getlength2",
      "guard": "((pType == large) && (pL' == 1))",
      "written": [
        "pL"
      ]
    },
    {
      "source": 1,
      "target": 2,
      "name": "getlength3",
      "guard": "((pType == xlarge) && (pL' == 2))",
      "written": [
        "pL"
      ]
    },
    {
      "source": 1,
      "target": 2,
      "name": "getlengthnoRow",
      "guard": "(((pType == sizeUndef) || ((pType != std) && ((pType != large) && (pType != xlarge)))) && (pL' == 0))",
      "written": [
        "pL"
      ]
    },
    {
      "source": 2,
      "target": 3,
      "name": "tau3",
      "guard": "(pL != 0)",
      "written": []
    },
    {
      "source": 2,
      "target": 15,
      "name": "tau2",
      "guard": "(pL == 0)",
      "written": []
    },
    {
      "source": 3,
      "target": 4,
      "name": "measure weight",
      "guard": "(pW' > 0)",
      "written": [
        "pW"
      ]
    },
    {
      "source": 4,
      "target": 15,
      "name": "tau5",
      "guard": "(pW > 10)",
      "written": []
    },
    {
      "source": 4,
      "target": 5,
      "name": "tau4",
      "guard": "(pW <= 10)",
      "written": []
    },
    {
      "source": 5,
      "target": 6,
      "name": "determinemode1",
      "guard": "((pL > 0) && (pL <= 1) && (pW > 0) && (pW <= 5) && (sMode' == Car))",
      "written": [
        "sMode"
      ]
    },
    {
      "source": 5,
      "target": 6,
      "name": "determinemode2",
      "guard": "((pL > 1) && ((pL <= 2) && ((pW > 0) && ((pW <= 5) && (sMode' == truck)))))",
      "written": [
        "sMode"
      ]
    },
    {
      "source": 5,
      "target": 6,
      "name": "determinemode3",
      "guard": "((pW > 5) && ((pW <= 10) && (sMode' == truck)))",
      "written": [
        "sMode"
      ]
    },
    {
      "source": 5,
      "target": 6,
      "name": "determinemodenoRow",
      "guard": "((((pL == 0) || ((pW == 0) || ((pL <= 0) || (pW <= 0)))) && (sMode' == modeUndef)) || (((pW > 10) || ((pW > 0) && ((pW <= 5) && (pL > 2)))) && (sMode' == modeUndef)))",
      "written": [
        "sMode"
      ]
    },
    {
      "source": 6,
      "target": 7,
      "name": "tau7",
      "guard": "(sMode != modeUndef)",
      "written": []
    },
    {
      "source": 6,
      "target": 15,
      "name": "tau6",
      "guard": "(sMode == modeUndef)",
      "written": []
    },
    {
      "source": 7,
      "target": 8,
      "name": "chooseconsent1",
      "guard": "((sMode == Car) && ((pW > 6) && (consent' == owner)))",
      "written": [
        "consent"
      ]
    },
    {
      "source": 7,
      "target": 8,
      "name": "chooseconsent2",
      "guard": "((sMode == truck) && ((pW > 8) && (consent' == com)))",
      "written": [
        "consent"
      ]
    },
    {
      "source": 7,
      "target": 8,
      "name": "chooseconsentnoRow",
      "guard": "((((sMode == modeUndef) || ((pW == 0) || (((sMode != Car) && (sMode != truck)) || (pW <= 0)))) && (consent' == noConsent)) || ((((sMode == Car) && (pW <= 6)) || ((sMode == truck) && (pW <= 8))) && (consent' == noConsent)))",
      "written": [
        "consent"
      ]
    },
    {
      "source": 8,
      "target": 13,
      "name": "tau10",
      "guard": "(consent == owner)",
      "written": []
    },
    {
      "source": 8,
      "target": 11,
      "name": "tau9",
      "guard": "(consent == com)",
      "written": []
    },
    {
      "source": 8,
      "target": 9,
      "name": "tau8",
      "guard": "(consent == owner)",
      "written": []
    },
    {
      "source": 9,
      "target": 10,
      "name": "sign declaration",
      "guard": "true",
      "written": []
    },
    {
      "source": 10,
      "target": 12,
      "name": "tau11",
      "guard": "true",
      "written": []
    },
    {
      "source": 11,
      "target": 12,
      "name": "tau13",
      "guard": "true",
      "written": []
    },
    {
      "source": 12,
      "target": 15,
      "name": "tau14",
      "guard": "true",
      "written": []
    },
    {
      "source": 13,
      "target": 14,
      "name": "fetch",
      "guard": "true",
      "written": []
    },
    {
      "source": 14,
      "target": 12,
      "name": "tau12",
      "guard": "true",
      "written": []
    }
  ],
  "variables": [
    {
      "name": "pL",
      "initial": 0,
      "type": "rat"
    },
    {
      "name": "pW",
      "initial": 0,
      "type": "rat"
    },
    {
      "name": "pType",
      "initial": "sizeUndef",
      "type": "size_type"
    },
    {
      "name": "sMode",
      "initial": "modeUndef",
      "type": "mode_type"
    },
    {
      "name": "consent",
      "initial": "noConsent",
      "type": "consent_type"
    }
  ],
  "functions": [
    {
       "name": "std",
       "domain": [],
       "range": "size_type"
    },
    {
      "name": "large",
      "domain": [],
      "range": "size_type"
    },
    {
      "name": "xlarge",
      "domain": [],
      "range": "size_type"
    },
    {
      "name": "sizeUndef",
      "domain": [],
      "range": "size_type"
    },
    {
      "name": "truck",
      "domain": [],
      "range": "mode_type"
    },
    {
      "name": "Car",
      "domain": [],
      "range": "mode_type"
    },
    {
      "name": "modeUndef",
      "domain": [],
      "range": "mode_type"
    },
    {
      "name": "com",
      "domain": [],
      "range": "consent_type"
    },
    {
      "name": "noConsent",
      "domain": [],
      "range": "consent_type"
    },
    {
      "name": "owner",
      "domain": [],
      "range": "consent_type"
    }
  ],
  "facts": "distinct(std, large, xlarge, sizeUndef) && distinct(Car, truck, modeUndef) && distinct(com, noConsent, owner)",
  "ltl": [
     { "property": "F end", "result": true },
     { "property": "F ((<init> true) && G ! end)", "result": false },
     { "property": "F ((pW > 6) && G (sMode != truck))", "result": true },
     { "property": "F ((pW > 6) && F (sMode == Car))", "result": false },
     {"property": "F ( <chooseconsent2> (consent == com) && G ! declared)", "result": false}
  ]
}

LTL_f property