Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Tool for automatic inference of minimal finite-state models of function blocks from execution scenarios and temporal properties

License

NotificationsYou must be signed in to change notification settings

ctlab/fbSAT

 
 

Repository files navigation

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

JetBrains-Research ProjectBuild StatusCodacy code qualityHits-of-Code

Build

To build fbSAT, use shipped gradle wrapper:

## on Unix:./gradlew## on Windows:gradlew.bat

By default, it runsclean build installDist gradle tasks.

Run

Gradle taskinstallDist produces fbSAT binaries infbsat-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 andfbsat.bat), which first builds (gradlew installDist) and then runs fbSAT with specified arguments.

## on Unix:./fbsat -h## on Windows:fbsat.bat -h

CLI

λ ./fbsat --helpUsage: fbsat [OPTIONS] COMMAND [ARGS]...Options:  -h, --help  Show this message and exitCommands:  infer
λ ./fbsat infer --helpUsage: fbsat infer [OPTIONS] COMMAND [ARGS]...Options:  -h, --help  Show this message and exitCommands:  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 --helpUsage: 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 widthSolver 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 modeOptions:  -h, --help    Show this message and exit

SAT solver

fbSAT is able to use any SAT solver supportingDIMACS 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 outminisat,cryptominisat,glucose,lingeling,cadical,splr, or any other.

Moreover, fbSAT depends onkotlin-satlib, which allows you to access various SAT solvers natively (via JNI technology).Currently, kotlin-satlib supportMiniSat,Glucose,Cryptominisat, andCadical (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 SATincrementally via stdin. In order to use it, you should pick the following flag:

Cryptominisat

In order to get cryptominisat, simply download one of therelease 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 thedocker container:

## Pull cryptominisat imagedocker 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, indetached mode, and laterexec cryptominisat inside it:

## Run cryptominisat in detached modedocker run -d -i --name cms --entrypoint="/bin/sh" msoos/cryptominisat## Specify solver cmd to fbSATfbsat ... --streamsolver --streamsolver-cmd="docker exec -i cms /usr/local/bin/cryptominisat5 --verb=0"## When finished, do not forget to stop and remove the spawned containerdocker rm -f cms

Incremental Cryptominisat

During inferring minimal models and performing the CEGIS, the fbSAT heavily relies on the ability of SAT solvers to solveincrementally — 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 developeda 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 fileincremental-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 modedocker run -d -i --name icms --entrypoint="/bin/sh" lipen/incremental-cryptominisat## Create the `incremental-cryptominisat` binaryecho -e "#/bin/bash\ndocker exec -i icms /usr/local/bin/incremental-cryptominisat" > ~/bin/incremental-cryptominisatchmod +x ~/bin/incremental-cryptominisat## Choose incremental-cryptominisat backend in fbSATfbsat ... --icms## When finished, do not forget to stop and remove the spawned containerdocker rm -f icms

TL;DR

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

Usage example

  • Minimizetests-1 usingextended:

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

  • Minimizetests-4 usingextended method with automatic search ofP (until first SAT: w=0):

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

  • Minimizetests-4 usingextended method with automatic search ofP (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, ontests-1:

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

About

Tool for automatic inference of minimal finite-state models of function blocks from execution scenarios and temporal properties

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Contributors2

  •  
  •  

Languages

[8]ページ先頭
©2009-2025 Movatter.jp