LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "paper examples: simple system with relations",
   "comment": "This corresponds to Example 2 in the paper.",
   "states": [
     {
        "id": 0,
        "name": "b0",
        "initial": true
     },
     {
        "id": 1,
        "name": "b1",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "increase",
        "guard": "(x' > x) && (rel(x', y))"
     },
     {
        "source": 1,
        "target": 0,
        "name": "reset",
        "guard": "p(y')"
     }
   ],
   "variables": [ 
      {
         "name": "x",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "y",
         "type": "uninterpreted",
         "initial": "a"
      }
   ],
   "relations": [ 
      {
         "name": "rel",
         "domain": ["rat", "uninterpreted"]
      },
      {
         "name": "p",
         "domain": ["uninterpreted"]
      }
   ],
   "functions": [ 
      {
         "name": "a",
         "domain": [],
         "range": "uninterpreted"
      }
   ],
   "ltl": [
      { "property": "(F (x == 3)) && ! p(y))", "result": true },
      { "property": "(x < 5) U rel(x,y)", "result": true },
      { "property": "G (! rel(x,y))", "result": false },
      { "property": "F (! rel(x,y) && ! p(y))", "result": true },
      { "property": "X (F (! rel(x,y) && ! p(y)))", "result": false }
   ]
}

LTL_f property