# Help

Ada is a tool for model checking of data-aware dynamic systems with arithmetic
(DDSAs) with respect to certain LTL_{f} properties,
i.e., linear-time properties with a finite-trace semantics.

## Input

Example systems can be selected from the dropdown menu. Here we provide a brief description of its components.

### DDSA

Ada uses a simple json format for DDSAs, according to this schema. The json has to specify states, transitions (possibly with guards), and variables, as in the following example:

Here the sources and targets of transitions refer to the numeral state ids. The names of states and transitions can be referred to in the LTL_{f}formula, see below. For variables, besides a name also a type (

`int`

or `rat`

)
must be specified, as well as an initial value.
Guards in transitions are expected to be formulas
written according to the grammar
guard ::= (atom) | guard && guard | (guard) atom ::= term == term | term != term | term < term | term <= term term ::= k | var | term + term | term - term var ::= v | v'where

`k`

is a number, and
`v`

is the name a variable in the DDSA.
In a guard, an occurrence of `v`

refers to the current value, i.e.,
the variable is read; while `v'`

refers to its value in the next
state, i.e., the variable is written.
### Formula

The LTL_{f} formula should adhere to the grammar

psi ::= atom | psi && psi | psi || psi | X psi | <a> psi | F psi | G psi | psi U psi | (psi) atom ::= b | term == term | term != term | term < term | term <= term term ::= k | v | term + term | term - termwhere

`k`

is a number,
`v`

is a variable in the DDSA,
`b`

is the name of a state in the DDSA, and
`a`

is the name of a transition (action) in the DDSA.
The temporal operators are
`X`

(next),
`<a>`

(next via action `a`

)
`F`

(future, ◊), and
`G`

(globally, ◻).
## Functionality

The tool checks several sufficient criteria for finite summary of a DDSA (monotonicity or gap-order constraint system, 2|V|-bounded lookback, and decomposability according to sequential or variable decomposition). If one of these criteria apply, Ada will construct

- the constraint graph as a faithful finite-state abstraction of the DDSA
- an NFA for the formula ψ
- the product construction of the two