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 ::= [azAZ_][azAZ09_]* 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 ::= ()?[09]+ real ::= ()?[09]+ '.' [09]+((eE)[09]+)? 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 

60 
Tomorrow 

60 
Weak tomorrow 

60 
Yesterday 

60 
Weak yesterday 

60 
Eventually 

60 
Globally 

60 
Once 

60 
Historically 

60 
Until 

50 
Release 

50 
Since 

50 
Triggered 

50 
Implication 

40 
If and only if 

40 
Conjunction 

30 
Disjunction 

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 