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})

G(visited({www.example.com}) -> downloaded({index.html}))

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
addition	+	20
subtraction	-	20