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 4 competitive categories in SYNTCOMP 2019:
- Safety Realizability (AIGER)
- Safety Synthesis (AIGER)
- LTL Realizability (TLSF)
- LTL Synthesis (TLSF)
In each category, tools can run either in sequential (single-thread) or in parallel (multi-thread) mode.
General Rules for All Categories
- The competition will be managed and run on the StarExec platform. Tools have to be uploaded to the SYNTCOMP space at https://www.starexec.org. 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 2019. If a (submitted or already published) tool paper that describes the current status of the tool exists, it 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 by a subset of the entrants of SYNTCOMP 2018, obtained by the organizers in preparatory experiments.
Benchmarks that are added this year will not be made available publicly before the competition. 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.
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. You can download a StarExec-ready SyFCo binary from here if you wish to use it in your toolchain (it will not be installed on the competition machine so include it as part of your tool).
- 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 (the precise model checker is to be determined).