Synthesis Format Conversion Tool / Library.

Library and tool for reading, manipulating and transforming synthesis specifications.

Synthesis Format Conversion Tool

A tool for reading, manipulating and transforming synthesis specifications in TLSF.

About this tool

The tool interprets the high level constructs of TLSF 1.1 (functions, sets, ...) and supports the transformation of the specification to Linear Temporal Logic (LTL) in different output formats. The tool has been designed to be modular with respect to the supported output formats and semantics. Furthermore, the tool allows to identify and manipulate parameters, targets and semantics of a specification on the fly. This is especially thought to be useful for comparative studies, as they are for example needed in the Synthesis Competition.

The main features of the tool are summarized as follows:

• Interpretation of high level constructs, which allows to reduce the specification to its basic fragment where no more parameter and variable bindings occur (i.e., without the GLOBAL section).

• Transformation to other existing specification formats, like Basic TLSF, Promela LTL, PSL, Unbeast, Wring, structured Slugs, and SlugsIn.

• Syntactical analysis of membership in GR(k) for any k (modulo Boolean identities).

• On the fly adjustment of parameters, semantics or targets.

• Preprocessing of the resulting LTL formula.

• Conversion to negation normal form.

• Replacement of derived operators.

• Pushing/pulling next, eventually, or globally operators inwards/outwards.

• Standard simplifications.