Skip to content

Latest commit

 

History

History
285 lines (218 loc) · 11.1 KB

README.adoc

File metadata and controls

285 lines (218 loc) · 11.1 KB
Raw

fbSAT

Automatic Inference of Minimal Finite-State Models of Function Blocks from Execution Scenarios and Temporal Properties

JetBrains-Research Project Build Status Codacy code quality Hits-of-Code

Table of Contents

Build

To build fbSAT, use shipped gradle wrapper:

## on Unix:
./gradlew

## on Windows:
gradlew.bat

By default, it runs clean build installDist gradle tasks.

Run

Gradle task installDist produces fbSAT binaries in fbsat-cli/build/install/fbSAT/bin/ directory:

## on Unix:
./fbsat-cli/build/install/cli/bin/fbSAT -h

## on Windows:
fbsat-cli\build\install\cli\bin\fbSAT.bat -h

There are also simple binaries (fbsat and fbsat.bat), which first builds (gradlew installDist) and then runs fbSAT with specified arguments.

## on Unix:
./fbsat -h

## on Windows:
fbsat.bat -h

CLI

λ ./fbsat --help

Usage: fbsat [OPTIONS] COMMAND [ARGS]...

Options:
  -h, --help  Show this message and exit

Commands:
  infer
λ ./fbsat infer --help

Usage: fbsat infer [OPTIONS] COMMAND [ARGS]...

Options:
  -h, --help  Show this message and exit

Commands:
  basic
  basic-min
  basic-minC
  extended
  extended-min
  extended-min-ub
  complete
  complete-min
  cegis
  cegis-min
  modular-parallel-basic
  modular-parallel-basic-min
  modular-parallel-basic-minC
  modular-parallel-extended
  modular-parallel-extended-min
  modular-consecutive-basic
  modular-consecutive-basic-min
  modular-consecutive-basic-minC
  modular-consecutive-extended
  modular-consecutive-extended-min
  modular-consecutive-basic
  modular-arbitrary-basic-min
  modular-arbitrary-basic-minC
  distributed-basic
λ ./fbsat infer cegis-min --help

Usage: fbsat infer cegis-min [OPTIONS]

Input/Output Options:
* -i, --scenarios <path>
    File with scenarios (required)
  -o, --outdir <path>
    Output directory (default: out/<yyyy-MM-dd_HH-mm-ss>)
  --input-names <path>
    File with input variables names (default: PnP names)
  --output-names <path>
    File with output variables names (default: PnP names)
  --smvdir <path>
    Directory with SMV files (default: data\pnp\smv)

Automaton Options:
  -C <int>
    Number of automaton states
  -Cstart <int>
    Start number of automaton states
  -P <int>
    Maximum guard size (number of parse tree nodes)
  -w <int>
    Maximum plateau width

Solver Options:
  --filesolver, --streamsolver, --icms, --minisat, --glucose, --cryptominisat, --cadical
    SAT-solver backend (default: icms (incremental-cryptominisat))
  --filesolver-cmd <cmd>
    FileSolver command (use %s placeholder to access the filename) (default: cadical %s)
  --filesolver-file <path>
    FileSolver file (for CNF) (default: cnf)
  --streamsolver-cmd <cmd>
    StreamSolver command (default: cadical)

Extra Options:
  --forbid-or / --allow-or
  --forbid-transitions-to-first-state / --allow-transitions-to-first-state
  --bfs-automaton / --no-bfs-automaton
  --bfs-guard / --no-bfs-guard
  --only-C
    [basic-min] Minimize only C, without T
  --fail-verify-st / --no-fail-verify-st
    Halt if verification of scenario tree has failed
  --initial-output-values <[01]+>
    Initial output values (as a bitstring)
  --epsilon-output-events [start|onlystart|none]
    Epsilon output events (default: ONLYSTART)
  --start-state-algorithms [nothing|zero|zeronothing|any|init|initnothing]
    Start state algorithms (default: ZERO)
  --encode-reverse-implication / --no-encode-reverse-implication
    Encode reverse implication
  --encode-transitions-order / --no-encode-transitions-order
    [DEBUG] Encode transitions lexicographic order
  --encode-terminals-order / --no-encode-terminals-order
    [DEBUG] Encode terminal numbers lexicographic order
  --encode-terminals-mini-order / --no-encode-terminals-mini-order
    [DEBUG] Encode AND/OR children-terminals order
  --encode-hard-to-explain / --no-encode-hard-to-explain
    [DEBUG] Encode some hard to explain thing
  --encode-totalizer / --no-encode-totalizer
    Encode totalizer when upper bound is null
  --encode-disjunctive-transitions / --no-encode-disjunctive-transitions
    Encode disjunctive transitions (adhocly forbid priority function)
  --reuse-k / --no-reuse-k
    Reuse K found by ExtendedMinTask during CEGIS
  --debug / --no-debug
    Debug mode

Options:
  -h, --help
    Show this message and exit

SAT solver

fbSAT is able to use any SAT solver supporting DIMACS format. Such solver has to either accept the input CNF via stdin ("stream solver"), or as a file argument ("file solver"). In both cases the solver must produce DIMACS-formatted output to stdout. You can choose the backend solver using the following flags and options:

  • --streamsolver for "stream solver"

    • --streamsolver-cmd <cmd> to customize the solver command

  • --filesolver for "file solver"

    • --filesolver-cmd <cmd with %s> to customize the solver command (use %s to access the filename)

    • --filesolver-file <cmd> to customize the filename

If you already have a favorite SAT solver — use it. If not, check out minisat, cryptominisat, glucose, lingeling, cadical, splr, or any other.

Moreover, fbSAT depends on kotlin-satlib, which allows you to access various SAT solvers natively (via JNI technology). Currently, kotlin-satlib support MiniSat, Glucose, Cryptominisat, and Cadical (all links are given to the source repositories being used). Those backends can be chosen via the followings flags:

Additionally, we provide a wrapper for Cryptominisat, which allows solving SAT incrementally via stdin. In order to use it, you should pick the following flag:

Cryptominisat

In order to get cryptominisat, simply download one of the release binaries for Linux or Windows (e.g. release 5.6.8 has corresponding assets). Use fbSAT in the following way:

fbsat ... --streamsolver --streamsolver-cmd="cryptominisat5"

Also, you may use the docker container:

## Pull cryptominisat image
docker pull msoos/cryptominisat

## Specify solver cmd to fbSAT:=
fbsat ... --streamsolver --streamsolver-cmd="docker run --rm -i msoos/cryptominisat"

However, a relatively large launch time of the container (up to 2 seconds on Windows) can lead to undesirable large total execution time, since fbSAT makes multiple calls to the SAT solver. The solution is to spawn a container only once, in detached mode, and later exec cryptominisat inside it:

## Run cryptominisat in detached mode
docker run -d -i --name cms --entrypoint="/bin/sh" msoos/cryptominisat

## Specify solver cmd to fbSAT
fbsat ... --streamsolver --streamsolver-cmd="docker exec -i cms /usr/local/bin/cryptominisat5 --verb=0"

## When finished, do not forget to stop and remove the spawned container
docker rm -f cms

Incremental Cryptominisat

During inferring minimal models and performing the CEGIS, the fbSAT heavily relies on the ability of SAT solvers to solve incrementally — continue solving the SAT problem after adding new constraints (e.g. tighter upper bound during minimization, and new counterexamples to forbid during CEGIS). However, such feature is only available via the native interface, and not via the standard input in DIMACS format. Hence, we developed a small wrapper around the cryptominisat library, which is able to process the incremental SAT problems written in iCNF format via stdin. In order to use it, create the binary file incremental-cryptominisat (sadly, this is not customizable via cli, yet) and ensure that it is located in your PATH. Then, simply pass the --icms flag to fbSAT.

## Run incremental-cryptominisat in detached mode
docker run -d -i --name icms --entrypoint="/bin/sh" lipen/incremental-cryptominisat

## Create the `incremental-cryptominisat` binary
echo -e "#/bin/bash\ndocker exec -i icms /usr/local/bin/incremental-cryptominisat" > ~/bin/incremental-cryptominisat
chmod +x ~/bin/incremental-cryptominisat

## Choose incremental-cryptominisat backend in fbSAT
fbsat ... --icms

## When finished, do not forget to stop and remove the spawned container
docker rm -f icms

TL;DR

ℹ️
 Add scripts folder to your PATH and execute start-icms. After this, you will be able to use fbSAT without any specific solver-related arguments.

Usage example

  • Minimize tests-1 using extended:

    fbsat infer extended-min -i data/tests-1.gz -o out/tests-1-min -P 3

  • Minimize tests-4 using extended method with automatic search of P (until first SAT: w=0):

    fbsat infer extended-min-ub -i data/tests-4.gz -o out/tests-4-min-ub-w0 -w 0

  • Minimize tests-4 using extended method with automatic search of P (up to an upper bound with plateau heuristic: w=2):

    fbsat infer extended-min-ub -i data/tests-4.gz -o out/tests-4-min-ub-w2 -w 2

  • Run CEGIS loop, maintaining the minimal model, on tests-1:

    fbsat infer cegis-min -i data/tests-1.gz -o out/tests-1-complete-min-cegis