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