LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: book writing and publishing",
   "comment": "This example was adapted from the VERIFAS problem set. Updates of relations Chapter, PublishBook were omitted.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/Book-Writing-and-Publishing.txt",
   "states": [
     {
        "id": 0,
        "name": "state",
        "initial": true
     },
     {
        "id": 1,
        "name": "initialized",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "initialize",
        "guard": "((text_edited == Empty) && (cover_completed == Empty) && (text_edited' == No) && (cover_completed' == No) && (published' == No) && (wid' != NULL))"
     },
     {
        "source": 1,
        "target": 1,
        "name": "addNewChapter",
        "guard": "(chapter == Empty) && (chapter' != Empty) && (content' == Empty)"
     },
     {
        "source": 1,
        "target": 1,
        "name": "retrieveOutline",
        "guard": "(chapter == Empty) && (chapter' != Empty)"
     },
     {
        "source": 1,
        "target": 1,
        "name": "publishBook",
        "guard": "(cover_completed == Yes) && (text_edited == Yes) && (published' == Yes) && ((pid != NULL ) || (EXISTS _x. BookWriter(wid, _x, pid)))"
     },
     {
        "source": 1,
        "target": 1,
        "name": "developBookCover",
        "guard": "(content == Empty) && (content' != Empty) && (cover_completed' == Yes)"
     },
     {
        "source": 1,
        "target": 1,
        "name": "developBookTextAndConcepts",
        "guard": "(chapter != Empty) && (concept == Empty) && (content' != Empty)",
        "written": ["concept"]
     },
     {
        "source": 1,
        "target": 1,
        "name": "editBookText",
        "guard": "(concept != Empty) && (content' != Empty) && (text_edited' == Yes)"
     }
   ],
   "variables": [ 
      {
         "name": "pid",
         "type": "id_type",
         "initial": "NULL"
      }, 
      {
         "name": "concept",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "content",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "text_edited",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "chapter",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "cover_completed",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "published",
         "type": "string",
         "initial": "Empty"
      },
      {
         "name": "wid",
         "type": "id_type",
         "initial": "NULL"
      },
      {
         "name": "pid",
         "type": "id_type",
         "initial": "NULL"
      }
   ],
   "relations": [
      {
         "name": "BookWriter",
         "domain": ["id_type", "string", "id_type"]
      },
      {
         "name": "Publisher",
         "domain": ["id_type", "string"]
      }
   ],
   "functions": [ 
      {
         "name": "NULL",
         "domain": [],
         "range": "id_type"
      },
      {
         "name": "Empty",
         "domain": [],
         "range": "string"
      },
      {
         "name": "Yes",
         "domain": [],
         "range": "string"
      },
      {
         "name": "No",
         "domain": [],
         "range": "string"
      }
   ],
   "facts": "distinct(Yes, No, Empty)",
   "ltl": [
      { "property": "F ((cover_completed == Yes) && G (published != Yes))", "result": true },
      { "property": "G (published != Yes)", "result": true },
      { "property": "F ((content != Empty) && G (published != Yes))", "result": true },
      { "property": "F ((published == Yes) && ((content == Empty) || (concept == Empty)))", "result": false },
      { "property": "F ((content != Empty) && X (content == Empty))", "result": true }
   ]
}

LTL_f property