<jupyter_start><jupyter_text>Experimental evaluation of PBS Check toolsMake sure you have [Spot](https://spot.lrde.epita.fr/index.html) version 2.7.0 or greater installed in you system and that the commands `autfilt`, `genltl`, `randltl`, `ltlfilt`, `ltl2tgba` are available in your `PATH`.<jupyter_code>%run Tools.ipynb<jupyter_output><empty_output><jupyter_text>Benchmark formulae preparation Run the [Formulae](Formulae.ipynb) notebook. For more information about the formulae consult the [notebook](Formulae.ipynb) directly.<jupyter_code>mkdir -p formulae
import os
if not os.path.exists('formulae/random_nd.ltl'):
    %run Formulae.ipynb<jupyter_output><empty_output><jupyter_text>Automata preparation Run the [Automata](Automata.ipynb) notebook. For more information about the formulae consult the [notebook](Automata.ipynb) directly.<jupyter_code>mkdir -p automata
import os
if not os.path.exists('automata/random_ba.ltl'):
    %run Automata.ipynb<jupyter_output><empty_output><jupyter_text>Run the Evaluation and Results The notebook [Comparison](Comparison.ipynb) and [Comparison_automata](Comparison_automata.ipynb) notebooks create tables that compare the different complementation algorithms. The compared algorithms are the following:- Seminator + NCSB implemented in Spot- Spot complementation via determinization (two variants, one with BA and one with TGBA results)- PBS- Potentially also Buechic and Fribourg.If you want to rerun the experiments by yourself, delete the `.csv` files with the results in the directory `data`,```ipythonrm data/*.csv```or set the variable `rerun` to `True` in the second cell of the [Comparison](Comparison.ipynb) and [Comparison_automata](Comparison_automata.ipynb) notebooks and then run (either using the next cell, or in the notebook directly) it **[can take more then 1 hour]**.```pythonrerun = True```The [Comparison](Comparison.ipynb) notebook then creates 8 `.csv` files in the directory [`data`](data) that are used to create the tables and scatter plots. With `rerun = False` you rerun only the analysis.The [Comparison_automata](Comparison_automata.ipynb) notebook then creates 1 `.csv` file in the directory [`data`](data) that are used to create the tables and scatter plots. With `rerun = False` you rerun only the analysis.<jupyter_code>%run Comparison.ipynb
%run Comparison_automata.ipynb<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.09445843828715365, 'fraction_numerical': 0.002938706968933669, 'mean_word_length': 6.541139240506329, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 17, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '4', 'dir': 'jupyter-structured-clean-dedup', 'id': '577744', 'license': 'MIT', 'n_tokens_mistral': 727, 'n_tokens_neox': 698, 'n_words': 249, 'path': 'experiments/Evaluation.ipynb', 'repo_name': 'mklokocka/pbs', 'size': '2382'}