Improved ReadMe

Author: pvdhove

README.md

@@ -1,6 +1,18 @@
-# Bolt
+# Bolt: Blazingly Fast LTL Learning
 
-Blazingly fast LTL learning.
+This repository contains the code accompanying our paper *LTLf Learning Meets Boolean Set Cover*. It provides instructions for running the code and reproducing our experimental results.
 
-This main branch is for LTL_f (over finite traces). 
-To learn LTL over infinite traces, using the branch LTL_infty
+## Requirements
+To run the code, you need to have [Rust](https://www.rust-lang.org/tools/install) installed. The code can be compiled using:
+```
+cargo build --release
+```
+
+## Running the code
+The three algorithms (`set-cover`, `enum`, `beam-search`) can be run with multiple parameters by changing command line arguments. For instance,
+```
+target/release/bolt example_input.json 8 10 beam-search 100 70
+```
+runs the beam search algorithm on file `example_input.json` with LTL2BS-switch = 8, size-dom = 10, beam-width = 100, and D&C-switch = 70.
+
+The Rust source code is in directory `src/`.

example_input.json

@@ -0,0 +1 @@
+{"positive_traces": [{"var0": [0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 0, 0, 0, 0, 1, 0], "var1": [0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1]}, {"var0": [0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 0], "var1": [0, 1, 0, 1, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 0]}, {"var0": [1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0], "var1": [1, 1, 0, 1, 0, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1]}, {"var0": [1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0], "var1": [1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 0, 1, 1, 1, 0]}, {"var0": [1, 1, 1, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0], "var1": [1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 1, 1, 0, 1, 0, 0]}], "negative_traces": [{"var0": [0, 0, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0], "var1": [0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 0, 0]}, {"var0": [0, 1, 0, 1, 0, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1], "var1": [0, 0, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0]}, {"var0": [0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 1, 0, 0, 1, 1], "var1": [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1]}, {"var0": [1, 1, 0, 0, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0, 0], "var1": [0, 1, 1, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1, 1, 1, 1]}, {"var0": [1, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 1, 1], "var1": [0, 1, 1, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1]}], "smallest_known_formula": "(! (var0)) U (var1)", "generating_formula": "F(var0) -> (!(var0) U var1)", "generating_seed": 42, "original_repository": "https://github.com/ivan-gavran/samples2LTL", "name": "Fixed_Formulas/absence2.txt", "atomic_propositions": ["var0", "var1"], "number_atomic_propositions": 2, "number_traces": 10, "number_positive_traces": 5, "number_negative_traces": 5, "max_length_traces": 16, "trace_type": "finite"}