Ada - the arithmetic DDS analyzer
Ada
Help
Load example
hospital billing
online auction
B1
road fine management
B3
B2
B4
Model
{ "name": "hospital billing", "states": [ { "id": 0, "name": "src", "initial": true, "final": false }, { "id": 1, "name": "p1", "initial": false, "final": false }, { "id": 2, "name": "p10p25", "initial": false, "final": false }, { "id": 3, "name": "p2p25", "initial": false, "final": false }, { "id": 4, "name": "p10p28", "initial": false, "final": false }, { "id": 5, "name": "p2p28", "initial": false, "final": false }, { "id": 6, "name": "p42", "initial": false, "final": false }, { "id": 7, "name": "p40", "initial": false, "final": false }, { "id": 8, "name": "p16", "initial": false, "final": true }, { "id": 9, "name": "p15", "initial": false, "final": false }, { "id": 10, "name": "p5", "initial": false, "final": false }, { "id": 11, "name": "p3", "initial": false, "final": false }, { "id": 12, "name": "p27", "initial": false, "final": false }, { "id": 13, "name": "p11", "initial": false, "final": false }, { "id": 14, "name": "p26", "initial": false, "final": false }, { "id": 15, "name": "p12", "initial": false, "final": false }, { "id": 16, "name": "p18", "initial": false, "final": false } ], "transitions": [ { "source": 0, "target": 1, "name": "NEW", "guard": "((caseType' >= 0) && (speciality' >= 0))", "written": [ "caseType", "speciality", "isClosed" ] }, { "source": 1, "target": 2, "name": "t1", "written": [] }, { "source": 2, "target": 3, "name": "CHANGE DIAGN", "guard": "(caseType == 2)", "written": [] }, { "source": 2, "target": 3, "name": "t4", "guard": "(caseType != 2)", "written": [] }, { "source": 2, "target": 4, "name": "CHANGE END", "written": [] }, { "source": 2, "target": 4, "name": "t25", "written": [] }, { "source": 3, "target": 5, "name": "CHANGE END", "written": [] }, { "source": 3, "target": 5, "name": "t25", "written": [] }, { "source": 4, "target": 5, "name": "CHANGE DIAGN", "guard": "(caseType == 2)", "written": [] }, { "source": 4, "target": 5, "name": "t4", "guard": "(caseType != 2)", "written": [] }, { "source": 5, "target": 6, "name": "t10", "written": [] }, { "source": 6, "target": 7, "name": "FIN", "guard": "((speciality != 5) && (closeCode' > 0))", "written": [ "closeCode" ] }, { "source": 6, "target": 8, "name": "DELETE", "written": [] }, { "source": 6, "target": 8, "name": "t12", "guard": "(speciality == 5)", "written": [] }, { "source": 7, "target": 9, "name": "DELETE", "written": [] }, { "source": 7, "target": 10, "name": "RELEASE", "written": [] }, { "source": 7, "target": 9, "name": "REOPEN", "guard": "(closeCode != 8)", "written": [] }, { "source": 7, "target": 8, "name": "skipRelease", "guard": "(closeCode == 8)", "written": [] }, { "source": 9, "target": 6, "name": "tLoop", "guard": "(isClosed == true)", "written": [] }, { "source": 9, "target": 8, "name": "t18", "written": [] }, { "source": 9, "target": 8, "name": "DELETE", "guard": "(isClosed != true)", "written": [] }, { "source": 9, "target": 8, "name": "EMPTY", "written": [] }, { "source": 10, "target": 11, "name": "CODE OK", "written": [] }, { "source": 10, "target": 11, "name": "t8", "guard": "((caseType == 6) || (((caseType != 6) && (caseType != 3)) && (closeCode != 1)))", "written": [] }, { "source": 10, "target": 11, "name": "CODE NOK", "guard": "(((caseType != 6) && (caseType == 3)) || (((caseType != 6) && (caseType != 3)) && (closeCode == 1)))", "written": [] }, { "source": 11, "target": 12, "name": "SET STATUS", "written": [] }, { "source": 11, "target": 12, "name": "t30", "written": [] }, { "source": 12, "target": 8, "name": "t39", "written": [] }, { "source": 12, "target": 13, "name": "BILLED", "written": [] }, { "source": 12, "target": 9, "name": "REOPEN", "guard": "((caseType == 2) || ((caseType != 2) && (closeCode != 1)))", "written": [] }, { "source": 12, "target": 9, "name": "t15", "guard": "((caseType != 2) && (closeCode == 1))", "written": [] }, { "source": 13, "target": 14, "name": "STORNO", "guard": "(((isClosed == true) && (closeCode != 1)) || (isClosed != true))", "written": [] }, { "source": 13, "target": 15, "name": "t31", "written": [] }, { "source": 13, "target": 15, "name": "STORNO", "guard": "((isClosed == true) && (closeCode == 1))", "written": [] }, { "source": 14, "target": 15, "name": "REJECT", "written": [] }, { "source": 15, "target": 16, "name": "BILLED", "guard": "(isClosed == true)", "written": [] }, { "source": 15, "target": 16, "name": "REOPEN", "guard": "(isClosed != true)", "written": [] }, { "source": 15, "target": 16, "name": "t9", "written": [] }, { "source": 16, "target": 13, "name": "t7", "written": [] }, { "source": 16, "target": 9, "name": "t29", "written": [] } ], "variables": [ { "name": "caseType", "initial": 0, "type": "int" }, { "name": "closeCode", "initial": 0, "type": "int" }, { "name": "speciality", "initial": 0, "type": "int" }, { "name": "isClosed", "initial": false, "type": "bool" } ] }
LTLf property
Check
DDSA
NFA
PC
LOG
Ada is ready.
Top