Difference between revisions of "Termination Competition 2025 technical details"
| (11 intermediate revisions by 2 users not shown) | |||
| Line 3: | Line 3: | ||
Starting from 2025, TermComp runs on the RWTH HPC cluster. | Starting from 2025, TermComp runs on the RWTH HPC cluster. | ||
| − | Tools must be submitted as Apptainer | + | Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your container: |
* solver --name | * solver --name | ||
| Line 14: | Line 14: | ||
A list with the exact category names will be published before the competition. | A list with the exact category names will be published before the competition. | ||
They will essentially be identical to the names of the corresponding TPDB directories. | They will essentially be identical to the names of the corresponding TPDB directories. | ||
| + | |||
| + | Resource limits: | ||
| + | * 4 cores | ||
| + | * 60s wallclock time | ||
| + | * 20.345 MiB RAM | ||
| + | |||
| + | == Testing Locally == | ||
| + | |||
| + | * Install [https://apptainer.org/docs/admin/main/installation.html Apptainer]. | ||
| + | * Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86. | ||
| + | * Convert your docker image to an Apptainer image via | ||
| + | <code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code> | ||
| + | <br/> | ||
| + | So in my case, the full command is | ||
| + | <br/> | ||
| + | <code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code> | ||
| + | * First test | ||
| + | <code> | ||
| + | apptainer exec $apptainer_image.sif solver --name | ||
| + | </code> | ||
| + | </br> | ||
| + | In my case, I get: | ||
| + | </br> | ||
| + | <code> | ||
| + | apptainer exec loat.sif solver --name | ||
| + | |||
| + | LoAT | ||
| + | </code> | ||
| + | * Then test | ||
| + | <code> | ||
| + | apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark | ||
| + | </code> | ||
| + | where $TPDB is the path to your clone of the TPDB. | ||
| + | </br> | ||
| + | In my case, I get: | ||
| + | </br> | ||
| + | <code> | ||
| + | apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2 | ||
| + | |||
| + | NO | ||
| + | </code> | ||
== Lessons Learned from Testing == | == Lessons Learned from Testing == | ||
| − | + | === General === | |
| + | |||
| + | * The image must be for an '''amd64-architecture'''. | ||
| + | |||
| + | === Docker - Apptainer incompatibilities === | ||
| + | |||
| + | The following things must be taken into account if you submit a Docker image. | ||
* The solver-command must behave as intended '''for all users''', not just for a specific one. | * The solver-command must behave as intended '''for all users''', not just for a specific one. | ||
* The solver-command must behave as intended '''independently from the current working directory'''. | * The solver-command must behave as intended '''independently from the current working directory'''. | ||
| − | |||
== Registration == | == Registration == | ||
| − | To | + | To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository]. |
| − | + | ||
| − | + | == Certification == | |
| + | |||
| + | We use CeTA version 3.6 for certification. | ||
Latest revision as of 20:25, 30 July 2025
Contents
Execution Environment
Starting from 2025, TermComp runs on the RWTH HPC cluster.
Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your container:
- solver --name
- solver --timeout=$timeout --category=$category $benchmark
So an executable named "solver" must be available in your container. The former command must print the name of your solver to stdout. The latter must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.
A list with the exact category names will be published before the competition. They will essentially be identical to the names of the corresponding TPDB directories.
Resource limits:
- 4 cores
- 60s wallclock time
- 20.345 MiB RAM
Testing Locally
- Install Apptainer.
- Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
- Convert your docker image to an Apptainer image via
apptainer build $apptainer_image.sif docker-daemon://$docker_image
So in my case, the full command is
apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86
- First test
apptainer exec $apptainer_image.sif solver --name
In my case, I get:
apptainer exec loat.sif solver --name
LoAT
- Then test
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
where $TPDB is the path to your clone of the TPDB.
In my case, I get:
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2
NO
Lessons Learned from Testing
General
- The image must be for an amd64-architecture.
Docker - Apptainer incompatibilities
The following things must be taken into account if you submit a Docker image.
- The solver-command must behave as intended for all users, not just for a specific one.
- The solver-command must behave as intended independently from the current working directory.
Registration
To submit a tool, please follow the instruction at this repository.
Certification
We use CeTA version 3.6 for certification.
