Ada

Model

{  "name" : "B1",
   "states": [
     {
        "id": 0,
        "name": "s0",
        "initial": true
     },
     {
        "id": 1,
        "name": "s1"
     },
     {
        "id": 2,
        "name": "s2"
     },
     {
        "id": 3,
        "name": "s3"
     },
     {
        "id": 4,
        "name": "s4"
     },
     {
        "id": 5,
        "name": "s5",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "credit request",
        "guard": "(amount' > 0)",
        "written": ["vip", "amount"]
     },
     {
        "source": 1,
        "target": 2,
        "name": "verify",
        "written": ["ver"]
     },
     {
        "source": 2,
        "target": 3,
        "name": "simple assessment",
        "guard": "((ver == true) && (amount <= 5000) && (0.15 * amount < interest') && (interest' < 0.2 * amount))",
        "written": ["dec"]
     },
     {
        "source": 2,
        "target": 3,
        "name": "advanced assessment",
        "guard": "((ver == true) && (amount > 5000) && (0.1 * amount < interest') && (interest' < 0.15 * amount))",
        "written": ["dec"]
     },
     {
        "source": 2,
        "target": 4,
        "name": "skip assessment",
        "guard": "(ver != true)",
        "written": ["dec"]
     },
     {
        "source": 3,
        "target": 1,
        "name": "renegotiate"
     },
     {
        "source": 3,
        "target": 4,
        "name": "proceed"
     },
     {
        "source": 4,
        "target": 5,
        "name": "inform normal customer",
        "guard": "(vip != true)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "inform vip customer",
        "guard": "(vip == true)"
     },
     {
        "source": 4,
        "target": 5,
        "name": "open loan",
        "guard": "((ver == true) && (dec == true))"
     }
   ],
   "variables": [ 
      {
         "name": "amount",
         "type": "rat",
         "initial": 0.0
      }, 
      {
         "name": "interest",
         "type": "rat",
         "initial": 0.0
      }, 
      {
         "name": "ver",
         "type": "bool",
         "initial": false
      }, 
      {
         "name": "dec",
         "type": "bool",
         "initial": false
      }, 
      {
         "name": "vip",
         "type": "bool",
         "initial": false
      }
   ]
}

LTLf property

Ada - the arithmetic DDS analyzer