# Input syntax#

Here we document the syntax accepted by BLACK when reading input formulas.

## General concepts#

BLACK expects in each input file a single formula. Formulas are given in a pretty natural syntax, with prefix unary operators and infix binary operators. An example

```p && G(p -> q) && !q
```

or

```x = 0 && G(wnext(x) = x + 1) && F(x = 42)
```

See the next section for the complete reference of supported operators and their precedence. `next`, `wnext`, `prev`, and `wprev` terms must always use parenthesis and can be applied only to single variables.

Quantified formulas are introduced by a quantifier (`exists` or `forall`), followed by a list of variables, a dot (`.`) and the formula. Example:

```forall x y . exists z . (x < z & z < y)
```

Parenthesis are needed because quantifiers bind very tightly to formulas.

Names of propositions, variables, functions and relations are symbols. A symbol can be either a simple symbol, i.e. an alphanumeric identifier like `p` or `q_42`, or a raw symbol. Raw symbols allow the user to use arbitrary data as symbol names without having to encode symbol names beforehand.

A raw symbol is any string of any kind enclosed between a pair of braces (`{` and `}`). Any letter, number or special symbol can appear between the braces, excepting for the closing brace itself, which must be escaped (i.e. `\}`).

Some examples:

```{input: x} = 0 && G({output: y} < {input: x})

```

Raw symbols come very handy when formulas are generated by some other software and variables and proposition names come from the problem domain and have complex structure.

## Syntax reference#

Formal grammar for formulas:

```symbol         ::=  `simple_symbol` | `raw_symbol`
simple_symbol  ::=  [a-zA-Z_][a-zA-Z0-9_]*
raw_symbol     ::=  '{' ('\' '}' | [^}])* '}'
formula        ::=  `boolean` | `proposition` | `atom` | `term` `rel` `term` |
`unary` `formula` | `formula` `binary` `formula` |
`quantification` | '(' `formula` ')'
boolean        ::=  True | False
proposition    ::=  `symbol`
atom           ::=  `symbol` '(' `term` (, `term`)* ')'
rel            ::=  = | != | < | <= | > | >=
quantification ::=  `quantifier` `variable`+ . `formula`
quantifier     ::=  exists | forall
unary          ::=  ! | X | wX | Y | Z | F | G | O | H
binary         ::=  && | || | -> | <-> | U | R | S | T
term           ::=  `app` | `variable` | `constant` | -`term` | `term` `op` `term` |
`uop` '(' `variable` ')'
variable       ::=  `symbol`
app            ::=  `symbol` '(' `term` (, `term`)* ')'
constant       ::=  `integer` | `real`
integer        ::=  (-)?[0-9]+
real           ::=  (-)?[0-9]+ '.' [0-9]+((e|E)[0-9]+)?
uop            ::=  next | wnext | prev | wprev
op             ::=  + | - | * | /
```

The above grammar is ambiguous since the precedence between operators is not explicit. Moreover, not all the equivalent syntaxes of each operator are shown. For example, the conjunction connective can be expressed both as `&&` and `&`. The following table reports the precedence and all the equivalent syntaxes of each operator.

Operator

Syntax

Precedence

Not

`NOT`, `!`, `~`

60

Tomorrow

`X`

60

Weak tomorrow

`wX`

60

Yesterday

`Y`

60

Weak yesterday

`Z`

60

Eventually

`F`

60

Globally

`G`

60

Once

`O`

60

Historically

`H`

60

Until

`U`

50

Release

`R`

50

Since

`S`

50

Triggered

`T`

50

Implication

`THEN`, `->`, `=>`

40

If and only if

`IFF`, `<->`, `<=>`

40

Conjunction

`AND`, `&&`, `&`

30

Disjunction

`OR`, `||`, `|`

20

The above precedence values means that, for example, `p && q || r` is parsed as `(p && q) || r` as expected, and `p & q <-> r` is parsed as ```p & (q <-> r)```. Unary operators and connectives have the higher precedence, so ```F p && q``` is parsed as `(F p) && q`.

Similarly, we give the precedence table for terms:

Operator

Syntax

Precedence

unary minus

`-`

40

multiplication

`*`

30

division

`/`

30

`+`
`-`