Termination Competition 2025 technical details - Revision history

Ffrohn: /* Execution Environment */

2025-10-02T07:14:24Z

Execution Environment

2025-08-25T06:49:52Z

General

2025-08-25T06:49:09Z

General

2025-07-30T20:25:06Z

2025-07-30T08:28:45Z

2025-07-24T13:47:02Z

Testing Locally

2025-07-24T13:37:59Z

Execution Environment

2025-07-23T13:20:06Z

Testing Locally

2025-05-21T11:18:22Z

2025-05-21T10:58:17Z

Execution Environment

@@ Line 10: / Line 10: @@
 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.
+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.

@@ Line 61: / Line 61: @@
 * The image must be for an '''amd64-architecture'''.
-* If your solver needs to write to temporary files, write them to `/tmp`. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.
+* If your solver needs to write to temporary files, write them to <code>/tmp</code>. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.
 === Docker - Apptainer incompatibilities ===

← Older revision		Revision as of 06:49, 25 August 2025
Line 61:		Line 61:

	* The image must be for an '''amd64-architecture'''.		* The image must be for an '''amd64-architecture'''.
		+	* If your solver needs to write to temporary files, write them to `/tmp`. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.

	=== Docker - Apptainer incompatibilities ===		=== Docker - Apptainer incompatibilities ===

← Older revision		Revision as of 20:25, 30 July 2025
Line 72:		Line 72:

	To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].		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.

← Older revision		Revision as of 08:28, 30 July 2025
Line 71:		Line 71:
	== Registration ==		== Registration ==

−	To ~~register~~, ~~you need to create a pull request for~~ [https://github.com/TermCOMP/registration this repository].	+	To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].
−	~~More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.~~
−	~~The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull"~~.

@@ Line 44: / Line 44: @@
 * Then test
 <code>
-apptainer exec solver --timeout=60 --category=$category $benchmark
+apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
 </code>
 </br>
 In my case, I get:
 </br>
 <code>
-apptainer exec loat.sif solver --timeout=60 --category=Integer_Transition_Systems TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2
+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

@@ Line 14: / Line 14: @@
 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.
 == Testing Locally ==

@@ Line 27: / Line 27: @@
 * First test
 <code>
-apptainer run $apptainer_image.sif solver --name
+apptainer exec $apptainer_image.sif solver --name
 </code>
 </br>

@@ Line 3: / Line 3: @@
 Starting from 2025, TermComp runs on the RWTH HPC cluster.
-Tools must be submitted as Apptainer or Docker images. The competition will run using Apptainer (which can run both Apptainer and Docker images). During the competition, the following two commands will be executed in your container:
+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