Please accept that the overall spirit of this competition is friendly, honest and well-spirited. The goal is to foster research and to motivate the implementation and optimization of new synthesis tools. However as it is still a competition, the following rules shall apply:
There will be at least 4 competitive categories in SYNTCOMP 2017:
- Safety Realizability (AIGER)
- Safety Synthesis (AIGER)
- LTL Realizability (TLSF)
- LTL Synthesis (TLSF)
In addition, we plan to set up two new tracks for synthesis from GR(1) specifications:
- GR(1) Realizability (TLSF)
- GR(1) Synthesis (TLSF)
In each category, tools can run either in sequential (single-thread) or in parallel (multi-thread) mode.
General Rules for All Categories
- Tools are to be submitted as source code, licensed for research purposes. Please contact us if this is not acceptable and you still want to participate. Click here for additional details on the preparation of your submission.
- Submitted tools must be accompanied by a 2-4 page description (EPTCS format) of the synthesis approach and important aspects of implementation and optimizations. This should include a list of all authors and their present institutional affiliations. We encourage tool authors to submit a paper describing their tool to the synthesis workshop SYNT 2017. In this case, the submitted tool paper can be included in the tool submission to SYNTCOMP instead of the description mentioned above.
- Not more than 3 sequential and 3 parallel configurations per author in a category. Two tools or configurations are different as soon as their sources differ or as soon as the compilation options or command line arguments are different.
- Competition organizers can compete, but have to make the MD5 of their code available until the deadline for submitting first versions of tools.
- Tools must not include pre-calculated results to any of the benchmarks and there must not be any intentional sabotage of the evaluation system.
- Tools write the solution to stdout. If the tool concludes that the specification is unrealizable, it should write “UNREALIZABLE”. If the specification is found to be realizable, the output should be “REALIZABLE”. In the synthesis categories, a “REALIZABLE” output should be followed by the solution (as an AIGER circuit, see below). No other output should be written to stdout.
In all categories, tools will be ranked according to the number of problems that can be solved within the time limit, with total computation time as a tie-breaker. For the synthesis tracks, we additionally require that produced solutions can be model-checked within a separate time limit.
Additionally, for the synthesis categories we will have a separate quality ranking: the size of solutions (in number of synthesized AND gates) is compared to the size of reference solutions; if a tool produces a solution of size n, and the reference solution is of size r, then for this benchmark the tool receives 2 – log_10(n/r) points. That is, a solution of the same size as the reference solution receives 2 points, a solution that is smaller by factor 10 receives 3 points, a solution that is bigger by factor 10 receives 1 point (with a minimum of 0 points for 100 times or more of the size of the reference solution).
For benchmarks that were already used in previous iterations of SYNTCOMP, the smallest solution produced by any tool in that competition will be the reference solution. For new benchmarks, the reference solution is the smallest solution produced in SYNTCOMP 2017.
A subset of all available benchmarks will be selected for the competition. Randomization and the consultation of impartial judges will ensure a fair selection. The exact benchmark selection scheme is to be determined.
The competition will be organized with the EDACC platform developed for the SAT Challenges. All synthesis tools will be tested on machines with a single Intel XEON processor (E3-1271 v3, quad-core, 3.6GHz) and 32 GB RAM (PC1600, ECC), running a GNU/Linux system. Each node has a local 480gb SSD that should be used for storing any temp files your tools need to create. The timeout for each synthesis task will be one hour (CPU Time for sequential mode, Wall Time for parallel mode).
During the competition, a complete machine will be reserved for each job i.e. one synthesis tool (configuration) running one benchmark. Olivier Roussel’s runsolver is used to run each job, set limits on cpu time, wall time, memory or stack and measure cpu and wall time. As all nodes are identical and no other tasks are run in parallel, no other limits than a timeout per benchmark (cpu time for sequential tools, wall time for the parallel tracks) will be set.
Please contact us if you have any concerns about the fairness of this setup or if anything about it is for whatever reason unacceptable for you and/or your synthesis tool.
The list of available software will be updated continuously as requests/questions come in.
Rules in AIGER Categories
- All solvers must conform to the Extended AIGER Format for Synthesis for inputs.
- In the synthesis category, solutions must also be in extended AIGER format, and will be model checked with the best-performing model checkers from the single-safety track of the Hardware Model Checking Competition. Additionally, tools may output, after their solution, a winning region of the system as a witness for correctness. The winning region should be output after the solution, separated by a line containing “WINNING_REGION”. It should be given as a boolean function in AIGER format, with one input for every latch of the solution circuit (in the same order as the latches in the solution), no latches, and a single output. If a winning region is given, then we check the correctness of the winning region for the given solution, and fall back to model checking if that is not possible.
Rules in LTL Categories
- Specifications are given in TLSF format. For tools that don’t support TLSF directly, the organizers supply a number of translators to different existing formats in the SyFCo tool (which will be installed on the competition machines).
- Like in the AIGER category, realizability is defined with respect to Mealy semantics, i.e., the outputs of the synthesized solutions can depend on the inputs without any delay. (Tools that only support Moore semantics can use a translation of the specification into Moore format, and then translate their solution into a Mealy machine.)
- In the synthesis categories, tools must produce outputs in AIGER format (if the specification is realizable). As a syntactical restriction, the sets of inputs and outputs of the TLSF file must be identical to the sets of inputs and outputs of the AIGER solution. Additionally, solutions are model checked with existing LTL model checkers (using the toolchain described here).