Ada - the arithmetic DDS analyzer
Ada
Help
Load example
hospital billing
online auction
B1
road fine management
B3
B2
B4
Model
{ "name": "B2", "states": [ { "id": 0, "name": "s0", "initial": true }, { "id": 1, "name": "s1" }, { "id": 2, "name": "s2", "final": true } ], "transitions": [ { "source": 0, "target": 1, "name": "write x", "guard": "(x' > 0)" }, { "source": 1, "target": 1, "name": "write y", "guard": "(y' > x)" }, { "source": 1, "target": 2, "name": "compare y and x", "guard": "(y <= x + 7)" } ], "variables": [ { "name": "x", "type": "int", "initial": 0 }, { "name": "y", "type": "int", "initial": 0 } ] }
LTLf property
Check
DDSA
NFA
PC
LOG
Ada is ready.
Top