From 54f4a8681a96c896e982948146d88b708a66bb32 Mon Sep 17 00:00:00 2001 From: Falk Howar Date: Sat, 9 Dec 2023 17:38:49 +0100 Subject: [PATCH] tacas2024 experiments with documentation --- README.md | 106 +++++++++++++++++- compare-learners.sh | 13 ++- configs/null | 0 configs/twalk-dtls-eq | 8 +- configs/twalk-eq | 2 +- .../lifo_size_3.register.xml | 1 + .../lifo_size_5.register.xml | 1 + .../lifo_size_7.register.xml | 1 + experiments/ct-datastructures/set3.xml | 1 + experiments/ct-datastructures/set5.xml | 1 + experiments/ct-datastructures/set7.xml | 1 + experiments/dtls-twalk-eq/hyp-10.xml | 1 - experiments/dtls-twalk-eq/hyp-12.xml | 1 - experiments/dtls-twalk-eq/hyp-4.xml | 1 - experiments/dtls-twalk-eq/hyp-6.xml | 1 - experiments/dtls-twalk-eq/hyp-8.xml | 1 - generate-plots-tacas2024.sh | 1 + generate-summary-with-ce-search-tacas2024.sh | 7 +- 18 files changed, 132 insertions(+), 16 deletions(-) delete mode 100644 configs/null create mode 120000 experiments/ct-datastructures/lifo_size_3.register.xml create mode 120000 experiments/ct-datastructures/lifo_size_5.register.xml create mode 120000 experiments/ct-datastructures/lifo_size_7.register.xml create mode 120000 experiments/ct-datastructures/set3.xml create mode 120000 experiments/ct-datastructures/set5.xml create mode 120000 experiments/ct-datastructures/set7.xml delete mode 120000 experiments/dtls-twalk-eq/hyp-10.xml delete mode 120000 experiments/dtls-twalk-eq/hyp-12.xml delete mode 120000 experiments/dtls-twalk-eq/hyp-4.xml delete mode 120000 experiments/dtls-twalk-eq/hyp-6.xml delete mode 120000 experiments/dtls-twalk-eq/hyp-8.xml diff --git a/README.md b/README.md index 3e811fd..6ed6a89 100644 --- a/README.md +++ b/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 ``` diff --git a/compare-learners.sh b/compare-learners.sh index 63a0283..706bb8b 100755 --- a/compare-learners.sh +++ b/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,8 +113,8 @@ 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 @@ -121,6 +122,8 @@ for phase in ${phases[@]}; 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 @@ -128,6 +131,8 @@ 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,6 +141,8 @@ 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 @@ -143,6 +150,8 @@ for learner in ${learners[@]}; do 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 diff --git a/configs/null b/configs/null deleted file mode 100644 index e69de29..0000000 diff --git a/configs/twalk-dtls-eq b/configs/twalk-dtls-eq index 3b98898..03e365f 100644 --- a/configs/twalk-dtls-eq +++ b/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 diff --git a/configs/twalk-eq b/configs/twalk-eq index 1438a3f..7dd3172 100644 --- a/configs/twalk-eq +++ b/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 diff --git a/experiments/ct-datastructures/lifo_size_3.register.xml b/experiments/ct-datastructures/lifo_size_3.register.xml new file mode 120000 index 0000000..7ba0930 --- /dev/null +++ b/experiments/ct-datastructures/lifo_size_3.register.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_LIFO/lifo_size_3.register.xml \ No newline at end of file diff --git a/experiments/ct-datastructures/lifo_size_5.register.xml b/experiments/ct-datastructures/lifo_size_5.register.xml new file mode 120000 index 0000000..2bda385 --- /dev/null +++ b/experiments/ct-datastructures/lifo_size_5.register.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_LIFO/lifo_size_5.register.xml \ No newline at end of file diff --git a/experiments/ct-datastructures/lifo_size_7.register.xml b/experiments/ct-datastructures/lifo_size_7.register.xml new file mode 120000 index 0000000..10e7608 --- /dev/null +++ b/experiments/ct-datastructures/lifo_size_7.register.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_LIFO/lifo_size_7.register.xml \ No newline at end of file diff --git a/experiments/ct-datastructures/set3.xml b/experiments/ct-datastructures/set3.xml new file mode 120000 index 0000000..f66a781 --- /dev/null +++ b/experiments/ct-datastructures/set3.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_FSET/set-3.xml.register.xml \ No newline at end of file diff --git a/experiments/ct-datastructures/set5.xml b/experiments/ct-datastructures/set5.xml new file mode 120000 index 0000000..2c96eb7 --- /dev/null +++ b/experiments/ct-datastructures/set5.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_FSET/set-5.xml.register.xml \ No newline at end of file diff --git a/experiments/ct-datastructures/set7.xml b/experiments/ct-datastructures/set7.xml new file mode 120000 index 0000000..4ecb739 --- /dev/null +++ b/experiments/ct-datastructures/set7.xml @@ -0,0 +1 @@ +../../benchmarks/models/DS_FSET/set-7.xml.register.xml \ No newline at end of file diff --git a/experiments/dtls-twalk-eq/hyp-10.xml b/experiments/dtls-twalk-eq/hyp-10.xml deleted file mode 120000 index 5678da9..0000000 --- a/experiments/dtls-twalk-eq/hyp-10.xml +++ /dev/null @@ -1 +0,0 @@ -../../benchmarks/models/DTLS/clients/MbedTLS-2.26.0_psk_epoch/hyp-10.xml \ No newline at end of file diff --git a/experiments/dtls-twalk-eq/hyp-12.xml b/experiments/dtls-twalk-eq/hyp-12.xml deleted file mode 120000 index 75021be..0000000 --- a/experiments/dtls-twalk-eq/hyp-12.xml +++ /dev/null @@ -1 +0,0 @@ -../../benchmarks/models/DTLS/clients/MbedTLS-2.26.0_psk_epoch/hyp-12.xml \ No newline at end of file diff --git a/experiments/dtls-twalk-eq/hyp-4.xml b/experiments/dtls-twalk-eq/hyp-4.xml deleted file mode 120000 index 1812115..0000000 --- a/experiments/dtls-twalk-eq/hyp-4.xml +++ /dev/null @@ -1 +0,0 @@ -../../benchmarks/models/DTLS/clients/MbedTLS-2.26.0_psk_epoch/hyp-4.xml \ No newline at end of file diff --git a/experiments/dtls-twalk-eq/hyp-6.xml b/experiments/dtls-twalk-eq/hyp-6.xml deleted file mode 120000 index 0b85bd0..0000000 --- a/experiments/dtls-twalk-eq/hyp-6.xml +++ /dev/null @@ -1 +0,0 @@ -../../benchmarks/models/DTLS/clients/MbedTLS-2.26.0_psk_epoch/hyp-6.xml \ No newline at end of file diff --git a/experiments/dtls-twalk-eq/hyp-8.xml b/experiments/dtls-twalk-eq/hyp-8.xml deleted file mode 120000 index 2b8a5bc..0000000 --- a/experiments/dtls-twalk-eq/hyp-8.xml +++ /dev/null @@ -1 +0,0 @@ -../../benchmarks/models/DTLS/clients/MbedTLS-2.26.0_psk_epoch/hyp-8.xml \ No newline at end of file diff --git a/generate-plots-tacas2024.sh b/generate-plots-tacas2024.sh index a15e219..8c82350 100755 --- a/generate-plots-tacas2024.sh +++ b/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 diff --git a/generate-summary-with-ce-search-tacas2024.sh b/generate-summary-with-ce-search-tacas2024.sh index 545f7ea..a89c311 100755 --- a/generate-summary-with-ce-search-tacas2024.sh +++ b/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