LinDMT: LTLf Model Checking Modulo Theories

input system

{  "name" : "VERIFAS: airline checkin",
   "comment": "This example was adopted from the VERIFAS problem set. Updates of Baggages relations were omitted. Moreover, one instance of non-linear arithmetic was simplified.",
   "source": "https://github.com/oi02lyl/has-verifier/blob/master/bpmn/Airline-Check-In.txt",
   "states": [
     {
        "id": 0,
        "name": "init",
        "initial": true
     },
     {
        "id": 1,
        "name": "verified"
     },
     {
        "id": 2,
        "name": "notVerified"
     },
     {
        "id": 3,
        "name": "customerRejected",
        "final": true
     },
     {
        "id": 4,
        "name": "itineraryConfirmed"
     },
     {
        "id": 5,
        "name": "hasProhibitedObjects"
     },
     {
        "id": 6,
        "name": "hasNoProhibitedObjects"
     },
     {
        "id": 7,
        "name": "addingBaggages"
     },
     {
        "id": 8,
        "name": "passengerInformed"
     },
     {
        "id": 9,
        "name": "paid"
     },
     {
        "id": 10,
        "name": "boardingPassPrinted"
     },
     {
        "id": 11,
        "name": "handedOutBoardingPass",
        "final": true
     },
     {
        "id": 12,
        "name": "baggagesAdded"
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "verifySuccess",
        "guard": "(EXISTS _date _tocity _fromcity _name _aid _n. Ticket(tid', _name, _fromcity, _tocity, _date, _n, _aid))"
     },
     {
        "source": 0,
        "target": 2,
        "name": "verifyFail"
     },
     {
        "source": 2,
        "target": 3,
        "name": "rejectCustomer"
     },
     {
        "source": 1,
        "target": 4,
        "name": "confirmItinerary"
     },
     {
        "source": 4,
        "target": 5,
        "name": "askProhibitedObjectsYes"
     },
     {
        "source": 5,
        "target": 5,
        "name": "removeProhibitedObjects"
     },
     {
        "source": 5,
        "target": 6,
        "name": "removeProhibitedObjects"
     },
     {
        "source": 4,
        "target": 6,
        "name": "askProhibitedObjectsNo"
     },
     {
        "source": 6,
        "target": 7,
        "name": "askForBaggages"
     },
     {
        "source": 12,
        "target": 8,
        "name": "informPassengerAdditionalFee",
        "guard": "(baggage_fee > 0)"
     },
     {
        "source": 8,
        "target": 9,
        "name": "collectPayment",
        "guard": "((baggage_fee > 0) && (amount_paid' == baggage_fee))"
     },
     {
        "source": 9,
        "target": 10,
        "name": "printBoardingPass1"
     },
     {
        "source": 7,
        "target": 10,
        "name": "printBoardingPass2",
        "guard": "(baggage_fee == 0)"
     },
     {
        "source": 10,
        "target": 11,
        "name": "handOutBoardingPass"
     },
     {
        "source": 7,
        "target": 7,
        "name": "initAddBaggages",
        "guard": "((weight1' == 0) && (weight2' == 0) && (weight3' == 0) && (weight4' == 0) && (aid == getAirline(tid)))"
     },
     {
        "source": 7,
        "target": 7,
        "name": "selectFirstBaggageToAdd",
        "guard": "((weight1' >= 0) && (EXISTS _mw _x _owcharge _z. ( Airline(aid, _mw, _x, _owcharge, _z) && (weight1' <= _mw))))"
     },
     {
        "source": 7,
        "target": 7,
        "name": "selectSecondBaggageToAdd",
        "guard": "(weight2' >= 0) && (EXISTS _mw _x _owcharge _z. (Airline(aid, _mw, _x, _owcharge, _z) && (weight2' <= _mw)))"     },
     {
        "source": 7,
        "target": 7,
        "name": "selectThirdBaggageToAdd",
        "guard": "(weight3' >= 0) && (EXISTS _mw _x _owcharge _z. (Airline(aid, _mw, _x, _owcharge, _z) && (weight3' <= _mw)))"
     },
     {
        "source": 7,
        "target": 7,
        "name": "selectFourthBaggageToAdd",
        "guard": "(weight4' >= 0) && (EXISTS _mw _x _owcharge _z. (Airline(aid, _mw, _x, _owcharge, _z) && (weight4' <= _mw)))"
     },
     {
        "source": 7,
        "target": 12,
        "name": "calculateCharge",
        "guard": "(EXISTS _mw _limit _owcharge _extracharge _num _date _name _fromcity _tocity. (Ticket(tid, _name, _fromcity, _tocity, _date, _num, aid) && Airline(aid, _mw, _limit, _owcharge, _extracharge) && (baggage_pieces' == (ITE(weight1 > 0, 1, 0) + ITE(weight2 > 0, 1, 0) + ITE(weight3 > 0, 1, 0) + ITE(weight4 > 0, 1, 0))) && (baggage_fee' == ((baggage_pieces' - _num) * 50) + ITE(weight1 > _limit, _owcharge, 0) + (ITE(weight2 > _limit, _owcharge, 0) + (ITE(weight3 > _limit, _owcharge, 0) + ITE(weight4 > _limit, _owcharge, 0))) ) ))"
        
     }
   ],
   "variables": [ 
      {
         "name": "tid",
         "type": "tid_type",
         "initial": "NULLticket"
      }, 
      {
         "name": "aid",
         "type": "aid_type",
         "initial": "NULLairline"
      },
      {
         "name": "baggage_pieces",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "baggage_fee",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "amount_paid",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "weight1",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "weight2",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "weight3",
         "type": "rat",
         "initial": 0
      },
      {
         "name": "weight4",
         "type": "rat",
         "initial": 0
      }
   ],
   "relations": [
      {
         "name": "Ticket",
         "domain": ["tid_type", "string", "string", "string", "string", "rat", "aid_type"]
      },
      {
         "name": "Airline",
         "domain": ["aid_type", "rat", "rat", "rat", "rat"]
      }
   ],
   "functions": [ 
      {
         "name": "NULLticket",
         "domain": [],
         "range": "tid_type"
      },
      {
         "name": "NULLairline",
         "domain": [],
         "range": "aid_type"
      },
      {
         "name": "getAirline",
         "domain": ["tid_type"],
         "range": "aid_type"
      },
      {
         "name": "StringUndef",
         "domain": [],
         "range": "string"
      }
   ],
   "ltl": [
      { "property": "F (amount_paid < baggage_fee)", "result": true },
      { "property": "F ((amount_paid < baggage_fee) && G (amount_paid < baggage_fee))", "result": false },
      { "property": "F (verified && G ! handedOutBoardingPass)", "result": false },
      { "property": "F (addingBaggages && G (baggage_fee == 0))", "result": true },
      { "property": "G ! paid", "result": true }
   ]
}

LTL_f property