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.

Design choice

Note how black’s output is so short and terse. By default, the tool only shows its result and quits, without any other information of any sort. This behavior is useful when calling black from shell scripts or from other programs: there is no need to parse complex logs of information to understand the result.

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.9.2

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 integers and reals:

$ black solve -d integers -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 integers -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 integers -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: integers, reals

-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

Command-line interface#

Tutorial#

Usage reference#

Synopsis#

Options#

black solve mode#

black check mode#

Other options#

`black solve` mode#

`black check` mode#