QuAK: Quantitative Automata Kit (artifact)
Fuente:
Zenodo
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Recurso digital |
| Sprache: | Englisch |
| Veröffentlicht: |
Zenodo
2024
|
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866902206506074112 |
|---|---|
| author | Chalupa, Marek Henzinger, Thomas Mazzocchi, Nicolas Saraç, N. Ege |
| author_facet | Chalupa, Marek Henzinger, Thomas Mazzocchi, Nicolas Saraç, N. Ege |
| contents | <p>The artifact to the paper <strong>QuAK: Quantitative Automata Kit.</strong></p> <p>You can load the provided docker image (built for x86_64 architecture) using this command:</p> <p><code>docker load < quak-isola24.tar.gz</code></p> <p>Once the image is loaded, you can run all the experiments with the following command:</p> <div> <pre><code>docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-all.sh </code></pre> </div> <p>All results of the experiments are stored into the directory <code>results/</code>. You can also run the experiments one by one by issuing the following commands:</p> <div> <pre><code># run the inclusion experiments (Figure 2 and Figure 3) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-inclusion.sh # run the constant-check experiments (Figure 4) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-constant.sh # run the drone simulation (Figure 5, table) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-drone.sh </code></pre> </div> <p>Running the inclusion experiments takes many hours on a multi-core system. If you want to run the experiments only on a subset of automata, you can specify the option <code>--num=X</code>, where <code>X</code> is the number of automata. Then, the experiments will run only on the first <code>X</code> generated automata, which means <code>X*X</code> configurations are going to be executed.</p> <div> <pre><code>docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-inclusion.sh --num=3 # you can use `--num` also with `run-all.sh` docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-all.sh --num=3 </code></pre> </div> <p>Running with <code>--num=15</code> should take about 1 hour with 4 cores @ 2.8GHz.</p> <h3>Building and exploring the artifact </h3> <p>For instructions on how to (re-)build the artifact and on details on its contents, see the <em>README.md</em> in <a href="https://github.com/ista-vamos/QuAK/tree/experiments-isola24/experiments" rel="noopener">https://github.com/ista-vamos/QuAK/tree/experiments-isola24/experiments</a>.</p> <div> </div> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_13132070 |
| institution | Zenodo |
| language | eng |
| publishDate | 2024 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | QuAK: Quantitative Automata Kit (artifact) Chalupa, Marek Henzinger, Thomas Mazzocchi, Nicolas Saraç, N. Ege <p>The artifact to the paper <strong>QuAK: Quantitative Automata Kit.</strong></p> <p>You can load the provided docker image (built for x86_64 architecture) using this command:</p> <p><code>docker load < quak-isola24.tar.gz</code></p> <p>Once the image is loaded, you can run all the experiments with the following command:</p> <div> <pre><code>docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-all.sh </code></pre> </div> <p>All results of the experiments are stored into the directory <code>results/</code>. You can also run the experiments one by one by issuing the following commands:</p> <div> <pre><code># run the inclusion experiments (Figure 2 and Figure 3) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-inclusion.sh # run the constant-check experiments (Figure 4) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-constant.sh # run the drone simulation (Figure 5, table) docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-drone.sh </code></pre> </div> <p>Running the inclusion experiments takes many hours on a multi-core system. If you want to run the experiments only on a subset of automata, you can specify the option <code>--num=X</code>, where <code>X</code> is the number of automata. Then, the experiments will run only on the first <code>X</code> generated automata, which means <code>X*X</code> configurations are going to be executed.</p> <div> <pre><code>docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-inclusion.sh --num=3 # you can use `--num` also with `run-all.sh` docker run --rm -ti -v "$(pwd)/results":/opt/quak/experiments/results quak ./run-all.sh --num=3 </code></pre> </div> <p>Running with <code>--num=15</code> should take about 1 hour with 4 cores @ 2.8GHz.</p> <h3>Building and exploring the artifact </h3> <p>For instructions on how to (re-)build the artifact and on details on its contents, see the <em>README.md</em> in <a href="https://github.com/ista-vamos/QuAK/tree/experiments-isola24/experiments" rel="noopener">https://github.com/ista-vamos/QuAK/tree/experiments-isola24/experiments</a>.</p> <div> </div> |
| title | QuAK: Quantitative Automata Kit (artifact) |
| url | https://doi.org/10.5281/zenodo.13132070 |