tacas2024 experiments with documentation

README.md

@@ -1,12 +1,111 @@
 # RaLib Benchmarking Setup
 
-## Installation
+This project contains benchmark examples and scripts to 
+run RaLib on these benchmarks. The project is organized
+as follows:
+
+1. **benchmark problems** are located in ```benchmarks/```.
+    Problems are collected from papers on RaLib, from the
+    [automata wiki](https://automata.cs.ru.nl), and some
+    are generated or manually created for this project. 
+2. **configurations** of RaLib are located in ```configs/```.
+    The different configurations are used in different 
+    series of experiments and specify aspects of the 
+    learning experiments (how counterexamples are found,
+    how counterexamples are preprocessed, max. runtimes, 
+    teachers/theories for types, etc.) 
+3. **configurations** are organized in series in ```experiments/```.
+    Series combine benchmark problems with a configuration.
+    The different series in this project originate from 
+    multiple papers on RaLib / register automata learning.
+4. **results** from running experiments will be stored in 
+    ```results/```. Results include logs and models from 
+    individual learning experiments. Some scripts will 
+    use the results to compute plots and tables. 
+    Templates and generated documents ce be found 
+    in ```plots```.
+5. **RaLib** is a git sub module in ```ralib/```.
+
+
+## RaLib Installation
+
+To install RaLib, you have to initialize the submodule 
+and build RaLib, which requires a JDK and Maven to be 
+installed.
 
 ```
+git submodules init
 ./build.sh
 ```
 
-## Scripts
+## Running experiments 
+
+Generally, experiments are organized in series and 
+do configurations do not specify whih learner should 
+be used and how many times experiments should be run.
+Shell scripts exist for running individual experiments,
+series, and complete evaluations.
+
+### Experiments for the evaluation of CT-based learners (TACAS'24)
+
+This section describes how one can run the experiments 
+that are reported in the TACAS 2024 submission.
+Concrete results may vary a little bit for every 
+execution due to randomization but trends should be
+stable.
+
+1. Running experiments from TACAS 2024 submission
+
+    ```
+    ./run-experiments-model-checker-tacas2024.sh
+    ./run-experiments-with-ce-search-tacas2024.sh
+    ```
+
+    results (logs and models) can be found in ```results/```.
+
+
+2. Generating table in TACAS 2024 submission
+
+    this step requires latexmk and a latex distribution
+    to be installed
+
+    ```
+    ./generate-table-tacas2024.sh
+    ```
+
+    The generated pdf is ```plots/tacas2024-table-results.pdf```
+
+    *Note:* The generaled pdf has more rows and columns 
+    than the table in the paper.
+
+2. Generating plots    
+
+    this step requires latexmk and a latex distribution
+    with pgfplots to be installed
+
+    ```
+    ./generate-plots-tacas2024.sh
+    ```
+
+    The plots in Fig. 4. are:
+
+    ```
+    plots/plot-dtls-resets.pdf
+    plots/plot-dtls-resets-noopt.pdf
+    plots/plot-dtls-counterexamples.pdf
+    plots/plot-dtls-wct.pdf
+    ```
+
+    The plots in Fig. 5 are
+
+    ```
+    plots/plot-gen-transitions.pdf
+    plots/plot-gen-registers.pdf
+    plots/plot-gen-registers-noopt.pdf
+    ```
+
+    *Note:* Some additional plots that are generated
+    were not included in the paper.
 
 ### Running individual experiments
 
@@ -26,7 +125,7 @@ run_series.sh [-h] -s series -i iterations -l learner
 Run the series of experiments specied in folder
 `experiments/[series]` with specified learner.
 
-### Running the complete evaluation
+### Running the complete evaluation (2015 RaLib Paper)
 
 ```
 run_evaluation.sh
@@ -35,6 +134,7 @@ run_evaluation.sh
 This script contains explicit calls to `run_series.sh` for
 all experiments that are to be run as part of the evaluation.
 
+
 ### Searching in logs
 
 ```

compare-learners.sh

@@ -63,7 +63,8 @@ print_count() {
             n=$((n+1))
         fi
     done
-    printf "%1d/%1d, " $n ${#files[@]}
+    printf "%1d, " $n
+#    printf "%1d/%1d, " $n ${#files[@]}
 }
 
 print_header() {
@@ -112,22 +113,26 @@ for learner in ${learners[@]}; do
         print_val "Sys. Transitions" "Sys. Transitions" $files
         print_val "Sys. Registers" "Sys. Registers" $files
         print_val "Constants" "Constants" $files
+        break
     fi
-    break
 done
 
 for phase in ${phases[@]}; do
     for learner in ${learners[@]}; do
         if [ -d "results/$series/$experiment-$learner" ]; then
             files=($(ls results/$series/$experiment-$learner | grep 'log' | sed "s/\(.*\)/results\/$series\/$experiment-$learner\/\1/"))
             print_stat "$phase" $stat $files
+        else
+            printf ",,"
         fi 
     done
 done  
 for learner in ${learners[@]}; do
     if [ -d "results/$series/$experiment-$learner" ]; then
         files=($(ls results/$series/$experiment-$learner | grep 'log' | sed "s/\(.*\)/results\/$series\/$experiment-$learner\/\1/"))
         print_stat "Counterexamples" "Counterexamples" $files
+    else
+        printf ",,"
     fi 
 done
 for learner in ${learners[@]}; do
@@ -136,13 +141,17 @@ for learner in ${learners[@]}; do
         print_stat "Hyp. Locations" "Hyp. Locations" $files
         print_stat "Hyp. Transitions" "Hyp. Transitions" $files
         print_stat "Hyp. Registers" "Hyp. Registers" $files
+    else
+        printf ",,,,,,"
     fi
 done
 for learner in ${learners[@]}; do
     if [ -d "results/$series/$experiment-$learner" ]; then
         files=($(ls results/$series/$experiment-$learner | grep 'log' | sed "s/\(.*\)/results\/$series\/$experiment-$learner\/\1/"))
         print_stat "learning \[ms\]" "learning \[ms\]" $files
         print_stat "ce searching \[ms\]" "ce searching \[ms\]" $files
+    else
+        printf ",,,,"
     fi
 done
 

configs/twalk-dtls-eq

@@ -5,11 +5,11 @@ use.suffixopt=true
 use.fresh=false
 use.rwalk=true
 export.model=true
-rwalk.prob.fresh=0.3
+rwalk.prob.fresh=0.2
 rwalk.prob.reset=0.1
 rwalk.seed.transitions=true
-rwalk.max.depth=10
-rwalk.max.runs=100000
-rwalk.reset.count=false
+rwalk.max.depth=20
+rwalk.max.runs=1000000
+rwalk.reset.count=true
 rwalk.draw.uniform=true
 teachers=epoch:de.learnlib.ralib.tools.theories.IntegerEqualityTheory

configs/twalk-eq

@@ -11,5 +11,5 @@ rwalk.seed.transitions=true
 rwalk.max.depth=10
 rwalk.max.runs=10000
 rwalk.reset.count=false
-rwalk.draw.uniform=true
+rwalk.draw.uniform=false
 teachers=int:de.learnlib.ralib.tools.theories.IntegerEqualityTheory

experiments/ct-datastructures/lifo_size_3.register.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_LIFO/lifo_size_3.register.xml

experiments/ct-datastructures/lifo_size_5.register.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_LIFO/lifo_size_5.register.xml

experiments/ct-datastructures/lifo_size_7.register.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_LIFO/lifo_size_7.register.xml

experiments/ct-datastructures/set3.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_FSET/set-3.xml.register.xml

experiments/ct-datastructures/set5.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_FSET/set-5.xml.register.xml

experiments/ct-datastructures/set7.xml

@@ -0,0 +1 @@
+../../benchmarks/models/DS_FSET/set-7.xml.register.xml

generate-plots-tacas2024.sh

@@ -40,6 +40,7 @@ latexmk -pdf boxplot-gen-registers.tex
 latexmk -pdf boxplot-gen-registers-noopt.tex
 
 latexmk -pdf plot-gen-transitions.tex
+latexmk -pdf plot-gen-counterexamples.tex
 latexmk -pdf plot-gen-registers.tex
 latexmk -pdf plot-gen-registers-noopt.tex
 

generate-summary-with-ce-search-tacas2024.sh

@@ -13,5 +13,10 @@
 ./compare-learners.sh ct-datastructures fifo_size_5.register
 ./compare-learners.sh ct-datastructures fifo_size_7.register
 
+./compare-learners.sh ct-datastructures lifo_size_3.register
+./compare-learners.sh ct-datastructures lifo_size_5.register
+./compare-learners.sh ct-datastructures lifo_size_7.register
 
-
+./compare-learners.sh ct-datastructures set3
+./compare-learners.sh ct-datastructures set5
+./compare-learners.sh ct-datastructures set7