Usage - black-sat/black Wiki

BLACK is a satisfiability checker for Linear Temporal Logic (LTL) and similar logics. It supports LTL, LTLf (LTL over finite traces) and LTLf modulo theories, where proposition symbols are replaced by first-order formulas over selected theories, in the spirit of Satisfiability Modulo Theory.

For an exhaustive description of the input syntax of formulas see Syntax.

See the Installation page for instruction on how to install BLACK.

For the usage of the tool itself, follow this document.

Once installed, you can run black --help for a brief usage description:

$ black --help

BLACK - Bounded Lᴛʟ sAtisfiability ChecKer
        version 0.7.0


SYNOPSIS
   black solve [-k <bound>] [-B <backend>] [--remove-past] [--finite] [-m] [-d
         <sort>] [-s] [-o <fmt>] [-f <formula>] [--debug <debug>] [<file>]

   black check -t <trace> [-e <result>] [-i <state>] [--finite] [--verbose] [-f
         <formula>] [<file>]

   black dimacs [-B <backend>] <file>
   black --sat-backends
   black -v
   black -h

OPTIONS
   solving mode: 
       -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
       -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)` 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.

   trace checking mode: 
       -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

   DIMACS mode: 
       -B, --sat-backend <backend> select the SAT backend to use
       <file>                      DIMACS file to solve

   --sat-backends                  print the list of available SAT backends
   -v, --version                   show version and license information
   -h, --help                      print this help message

The tool operates in three modes, determined by the given subcommand.

black solve

This is the main mode of the tool: the satisfiability checker! The tool accepts a file name as a command line argument, and checks the satisfiability of the formula contained in the file:

$ black solve benchmarks/formulas/future_only/acacia/demo-v3/demo-v3/demo-v3_1.pltl 
SAT

If the filename is -, black reads the formula from the standard input.

Alternatively, a formula can be directly given on the command line with the -f/--formula option:

$ black solve -f 'G F p'
SAT

With the --finite option, you ask BLACK to interpret the formula over finite traces.

With the -m/--model option, you ask BLACK to print a model of the formula, if it exists:

$ black solve -m -f '!q & G F p'
SAT
Model:
- t = 0: {¬q}
- t = 1: {p} ⬅︎ loops here

In the output, at each time step the list of literals of each state is shown. If a proposition letter is missing from a state, it means its truth value at that state is not important for the satisfaction of the formula. If the found model is infinite, the ⬅︎ loops here mark signals the begin of the periodic part of the model. In the example above, the found model is ¬q,p,p,p,p,p,p,.....

The -o/--output-format option lets you select the output format to be used to print the results. The default is readable, which is the human-readable format shown in previous examples. The other available option is json, which is handy when you have to parse the result.

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

The -k/--bound command line option sets the maximum number of iterations of the underlying algorithm (useful for very hard formulas).

Since BLACK uses an incremental algorithm, a termination check is required at each iteration to decide whether to stop or continue the computation. This termination check (the PRUNE rule of the underlying tableau) can be disabled with the -s/--semi-decision option. If this option is given, termination for unsatisfiable formulas is not guaranteed, but the solver can work faster on satisfiable ones.

The -B/--sat-backend option sets the SAT backend to use. The list of available backends can be retrieved by invoking black with the --sat-backends option.

Use with LTLfMT formulas

If the input formulas contain any LTLf Modulo Theories syntax, BLACK requires the user to give the -d/--domain option, which specifies the domain over which variables have to be interpreted. Currently, BLACK does not support the declaration of custom sorts, and the only supported sorts are integers and reals.

$ black -d integers -f 'G(x = y + y)'
SAT

Also, note that in this kind of formulas the --finite option is implied, since infinite trace semantics is not supported.

If the input formula uses the next or wnext term constructors, termination for unsatisfiable formulas is not guaranteed, because the logic is undecidable. BLACK warns you about this issue:

black solve -d integers -f 'G(wnext(x) = y + y)'
black: warning: use of `next` 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 from the message, you can silence the warning by explicitly passing the -s/--semi-decision option.

black check

In this mode, the solver checks that a given trace is indeed a model for the given formula. The formula is given as a file or as a command-line argument with the -f/--formula option, as with black solve. The trace is given as a file with the -t/--trace option (which is required). For the formula or the trace file (but not both), if the filename is -, the tool reads from standard input.

The trace file is read in the same format give in output by black solve with the -o json option. This means the black check option can be used to directly validate the output of the solver, for example:

$ black solve -m -o json formula.pltl > trace.json
$ black check -t trace.json formula.pltl
TRUE

Or, more compactly:

$ black solve -m -o json formula.pltl | black check -t - formula.pltl
TRUE

In the trace checking mode, a few other options are available.

The -i/--initial-state option sets the index of the state over which to evaluate the formula. The default is zero. For example, black check -t trace.json -f 'G F p' -i 2 checks the G F p formula over the third state of trace.json (indexes start at zero).

The -e/--expected option is useful when validating the output of the solver, as in BLACK's test suite. It accepts as arguments either SAT or UNSAT, and checks whether the answer reported in the trace file is the same.

The --verbose option turns on a verbose log of evaluations of the subformulas that lead the trace checker to give a certain answer. It is useful for debugging.

Example:

$ black solve -m -o json -f 'p | !p' | black check -t - -e UNSAT -f 'p | !p'
MATCH

In trace checking mode, black returns a non-zero status code whenever the checking fails, useful in shell scripts.

black dimacs

In the DIMACS mode, the input file is parsed as a DIMACS file an directly solved by the selected backend. The -B/--sat-backend option selects the backend among the ones available, which can be listed with the --sat-backends option.