We have just published a small update to the temporal logic synthesis format (TLSF). The main changes are:

• additional sections for initial properties of environment and system, and for invariant properties of the environment (these have also been renamed, but the old names are still supported), and
• support for user-defined enumeration types.

The changes are described in the new TLSF format description, and are supported by the first release of the synthesis format conversion tool (SyFCo).

The rules and call for benchmarks and solvers pages have been updated accordingly.