From 9b1239d38f9125438702756fc68f9e5a3fe9e275 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Mon, 20 Apr 2026 11:38:40 +0200 Subject: [PATCH 1/3] improve artifact evaluation README, fix eval scripts This commit improves the artifact evaluation README and fixes issues in the evaluation scripts. Most importantly, it fixes a conidition that would lead to the smoke tests not having their timeout applied. Additionally, it adds a check for correct permissions on the mounted local storage and improves error messages throughout the script. --- CHANGELOG.md | 2 + artifact-evaluation/artifact-evaluation.md | 262 +++++++++++---------- artifact-evaluation/bench-bymc.sh | 26 +- artifact-evaluation/bundle-ae.sh | 11 +- artifact-evaluation/table2.ods | Bin 0 -> 34483 bytes scripts/bench-taco.sh | 40 +++- 6 files changed, 211 insertions(+), 130 deletions(-) create mode 100644 artifact-evaluation/table2.ods diff --git a/CHANGELOG.md b/CHANGELOG.md index d699d95..99063ca 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,11 +15,13 @@ consistent (#3) - replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#2) - fix clippy issues with 1.95 (#8) +- remove old default timeout that caused timeout for smoke tests not be set (#9) ### Added - Elaborate on the function of the different preprocessors (#6) - upgrade CI pipeline & Dockerfile to Rust 1.95 (#8) +- improved artifact evaluation README (#9) ## [v0.1.0] diff --git a/artifact-evaluation/artifact-evaluation.md b/artifact-evaluation/artifact-evaluation.md index c4a9ca5..106906b 100644 --- a/artifact-evaluation/artifact-evaluation.md +++ b/artifact-evaluation/artifact-evaluation.md @@ -2,23 +2,22 @@ Welcome to the TACO model checker artifact README. -## Artifact Details - -**DOI artifact**: [https://doi.org/10.5281/zenodo.18233866](https://doi.org/10.5281/zenodo.18233866) +This document will provide you with instructions on how to reproduce the +benchmark results and instructions on how to access the TACO documentation. -**Paper**: "TACO: A Toolsuite for the Verification of Threshold Automata" +The TACO documentation contains more information on how to model and verify +systems and protocols using TACO and on TACO's configuration options. +Additionally, the developer documentation contains details on the internals of +TACO. See [Section `Documentation`](#documentation) for how to access the +documentation. -**Tested on**: amd64 +## Artifact Details -Host OS: +**Paper Title**: TACO: A Toolsuite for the Verification of Threshold Automata -- Ubuntu 22.04/24.04/25.04 -- Fedora 42/43 -- Container Runtime: Podman or Docker +**DOI artifact**: [https://doi.org/10.5281/zenodo.19659446](https://doi.org/10.5281/zenodo.19659446) -Also tested on MacOS with arm64 running Podman, however for this setup we -observed significantly decreased performance especially for the tool we compare -against ([ByMC]). +**CPU Architecture (for Evaluation)**: x86_64 (amd64) ### System Requirements @@ -36,31 +35,31 @@ TACO does not have any special system requirements. However, we did not attempt to build the tool we compare against [ByMC] for an architecture other than x86, as the tool is no longer maintained. -The evaluation as presented in the main section of the paper took in sum 14h +The evaluation as presented in the main section of the paper took, in sum, 14h (including around 2.5h for a run of ByMC). -Please be aware that the extended evaluation can take significant time, on our -setup, all runs took in sum 90h. Therefore, having access to multiple machines -might be beneficial. - However, you can decrease the runtime and resource consumption drastically. By reducing the timeout per benchmark, e.g., reducing per benchmark to <= 10min, you can limit the overall time and resource consumption such that a considerable subset of benchmarks should be solvable by TACO on a decently powerful laptop within 8h. - We will explain how to configure the timeout in the relevant sections. -## Introduction +Please be aware that the extended evaluation can take significant time. On our +setup, all runs took in sum 90h. Therefore, having access to multiple machines +might be beneficial. -This document will only provide you with instructions on how to reproduce the -benchmark results and instructions on how to access the TACO documentation. +### Tested On -The TACO documentation contains more information on how to model and verify -systems and protocols using TACO, as well as all the configuration options. -Additionally, the developer documentation contains details on the internals of -TACO. See [Section `Documentation`](#documentation) for how to access the -documentation. +Host OS: + +- Ubuntu 22.04/24.04/25.04 +- Fedora 42/43 +- Container Runtime: Podman or Docker + +Also tested on MacOS with arm64 running Podman. However, for this setup, we +observed significantly decreased performance, especially for the tool we compare, +against ([ByMC]). ## Reproducing the Benchmark Table @@ -69,9 +68,9 @@ model checkers. ### Preparation -First, you need to load the container image from the files of the artifact. This -can be done by navigating into the unzipped directory of the artifact and -executing +First, you need to load the evaluation container image from the files of the +artifact. This can be done by navigating into the unzipped directory of the +artifact and executing ```bash docker load -i taco.tar @@ -87,31 +86,36 @@ docker run --rm -it localhost/taco:latest
Details - `--rm` specifies that the container will be deleted once you exit the - shell, and -- `-it` starts the container in "interactive" mode, i.e., it opens the -shell for you. -
+ shell. This removes the need to clean up old containers. +- `-it` starts the container in "interactive" mode, i.e., it directly opens a +shell in the container. +
-Now you can already start executing benchmarks as described in sections -[`Smoke Tests`](#smoke-tests) and -[`Main Evaluation Benchmark Run`](#main-evaluation-benchmark-run). -However, the log files of such a test run will not be moved outside the -container and therefore will be gone as soon as the container terminates. +Now we are ready to start executing benchmarks. +You can find the instructions to execute smoke tests in section +[`Smoke Tests`](#smoke-tests) and the instructions for a full evaluation run in +[`TACO Benchmark Run`](#taco-benchmark-run). -##### Mounting Local Storage to Obtain Results +Note that with the current setup, the log files of a run will not be moved +outside the container and therefore will be gone as soon as the container +terminates. If you prefer our evaluation scripts to automatically move log files +outside the container onto your local storage, you can follow the instructions +in the next section. + +#### Mounting Local Storage While the previously described is sufficient for running the tests, you might -want the result tables and logfiles to be moved outside the container to +want the result tables and log files to be moved outside the container to inspect them later. -This can be achieved by mounting your local storage into the container using -the `-v` flag. For example, use: +To do so, you can mount your local storage into the container using +the `-v` flag. For example, use ```bash docker run --rm -it -v ./:/storage localhost/taco:latest ``` -
Details +
Details & Trouble Shooting Here, `-v ./:/storage` specifies to mount the current directory, i.e., `./` to the container and makes it accessible in the running container under the directory `/storage`. @@ -121,34 +125,37 @@ option; This however should never be done in the directory `/home` or `/usr`. See [Docker Documentation](https://docs.docker.com/engine/storage/bind-mounts/#configure-the-selinux-label) -
+

-If the directory `/storage` exists, the benchmark scripts will automatically -move the result table(s), logfile(s) and potential crash reports to your local -storage after all benchmarks are finished. +Our scripts will check for the existence of the path `/storage`. +If this directory exists, the benchmark scripts will automatically move the +result table(s), logfile(s) and potential crash reports to your local storage +after all benchmarks are finished. ### Smoke Tests -As mentioned before, a full benchmark run can take more than 14h (or 90h -respectively). Therefore, we include a set of smoke tests to first verify that -TACO is running without issues. +Before running a full benchmark run (which can take significant amounts of +time), we recommend to test the setup with our set of smoke tests. -In the shell of the TACO container, you can execute the smoke tests simply by -running: +In our evaluation image, this can be done by opening a shell in the TACO +container, and executing our benchmarking script with the `--smoke` flag: ```bash benchmark-taco --smoke ``` The smoke tests will execute the benchmark set "Small ByMC" with a timeout of -30s for each model checker. Additionally, this setting will print all the output -of TACO to the console to make any errors that might occur directly visible. +30s for each model checker. + +Additionally, this setting will print all the output of TACO to the console to +make any errors that might occur directly visible (note that in a full run the +output will only be written to the log files to avoid cluttering stdout). The script will also create a preliminary result table called `taco-exec.csv` which should roughly match the results we reported in our paper for these benchmarks. -### Main Evaluation Benchmark Run +### TACO Benchmark Run To run the set of benchmarks used for the experimental evaluation in the main section of the paper with a timeout of 20min per benchmark you can simply @@ -159,9 +166,22 @@ benchmark-taco ``` This will run the full benchmark suite with a timeout of 20min per benchmark. -Note that in sum such a run can take around 11.5h. -The [next section](#setting-a-different-timeout) will describe the flags to set -a different timeout per benchmark. +Note that in sum, such a run can take around _14h_. To start a run that should +complete within 8h, we recommend to lower the timeout per benchmark to a time +<= 10min. + +This can be done using the `--timeout` flag, for example, use + +```bash +benchmark-taco --timeout 10m +``` + +
Details + +The time limit must be specified in the input format of the `timeout` command, +i.e., 3s are specified as `3s`, 3min as `3m` and 3h as `3h`. + +

The benchmark script will then only report time and memory statistics per benchmark (and errors in case any occurred). This output will also be parsed @@ -169,23 +189,12 @@ into a CSV table named `taco-exec.csv`. This table should match the results reported in the paper. The model checker output will be written to a separate log file (`taco-exec.log`). Both files will be moved to your local storage in case you -mounted it to the container (see section [Preparation](#preparation)). - -#### Setting a Custom Timeout +mounted it to the container under path `/storage` (see Section [Mounting Local +Storage](#mounting-local-storage)). -For example to set a timeout of 10min per benchmark, use +#### Benchmarking Options -```bash -benchmark-taco --timeout 10m -``` - -(The time must be specified in the input format of the `timeout` command, i.e., -3s are specified as `3s`, 3min as `3m` and 3h as `3h`). - -The above timeout of 10min per benchmark should be sufficient for all benchmarks -to be completed or timed out within 8h. - -#### Running only a Single Model Checker +##### Running only a Single Model Checker To run the full set of benchmarks for a single model checker, e.g., if you split the benchmark run across multiple machines, you can simply pass the model @@ -198,7 +207,7 @@ use: benchmark-taco --smt ``` -#### Other options +##### Other Options If your environment has the need for more configuration, e.g., we include more configuration options in the TACO benchmark script, which you can get an @@ -229,10 +238,10 @@ benchmark-taco --extended --smt-solver cvc5 ### ByMC -Since [ByMC] has not been maintained for a few -years now, compiling it requires installation of old versions of dependencies. -Unfortunately, this also includes components that TACO uses, like Z3. -Therefore we needed to package ByMC into a separate container image. +Since [ByMC] has not been maintained for a few years now, compiling it requires +installation of old versions of dependencies. Unfortunately, this also includes +components that TACO uses, like Z3. To avoid conflicts, we therefore decided to +package ByMC into a separate container image. We made the Dockerfile which we used to compile ByMC openly available on GitHub in the form of this [pull request](https://github.com/konnov/bymc/pull/2). @@ -265,12 +274,11 @@ or again with docker run --rm -it -v ./:/storage localhost/bymc:latest ``` -If you want the logfiles to be moved to your local storage outside the -container. +If you want the log files to be moved to your local storage outside the +container (see Section [Mounting Local Storage](#mounting-local-storage)). -Analog to the TACO benchmarks, you can execute the set of benchmarks used in -the evaluation section in the main part of the paper by -running: +Analogous to the TACO benchmarks, you can execute the set of benchmarks used in +the evaluation section in the main part of the paper by running: ```bash benchmark-bymc @@ -286,21 +294,21 @@ benchmark-bymc --timeout 10m will set a benchmark to timeout after 10min. -Analog to the TACO benchmark script, the script will only report benchmark +Analogous to the TACO benchmark script, the script will only report benchmark execution time and resource consumption and will store the benchmark results in -`bymc-exec.csv` and the model checker output as a logfile called -`bymc-exec.log`. ByMC additionally stores counter examples in the `x` directory. +`bymc-exec.csv` and the model checker output as a log file called +`bymc-exec.log`. ByMC additionally stores counterexamples in the `x` directory. #### Extended Evaluation Benchmark Run -Analog to the TACO benchmark script, you can start an extended evaluation run -using the `--extended` flag: +Following the example of the TACO benchmark script, you can start an extended +evaluation run using the `--extended` flag: ```bash benchmark-bymc --extended ``` -In this case, the script will directly also run ByMC in the `cav15` mode. +Note that this script will directly run ByMC also in the `cav15` mode. ## Documentation @@ -318,18 +326,29 @@ The user documentation is generated using There are multiple ways to access the documentation: -- Checkout TACO's website [`taco-mc.dev`](https://taco-mc.dev) (_easiest_) +- Check out TACO's website [`taco-mc.dev`](https://taco-mc.dev) (_easiest_) - Serve the documentation from the container image -- Read the source files +- Read the source files (packaged in the artifact and available on + [GitHub](https://github.com/cispa/TACO)) - Build the documentation from scratch -The first option might already display an updated page as TACO is still actively -maintained. To get the documentation at the time of submission, you can serve -it from the provided container image by following the instructions in the next -section. +The first option might already forward you to an updated page, as TACO is still +actively maintained. To get the documentation at the time of submission, you can +serve it from the provided container image by following the instructions in the +next section. + +Additionally, TACO's source code has been published to GitHub under +[https://github.com/cispa/TACO](https://github.com/cispa/TACO) and is available +on `crates.io` with the source documentation therefore also available under +`docs.rs`. The README of the source code (title page of the repository) contains +the links to the artifacts on `crates.io` and `docs.rs`. ### Serving the Documentation from the Container +We have included a preconfigured Apache server with the artifact container image +such that you can serve the documentation from the local files without needing +internet access. + To be able to access the documentation server that will be running inside the TACO container, we need to publish the port `80` (which will be the port of our server will be serving the documentation) of the container by additionally using @@ -356,7 +375,7 @@ the container. The documentation will in then case be served under the address [http://localhost:3001](http://localhost:3001). - +
You can now start the documentation server by executing (and leaving the shell open) @@ -390,16 +409,7 @@ in the file `src/docs/dev-docs.md` in the sections `Building the Developer Documentation` and `Displaying & Editing the User Documentation`. -## Additional Contents of the Artifact - -We have included the full source code of TACO inside this artifact in the `src` -directory. Alternatively, you can also find the source code in [TACO's Github -repository](https://github.com/cispa/TACO). - -You will also be able to find the Dockerfiles, scripts, documentation, etc. in -the `src` directory. - -### Running TACO +## Running & Using TACO If you want to test out the TACO CLI in the image we provided, you can call TACO by simply using @@ -408,12 +418,24 @@ by simply using taco-cli ``` -as TACO has been correctly installed in the container image. +as TACO has been correctly installed in the container image. The [User Guide +CLI](https://taco-mc.dev/usage-cli/) will provide you with more information on +how to use TACO with other examples and on TACO's configuration options. + +## Additional Contents of the Artifact + +We have included the full source code of TACO inside this artifact in the `src` +directory. Alternatively, you can also find the source code in [TACO's Github +repository](https://github.com/cispa/TACO). + +You will also be able to find the Dockerfiles, scripts, documentation, etc. in +the `src` directory. ## Benchmarking Considerations This section will elaborate on some choices that were made when designing the -outlined benchmarking process for this artifact evaluation. +outlined benchmarking process for this artifact evaluation. It is intended to +document our methodology and can be considered optional for artifact evaluation. ### Metrics & Limits during Evaluation @@ -421,11 +443,11 @@ The benchmarking scripts always report the elapsed real-time and maximal resident set size as reported by the GNU `time` command. Additionally, we use the `timeout` command to stop benchmark runs that exceed -the maximal runtime. In our evaluation we set the timeout to 20min. +the maximal runtime. In our evaluation, we set the timeout to 20min. The memory limit was set using `ulimit -SHv`, i.e., we limited the memory consumption by setting a limit on the virtual memory the model checkers are -allowed to use. For the evaluation the limit was set to `2071552`MB. +allowed to use. For the evaluation, the limit was set to `2071552`MB. We conducted our evaluation on Dell R6525 nodes equipped with 2x AMD Epyc 7773x with 128 physical cores + 128 Simultaneous Multithreading and 2TB of RAM. @@ -456,12 +478,12 @@ There were two main reasons why we chose to build our own Dockerfile instead: - Cumbersome benchmark process. The ByMC VM is based on Debian 9 and by now is difficult to work with. For example, in our testing the guest additions (providing functionality like shared folders, drag and drop) did not work - properly, making file transfer difficult. We would have not been able to + properly, making file transfer difficult. We would not have been able to provide the reviewers with the same level of automation as with the current container-based method. - Even older dependencies. The VM comes, for example, with [Z3] `4.4.1` (released Oct 5th 2015 on - [GitHub](https://github.com/Z3Prover/z3/releases/tag/z3-4.4.1)) installed + [GitHub](https://github.com/Z3Prover/z3/releases/tag/z3-4.4.1)) installed, which is three years older than the version of [Z3] we were able to use in the container image, which is `4.7.1` (released May 23rd 2018 on [GitHub](https://github.com/Z3Prover/z3/releases/tag/z3-4.7.1)). @@ -484,10 +506,10 @@ the benchmarks in the folder `isola18/ta-(handcoded)` for - `c1cs.ta` - `cf1s.ta` -this mode reported the benchmarks to be unsafe, even though all other model -checkers (including ByMC in the `isola18` mode) report them as save. +This mode reported the benchmarks to be unsafe, even though all other model +checkers (including ByMC in the `isola18` mode) report them as safe. -Here is an example of the counter example ByMC reports for `bosco.ta`: +Here is an example of the counterexample ByMC reports for `bosco.ta`: ``` ---------------- @@ -505,19 +527,19 @@ Here is an example of the counter example ByMC reports for `bosco.ta`: Gute Nacht. Spokoinoy nochi. Laku noch. ``` -This counter example should represent a counter example to the property +This counterexample should represent a counterexample to the property ``` lemma4_0: []((locD0 != 0) -> (locU1 == 0)); ``` -i.e. this should be a run that satisfies the negation, i.e.: +i.e., this should be a run that satisfies the negation, i.e.: ``` <>((locD0 != 0) && (locU1 != 0)) ``` -analyze the example. Configuration `1` has the variable state +We analyze the example. Configuration `1` has the variable state `nsnt0 := 3; nsnt01 := 3;`. The only rule incrementing `nsnt0` and `nsnt01` as in configuration 1 is: @@ -547,7 +569,7 @@ executing rule `6`: do { unchanged(nsnt0, nsnt1, nsnt01); }; ``` -Substituting with the parameter assignment of the counter example `N := 4; +Substituting with the parameter assignment of the counterexample `N := 4; T := 1; F := 1;`: ``` @@ -576,7 +598,7 @@ Therefore, either - or some processes must be able to reach `loc1`, which is impossible as `loc1` has no incoming rules. -Therefore no process can transition to `locU1` and the counter example is +Therefore no process can transition to `locU1` and the counterexample is invalid. We saw this behavior in the official ByMC VM diff --git a/artifact-evaluation/bench-bymc.sh b/artifact-evaluation/bench-bymc.sh index c104386..f20912a 100755 --- a/artifact-evaluation/bench-bymc.sh +++ b/artifact-evaluation/bench-bymc.sh @@ -478,6 +478,26 @@ options.\n" 1>&2 esac done +# Test whether permissions are correct on OUTDIR (need write + create of files) +if [ -d "${OUTDIR}" ]; then + # Verify we can create files in OUTDIR + OUTDIR_TEST_FILE="${OUTDIR}/.taco-write-test.tmp" + touch "${OUTDIR_TEST_FILE}" + if [ ! -f "${OUTDIR_TEST_FILE}" ]; then + printf "Directory '${OUTDIR}' exists but is not writable / cannot create +files in it. This error might be resolvable by adding :z after the volume mount +description. Check the README for details. + +If you chose to continue anyway, results will stay in the current working +directory. Sleeping 10s to give you time to abort.\n\n\n +" 1>&2 + OUTDIR="" + sleep 10 + else + rm -f "${OUTDIR_TEST_FILE}" + fi +fi + # Make the user aware of extended setting if [ "${EXTENDED}" = true ]; then printf "Executing the extended TACO benchmark suite. This can take a lot of @@ -502,12 +522,12 @@ fi if [ -d "${OUTDIR}" ]; then echo "Moving the benchmark execution log '${LOGFILE}' and counterexamples (which can be found in directory 'x') to local storage" - mv "${LOGFILE}" "${OUTDIR}" - cp -R ./x "${OUTDIR}" + cp --backup=t "${LOGFILE}" "${OUTDIR}" + cp --backup=t -R ./x "${OUTDIR}" if [ -f "${CSV_FILE_NAME}" ]; then printf "Copying the benchmark result table '${CSV_FILE_NAME}' to local \ storage\n" - cp "${CSV_FILE_NAME}" "${OUTDIR}" + cp --backup=t "${CSV_FILE_NAME}" "${OUTDIR}" fi else printf "No output directory specified, or directory does not exist. diff --git a/artifact-evaluation/bundle-ae.sh b/artifact-evaluation/bundle-ae.sh index bd19eea..b9ffaaf 100755 --- a/artifact-evaluation/bundle-ae.sh +++ b/artifact-evaluation/bundle-ae.sh @@ -2,6 +2,11 @@ # Convenience script to package an artifact for TACO, designed to be run with # podman +# Strict mode with error reporting +set -euo pipefail +trap 's=$?; echo "$0: Error on line "$LINENO": $BASH_COMMAND"; exit $s' ERR +IFS=$'\n\t' + # Remove all unnecessary stuff first # Remove build output cargo clean @@ -11,12 +16,14 @@ rm -rf docs/_build mkdir artifact # Artifact README -cp resources/artifact-evaluation.md artifact/README.md +cp artifact-evaluation/artifact-evaluation.md artifact/README.md # LICENSE cp ./LICENSE artifact/LICENSE # Paper pdf -#cp resources/paper_5548.pdf artifact/paper_5548.pdf +#cp artifact-evaluation/paper.pdf artifact/paper.pdf +# Table 2 ods +cp artifact-evaluation/table2.ods artifact/table2.ods # Create source directory mkdir artifact/src diff --git a/artifact-evaluation/table2.ods b/artifact-evaluation/table2.ods new file mode 100644 index 0000000000000000000000000000000000000000..42fbfdf7630df2201de6088228767de33a673f18 GIT binary patch literal 34483 zcmbTc1#nzV(k&=vW=4y-#mvl-EoNqBw8*lUp~cM1%*7vg355j)1_uT{ zgR+~Wqn(qngSp**(Zl->dKPw$#%|{S&DH;8&DG7=&E3_+_`m7>Cu{$B`QNqvQ%Id$ z94%eUUH=dE{*#|hj!y1QpZRqE{}`2jRQ@kN;o#u@)tx@W_rD*6&zh^7x1G5wvzNWy zmhPXpjW+C$?cM>ExdP~k`8{C7`3QD0 z)B|q;2AsEYe0sKv*l@+J3>kg?FV{0(eKy)UE!A|&`o!xUQc~IZfkOo&C5Q=^6$%vJ+~E-rN01kMd16v3-{S+oY%*@G%56$ z(|StymO~FA)x+QEXuyckQU;u(()Y!b+;^N-h?VhYOXV20JM2&n9r{YcK5!X-h`KwSfkI(?OBdk(AW8 zUFuS-7Pn)Wf%1XKR%ZEC=wbW$QZ8|SxsKV^pUN}D$#v>`bW%g+y;Fv@RMA0tUf ztF)Girrk6eTG9=C30qxCqUGWT@PeR*CF~6F_$T&&PgTEay1Big+G5AfAd3bvBgBui zToo=>wn>fphYWT6EaoyfOEg}|#Ic--Y6YE##5i~m827i<`9)&grJwdox=jJ8-GYWI`1?DWA1WOxwjQ zF~ONg{5)Po95Ws$L+LqDSx+*4 zLtpOPI%0^}DI0`!OE|uc@6Xeq^z-tAhtH0QYT&B_2K}R{HGp2KxQ~s1^T!DX?|Nx= zp;k)l)v3N_{eViaQpoVUnqk8Ofr^@Eo4uIq^HVnS_navu+143`*h#&O*_deJhLrfM zEjnMgecQ{m*XMf}17G&$wrVv68Ch=E&F8=@w*`@H)QGQ#Rdv8Z{ModjvCU# z=eIUpqxTR&lqK}>I_-)H2fhc>Qwt->KIOk(UMensh>|*IDSc<0agmWmuiV<7hxExJ zqeF-F{HadNyRW=Lv{5*+y>b$GCH!JNnVLi-W*}YLg+Gvda?3WHq2b|c%fx%BK*xKc zG|qOW5~k+QEQlhvG(TR2REwO+4W|8Gcfe0QAHQ04R(dlIVRcH_FBYOifV7fh1Vw{W z?=p6Y1}k>jeS@0SxR25=@k#*Q`$JG*_a~-%BuY*2anv!@6{nU-(R~04A$^^_jYA)c zP9N=0MoDnuF&_S4;(;}#4g+iSYAOx+2@Pn4Uy%4@+WE*?EVXR*DlH0fcWnh}GAi`2 zGMnkD^EOt!_b6IM`T^p$5^-NmW9t4&ulfqSjkJ1Zx{foKpk9!45e5iMf$mJ7OHPos z1ac8Cej)fA`LW6@w_H>5 zJb6NWGmM2(mY$R=+ja?g5wTr}HT8l00!f#O5(4wmx(1kU-r`JWyWNZcBH{~dQ#+*+&}qm5p1%#TwQVN{4>h9HOtQ-R9}|J3p>-17A9*N zh!)9Ddqg%jS^N#rk%GxY%(prBbEwyG4+gAJ`MMeJHw#bzkVH(1N#f6Fi)f;Jj--rm?d^&X6yOD!o!MN7t4K}{|=d<$s3aDUZOhZK+jJt}`3`Xcv|3Mb} zjawPDKQKQ)>9NT8k(%g@;W#?*sb@t>NE=PD^GM>}8@7Vf6%iR_W0*he%EMk$p`C5@O-m{O%V`8p+Y!T;quGDmdw?mxy`T4RK9@*1KHIm0=4HkfReEkcEUtaN4tmYk^H;@VqV)a= zxo&x@QlQyssu|8yfe{z#lvl(3_K$u>GP18BowScdjBG2tF5xa_wZYRvAAnjlE<6Q2 z$&gFrZI@pr%XY{$P&b`(Tb!*NVrZUQ?rO3 zOxZikdrx~ zb(C^_yF}dF#->F*gEon(^`%*G?_pL+TP8AYIT_tGPwm+=sh_g-6vmAI z2Br=^C!JoMmiVaXZ;Wj`AT)iw5^z%!JpLu}mWp2Cyh~(Jrp`j_*c%u8EM@A^)A1(i z)Er6_=@NO<&COqCLC}d=`yh^bfPc%)^7jEA;iYz!+^mh8#jwY3uNC%OW*$L|;e|e7 zno`~p_B=SeooCc$K#Snn@v!ABPkQ8s(Y?_Hh7134y!e5-(o0fRQX_8DY+2f5xk zmYJfk3pQ@hy^JQ&N(LwD2C@(CTL}#A)5*u<4$R>VaczPRPI*@+*wV~WeCdgbbRWM4 zK|D7POuJ~~vYHz94!i{v-MsWpwml)M$iu?9K+)3Yz=MGy@`8c=8gET-e99YREqLNC1$ns^5>e5_T-!YO9HJwv%&Q&$GZESL0cXp&oFOIB38 z%kr)hO#88Cp09HCGkAG~0(B(o5x|g_P#%D%!#^HuGFiBKTK?3~hSb}~s~c`85KDA? z1sUTN>@idHu2kOnRPRgB$e!2|-h`^fkl&~sMvPGJn<1dhlY^%I_ZZ>bE&(1+3jcX(C$U z2!5!ZvuLZC{Pg=@@oRdpT7Uru0}FxtZ}I!rCd=H-_#aFhqdpm%#fsK-%n;wGd1ZQL=z4-_L>!GyiPvLk(JUc zoUlp)?Kt=+K=Vl}hAITR_+`3BWz@r=M>UIs6#*V++3Q}?=tgMlI z3Yd|a7fV(z$IBK?vF9}4Ttg(knU zp+X*Mp%TnSn0jm$wDrV2R>uW5FnI>U=!KqDOZsDpau=ezaEvZaTYI_sx z0r2(eCMp)|as~-n`7jN#7 zjrb3F`-N!|WOqFf)$K^Xwka^w+y#=^N!+qS&0vAQD=4+0Dhj(%M#wbd+)3gt%m!{4 z5c?1PSKymt`D3IqN?`xYgR9M1uAq5_-{;58z%Luq^N|%4HpXHPo;qo0er>p{znOM${``2Zt-)}BjUbOvI2lt2I z>R;8~`ZbByfs(fVhd75TN8A9qCm7fw{yySQoSMH;UHFOTUa79g7{9%VH~PCZ(FF>d zTnnWMG4>gzL0doRPUL`>TenAy#G|}%a;8u-LzY?+6+F=^BD*Qh!e=5prW7cXI*WsC zZT3OJ!qXL@)7S7$T$(RCEdNa|J^7fJ8|9q$SH9(KtKapRG6MrGqb4*h+Af9Ea%^7@ zXd91yGw7!BYy~%y6cn#!TPJ^nHQ~@6!LGGKJR!y$=WD*&>EJQ~PhWbY=+?))_>umu z=qKo;fDX<2=Pw79imS5>iv&a<1foAXYzDkSEt%1FgWPg7{5N$i6pwZ!C_QI*Tw3=? zH%HN5V8u|%lw0&pR8gb5)wPBCKk;EO;Ah}g{R2yaYB2NLS=IN+=nYp8A>^5bW>~(p zHcHf4(@v>LNTN)*iVB+QQC#QJa$?p<(+(x8nlC#N2R=WNV7A1-ONku$Q9`H-YF#-| z9>JnnJXdbPk_~=Du2Xm9o}i7Rd_d62L8-4qUoe!`6+fLz1c(#od0C`y9_pSKYJkM2 zJ6ITmMpE{LM);?mw)vC`7VnZ8dhyc6m?h)!DpGF-A6+JtKb!3 z)B(_18ATP7npzZrj5dKVH(8izg*Ggpd-NX$x(WWS=ZcyVV~dYqyG5(3V>yw$#{qGN z7_v?8^l5PeT=i{T>$QkJ;D>F8An?$qzQeuV&O3!O_2%=jC>d?WClt%w8Il2+K&lji z*=E;kk$K#7H#-$x4F-FL&fbB9FA9U4&)5lm`-NGY9DqQiDQP;pucq2HFwYYOks~^$ zrXxRxMQ}qC5c#w(7cNy+)CAP$goO4J=Up&Uc3RCccLPV6fRjh8@JUwm_^m3w1h4u5 zu>q8@5GlwzPu(xBj`Q73t6t4(AB|f{Gp_Lw{g^+0>z^A|D4pHfc*pD0-$$m#Ue1S~ zBHjI-pY<43OCkI-(kML3QSq+v>xJ~6>8t4tf;9{Z3@rW2|Ex#oxw5$ZPnFrp!7@TcNg5e};2$CfSyo0u4Gaw2;+>&=fyqjUe)U>E&yElSwP8pc`tLkQE_{3( zer?S{!^0Uwj)yw#ZjWDemT70&DAipOTOHm1ZR{UMGGK6U%_FF>1$D~L#b{R^H@aAe z*kj%pKJ|Z>(f#) *x zz@OI(8_0CCGPd?@qCo(u?EmMdStbW zPnEc>qqTwlZ=6-nk15;X`gJmw%qCraL3Jce?U=Muib`ucp#ts83i3a%D+sb!$ONRq zQV;P@q=md|*GJ?2zH{k^J_1UpOOLgaY|8xG-AIm1=mUZzxTvE(Z|<`j*GH|IzpYX= z-#+M9P*-#ws_zFsj;%C^0&Z?*3#m#q-&+s<-kc2(R0<&W@hv1vOOOag+DhVEsWfPHQ_ zrfWDnmz8B%4`u=D(mhu18B;hVhja?mgKz*2eR7E{F3MTTTS+%^*R|Fd>D#}wZL^Wt zN3R)aT1U5H1|B-1HK*1T^~#Hi(HC;>;6S$9ndSsol~miKl$hTfi}SeIt~qx<^KyBP ztT`_IMU%ced+u!9qJ5N9amvIwY!a){9}(e zn|uYOQ|kavy8zvv7Q#P*yT@cK!paq>3B{jHh1B0ZyZu1&(W?n|%p;%yE` zNg;N+XEj;lvGIxZmB$969s1)VO+FjH4UwHacB-Q!(KI==qP6mu^g80VAW=#ywsSV@ z?CE)dbgL160gE>e%P44q0VX`IP_3Wk%U>9sTKX6p2-vBLWANALn_v}`qO8O40H$FX zP_=cv%Uy{bp;?uR4DnOEY&XFBRGST9Rx2-#?s;c)%ZBcyu4*Oyb zRw&uuw+G$H1>0)J2{4mR%Z%Q?o3*ClIO>x9bHX39mVUby#X0XJywZ8-)jp#l5!9em zDIHAcNjT0&tA_s8y!vx(ZD*iAR7Rz@gZN4mE}|sQxRlG>H=QCi44_<~@$tt(8LM)F zz#WA#%h9$lUS!KJjTcb7`E-g5olJl&#~g>zm12_>&VMhv5NI|6Ei0E4G95K8dlUit zw_NwH_7TuyMP`G@X)2lHxPt?r%;*|s?zcJyj>~;ph)VF~HuzB@2gI#TvGvr6a5sok8ys1bITh3ZooPgCF zG_=w)UDLKw5S&677;5(NFatoH!xYX%GMF

EUT!TeI*9p&a~Ing0^M;yJ6_9<0R!Y_<{06`cp^82`%lsR8Vv{QVOYWWJq-$5PXlM^zx zl>}|UT)FC;TiCl-VRHlZQo|YBinLkgmKVDi?v(}ZctnAMr<%g2G3bkN==XioK;}8$ z>*)8^x2qh3&esQ%c@SayYN97$xyWU;-mb6^ZHDK4Ucj}T|HO}Ku%*@9`%XL>G=wjj;ue!*!-t|QbLmC2vs<!xW$l-KHx=5U<(=Q;pu0ihk}-JW9YtiRXour5F;Har|qyVB;>f zoeG$gI!mD-d=*7az}*XD&H?ml0F}`-;m=dd-> zbSX)t4JLzMhm{2enTW}KRVns4L`)`+bj97#r@v4YyNuT@G|QB%61G}d05w$@%v#Q@ z(Ht(osZ$0<_b`H}njZz}`U?0wdKDXDjJB@x`d@oYF_rDT51eV~sp#W4(sN>0UnPLW z)ABcOSS)yzw(7=J;~;Antux^Jn%gAOCv z@vs7!vC3(WDdIeT+)-JzE$RGHq=T4VstLk?24n1Kf)@#kJep%%}rEo_}ROHAdF^7~_hjfJM0R|O$EE6@s!|0fEnCs{<%QKIQEvMCQoWI_<8Y+BsFsaOnZ^vc8#(ro`mv4KZV|I#RCP+P?Ki;eX09~w4qJ<7m0R8}s^?rPp_(E%hp zREro~E>=%F`wm^f5|uNo zeOh1wTFL2l{ zZZGP$vA5_>9j32@y>`@a?b&iBR@f&rm%3-yxb*#15k+$v6ZqlDQtF|-Rq=pRCM_mC zS#XCwEuHv@O#cyPGm-=HTX!>!%Pdf_puqz>)l8G^nS-BUEl7WS)5if!G&&{C~j0}AS=I=J<@2BkIdxZ)+V$Kt{&m(oM#65t|~Dl2O;cx7ejCZ znZId1*0=X0DJ78^a$;;}HBiM;Rsca$nMbr`8# zScjUDIY~`_NyOEtDH2WnkQhZX5T^cWJgqcvFzxVsgb_JcQ(EbmhKAlw9zv zhbC6chvykYr|dZ%2AxRyqgw4f$t(V9GIrzB{?qW&MV8o|)Rdj9wpbnzO6wnx0qt9$ zt*U}>B@eYaab%+kgGoAObe~v+@0U_&nn#$HNXI0WFtQ?BmeALjd9u2*c{!k`UhZ;y z0zsj{l?gF?=D5T_A^Q`|uB^zNKeP3c%c7|#LhdHcT#7{rN>xhTg;vW+Pj|6Kl=5K^ zY*A6oBR6rm2rV%=daz#wsw}m*zP*tnHYte0fjYAEL{Y4{2+NGJkQFNumNv;?ZiD5j zt`}0yurVq9GOqhhAE8gIsWnxik@iyAX0%`-(d38x~zS-V%NZSS+H6U%C`WB0U7= z?xXJN4uUEB@ zfqhv@A#da#tN`430e+$`_An%(E_z2tUIqIU>mxJbPGw`2s|entDFH5Z7#3Ot0@^Rr z=x35y#mTtU3sXOOlybbvopF)6_(WwiG*nIaY~Qh_GkdY)dbHSE;~kqK=k%R{qK+WZ zo5iV^CE~FxEm^F>1&T&_fL2rYmq?R#OFM@~skq{dHGc#`igBNz^M)m;JKOAQ<}ZsQ z#pRUiqm_CfLfis}^-+^pMG37h@*$CVo~}5{J5(f=Z|cgimc069Y$|7vSZV zB6D(J;kT%39PEX_`UZ&=nAE5u=~}TOxx-03d4P~DaiNj=N}_$4+9#U1Ffj`x)I^B1 z#X0j+V!Q#|>v{viYvT=C!-;FB8lx6s77E*@g?6KbqFHCd&o*^A#%~AFcPZa8RWVuJ z$OMQ_@d6bFQyPcqP^F+qi_{k?fwkps?N_|@bs4_SCVr3D08FEtsbgj`Kac4rdhBkY}%&l7<4LTWUQrv7$v)B&Ng7*OE}qN3!1>2s44`5Du! zNZ4%32V-Br#hMJXDTG}h#4nnnLyQzn)Mv7cx1rtZ(~%~_r1hd=y>P6JIPOoJyv7l`HHs%WrVjv*KC{+T;6@D2y;!h~? zgF$LobYNEGsMXN2_NLhL6vcl|Dw1{avx zkwoB&3YtVF75F7Rw}3$uK0_B@izGK z=-G93zCTZ={JD982Ii^IfzL+EIfK~d^VeYt@`z%n0z3voW{EP*rr<& z$o9zT9wFR4%g*<~LPaB%(cmy~VWX9MxtNvNq~BAUX@5t(yo2+JV%V5epQm*K-+G_@ z@7fpMbjud!90LpAv_7^5-GR+Q1y5l4|IkpQ`#WYmf>nVMx0ZE1ppxjj5YM`I*M8h5 zFhJbuplc=f`S6C`wZ|d6lCfJ}4aA<}dPcE^RQ)WI8T1 zP1TORi9h{XX|I)8s&eO!7@1wJTQ8upZdHUh3o7G?ur7eRH{x#G=NNi<_S{k{w<5R^ zn;HOhbLnkIEf#)+a&6-x9dFakRD~)gF&6MntL?Q9z+5IJZeNYQ%XaL0z97^J1Yfo+ zYBDf+BWqCB$|a@s<)V6@?3Ql)0ooooZYmcv^>-((BJBye1Fh7(%gx)>y~`eD3IB;T z=hEuMW;=Tf{)4}~!u|cO9E3HO^HkIsYccZdzp{iUtG#J!`bIAr^h~H_*d2TadJMf& z*EfarCh>z({e4+8GjWpE~9|_>2P?~l_r;J-E zV}q{NdlG1x5U662(#fn$R`d4c3g|8Vt?^~M!xI@)%jkNh&EwJNh75kwxnpMDEy?&EhH5j`$7E7{Of*=ydkha4Um zSkp@c1_)UGdcnEiWA^gnKhBvrPxT)KXS4WZ=}(~~buw#?en2CE97jcuk4KKCy^mc1 z;uN(Rbbo$TK|SqB0~+EYz_ZUZC1Vf~DkLwo=e-7>2&)W-Ut5o$JtShApQrMIo=C4~ zDUQj_H{Jcdr~xL$U+}tU3t8id$C16Fb*?z}*1%2`68>eNz}t2ENrB_`n?(G>$nJO> zXs#)K*^@S-{nxu$3;TK{w;J-@BhSd;aN z31htclCv}pt{#LVGwjIPHigZ;_(9|rAb0e9&;=PLMDD5&41#xZFCAUy|Xma81aUUS*1h|eKT-;bDmifD5WYT z+N$e}r5;mmuoz(q)SKcH_=6$E@wF)+_>Ox&?^Ye)IpS?u{_|#br=MfsD`?;1C6~x? z=Vm0ZVd?UGw|I6Y<__nbxG*8$?B;w*~&ICUNQu(FfC<1=uGM~ zF?~FegNq)QZ9TTCJ1j?v^W@3HbqlBR?7v;6Z0!Glzl_ULFN93Mp>KkX`1+#jNu^08 z(YU2nD7h5$eCuU|fDf#$&@qh-D>+AJZXOGSZ-k&$x3@X9r+I`} zUdgn6m#^woK^Ky(I131#Y7sx&GtQT3{#NCNluzY}##bXJ7P$S(qA+7Ud|yb4XflRI zJjZWQnxF~?xmkS2;8NK_h`$<&rTR!+tM^3lKD1s4-74hHe&qQ^_Q<&4qLvE#hl4&j z+8$#gXTQ4PX$d`5Yh_wTaTEd4A5Q*M(4Ft>V8_@cv3v_isIHXsDnh`&$i8^1|S!e=d1*o zH$?(TKtJaJ^(8VDlj$;M=5eL4*IzJh%Ise`>A^R|WX#%6?yVD?@W~ zR0RO*QNCeCI^yFew?f^WHCOoiOJX|7~0U$qjo#5qnY5S3QdP^aWV)#6Up%}wGK zTnrV63UpMla3Axl6?%LSU{Nu2n|qtWk-@HSb3IZ%L$yghI`&_7Xzq)6PllIBUzDP3dB&O3;GFZ>nERLk4s^ z_2_+5JbJKb#oYz*4lMalj{D1%XI4~0En~(BOR^B$egk)ms~_k;?~e>U*hY}JhEI%a zg~yIznp$IHhYr2~?UJ$6snd>2iKY*-$O%vHWaeB82=rQ253re#M`72#pu$PmiP*@c z;u{DCjLfc9k3=g9ZPHkbEI-h@UL-1t@-BhA~5saJK!T;oc*`j`wyuuUjm&A|V?6Ra`QYdQ~_idmf(OrVA`S z{=tT_Iu*&<_@}$wkEMY3_b1o>A~|-%$ewnLS)?qEa*DZJnnZoqpR8|It^Hl7z0wTG z+YkuX2(*(`b~(#M9f<`O=*Sf<096oYkPAQwD6%G_p<1uZnXZPL2tv zl_GT~7_A$+_CZ37Bu12Edo>rat=M-~D>F|Lk)_GRn0v+bDOD#3c-Scke%*|-Dj}&I ze3QCWagLP3ahoY%=*SNF@uiUHC1S3VIuNVvn@MSwtyre#%>XI#GO3J3^t6T^6&|7= zslN*@4o=7?+7A+mXJP*KODe@}1$ahh`AD39UWGTpl%KH@z{|U_KUV|N0_%`z<4yRXFQ0 zd{}_c`M&7)JxqWb-1jaa=XYOXj-%it+{egl^4IA!ogi-? zwvU?Q9KW0&#Pfbv|EvT55@E*Ms`u}mGtK5wG|Iit(Z$Jsmq?vf+8d@8n2i{>FVegt z#;r;bLiA)SvNX?fXEh$Trgir|GN$xWx&tjZVPY`&!#Y-j@4U(=h})`s8wU(cF5{n; zbg_yUgpB1G##l%hYxW5I3lt;PBv*%swe~)?S2q!NECpi-JP1yXc`!LaxT*ARN! zycu2%lklej2WQ`M(eN>QMf!hea{U*Mp*wvf7uXwt7-Pmx15Vx9cLv3w?%$S zev1NJA|*}w5aD2Xdwv9f`cVah$I@IA0*=GoB-33)EzdWUTr#@W!&)$bISS>SX-o5d^Ta9B=6M>r6iSvC^8$g!y9bC2(nQax(Gn?K zhes&F-q$QKzpNpC3&}!s88=FiJ2EH~khcX#-jh$2qwX$Up1Ez|?CQ3g#87 z$5TA7#uo=I*7nfaG%SlYzz7z$53ESA`zSNaY9+xo-7+G{pxlotB-RAC@E8Z)@o+rL zYQ>tuj{{(1c0x(m{z zUs_Vyd~+`EeI`7y(ndk^`JXvxW5NzKR~V9Mk^GkC{GHiv%TxGfcVbzULptxS%gT~Z zlDZVZwEZ=Csv6c+{k1s%7=3YEk2@jv=Ml@epFP5!vYAG`)QgGDO&8{N%>rp+dsv#( zzggIHuAz&6v#`t)hG$$QW|+}X!P8)og6=lm+Mus)s9RqrEd~ayIP6}H<^&EqPc~SU zeqa2hUcDFM_j;u&! zd=si|mu8v5POJ&~Lb{-)Y-g`@ZcLJ4?JkoUCI`}}hOPELa;(K;xjuMEA#Nx^TAJYa z40en1yKAb&2d` z9jn}Tf#B@OrURyCv{tz~#4+3@lwY*17c-5##CkoN)^alN)mc#3lMC-N^m6i@hO*Og=A2`$5{D-ivVcEu8FU)tOm!NcWFm)%{Y{N;0JB)lUGK-UEf*-j%dW z*-d9om^`ebLEEZh0QcTfgmd-~bTD=ia%A5&MzM?iU5#GC9B8=?l=GzlrXk;Q8pv3O z63hr=@-SuvR-I5}SofZ$Zu^!Pfrn&FDD3Xi2UZs-Q(PvXy9_4+_jlp)w|F)CQfe3Q% z0RBRfivt0AzY<0IHK`+i%G6>_6J=pU1B1KMl;<~ZO8et;3xHLD`^hzNG>XTGkff7a3ej^!h9%z|O%EeDl{3YAF%!glV>kJR>vb9+V<{Q| zZO_UYIz>U;fsPzB8W_WEC*x;{J?(#TIwwO%u?{B#!Y*T}<#SY9sl&SuconW;t3;Ri z;8qUDL&I70N+XCL6^}z}$}1X1GgU@nxvRg$)oWu;uDIrSp6Mm2+HR%7q!05vAlbc% zGruC(qWp2Xf#O3A^RCAWe@`KPUh9D^zL{JDmnK&yi&9g@Kb-5)J_;fVI}ztQmB`as z6nv;qpp4z&d+7mu@u&w574$ktRt4mUd@%B4e%{*UN?ppV_v3IxfRfhOg!bg=;y{Moh znhNJ~k^m$SB;(Ly6wQQRUXr28d38Qz6{(@go3kGwsI%7i?Jr?{z&-P_CRFDt8zquo>fe1vp6jAVv2yjb za!*cXjozxSFI=mXe>wpMan0WGs|>$nnExn*A(m$M)lS2Kl%e}r;$_&3g9&r5zo=<(WKAMrw zvl*O>-XKAwUH>{MbR4S^Vt;cXMs*J~0sck{A2&z53#zuq@0xSsLD_;Zh9RaWneW?YJl z?l~kF2*>%n)fsZipkyRI+C!(`CN@#S=2(I z9*~E9IDm+w6oE9008f_#8y5ai3j}|MMBR;(u=An8a&*R4ev}4wJI;`RV_5XMWbH;O zz~$Uy&v=#A5sA|W%qv@u=ux>Mq_+()D#+RSK4#h?eUG|bAhST(c*W$lSxn?Y?>Mh0 z8a-hfQ<&SfK$nBvV|rZ72W$cIbs{|4LUt!1_7R_V!33=@p90SlnZT@g2Y?q#sqdPj zsCEI!qN6LTa_vZeF2MTMdF|R*QgE;=!5fj0ac%bF`fDEutX@vl3as~j-CIsOov8Y!BQZM{t^1#hML z&gXn~M1W2OJ=jguw{QFVG1KxuRd*o_q%EmoUw5XG{P)O>t5)Thz@)6f z7o=$7_-uk!x;Nm$Q+Tqr{~qB*)X|cNhxh*w8@2R}d}cy*@5n}P3=*an9oIff3s1Vq z?IPX*V0ol3k8BrQd+iv@(wt?2GaJbJl%{XxAfL8N+RD=nl%=$E)?LZm!RP)TclgVJ z5TM(a$RNCIK4X8o7!Ch1QOfBV&sASVulKk+_+?aFEn(l-yWvbNL;J&HfR9;KoR~0J z-uMLqH5R|37gyD#M)a}a@Ut?sOY~j%N?m|R?uw%nU0lo^CxYl63dunb(6?nW^pl47 zd(tK!fcu{S%lY=V_|}ck zV+hc!p3V#XvSzJ`|6S;vD#m#RC?lnC&FJm3OE|nt;i?;VP1`N(MBKe0R>e{H;}+lc zJ#X3-`e;?fiFcSLarDBWk98_~G1mupN8G88JTEb51r9y;J(qI6RQ1Kh${o*Y845Bk zAGgDxm6UiRRCM;h$MHF|^n!zg1$7~OLN}@gKav8AcVz0y!c(9AHZL{95tj*(z%C1W zeQpl_k)XQ|xaE&ccL?wcWKiW{zPW*(I7y+x2gmXXRGa1Hb-mD*sXDI8DHs9Bu#Q&85p2fHA^kfhJ7DF?oSM&VW|t~!3EiR?B|ng_C3EBn)s(*K^^q&-nlzbRn;1N z1tkGzK%b`=cc!+P>VN07NT~%5s1v0-;O?3~Jt8U;Kf!{4vxjQ1||CD()XT4i)$<@x&7Zx9#Qe*3-<* zaEm1VHld&}HXaTO{ephsK{;!C?*mfqd7Z^2XGs z+~ih*cdrlJOF=DtbYQ(;7MCG*Jx!3y z{`)wT(n z5bLkwtFUDm7z?vF#g30qUUGIsL+s_ZME;%t&dks!ed?!n#NJ-7vTclY4I2@pKEySux) zyKB(FVQ_hq-Me@9-?#U^^O^&PKJ#@=cYW2>Rn;YO$KNDhKc7kYD6ChD4R(d|Jq*Zv zwDv9&x>%+0;(_AGl`P*kakvO!YR)on&^LVuGWW3tlwq%Lm5wvbOSG*^BdbXhcwN;y z)c9Ir<|ZRqd_p?TdEDPyKxlnL~50<6e-b>`TgRgAXJH!#m&1lqdEEuM^r?JWn*)uU1`6Z-T}?=h}GhAIt5}KeVy; zOQ&$&>$J2?Y5OrQB5(FSDfn1R3{kJ7c6k}3{4ft7pe8}34W?=b-g9qu_CLk2$!=vCzutZX(7I|0`1%9a4mGyeuonCv0f!78 zT<#r0fs!%1BbrOPZxf6lG0Lyp??ij;+m5wH*Rm(Gy+#)8Baxcfaf_ji=)td!HE@zd zp9~T`gV$4xa{F4!NT4m;{u>0qc}olJekRY@$M-hSiNd9Rz&os((%#29sp$>A`~r1R zKhxMJ^*3bsg|5-7W#3a#JNU3fIv>|!5p7U7ve)@L0Y&SD=Qlu=*J?^v2r$E3qpOjj z`mNpYHM#n&m|idnWiSZH`dm{Zz)ult;^GuQR>OaBzql0vZ0c+%>v^i{dAe!3t>`!w zHfE5GUiW7un1=*zbpVme-&r-Xc$NeVU$H7#?LXN8r&-Eqy#Qqk4u52$p!0u37IZ&V zt^Y2nOdIV|tzi7A@{{-_6?K)<__aH$sA6eZzhrTXg32XVmvjrgD;UJJuVnY(*BqvK z-=!PgIE4Mb=hyrH#AHP7LS-H-OCX z%hP&SnbqYId!W^YrmB8-E3bM=Ec0sVeB3DmPJAAR>AcRMa>G4lXuayf1I(4Up#!o? z7AYwtC`rFs9{u7qQw#WXabF?R83mMUcq17Q3XS@0_4?ah1z5sBOryZigdWsMUX-}%&+41B1OttQW1r`bdklPhu{W#AJ`dNZt%Ra0 z$)L|urhq@7wHF`;x-2OB18V|@s9?SHFn0*4iJXWk&`k(YP=+tD8ZcI_V93oXw#{lh zrB^;HpzJl)_AHXUOIEiZ+5)}?r;QiDdOr1=Jj&U>Qgfa!3O6)ejD!Fo+X{&A7R@Ep z>pnLPjYN+G_!$)wF*Zo1C`(bMkzyItr;#G7P=mh^HRw(@bkM+XgI!a*t&K>zej11D zCg5iDw;$T!tN!&;cLlTmULqdPTliTle$Q7PLIa1>`4m7Yh|&JFJkR1__?_MUbwVQ< zwkwPCQGoLr5#aUliZc+1h%7Y$A(EA+NI>`Si+}vP<0|JW%6j6h(gSf}N^$)f)o#)3 z{9Z_l8ywGW$rn}H5i{B9pnGNCFJf1gU%?OH(&dfnvZBT|JMZJ@yEd#4q4M-#Ev_NzvsZDM})vaJu!1F zM_MrCrif3yOgAm*-!2NGzNG|+48JZsxpW4Nf6@MkF8+{A5`OJdrXgh}Hfuoa4h6TY zQn34mLdR;>aT^~@IWH#c78}#j#RPOGMwPfrHm;U2(_FUc;TN2gTOs zUBI|i${KfIpxjU^R)B7x0+eANtv8>zv?h8AECj^NM?h=qOj7T@p*4I>cTZr0*D9kr zo6WCA`I)0lep)V8q*dian$BK_Yu@4y^Ye=)vzkVAxqNk6lQ5~%7=+K)Pi>LMZ<$lxoWJ$j%A?r7&>FvliFFXFkQVl=}m!3Rp?$OXvjayk^^aKQ68ZSzf zpwUi=0YN;*@R$Wo>}DLF7~>sI)F)_hHpQ)`R65kM%|%sC+8%tf&`jpmI#dm{;OfYp z#p!ei-jm{HAd(~Z#6{z>JjXl^{*`f^Jq@88fAcNl+`9IJa_Z^V#H*?<$cshC7?c}~4cv#5d%V$Byw23;W=m!mW&zij`mf7OB6*=aV-lWZne0JQqhNgX=;RcVE zIm&lD*GES2{QC|5^UcL$!uScij{;Kpdjv?#%6LGv-)u?K2g$~FX7aArAa4`vEbXs2 zXoSI4iboPXPenYBc->F2Q=OP8@MxLxLz{f73m^jlGeRxMC+46H;@vk0C_4BA+Ol;? z8eQIy0LJ&er{A}@A*Dy$chH8k-gTl%{!P5xFVVvgT%y_k%wwyTvMUq_q=0p3-Mt`RGhJSo zd=V|z*E8}tFMkG!`JMj2eb(|Wjku>kl*KI;e{4%%EWphU+ngZ3!sjyRb5?JHa(&HT zDbJxEDxjl@_JVs685;nTdEO%L+xPTlZ}iF>DHdiuI!Z%wq#H)!wCFeZw2@TPxmo>o z4KgZlOjY|j4?aBqlfF6v85GmW#k`giSjZ(Vmkxd#Ee4nl7ADBBf`U)4V$ zHu(b={DGji`^O?K_!GFGQ~~miVh6eMd|F&u>Uk>E*aDuUbw8ywyiY~Wbyw&Vu7e+pJi$k%=no8)3Y)zA$7Mq$CTfQ0lq!fJc zDVOP52X2{oRmjG@fzR})TVWp+s8*dD-YgnqQ1lT2?@kQ@jVI=@o&Hv@6G7%1S_iYl zg^6XV0EsT$iVL7>v3-sfNCRWyI^mmRS+Y&b_rfoaR%D1A=QQYr3|mgN^4Ujm7z5F3 zR>~!x;p_A}clp-D(YRg+{@XQ$>^Ip4-*V~#R*mbmY5_IH?E%36AQk~P^9$gyRBYq> z$LP7##FkFC)gmP1Ewu{!SCxjhbyv~TpI!PDT`8AzR%MGt(mqJx)~bN6aG+1`(;mov zMyMj-*wruluK{+O0TU=2Lis-4k zzTOoO`CBFk$KYH?A#`hezvoOx4uj@bl;S_?@MvV89WPm9;AdwUGa=dJ6eDi600~4e z4o^(HP~td22F^YUP~Z)AW6dy(4Z9U`C2uIPfX?x! zZ9Z8lV)2!7yW3gqz~gw~@BRqgHXxj0cm%GJOpP62sw7p5n<5iDr0M#i|%RGTo zx`=_;wq};`#L8+Cd#>7L;i}#%&0^Km91N`OndAz{J%o?1!I=H0*aY^M4*rnXA2g#8 zePOY@ShzBJA%w}09@AU|d)>bdVX4f2n_u%;pq$QenO%mikotVCwvyh0^-c}%r>0wR zg|aV1fLAoMos(hpO5d|5^`a{YJ67HWhmF}%PhTU3csOpD85$frS$D5i4noW+yN(5LT+J5~F(pTPB^uX^kN&O?4VXApY@#U#4^*7j7< z(#s@IE^NXFwaW4*r(XRu|k0BC7C=wJzQHpN-W8M=nT%2#jnP<(-JD89HwI*#h z;=`-Pp)p9u{@wn0A!q%N_BcMC!cQ_2dR&Kl3%A*e)~6CtRi*|zfxq@<^||=sJ$jP& zCG02so)iyue^+!FJb?`!eAAtCaBt}J3^z0N+>LUGI-;si;2)v@5@2tz7rhHD2xlO7xZeKB3WH6 zlfkyA8LrP$f|ify0rtm0RjE~eg@S9auJm-F#pFPvN_=k}_PSu?Hs6x?al`6P?o8h> zApPB9)uZHuh`8VBqS7~_#i>4J=Kj@mxviLvZX~+n=)7+`7H%%Qb*tX__qPzpxCF+2 zqepT^T3XJ!H3Y;uw$Y-=^8S!dD|DMQTy7fM+VkjG~J` z$c47Ns9F_SL(1f&$I@sH^q140XrA-v_}J-1&D5Q>JIbG}UM;7yktI8+>Tq!YRWHFP zjBM(T>wD|2y-(O|DxcP}pT2>=I!#bl7lkx)ajf$|^%qjCPct`-%|Z<|vE)9jFQpG2 z)Q9UfXgQ{6^cj(}7i7=71w9C(d4>;}p>u|z+Q-?=cSl8p{>CZu@^7iNDX*=!np~j~ zv$0a=enH>J?j7fT!M;3P$jOUgpn-Snyi(FrT%jgMh?}>X0XFqox>V2N`t5ug=#9pW zGi}J@c8x**7C3M*@Z^*xpeO`K`TSv#QUw|285-#>>D8&{R?bT&V7brah`;r>TcJb8 z+BZQ5fo^OF+ig%-IT7C*B!!8He%1hYFDN|#n3TA@Sfz+T!2g`X2m|z#oVbcG zy_EbH#{W)c1WL$L5ie}j$Alt&&mBC|s39$bCEh=oJB^kPqgWA38uLX27wYhCfI?nJ z`g6#s8QbowAdy)UQG1zuOfBMawR)#1h5=UnK&RnWXw_5T+1kV;Z9O#0NJ}yF1(W_- z$gd!lVw*a#ePWptld$hRE(4HpFVFh&(o1%R+Znpk4Bbr5%8ceQAE6pZ@GeO{hz6Mq z#X7NI8}r7%_vX*rm9D`J@)UzpXV^o_I#x!7MKi)@*xt_NPv%$?e`?ze5b0I+J$2H zipOa-dG|EOT{wm*=6C~-Q^aGEpvY$$r$150xU}&PMgsJ;T+f4t~=9iroTzqx%GsYrilM_0+1tuw*;m>$n~P zh%o(1URPCid#=z%*}0*Twn+I6e+Ua$6rI0sHKl$N@&0%_cQ_!|DrHtyULI!?E5P62 z{azxmTh_ju;B_=0esdM|Eye!M_oivWGtpPB?j*KV2ffTTxHBr`=`kWk@TUO1WtL!@ zRB0MNOB90u`GVYQmV)5f5gt&)?@Smc>s2rFFj|n3$b!mk_KG3ZPtY;sZMMmYzire! z!n;ncbiw=eN#X+O?L@bxbawYjwMu;@={1~E(8qg5+{rzL{9H#e)tpunUuT3wlaa9N z<%f%xcDZ%#{w|4bQQXya0P9@StpyN3$u3ILD$os$K|L-poxpKV#bH!~LfqEJ`5&f*`LUBb6bWM?#O zzMa#iI}BGt8~Zor5w@-d8E@jTb~m}6onu}6FY~01YrGTAmPXh63pT%0Eo1HPZC@Rj*dKW8N5o!6~x18i&M8tomeRn1E0IsFgOHYTApWT=*J)*Yl3m;5%?mViSHKloI zb&tlVjHJ;!H%KqZoDv+?$vr+njTNO;d40Ra(Yc)L+A<70_(07_`0nt_eBqQvGr!KX zRU>K3Z;9^oYRY_~YoCW<%1>)zE*EoV<&cbaYHGAzby@@AP!f@AZD=FxqSB zE)_*{-AA(^%~$RI;&_QnrZV0Ls{HatbCasxsn-RvpMqVPcf3m3K>1syL~!x@b3l>! zB$3~#;VY0MgZ>(LM!~zq|M(JJXB%rjm#bBKq) zCi6q-Lj)gTWo@dzIe@#Ki+O$*A5*+$b#*;w@qlIMM)%hM#`C6C>{f@CX6zQfzS>Rf z%br|oYiCKm$v5nZ+M7PwPWm~`&I+|O6MnBZ7uEGb8o=gFZ?smE1BrWfu)0)Rx4Yju zndvXgI$NiV$yCZW{tjuor3Ko`Ovm~3#4*(tUCMi8fX4&J4>!<$wTWk(8@q93E<1n= zPdi_`I`-^%Hc3OjKG%HT+YZEgXq_}O_0=AJ9$YwCJ0FX1Nu!9yS{u75 zGtn)aupW&l;PWTI^jteBA73ilU&%^;@@p&V8r9b#0~|avPH~p)U$>lXQiwb0lC7nw zx1CwaeTBYW_wg)zJ07k=mmuh@B{?WX6+yny=%vnEm3cLy- z9Ndbi2YQ+?j-K~t?+GYcIl^?tsDhkLnTtzdiU8tQ$xzLXau40Shd zc_QuLJ2cYH=;{(Bzq0e=h~8dn^1XAsIrn-x+Bj2iaR*q+1jfhR)pZ>-EqMMah&}|= zMgQJ1UyzI4(%WLQxlrqjE^giG%q`KM%*5L-BLMK7F1yC*Zc!{9?|ZCv*NXe5sSdn? zSYB2Zf4#Osjnv{{w1m4yJY50S9{bo*R!SF_SBnHwez*CE{H9vYLvDU+l=oIltp-_6U*smN{L3 z2Pa!8NT9r^8&s23b}95_#Ial3`PINJF5&TEB*4x6OxJQKA^6DcCuyvB?Sqr< zaDRP<`=tV^z9%1!=GP574@fDRpOrzfmDs9ZH!973KLf(x`)RX_NFwdj3n6=(xgP2^ z7#ITA{6=|yVqeMEEhUzKLb}R3mU@fJ{aQaeMz8K(1)#OkhQ)ri3|*4Dax!rI8TJ)f zv!Y|PfmBtHbOTlR2v4nyWMuSUDd8J7Dq*LOuDUv-PycHt1M8J8%ur^y!|>(iL$A`L zOa?S;LF`YnD7S`)`|P;c@ddv2d@7q}v*eeJyl*-f^Mh%gl2AlQKE^7FtemH;m_zND zncfyNc*h*mJFi*OV>rjD&M#vrzBHMfvp(Yqh&Lx;xbHreZsMm`+W`Korv%wDj;4KM z;>Q@_FA8bTH@=m;Tc4g|6HxCDef$B$RUU+{!b(IlLeZ^uh5JT0Is-Bama+5u#GyKy zj94BuO(SD{FgM;F@AI@4+W8~3?NW0m&ljngpK6ts&sr;&(tlZ!YfGK3%JKOeF3@OC zE{^c&CPjxDi<0u1p&tX!c&N>eIahQP8>y`FTD2>ZBJwp770%dFkpb@lC>#M#bXddg z$bwioHWgR9Eum&K^!cu=X`!7sKezFey0WDP%3SfE1Zti;3pwW@ExE0yMO)kXu(}zY z4wJLipM!Y|PHuPsWVJc_Bn^(vNk}ens->x?X0KWp;`^DOuVLTkOzCE77eE$(#&ZLl3cds{IH;3r+ zyCV039QeazpCAFl?{4!#(C3t-;{N`Swl0@J;hw&GSw_0R>!m?>m3Df|_u+x{hma}% z8OkSq2P>U+qvGKUm9uP~EyB(;h}hy946r1!C@u9yD4JUzkD{PAD-Nh8sMFB#AI ze4dlbW>+^wTap~izHE|2m(45>J9~$*rb2~)YJ@j;Nu2Id)JEw`E-8M|@20M56&%OH zArcMmRABJP{JBrIBmtdg9qwO(FAWW@uP%swR5W6z4ZOQb;oyJNM|eb%5W(u}5M{A2 z+#(*}4brz3^CZjM*vMbee6p?S{IwT6i8-?5{+Vfo`|*S#R6i<8;5*^Km0#Cp<=pjq zt5?{Q#+brmZdCJaEn(G-=jd;mS7&6}A3Rn0i%Wjg?+wpJV(v9BPdGhOw}2xBs!ELT z1@yciBir!vRM4LVbX#_)kZt?DQ+}b#F0%+eT6I(Y+B(UxHCI=+rc%4f>k|t4NfYx+ zAm}bx*IOzg4lEX)Enw|+!29Vev~Gy$)KJeLVdLdhC{TN8)z>GF*CcKP%a) z@p*+cFr^zIkqjSK=UXv7FwDlXTVy;&N`!`W*U+6xii-;24RNH611N8pQa6s+uhX{I zYbapmX(e5oh8Vv0Vdm2Zi6uqluOs06VLIYWmTYl(eGY`-JA5<y4(BNPR#WmIf)p)K z6V|R%a#R}H?^vXB*^#!`0S|g@9RB{iEje4jEQ#SrP<=zonBB^^M zk;!v?$Pft=G9gHL5sHgRp^3EECFi+ezUO-i*(q_ThOH&;5fZM$wwR{2=Q1ifGmnds z3ym%lYQ5e*fDzCxX&ymBZGYq)oqQlnpc(bxG0x=LMQ;_T&n{%Qx2Nv!;Xt0_*!X2< z9fvzJAmmw!PUtbpMQ;|F)vg;LRj+e6tb#X^4bc*$xk0j(jem zFL+m{js_krl^kmKQ0Uz&VGc~)qCey@Xdc3Mg>aT2OP794%TkH*zKFs_pPgtVz+czPKWmI5Y| zPENjX#qD_^(}Qz_Tue=={YWug84*x_M$$^JvX;}0i<7HeSI9P5Of%dQxW7F!0uJ?1 z%Fb^lyyl_D;AGTPj%UnsI4DMQXiPDEVF#uv=9h+Qq>1XES&tu<)c9N#9DnEEGtb>oS`v%$_C-q&$&SpoL_>Ii4-WFX^5TeZJYFRODQ zgf!2R#gXx$$Pt>j6baMWvZN4qL&nX?=bu-B^ARKz)on7OtB~?4JcmljNB7`W7;2aj zs7E&?)G&G(eI)4WUm86+K^wt5rEXgR@ukJZ(b3`h$5P*R{9T*i-E&X11WW;E?6Uwa zj=kj1h{z@pxL;uo-=D^;M&oZNuVJUm!>L$Phj}7gp$fny_-EPor^8l6mCHK}+oq3w zJhef@h09`&S*&v@E~Uryo7Z4Jrj!;+fVjs+LEw@N8=%5>9X!bFoy(c85<@8x0ZJVN z2;f7l!Iputk_^?=3z}SxJdKnaTNg{Q=CsY6;+yW$kB{3p*!~zPhBYe5RZNEal|?E$ zAo-SRRH9gNS&0=4L-4cbl7XHVvgR2k1(Jb`$A_gV&U_R0?&3i6Z525|v7w5kgg%C- zyv3}0!)FBtcZW$M2So!pX}2FDuUV)w&=}wnUbbxcDsiwg>pxk$*5E6XE)NokKzycnOx=ezmVu)-`sZE$+4iR%;9h*KOnTq< zzk7l!!C8d$R4O96YEB!sunvCt!xli}*GmF2Y4rraGgnkQ-)bi#ToTPKH4C&)_$a2w z&Vbv$Hr8D zq~*!s%`7v<6%Lz$MF35+*#u;I;Mf<65Kgg~$6$X8h$5Y5mh zM3s+IrpYFk6d}nc!yfAY{IR03EGv(}ld*()1dRJ+^tNP|k=dD9QcoF|GPE*T=fgK^ zf&De(r2$K(*CF^6n8xmy1QRUpTVKIr!V&cWZw`GjQ(%xdmiX7rX+uSabF|pkeuSlJ z<%lD`G9;@K0ufO;H=yz|;7D^uG*3jg&l{J^jol%HYg`y6o6F=FLJh0lt+bbZc>%Aw ziGHHm1-y(`&3$~ZeT7eRJnmW`4dc&={JZP;vJwUf=U0%Jl4&(#^Qy;^8ufgu7ru_T zZpg@}srPmZ8WQ9hhqOqo1!i)xNTSP0c8^9;w83eeP7KT-cfZ?@HKS_!;XNFFAq zvzUPjNN5sgDM?HoiM`Kmr4@fjAK&>bamd_&LPJgpGhM`3Sqz7@(tz;DAts^lM-LyD z`$l&QV6EPPt3n@%uAs0q57U6W>CM@z%}6ZNKSt{l()l=%pxaq4*hGPhA(7z0hsAy= z5f*AiC^v-GS_E1sj5(l}+NNEK;kL~+!nsl|ifZn3dmIB)T8MNHrvjXr;Z&`sY+(A< zyD(QRmP;<$fPW3srHd1h(!SdSt=AlwE?zJZcX)1#M{qX3jx(EH>H-1(bU5@9Q5k&e zQE!lQG0c}rTTB)U_86M#lc8q?qAB0U$E2)p-|l2$?PnWE@_i)W-nelY+z8Uy_=H;B zsYOhwbvtb?MAHGTX(c{KH_w7`01`P)OEqp6PTcCAknEExa5ulx9AF+{6YhB*fxh>C zA|tdvcv7&1a{M%(SBDYSa*`NVr%C_8<_^mYiI34YJu7pfvO&XFCo_jfbk-W!y@~ zG}kMk4khE}6Ota;(2Na}Jh~{FL!WJ}r5w^K&fsw#^SH~T-5*|xaIkvD5+c=XfRqC1 z=HiW=qd9|Ws8%l?$}ZCwR^cCnCUrkgdRZp?kX9@nt~6us;1WW{#@0PYEfrWwQ4m^S znaztaoaSvn;?0gU!f*FV z+yvu&Wuf{>!$*lLHcWs#kqcsPWWpG1Z18Ce54rh)g%I^uATfMvnk?Y_a2@vY_7(|a z%P}R?{~{!TZi9gRGvQ3mr;oQT71SkPiKdb8%R@2o!A^(-!hMaup&_Zfv-E+&iv5t0!DcoAn)bpK0Y^+-%qZ7mQLh=u&3_@j2Lo7jY3_VXNRS**kn z-%hGitKmn?Z2F;qV-9B2BOe_q{UOBB=st8}l5$cZQDx>8IB&L@<)X3UY4)@pL&8?2 z4nnO~t2m1gMq(i}8i<=X^egggN-Yb$%$IJaMqB0ji;w%AFYhTPW8$5%N#=g9FEl#Sa+~q%P#bNfrGsOoC6T?F*Q9?Mh;N?vYhs-yx zSpzB$A1afMNe$dXj)vK;)gvMjWM`L?AfsEB_k}*;CVig;a_t?Z^hEQq%BDzhWavmf zEZm@UaB}7=UlOHnTO;AKJ(d%*qtB*6$V-*&=pv+jZHVbFAF1|{w?Xu-a+tf(fW6a> zO%UyqtCs2%T_nrO+ua$Row=>e4LKG%=IS_#B3Z{@b0^4V^@P|*<%i~u0v2OqufYS_ z=(-!F{`(pM-NLU`n34yHQ%0NS7Yf%xuiFY+>^orbz30~eWBqqP%&9;LP zr(1NJEal=OsK+SITZgT8wKNl70#ae%wRHqS(<1_>p;X|4e3pT7_+)l4m8QGdz3k}x zVBR;M5;0C;Q`>kVZ$Db|*i$a!g&%eERFHiQZJ`ozIOcKu>BqN5Q-V90 z2P22vaWoD|4WX*c{B6wvG3t;y5WUYu0(Cp8iWm2`0#_e)j+iu%v(r-=pbAw6XQrcFJXuLtNsnf!u|V-7 zlY*LWT!HJkV3_k*3w5%SG~}V(*2V&0?K-(dFzT>9b|=u^qL&n6lKEmBn?OxzLj;Y) zdSRI80f5jMmpPFi;GOgt?BU>ybE<`DfIsv=GxM-sPx<^MdgR;Xc<4-qGz8EGuD7z) zyXk$=LX)q%p99M-9*Sfb{lQ&Kb$=D52=Ce(C&N8;W(rGm!4QoSOYTe@C zqaO`0l;o`N=>o}jzR`UkSBj65g4lQ}_4QK*r^zT&&9)Py$;t|qi#y8UFJ}N_zlAyx zvzDX;5dI*=G_o$HF8a>4+EZ+RYUXY&UE6Q3tIg7kiu<908pfSB@0%_H9wQ4rM^RE3uVY_V(L5bRVhdvHiKNVXOP^IguY>|6A~z58f-Ih7Av%Jxf*c*O@C~RxR;4TK#&8VdCG^mUPqedPgKfFL9<% z$4ZYCqT^_oZufzf=OL*aqsbiZ6v^#KdK{WIux=L~*#vI>s1e->Vwfu~LZEMuw?2pr zvT&K{{S3`&MMkVdK)-yxu6pWbr>m66+c!SDhN>EGw)%G+>g9&v?dnLx5x?C_TBKAF zKbgK@8De3VXe@)-Y~;VxEP0GW9mf+lbdufxM-mdaL4R^Ge)O1P$xH`X`+gmi6)EY` zaEw~;hH88bu*I+%gH~mh4}AAgPA41RZM*J1%yskJO12;oBtfhOb5oQR-poJ`3+SSW z>%tUr9eq%f@PM#ho1GtB{*pBd$R?+bauN=QZZ%FsFLvosJd)<(?G;(_&nY9F&Ot<^ z#xW4Sf?J4?KqifL!hcxaWBqW`?TK*^3yv9;sx5y@A_6TBpAiaa2=m&v@zTzB;&)F^AUFm%xl6FnL%D+Q4(G+S$XFD2mk4$9iq;jSu_=+37L>2Ff13Cd!ZM-^=;wosi97A~;3% zcYmI1pstS~tq34#MjE0@Nt#IyCPKJtgf%Xi5NGf@p6 zALI7>X9$MzaW5;)@MBhlQZ5)WoG>~bzmOYmy%5w3wu^GPe}$xu6!4L?-b!giJ1ale z*kE41uyP$biCS^sN~4Uh<{_eo4lB{R@}K*vYF^-m{>Ut6rPV~DKI2}xvRy$7pWsG< zyR2OP^`b92Xfs6|nLeDoMjsAU^LG2{*eJ@Fl86^!K`)x&fU6TlWPSlVm9s%x7-Nud zKSu(E@RtamDYdL7)_7nuRL0bjuuLp|sdPSy%S)+;?^^h}HtH{t>6kjONSGRf?HpuW zSr)9wK<8xaBD}sJ!n}1PfSta0TAgERD#w3Rf=THq!L*9<+0$c+VQFP|2#Lh}!N z^`KZ!2M6|r<&*e``8@egNtHB7qhrONp>Cxmmun5Yt9FhSzIaNE7kf(IRy*gbY(>}mcEt=+ixzPe!hIe(Cy#zbnYzXq) zkUOyC7(4bJHDG5`rDq%R6uF(o`F`g+YlZPEjzY-(d)_Ich3=|KEk%ed`^;}D;iPS5 zqMIt2-VwKsZMs3dpg-#Q_l;+YGo{AA$@_K&R9oz%hKpdsAR9JvYyXGp)QsUl>-Gr<42YcX>3470X%3gn7=|0@eh4UdmwjkSNLc1d|+1HWnEbk$skNYC!Gx z%CNCkQu@y|<8p!AtT|-5e0X)X0amhc;xWjfvOz{U!z7ZdD8H8{hruSSkYMXl*}J2+ z2~wb3(1t_MdR>sL{_qOX1KGZ4{n2_7(P#nevs^ef{}Sm9WDWk(hIMS)axLXlw{+Lg zK-80lh!7$%R=2JA&qfBE;i+-uL728ipTlmKFtQT>6|>cYMkygMdG8cY zikrsbSz!`BIHQ}+Y)~DaUguk>PD2h7Z0wKB5JH2FacYT%P&C6=Z2IVkk7@e|D{@9W z7E>TLH5bE8Dr~~NK%vTE)5&X6tmS}58;X}pAaskBTllB1-8dISYW73Q?^ zTV|fjULfN{p}?xGeM%af^B{P$6UWq;xIFYO-}t$w%4eio<)h6J^Vzh6`Q){vW?Wun}njT^~3HRkuF{Ne(^ux~)S_G9MH^x2YG(M4w6jrv)x zRSvC|gM{`4cr2hUFD1Y3rGBcvlWmB%K$dj6{SpbXgy7F76k=@jK}Y#>PsL3iK%Tgm z{g-KzBB4GWswnDnPrJJW_l3_Y%4{Mzk;9jO40pcXLEb!GQm7jyI>wLm0rSVj|3$WJ zAEeeIP;Yh~RCE*ME3onc8rjmEH8yizIHO z=CY|>=ftb`!>syHbr6LK=J7Kc?Iaqcf-U&i&q=c!SvKW%zmk|>iuq7aiSo$ zcU3r~h3?Q7TSB0N=ClE;q*S=-bRuSRA(~x)wodm84>{5uK=COXV50N-F1}rmE^e}f zUt8=^c1}e;5LB!c+II**pk`n3F_;xX`{jl1jAoWV0Q#YVWFCp?Q5`n(5qoD%!ySKQ3z-Sxxs|s7qm#gLC^^s7=1$2&`v^OaX82# z%a0QY%6$zx5)Xy&W$ ziIN@nM;ovblel|h|owg<=Qfn=ELRr+yhVPc(+^VUIlzM$0W7-bGfLm8g{R1Cz zyiYNhEMGH#h#5KX>5sy}l;JY+Mc%>1+Nl>1GKr0*t2N&@E01Q}dE=}@Ec%@aChcZV z6VpOZVwt;YkFo33;m$af-i|}+s$eTJ>gr~@tsRo9iQ?o1>CNkxZkEq@9m~Y1_A^o# zz{5U{CBsM4bgAy~3<%_x8M!`VF3(;iUO(+mHD)>AnyD^Ur8iWhoTjptlY%kJro&EzSww+twbTwDE{#o4n{TEMa-%; z`njC9AEW778_X*12m&xI{4fen`1z@0Hnu4_jpLbtAY;Y>{tLVAy9S+kq@eZD{!=q_H!mHTucFqFSB~l)e}3Y+{{A23*pBJ zuEf=!*nAYRWm8i9oJU8Gx9NE)A%9a_Mfbn{>=OTTEt_3)7|qJG^T$B^m}g~d|3)m~ zabFvneiy291YPWEFZpBh*N{>5oyym*1TJ<#U)%{Tew4m&r?*Z1a$edIuSW4Ajf**L z#$z!S-EY3xLDC;Z?DXV1w=i}%AaK9M;=#h_R9M*bBsn{hn&LryLU0{k%s08Gc7Px* z!V@}bz5KBj^J%0v7$&)O6iv2m^_zd8ayV&OJ@2b%_Qy&?*~D)be=jr$ej-WdVb z+LiZF&TBm0Ea9n7n_hjHb-z({UwuBln`7@!O|VQTc1z@YVvLm*2RtM77G%e@T|V|m ze-Hg2rxt~!0>m>LwQmIs@YS3&A43;7&X`7Sx=uS)SQ^s{wi?B?63h5#_v4Yh6V^!N z68Gg&)fD{F567O1{OE56&L}2IS4gHx*~&WK{rDTzkPG(818b z{!v6O*oHft0p!&C=l4%h)4w)bOIuSH4+qnKAN8+K;s0v~Oa;^vwYM{~GsU!Si0C6IynEYz;OQpZ0tV(bFsI# zaWJ$qwfSG+{Hd(>&jtzdkpB1Onc3JIx|sg&OZ)3=xc>tbXBR^kS7#%`{~gX>XXE%E z;QU$D{|m}rUs=(Afa2g}Z|-F3{QsQKU)QzspCH*gxH{OH+PVIJU>OJE|Hkqk5dXTa ze^fR8*Luf)N*w;PDS)6jyLi}`{;iA5%~~0aw7E-v0rd CWbXt3 literal 0 HcmV?d00001 diff --git a/scripts/bench-taco.sh b/scripts/bench-taco.sh index b26b8d8..1a73af8 100755 --- a/scripts/bench-taco.sh +++ b/scripts/bench-taco.sh @@ -205,6 +205,15 @@ write_taco_bench_res () { # Arguments: # 1. Benchmark file parse_and_write_n_rules_locations () { + + # If LOG_TO_STDOUT then we cannot pares the number of locations and rules + # because we cannot read back log file. This check prevents error messages. + if [ "${LOG_TO_STDOUT}" = true ]; then + printf "Skipping parsing number of locations and rules as logs are sent to stdout\n" + return 0 + fi + + local n_rules local n_locations @@ -636,7 +645,7 @@ should roughly match the table reported in the paper. FAIL_ON_ERROR=true # if the default timeout has not been overwritten - if [ $TIMEOUT = "1h" ]; then + if [ $TIMEOUT = "20m" ]; then TIMEOUT='30s' fi @@ -652,7 +661,7 @@ should roughly match the table reported in the paper. run_small_benchmarks acs true fi - printf "\nFinished executing smoke tests" + printf "\nFinished executing smoke tests\n\n" } @@ -725,7 +734,7 @@ This scripts supports the following options: checkers (default: all) that should terminate within 5min -e | --extended : Benchmark the full extended set of benchmarks (this can take a lot of time!) - -t | --timeout : Override the per benchmark timeout (default: '1h') + -t | --timeout : Override the per benchmark timeout (default: '20m') -r | --reset-only : Only execute reset benchmarks --mem-limit | -m : Memory limit for the execution in MB (sets `ulimit -SHv`, default: unlimited) @@ -796,6 +805,27 @@ if [ "${ACS}" = false ] && [ "${ZCS}" = false ] && [ "${SMT}" = false ]; then SMT=true fi +# Test whether permissions are correct on OUTDIR (need write + create of files) +if [ -d "${OUTDIR}" ]; then + # Verify we can create files in OUTDIR + OUTDIR_TEST_FILE="${OUTDIR}/.taco-write-test.tmp" + touch "${OUTDIR_TEST_FILE}" + if [ ! -f "${OUTDIR_TEST_FILE}" ]; then + printf "Directory '${OUTDIR}' exists but is not writable / cannot create +files in it. This error might be resolvable by adding :z after the volume mount +description. Check the README for details. + +If you chose to continue anyway, results will stay in the current working +directory. Sleeping 10s to give you time to abort.\n\n\n +" 1>&2 + OUTDIR="" + sleep 10 + else + rm -f "${OUTDIR_TEST_FILE}" + fi +fi + + # Run the smoke tests and exit if [ $SMOKE_TEST_ONLY = true ]; then smoke_tests @@ -852,11 +882,11 @@ storage\n" fi printf "Copying the benchmark execution log '${LOGFILE}' to local storage\n" - cp "${LOGFILE}" "${OUTDIR}" + cp --backup=t "${LOGFILE}" "${OUTDIR}" if [ -f "${CSV_FILE_NAME}" ]; then printf "Copying the benchmark result table '${CSV_FILE_NAME}' to local \ storage\n" - cp "${CSV_FILE_NAME}" "${OUTDIR}" + cp --backup=t "${CSV_FILE_NAME}" "${OUTDIR}" fi else printf "No output directory specified, or directory does not exist.\n" From 41370493f49bd33129ef78aa76ee05ae648d2e43 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Tue, 21 Apr 2026 10:33:17 +0200 Subject: [PATCH 2/3] fit artifact README to CAV guidelines, add ByMC smoke tests --- CHANGELOG.md | 1 + artifact-evaluation/artifact-evaluation.md | 286 ++++++++++++--------- artifact-evaluation/bench-bymc.sh | 43 +++- scripts/bench-taco.sh | 2 +- 4 files changed, 208 insertions(+), 124 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 99063ca..1f714c1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,6 +22,7 @@ - Elaborate on the function of the different preprocessors (#6) - upgrade CI pipeline & Dockerfile to Rust 1.95 (#8) - improved artifact evaluation README (#9) +- artifact README in CAV format (#9) ## [v0.1.0] diff --git a/artifact-evaluation/artifact-evaluation.md b/artifact-evaluation/artifact-evaluation.md index 106906b..1dd9c1a 100644 --- a/artifact-evaluation/artifact-evaluation.md +++ b/artifact-evaluation/artifact-evaluation.md @@ -1,72 +1,76 @@ -# TACO Artifact +# CAV 2026 Artifact -Welcome to the TACO model checker artifact README. +**Paper title:** TACO: A Toolsuite for the Verification of Threshold Automata -This document will provide you with instructions on how to reproduce the -benchmark results and instructions on how to access the TACO documentation. +**Claimed badges:** Available + Functional + Reusable -The TACO documentation contains more information on how to model and verify -systems and protocols using TACO and on TACO's configuration options. -Additionally, the developer documentation contains details on the internals of -TACO. See [Section `Documentation`](#documentation) for how to access the -documentation. - -## Artifact Details +**Justification for the badges:** -**Paper Title**: TACO: A Toolsuite for the Verification of Threshold Automata +- _Available:_ [https://doi.org/10.5281/zenodo.19659446](https://doi.org/10.5281/zenodo.19659446) -**DOI artifact**: [https://doi.org/10.5281/zenodo.19659446](https://doi.org/10.5281/zenodo.19659446) +- _Functional:_ + The artifact enables full replication of the results presented in the paper. + It contains a container image for TACO, its documentation and + source code, as well as a container image for [ByMC], a tool the paper + compares against. Additionally, it contains the benchmarking scripts that were + used to obtain the results presented in the paper. -**CPU Architecture (for Evaluation)**: x86_64 (amd64) + More specifically, it enables reproduction of Table 1 in Section 5 + Experimental Evaluation, and Table 2 from Appendix C.4 Extended Evaluation + Results, as well as the errors reported in Appendix C.2. -### System Requirements +- _Reusable:_ + TACO is Apache-2.0 licensed, with the code being publicly + available on [GitHub](https://github.com/pleich/TACO) and published on + [`crates.io`](https://crates.io/crates/taco-cli). + Additionally, TACO is extensively documented in its source code and in its user + documentation hosted on its tool webpage [taco-mc.dev](https://taco-mc.dev). -We provide both our tool and the tool we compare against ([ByMC]) in the form of a -Docker/container image. + Potential users of TACO can easily install TACO using `cargo` (package manager + for Rust) by following the installation guide on the TACO webpage. + Alternatively, users can also utilize the container images provided on GitHub. -> **TLDR** -> -> Minimal requirements: amd64 (x86) based system, with at least 32GB of memory; -> Docker (or alternative container runtime installed) -> -> Extended evaluation: multiple machines recommended + The TACO documentation describes how to use and configure TACO and it + provides details on TACO's architecture and implementation. -TACO does not have any special system requirements. However, we did not attempt -to build the tool we compare against [ByMC] for an architecture other than x86, -as the tool is no longer maintained. + All of TACO's modules, i.e., Rust crates, are available on `crates.io` enabling + third parties to easily integrate them as part of their own projects. + Together with the extensive documentation and the publicly available code, + TACO's modularity enables third parties to easily build on TACO or to reuse + individual components. -The evaluation as presented in the main section of the paper took, in sum, 14h -(including around 2.5h for a run of ByMC). + Additionally, source code, container images, benchmarking scripts, and + documentation are permanently available on Zenodo by this artifact. -However, you can decrease the runtime and resource consumption drastically. By -reducing the timeout per benchmark, e.g., reducing per benchmark to <= 10min, -you can limit the overall time and resource consumption such that a considerable -subset of benchmarks should be solvable by TACO on a decently powerful laptop -within 8h. -We will explain how to configure the timeout in the relevant sections. +**Requirements:** -Please be aware that the extended evaluation can take significant time. On our -setup, all runs took in sum 90h. Therefore, having access to multiple machines -might be beneficial. +- Container Runtime, e.g., Docker or Podman +- CPU architecture: x86_64 (amd64) -### Tested On + > Also tested on MacOS with arm64 running Podman. However, for this setup, we + > observed significantly decreased performance, especially for the tool we + > compare against ([ByMC]). -Host OS: +- RAM: >= 32GB recommended +- CPU cores: >= 2 +- Time (smoke tests): 10min max. +- Time (full review): + - ~13.5h (7h TACO + 6.5h ByMC) for ~90% replication of results presented in + the Experimental Evaluation section + - ~22h (14h TACO + 8h ByMC) for full replication of all results presented in + the Experimental Evaluation section + - ~90h for replication of results presented in the Extended Evaluation Section + in the Appendix of the paper -- Ubuntu 22.04/24.04/25.04 -- Fedora 42/43 -- Container Runtime: Podman or Docker + > Note that the benchmark suite has been designed such that they can easily + > be distributed across multiple machines, e.g., by running only the + > benchmark suite for one model checker per machine. -Also tested on MacOS with arm64 running Podman. However, for this setup, we -observed significantly decreased performance, especially for the tool we compare, -against ([ByMC]). +**External Connectivity**: No -## Reproducing the Benchmark Table +## SMOKE TESTS -This section describes how to reproduce the benchmark results for all the TACO -model checkers. - -### Preparation +### TACO Preparation First, you need to load the evaluation container image from the files of the artifact. This can be done by navigating into the unzipped directory of the @@ -91,11 +95,6 @@ docker run --rm -it localhost/taco:latest shell in the container.
-Now we are ready to start executing benchmarks. -You can find the instructions to execute smoke tests in section -[`Smoke Tests`](#smoke-tests) and the instructions for a full evaluation run in -[`TACO Benchmark Run`](#taco-benchmark-run). - Note that with the current setup, the log files of a run will not be moved outside the container and therefore will be gone as soon as the container terminates. If you prefer our evaluation scripts to automatically move log files @@ -132,7 +131,7 @@ If this directory exists, the benchmark scripts will automatically move the result table(s), logfile(s) and potential crash reports to your local storage after all benchmarks are finished. -### Smoke Tests +### Running TACO Smoke Tests Before running a full benchmark run (which can take significant amounts of time), we recommend to test the setup with our set of smoke tests. @@ -144,8 +143,8 @@ container, and executing our benchmarking script with the `--smoke` flag: benchmark-taco --smoke ``` -The smoke tests will execute the benchmark set "Small ByMC" with a timeout of -30s for each model checker. +The smoke tests will execute the benchmark set 'ByMC Handcoded ISOLA18' with a +timeout of 30s for each model checker. Additionally, this setting will print all the output of TACO to the console to make any errors that might occur directly visible (note that in a full run the @@ -155,10 +154,71 @@ The script will also create a preliminary result table called `taco-exec.csv` which should roughly match the results we reported in our paper for these benchmarks. +### Running ByMC Smoke Tests + +#### ByMC Preparation + +Since [ByMC] has not been maintained for a few years now, compiling it requires +installation of old versions of dependencies. Unfortunately, this also includes +components that TACO uses, like Z3. To avoid conflicts, we therefore decided to +package ByMC into a separate container image. + +We made the Dockerfile which we used to compile ByMC openly available on GitHub +in the form of this [pull request](https://github.com/konnov/bymc/pull/2). +We built the image included in this artifact from the same Dockerfile, only +adding additional steps to include the benchmark files and a convenient +benchmark script. + +> **Note** +> +> You can find more details on why we chose to create a custom Dockerfile +> in section [Container Image vs ByMC VM](#container-image-vs-bymc-vm). + +Similar to the TACO image before, we first need to load the container image +using + +```bash +docker load -i bymc.tar +``` + +which will load the image `localhost/bymc:latest` onto your machine. Now you can +start a container and open a shell using this image using + +```bash +docker run --rm -it localhost/bymc:latest +``` + +or again with + +```bash +docker run --rm -it -v ./:/storage localhost/bymc:latest +``` + +If you want the log files to be moved to your local storage outside the +container (see Section [Mounting Local Storage](#mounting-local-storage)). + +#### ByMC Smoke Tests + +Analogous to the TACO smoke tests, you can execute the smoke tests by running: + +```bash +benchmark-bymc --smoke +``` + +This will again execute the benchmark set 'ByMC Handcoded ISOLA18' with a +timeout of 30s. + +## FULL REVIEW + +### TACO Preparation + +Please follow the preparation steps from the `SMOKE TESTS` section to load the +container image and start a container using the TACO evaluation image. + ### TACO Benchmark Run -To run the set of benchmarks used for the experimental evaluation in the -main section of the paper with a timeout of 20min per benchmark you can simply +To run the set of benchmarks used for Table 1 in the Experimental Evaluation +Section of the paper with a timeout of 20min per benchmark you can simply start the TACO benchmark script by running: ```bash @@ -166,11 +226,14 @@ benchmark-taco ``` This will run the full benchmark suite with a timeout of 20min per benchmark. -Note that in sum, such a run can take around _14h_. To start a run that should -complete within 8h, we recommend to lower the timeout per benchmark to a time -<= 10min. +Note that in sum, such a run can take around _14h_. + +Alternatively, you can lower the timeout to, for example <= 10min, which should +lead to a run that completes within 8h. +This should be enough to reproduce most of the results reported in Table 1. -This can be done using the `--timeout` flag, for example, use +To set the timeout use the `--timeout` flag, i.e., you can start a run with a +timeout of 10min per benchmark using: ```bash benchmark-taco --timeout 10m @@ -236,46 +299,10 @@ SMT solver, you need to start an additional run and additionally set the benchmark-taco --extended --smt-solver cvc5 ``` -### ByMC - -Since [ByMC] has not been maintained for a few years now, compiling it requires -installation of old versions of dependencies. Unfortunately, this also includes -components that TACO uses, like Z3. To avoid conflicts, we therefore decided to -package ByMC into a separate container image. - -We made the Dockerfile which we used to compile ByMC openly available on GitHub -in the form of this [pull request](https://github.com/konnov/bymc/pull/2). -We built the image included in this artifact from the same Dockerfile, only -adding additional steps to include the benchmark files and a convenient -benchmark script. - -> **Note** -> -> You can find more details on why we chose to create a custom Dockerfile -> in section [Container Image vs ByMC VM](#container-image-vs-bymc-vm). - -Similar to the TACO image before, we first need to load the container image -using - -```bash -docker load -i bymc.tar -``` - -which will load the image `localhost/bymc:latest` onto your machine. Now you can -start a container and open a shell using this image using - -```bash -docker run --rm -it localhost/bymc:latest -``` +### Benchmarking ByMC -or again with - -```bash -docker run --rm -it -v ./:/storage localhost/bymc:latest -``` - -If you want the log files to be moved to your local storage outside the -container (see Section [Mounting Local Storage](#mounting-local-storage)). +Again, follow the steps of the smoke tests under ByMC preparation to load the +image if it is no longer stored on your machine, and start a ByMC container. Analogous to the TACO benchmarks, you can execute the set of benchmarks used in the evaluation section in the main part of the paper by running: @@ -285,8 +312,9 @@ benchmark-bymc ``` This will start ByMC in the default (`popl17`) mode with the same timeout of -20min. A full benchmark run in this case took us around 8h. Again, you can lower -the timeout by using the `--timeout` flag. For example: +20min. A full benchmark run in this case took us around 8h. + +Again, you can lower the timeout by using the `--timeout` flag. For example: ```bash benchmark-bymc --timeout 10m @@ -308,9 +336,16 @@ evaluation run using the `--extended` flag: benchmark-bymc --extended ``` -Note that this script will directly run ByMC also in the `cav15` mode. +Note that this script will also directly run ByMC in the `cav15` mode. + +## Additional Artifact Contents -## Documentation +The following sections no longer adhere to the official CAV 2026 artifact +README template. They will explain how to access the TACO documentation that +we included in the artifact and provide details on some considerations we made +when selecting and designing our experimental evaluation section. + +### Documentation The TACO documentation consists of two parts @@ -343,7 +378,7 @@ on `crates.io` with the source documentation therefore also available under `docs.rs`. The README of the source code (title page of the repository) contains the links to the artifacts on `crates.io` and `docs.rs`. -### Serving the Documentation from the Container +#### Serving the Documentation from the Container We have included a preconfigured Apache server with the artifact container image such that you can serve the documentation from the local files without needing @@ -392,13 +427,13 @@ Internally, the `serve-docs` command simply starts [`Apache2`](https://httpd.apache.org/) which serves the static HTML file under `/var/html/www`. -### Source Files +#### Source Files The user documentation is generated from the LaTeX and Markdown that are located -in the `src/docs` directory both formats are (more or less) human-readable. +in the `src/docs` directory. Both formats are (more or less) human-readable. Additionally, the developer documentation is part of the source code files. -### Building the Documentation from Sources +#### Building the Documentation from Sources You can also build the documentation yourself. However, this will require `cargo` to be installed on your machine to build the developer documentation @@ -409,7 +444,7 @@ in the file `src/docs/dev-docs.md` in the sections `Building the Developer Documentation` and `Displaying & Editing the User Documentation`. -## Running & Using TACO +### Running & Using TACO If you want to test out the TACO CLI in the image we provided, you can call TACO by simply using @@ -418,11 +453,12 @@ by simply using taco-cli ``` -as TACO has been correctly installed in the container image. The [User Guide -CLI](https://taco-mc.dev/usage-cli/) will provide you with more information on -how to use TACO with other examples and on TACO's configuration options. +as TACO has been correctly installed in the container image. The section 'User +Guide CLI' [(webpage link)](https://taco-mc.dev/usage-cli/) will provide you with +more information on how to use TACO with other examples and will point you to +more configuration options. -## Additional Contents of the Artifact +### Source Code We have included the full source code of TACO inside this artifact in the `src` directory. Alternatively, you can also find the source code in [TACO's Github @@ -431,13 +467,13 @@ repository](https://github.com/cispa/TACO). You will also be able to find the Dockerfiles, scripts, documentation, etc. in the `src` directory. -## Benchmarking Considerations +### Benchmarking Considerations This section will elaborate on some choices that were made when designing the outlined benchmarking process for this artifact evaluation. It is intended to document our methodology and can be considered optional for artifact evaluation. -### Metrics & Limits during Evaluation +#### Metrics & Limits during Evaluation The benchmarking scripts always report the elapsed real-time and maximal resident set size as reported by the GNU `time` command. @@ -457,7 +493,7 @@ runtime and Ubuntu 24.04 as the node host OS. For the evaluation, a node was always allocated exclusively to ensure no other workloads were running on the node. -### Origin of the Benchmarks +#### Origin of the Benchmarks The benchmarks have been taken/generated from the [`fault-tolerant-benchmarks`](https://github.com/konnov/fault-tolerant-benchmarks) @@ -467,7 +503,7 @@ You can find more information about the generation of these benchmarks, and about why some of them have been excluded in the `README` of the `src/benchmarks` directory. -### Container Image vs. ByMC VM +#### Container Image vs. ByMC VM Note that instead of using our Dockerimage for [ByMC], we could have also used the VM that is still available (see the README of the @@ -496,7 +532,7 @@ There were two main reasons why we chose to build our own Dockerfile instead: build system [`ocamlbuild`](https://github.com/ocaml/ocamlbuild)) or modifying the source code, as we would expect users to go through this process. -### Exclusion of the CAV15 Method +#### Exclusion of the CAV15 Method We did exclude the benchmark mode `cav15` of ByMC in the main benchmark evaluation. This is because we had major issues with this mode. For example, for @@ -609,10 +645,16 @@ method we decided not to include results of this mode in our main comparison. For completeness, we still reported performance results in the extended evaluation in the appendix of our paper. -#### Screenshot ByMC Counter Example `bosco` +##### Screenshot ByMC Counter Example `bosco` ![](./bymc-spurious-cex.png) +### Table 2 + +Lastly, the artifact contains an easier-to-read version of Table 2 from +Appendix C of the paper, which is called `table2.ods`. This should make it +easier to compare evaluation results. + [ByMC]: https://github.com/konnov/bymc [CVC5]: https://cvc5.github.io/ [Z3]: https://github.com/Z3Prover/z3 diff --git a/artifact-evaluation/bench-bymc.sh b/artifact-evaluation/bench-bymc.sh index f20912a..4ae1e95 100755 --- a/artifact-evaluation/bench-bymc.sh +++ b/artifact-evaluation/bench-bymc.sh @@ -24,6 +24,8 @@ EXECUTABLE="${EXECUTABLE:=./bymc/verify}" # Configure whether to run the specified model checkers on the extended set of # benchmarks EXTENDED="${EXTENDED:=false}" +# Smoke Test Run +SMOKE="${SMOKE:=false}" ################################################################################ @@ -423,6 +425,32 @@ run_rb_wo_reset_benchmarks () { } +# Execute the smoke tests +smoke_tests () { + printf "Executing the smoke tests + +This mode will execute the 'ByMC Handcoded ISOLA18' benchmarks for ByMC. All of +these benchmarks should be reported to be safe, and some benchmarks should +finish within the 30s timeout set for this benchmark run by default. + +(In case all dependencies are met,) this script will also produce a table +summarizing the results in a CSV file called '${CSV_FILE_NAME}'. The table +should roughly match the table reported in the paper. +" + LOGFILE=/dev/null + FAIL_ON_ERROR=true + + # if the default timeout has not been overwritten + if [ $TIMEOUT = "20m" ]; then + TIMEOUT='30s' + fi + + run_small_benchmarks "-O schema.tech=ltl" "ltl" + + printf "\nFinished executing smoke tests\n\n" +} + + ################################################################################ ### Main functionality of the benchmarking script @@ -448,13 +476,20 @@ while [ $# -gt 0 ]; do LOGFILE=/dev/null shift # past argument ;; + -s|--smoke) + SMOKE=true + LOG_TO_STDOUT=true + shift # past argument + ;; -h|--help) printf "ByMC Benchmark Script help This is the ByMC benchmark script designed to benchmark the ByMC model checker. This scripts supports the following options: -h | --help : Print this message - -t | --timeout : Override the per benchmark timeout (default: '1h') + -t | --timeout : Override the per benchmark timeout (default: '20min') + -s | --smoke : Execute a small set of benchmarks for the specified model + checkers (default: all) that should terminate within 5min -e | --extended : Benchmark the full extended set of benchmarks (this can take a lot of time!) --log-to-stdout : Print the logs of the model checker to stdout instead of @@ -498,6 +533,12 @@ directory. Sleeping 10s to give you time to abort.\n\n\n fi fi +# Run the smoke tests and exit +if [ $SMOKE = true ]; then + smoke_tests + exit 0 +fi + # Make the user aware of extended setting if [ "${EXTENDED}" = true ]; then printf "Executing the extended TACO benchmark suite. This can take a lot of diff --git a/scripts/bench-taco.sh b/scripts/bench-taco.sh index 1a73af8..b55f472 100755 --- a/scripts/bench-taco.sh +++ b/scripts/bench-taco.sh @@ -628,7 +628,7 @@ checker '${1}'\n\n\n" | tee -a "${LOGFILE}" smoke_tests () { printf "Executing the smoke tests -This mode will execute the 'Small ByMC' benchmarks for all of the selected model +This mode will execute the 'ByMC Handcoded ISOLA18' benchmarks for all of the selected model checkers and print the output of the model checker to stdout. All of these benchmarks should be reported to be safe, and most benchmark should finish within the 30s timeout set for this benchmark run by default. From 5f814581c2a1c9440008b51cf6d0199aef507912 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Wed, 22 Apr 2026 09:46:24 +0200 Subject: [PATCH 3/3] small grammar fixes --- artifact-evaluation/artifact-evaluation.md | 48 ++++++++++++---------- 1 file changed, 27 insertions(+), 21 deletions(-) diff --git a/artifact-evaluation/artifact-evaluation.md b/artifact-evaluation/artifact-evaluation.md index 1dd9c1a..9d57765 100644 --- a/artifact-evaluation/artifact-evaluation.md +++ b/artifact-evaluation/artifact-evaluation.md @@ -30,7 +30,7 @@ for Rust) by following the installation guide on the TACO webpage. Alternatively, users can also utilize the container images provided on GitHub. - The TACO documentation describes how to use and configure TACO and it + The TACO documentation describes how to use and configure TACO, and it provides details on TACO's architecture and implementation. All of TACO's modules, i.e., Rust crates, are available on `crates.io` enabling @@ -80,8 +80,10 @@ artifact and executing docker load -i taco.tar ``` -This will load the image `localhost/taco:latest` onto your machine. Now you can -start a container and open a shell in the container using +This will load the image `localhost/taco:latest` onto your machine. This step +only needs to be done once, the image will stay available on your machine. + +Now you can start a container and open a shell in the container using ```bash docker run --rm -it localhost/taco:latest @@ -119,8 +121,9 @@ Here, `-v ./:/storage` specifies to mount the current directory, i.e., `./` to the container and makes it accessible in the running container under the directory `/storage`. -If your machine has SELinux configured, you might have to append the `:z` see -option; This however should never be done in the directory `/home` or `/usr`. +If your machine has SELinux configured, you might have to append the SELinux +option `:z`; however, this should never be done in the directory `/home` or +`/usr`. See [Docker Documentation](https://docs.docker.com/engine/storage/bind-mounts/#configure-the-selinux-label) @@ -128,16 +131,16 @@ See [Docker Documentation](https://docs.docker.com/engine/storage/bind-mounts/#c Our scripts will check for the existence of the path `/storage`. If this directory exists, the benchmark scripts will automatically move the -result table(s), logfile(s) and potential crash reports to your local storage +result table(s), log file(s) and potential crash reports to your local storage after all benchmarks are finished. ### Running TACO Smoke Tests Before running a full benchmark run (which can take significant amounts of -time), we recommend to test the setup with our set of smoke tests. +time), we recommend testing the setup with our set of smoke tests. In our evaluation image, this can be done by opening a shell in the TACO -container, and executing our benchmarking script with the `--smoke` flag: +container and executing our benchmarking script with the `--smoke` flag: ```bash benchmark-taco --smoke @@ -148,7 +151,7 @@ timeout of 30s for each model checker. Additionally, this setting will print all the output of TACO to the console to make any errors that might occur directly visible (note that in a full run the -output will only be written to the log files to avoid cluttering stdout). +output will only be written to the log file to avoid cluttering stdout). The script will also create a preliminary result table called `taco-exec.csv` which should roughly match the results we reported in our paper for these @@ -167,7 +170,8 @@ We made the Dockerfile which we used to compile ByMC openly available on GitHub in the form of this [pull request](https://github.com/konnov/bymc/pull/2). We built the image included in this artifact from the same Dockerfile, only adding additional steps to include the benchmark files and a convenient -benchmark script. +benchmark script (the exact Dockerfile the image was derived from can be found +under `./src/artifact-evaluation/ByMC-Dockerfile`). > **Note** > @@ -181,8 +185,10 @@ using docker load -i bymc.tar ``` -which will load the image `localhost/bymc:latest` onto your machine. Now you can -start a container and open a shell using this image using +which will load the image `localhost/bymc:latest` onto your machine. This step +only needs to be done once, the image will stay available on your machine. + +Now you can start a container and open a shell using this image using ```bash docker run --rm -it localhost/bymc:latest @@ -257,7 +263,7 @@ Storage](#mounting-local-storage)). #### Benchmarking Options -##### Running only a Single Model Checker +##### Running Only a Single Model Checker To run the full set of benchmarks for a single model checker, e.g., if you split the benchmark run across multiple machines, you can simply pass the model @@ -291,7 +297,7 @@ benchmark-taco --extended ``` This flag will execute the complete set of benchmarks **with only one SMT -solver**. By default this will be [Z3]. To obtain the results with `cvc5` as +solver**. By default, this will be [Z3]. To obtain the results with `cvc5` as SMT solver, you need to start an additional run and additionally set the `--smt-solver` flag set to `cvc5`: @@ -312,7 +318,7 @@ benchmark-bymc ``` This will start ByMC in the default (`popl17`) mode with the same timeout of -20min. A full benchmark run in this case took us around 8h. +20min. A full benchmark run in this case took us around 6.5h. Again, you can lower the timeout by using the `--timeout` flag. For example: @@ -385,9 +391,9 @@ such that you can serve the documentation from the local files without needing internet access. To be able to access the documentation server that will be running inside the -TACO container, we need to publish the port `80` (which will be the port of our -server will be serving the documentation) of the container by additionally using -the `--publish` flag. +TACO container, we need to publish the port `80` (which will be the port our +server will be serving the documentation on) of the container by additionally +using the `--publish` flag. ``` docker run --rm -it --publish 3000:80 localhost/taco @@ -397,7 +403,7 @@ This command will start a shell in the container while also mapping the port `80` of the container to port `3000` of the host.

In Case of Errors -IT might happen that you get an error of the form +It might happen that you get an error of the form ```bash Failed to bind port 3000 (Address already in use) @@ -407,7 +413,7 @@ In this case, a different application is already using the port `3000` on your local machine and you can just use a different port, e.g., `3001` when starting the container. -The documentation will in then case be served under the address +The documentation will in that case be served under the address [http://localhost:3001](http://localhost:3001).

@@ -425,7 +431,7 @@ documentation. Internally, the `serve-docs` command simply starts [`Apache2`](https://httpd.apache.org/) which serves the static HTML file under -`/var/html/www`. +`/var/www/html`. #### Source Files