This file accompanies the B2SAT paper

The following folders should be present:
- benchmarks
  contains a Makefile to re-create the benchmark table results of the article on your system
  run "make install_prob" to install a local copy of ProB inside the benchmarks folder
  then run "make bench" to run the experiments with all solvers.
  You can also run "make sat" to just run the benchmarks with b2sat or
  run "make version" or "make help".
  The Makefile requires curl (which you can install on Linux using "sudo apt install curl").
- 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://stups.hhu-hosting.de/models/B2SAT/b2sat_prob_artifact.tgz -o artifact.tgz
shasum -a 256 artifact.tgz
tar -xvzf artifact.tgz
cd benchmarks
make install_prob
make sat
make bench
```