# Command-line interface#

BLACK’s main interface to the user is the command-line tool `black`

. Here we
document its usage. For the input syntax accepted by the tool, look at the
Input syntax page.

## Tutorial#

The main purpose of `black`

is to tell you whether a given temporal logic
formula (see Supported logics) is *satisfiable*. Let’s suppose you have written
such a formula in the file `spec.pltl`

:

```
$ cat spec.pltl
!p & X !p & F p
```

Then, asking `black`

about this formula is as easy as:

```
$ black solve spec.pltl
SAT
```

`black`

replies `SAT`

on the *standard output*, so the formula is
satisfiable. Let us try an unsatisfiable formula:

```
$ cat unsat-spec.pltl
G((p & q) & c) & F((w & r) & !c)
$ black solve unsat-spec.pltl
UNSAT
```

If the filename is `-`

, `black`

reads from the *standard input*:

```
$ cat spec.pltl | black solve -
SAT
$ cat unsat-spec.pltl | black solve -
UNSAT
```

This is useful when the formulas are generated by other programs.

Alternatively, we may give the formulas on the command line with the
`-f`

option:

```
$ black solve -f '!p & X !p & F p'
SAT
$ black solve -f 'G((p & q) & c) & F((w & r) & !c)'
UNSAT
```

Tip

Formulas usually contain spaces so they have to be quoted. Moreover, they
usually contain many symbols which have special meaning for the shell,
therefore it is recommended to use single quotes (`'like this'`

) rather
than double quotes (`"not this"`

) to tell the shell to not interpret the
quoted contents.

Satisfiable formulas can correspond *e.g.*, to bugged specifications or planning
problems that admit a solution plan. In these cases, one may want to obtain the
counter-example showing the bug or the solution plan to the planning problem.
To do this, we can ask `black`

to print the *model* of a satisfiable formula
with the `-m`

option:

```
$ black solve -m -f '!p & X !p & F p'
SAT
Model:
- t = 0: {￢p}
- t = 1: {￢p}
- t = 2: {p} ⬅︎ loops here
```

By default, `black`

solves formulas with the *infinite trace* semantics (see
Supported logics). So here it is telling us that the model of the formula starts
with two states at `t=0`

and `t=1`

where `p`

does *not* hold, followed by
a state where `p`

holds, and then the model infinitely loops through this last
state. LTL models always loop in this way.

If, instead, we want to interpret the formula over *finite* traces, we can tell
so to `black`

by passing the `--finite`

option:

```
$ black solve --finite -m -f '!p & X !p & F p'
SAT
Finite model:
- t = 0: {￢p}
- t = 1: {￢p}
- t = 2: {p}
```

Note that the model does not loop anymore, but ends at `t=2`

.

Complex specifications may have huge and complex models, and we probably want to
process the output model with other scripts or programs. In this case, we need
`black`

to print the model in a more easily parsable format. The `-o`

option
lets us choose the output format. Currently supported formats are `readable`

(the default, that we saw above), or `json`

:

```
$ black solve -o json -m -f '!p & X !p & F p'
{
"result": "SAT",
"k": 1,
"model": {
"size": 3,
"loop": 2,
"states": [
{
"p": "false"
},
{
"p": "false"
},
{
"p": "true"
}
]
}
}
```

Tip

If you need to parse `black`

’s output from shell scripts or from the
command line, consider using the `json`

output format and the
jq command-line JSON manipulation tool.

BLACK supports many backends. The list of available backends can be retrieved
with the `--sat-backends`

option:

```
$ black --sat-backends
BLACK - Bounded Lᴛʟ sAtisfiability ChecKer
version 0.10.1
Available SAT backends:
- z3 *
- cmsat
- cvc5
- mathsat
- minisat
```

The one marked with `*`

is the default used when no explicit choice is made.
To choose the backend, use the `-B`

option:

```
$ black solve -B cvc5 -f '!p & X !p & F p'
SAT
```

Note that not all backends support the same features. In particular, first-order
formulas are only supported with SMT solver backends (`z3`

, `cvc5`

and
`mathsat`

), and only `z3`

and `cvc5`

support *quantified* first-order
formulas.

Now, let’s consider again the unsatisfiable formula above. Why is it
unsatisfiable? `black`

can help us answer this question by finding a *minimum
unsatisfiable core* (MUC). This can be done by passing the `-c`

option:

```
$ black solve -c -f 'G((p & q) & c) & F((w & r) & !c)'
UNSAT
MUC: G({0} & c) & F({1} & !c)
```

Let us look at the output. `UNSAT`

is printed because the formula is
unsatisfiable. Then, the MUC is shown to be `G({0} & c) & F({1} & !c)`

. This
is a reduction of the original formulas, where the subformula `(p & q)`

has
been replaced by `{0}`

and the subformula `(w & r)`

has been replaced by
`{1}`

. Let’s try to give this formula back to `black`

:

```
$ black solve -f 'G({0} & c) & F({1} & !c)'
UNSAT
```

The formula is unsatisfiable. Indeed, the MUC is the smallest *unsatisfiable*
formula obtained by replacing some subformulas of the original one with
propositional placeholders. It tells us that the replaced subformulas are not
involved at all in the unsatisfiability of the formula. In this case, from the
MUC it can be seen directly that the formula is unsatisfiable because we require
`c`

to always hold and then we require `!c`

to hold eventually.

Until now, we have always given to `black`

propositional formulas. But as you
can see in the Supported logics page, `black`

also supports first-order formulas
in place of propositional letters (*i.e.*, the LTL\({}_f\)^{MT} logic).

In this logic, we can use *variables* that take values over certains domains.
Since BLACK supports the LIA and LRA theories (possibly combined with EUF),
variables can be either *integer*- or *real*-valued. When giving a LTL\({}_f\)^{MT}
formula as input, we have to choose the domain using the `-d`

option. Accepted
values are `Int`

and `Real`

:

```
$ black solve -d Int -f 'x = y + 2'
SAT
```

Note

The `-m`

option is not (yet) supported for LTL\({}_f\)^{MT} formulas.

Note

The `--finite`

option is implied when solving LTL\({}_f\)^{MT} formulas, since the
infinite-trace semantics is not supported for such formulas.

We can refer to the value of a variable at the next state using the *strong* or
the *weak next* term constructors. For example:

```
$ black solve -d Int -f 'x = 0 & G(wnext(x) = x + 1) & F(x = 42)'
black: warning: use of `next`/`prev` terms implies the --semi-decision option.
black: warning: execution may not terminate.
black: warning: pass the --semi-decision option explicitly to silence this warning.
SAT
```

As you can see, `black`

warns you about the fact that, by using such terms,
the solving procedure may not terminate (in the case of unsatisfiable formulas),
hence `black`

turns on implicitly the `--semi-decision`

option which
disables the termination checks. To silence the warning, you can pass the
option yourself (here we use the `-s`

short option):

```
$ black solve -s -d Int -f 'x = 0 & G(wnext(x) = x + 1) & F(x = 42)'
SAT
```

Note

You can use the `-s`

option on propositional formulas as well. This may
cause `black`

to not terminate on unsatisfiable instances, but can
substantially speed up it on satisfiable ones.

## Usage reference#

### Synopsis#

```
$ black solve [-k <bound>] [-B <backend>] [--remove-past] [--finite] [-m] \
[-c] [-d <sort>] [-s] [-o <fmt>] [-f <formula>] [--debug <debug>] \
[<file>]
$ black check -t <trace> [-e <result>] [-i <state>] [--finite] [--verbose] \
[-f <formula>] [<file>]
$ black --sat-backends
$ black -v
$ black -h
```

### Options#

`black solve`

mode#

Check the satisfiability of a temporal logic formula.

- -k, --bound <bound>#
maximum bound for BMC procedures

- -B, --sat-backend <backend>#
select the SAT backend to use

- --remove-past#
translate LTL+Past formulas into LTL before checking satisfiability

- --finite#
treat formulas as LTLf and look for finite models

- -m, --model#
print the model of the formula, if any

- -c, --unsat-core#
for unsatisfiable formulas, compute the minimum unsat core

- -d, --domain <sort>#
select the domain for first-order variables. Mandatory for first-order formulas.

Accepted domains:

`Int`

,`Real`

- -s, --semi-decision#
disable termination checks for unsatisfiable formulas, speeding up the execution for satisfiable ones.

*Note*: the use of`next(x)`

and similar terms in formulas implies this option.

- -o, --output-format <fmt>#
Output format.

Accepted formats:

`readable`

,`json`

Default:

`readable`

- -f, --formula <formula>#
LTL formula to solve

- <file>#
input formula file name. If

`'-'`

, reads from standard input.

`black check`

mode#

Check the correctness of a trace (a model) against a temporal logic formula.

- -t, --trace <trace>#
trace file to check against the formula. If ‘-’, reads from standard input.

- -e, --expected <result>#
expected result (useful in testing).

- -i, --initial-state <state>#
index of the initial state over which to evaluate the formula.

Default: 0

- --finite#
treat formulas as LTLf and expect a finite model

- --verbose#
output a verbose log

- -f, --formula <formula>#
formula against which to check the trace

- <file>#
formula file against which to check the trace

#### Other options#

- --sat-backends#
print the list of available SAT backends

- -v, --version#
show version and license information

- -h, --help#
print this help message