This file accompanies the paper B2SAT: A Bare-Metal Reduction of B to SAT in the FM'2024 proceedings. B2SAT is a new SAT backend for the B-Method to enable new applications of formal methods. The new backend interleaves low-level SAT solving with high-level constraint solving. The backend is integrated into ProB, not as a general purpose backend, but as a dedicated backend for solving hard constraint satisfaction and optimisation problems on complex data. A documentation page for B2SAT is available at: https://prob.hhu.de/w/index.php?title=B2SAT The following folders should be present next to this file: - benchmarks contains a Makefile to re-create the benchmark table results of the article on your system. Run "make help" to get a full list of commands. Run "make install_prob" to install a local copy of ProB 1.13.1-beta1 inside the benchmarks folder then run "make bench" to run the experiments with all solvers. Note: the files will contain an additional first benchmark pigeon_10_bv.eval which is not included in the article and meant to avoid discrepancies in runtime due to warmup/loading times. You can also run "make sat" to just run the benchmarks with b2sat or "make cdlct" to run the benchmarks with the Prolog CDLCT solver (not included in make bench). Run "make version" to obtain version information about ProB. Run "make simple" to run b2sat on the simple example from Section 3 of the FM'2024 paper. The Makefile requires curl (which you can install on Linux using "sudo apt install curl"). Note: you can also download the Linux version of ProB by hand from the [ProB Linux 1.13.1.beta1 Zenodo artifact](https://zenodo.org/records/12166295) or run "make install_prob_linux_zenodo" - prob_screenshots contains some screenshots of ProB showing the tool in action on the examples from the paper - prob_html_visualizations contains HTML trace exports of some of the examples which can be visualised in a regular browser without needing ProB - examples contains some B machines which can be loaded with ProB Tcl/Tk (also downloaded in the benchmarks/ProB folder when running make install_prob; simply run "benchmarks/ProB/StartProB.sh" to start ProB Tcl/Tk) or ProB2-UI. It also contains a TLA folder with a simple dominating set example which can be loaded with ProB, and TLA+ translation of one of the benchmark programs with type annotations for Apalache (but Apalache fails to solve this version as the provided log shows) These are the steps needed to run the benchmarks in the [iFM2022 virtual machine](https://zenodo.org/records/5794839): ``` sudo apt install curl mkdir b2sat cd b2sat curl -L https://zenodo.org/records/12166663/files/b2sat_artifact.tgz?download=1 -o artifact.tgz shasum -a 256 artifact.tgz tar -xvzf artifact.tgz cd benchmarks make install_prob make simple make bench make cdclt ``` You can also download the artifact from the ProB website: ``` curl -L https://stups.hhu-hosting.de/models/B2SAT/b2sat_prob_artifact.tgz -o artifact.tgz ```