LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "BPM: IT service provider",
   "comment": "Adapted from Fig. 2 in K. Bhattacharya, C. Gerede, R. Hull, R. Liu, J. Su: Towards Formal Analysis of Artifact-Centric Business Process Models, BPM 2007",
   "states": [
     {
        "id": 0,
        "name": "b0",
        "initial": true
     },
     {
        "id": 1,
        "name": "b1"
     },
     {
        "id": 2,
        "name": "b2"
     },
     {
        "id": 3,
        "name": "b3"
     },
     {
        "id": 4,
        "name": "b4"
     },
     {
        "id": 5,
        "name": "b5",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "create order",
        "guard": "(order_state' == planned) && (date_created' > 0)"
     },
     {
        "source": 1,
        "target": 2,
        "name": "initiate accounting",
        "guard": "(invoice_id' > 0)"
     },
     {
        "source": 2,
        "target": 3,
        "name": "plan schedule",
        "guard": "(plan_id' > 0)"
     },
     {
        "source": 3,
        "target": 4,
        "name": "approve install",
        "guard": "(order_state' == live) && (install_approved' == True) && (date_install_approved' > 0)"
     },
     {
        "source": 1,
        "target": 5,
        "name": "cancel order",
        "guard": "order_state' == canceled"
     },
     {
        "source": 4,
        "target": 5,
        "name": "complete accept",
        "guard": "order_state' == complete"
     }
   ],
   "variables": [ 
      {
         "name": "invoice_id",
         "type": "int",
         "initial": 0
      },
      {
         "name": "plan_id",
         "type": "int",
         "initial": 0
      },
      {
         "name": "order_id",
         "type": "int",
         "initial": 0
      },
      {
         "name": "order_state",
         "type": "order_state",
         "initial": "pending"
      },
      {
         "name": "credit_check_approved",
         "type": "bool",
         "initial": false
      },
      {
         "name": "install_approved",
         "type": "bool",
         "initial": false
      },
      {
         "name": "date_created",
         "type": "int",
         "initial": 0
      },
      {
         "name": "date_install_approved",
         "type": "int",
         "initial": 0
      }
   ],
   "relations": [
   ],
   "functions": [ 
      {
         "name": "pending",
         "domain": [],
         "range": "order_state"
      },
      {
         "name": "planned",
         "domain": [],
         "range": "order_state"
      },
      {
         "name": "live",
         "domain": [],
         "range": "order_state"
      },
      {
         "name": "canceled",
         "domain": [],
         "range": "order_state"
      },
      {
         "name": "complete",
         "domain": [],
         "range": "order_state"
      },
      {
         "name": "id_undef",
         "domain": [],
         "range": "id"
      },
      {
         "name": "invoice_state_undef",
         "domain": [],
         "range": "invoice_state"
      }
   ],
   "facts":"distinct(pending, planned, live, complete, canceled)",
   "ltl": [
      {"property": "F ((credit_check_approved != True) && (install_approved == True))", "result": true },
      {"property": "G ((install_approved == True) -> (order_state == live)) && F (install_approved == True)", "result": false},
      {"property": "F ((order_state == planned) && G (order_state != complete))", "result": true },
      {"property": "G (install_approved != True)", "result": true },
      {"property": "G ((install_approved != True) && (order_state != canceled))", "result": false}
   ]
}

LTL_f property