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.
Final versions of synthesis tools are due June 1, 2020.
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
- /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. Be very explicit in your naming convention for sequential, parallel, realizability, and synthesis configurations. Recall that only three configurations per track are allowed.
- /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 licence, 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
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->SYNTCOMP2020->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 SYNTCOMP2020->Tests->AIGER and SYNTCOMP2020->Tests->LTL spaces which you can use after you uploaded your solver to these spaces. To run a test:
Go to the root->SYNTCOMP->SYNTCOMP2020->Tests->AIGER subspace (or the LTL 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 SYNTCOMP2020->Tests->AIGER” 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 out 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
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 or benchmarks
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->SYNTCOMP2020->Competition->[track], where [track] is one of AIGER-Real, AIGER-Synth, LTL-Real, LTL-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. For benchmarks, use the root->SYNTCOMP->SYNTCOMP2020->Benchmarks->[type], where [type] is AIGER or LTL, and make sure to choose the right benchmark type for your upload.
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.