Submission of Benchmarks:
- Submit an issue in the SYNTCOMP benchmark repository with your new benchmarks attached.
- We will review your submission and add the benchmarks to the repository.
- Note that all accepted benchmarks will be copyrighted using the Creative Commons CC-BY license.
Submission of Tools:
Preliminary versions of synthesis tools can be uploaded and tested at any time on www.starexec.org. We encourage participants to test their tools within the execution environment well in advance.
Preparation of Tool Submissions:
To submit a solver, use the web interface at www.starexec.org to upload a zip or tar file with the following structure and content:
/bin/<your_tool_binary> /bin/starexec_run_default /code/<your_source_code> /doc/<your_tool_description>.pdf readme.txt license.txt
where
- /bin/<your_tool_binary> is your executable compiled for the StarExec architecture (you can in fact have StarExec compile your tool’s source code and create the binary, see here)
- /bin/starexec_run_default is a StarExec configuration. It is just a shell script used to invoke your solver. A bare bones version would be
#!/bin/bash ./<your_solver_binary> $1
which will invoke your solver on an input file passed into the script as the $1 variable. More elaborate versions might supply various parameter settings to your solver.
- /code/<your_source_code> contains the source code of your tool.
- /doc/<your_tool_description>.pdf is a short tool description (2-4 pages, EPTCS style) or alternatively a tool paper that has been submitted or published elsewhere.
- readme.txt is a short text description of your solver. This description can alternatively be directly entered in the StarExec upload page.
- license.txt is the license under which your source code is published. We do not require any particular type of license, but the minimum requirement for the license is to contain the permission to use the tool for evaluation. If you are using source code of other tools please be sure to also include their license information in your license file.
Example: StarExec-Ready Tool
You can download a minimal StarExec-working version of the tool AbsSynthe from here.
Using StarExec
Getting an account
Register for an account in the SYNTCOMP community (unless you are already registered). Wait until one of the SYNTCOMP community leaders approves your request.
Uploading a solver for testing
A solver is submitted by uploading an archive as specified above. StarExec runs an older version of Linux so dynamically linked binaries are likely to fail. A statically linked binary should work.
Building your solver on StarExec
Instead of uploading the binary of your tool (using the StarExec virtual-machine image to compile) you can include a build script, in which case your solver will be built on the StarExec system on upload. To do this you include a script “starexec_build” at the top level of your archive file. On upload StarExec will detect if this file exists and execute it to build your solver. Note that your archive must still include the other files specified above (as well as, of course, any Makefile or other files you need to perform the build). You should still make sure the build creates a static executable. See the StarExec Users Guide for more details and the reference solver on how to prepare your solver to be compiled on upload.
To upload your solver to StarExec
Login to the StarExec website and click Spaces->Explore (on the top) then in the left frame open root->SYNTCOMP->SYNTCOMP20XX->Tests At the bottom of page click “upload solver” to open the upload dialog. Click “Browse” and select the archive with your solver’s code, enter the solver name, change downloadable to “no” (so as to keep your source code hidden until the submission deadline is over) and click “upload”.
Testing your solver
We put a few testing instances in the subspaces of SYNTCOMP20XX->Tests which you can use after you upload your solver. To run a test go to the subspace. Click “create job” on the bottom of the page. This opens a page where you don’t need to change anything so just click “next” On the next page select the “choose” option and then “all in X”. A page with all solvers (and their configurations) comes up, select the solver you want to run and click “submit” at the bottom of the page. You can check the status and results of your test job by clicking on Jobs on the top and selecting your job.
To check the correctness of your solver
You can add a post-processor to your job. There are post-processors for realizability and synthesis already available in the SYNTCOMP subspaces.
To check the output of your job
Once the job is finished, you can check the logs of your solver by downloading the “job output” in the job webpage. You can also download the “job information” that will contain a .csv file with a summary of your job. This .csv file will contain default attributes such as “benchmark id”, “solver”, “wallclock time”, “memory usage”.
Uploading the final version of your solver
The submission of the final version of a solver is essentially the same as uploading the solver for testing (see above). To submit the final version of your solver upload it to the space root->SYNTCOMP->SYNTCOMP20XX->Competition->[track], where [track] is one of AIGER-Real, AIGER-Synth, LTL-Real, LTL-Synth, PGAME-Real, PGAME-Synth, depending on the track you want to participate in. If you want to participate in several tracks upload your solver to each one of them separately.
Don’t forget to select “downloadable:no” when uploading your files to prevent other participants from seeing them before the start of the evaluation. After the submission deadline we will ask all the participants to update the downloadable option to “downloadable:yes”. This will make the source code visible to the organizers and all the participants. The participants must comply with this request in order to participate in the evaluation.