# Synthesis Format Conversion Tool

A tool for reading, manipulating and transforming synthesis
specifications in [TLSF](https://arxiv.org/abs/1604.02284).

## About this tool

The tool interprets the high level constructs of [TLSF 1.1](https://arxiv.org/abs/1604.02284)
(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](http://www.syntcomp.org).

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](http://spinroot.com/spin/Man/ltl.html), [PSL](https://en.wikipedia.org/wiki/Property_Specification_Language), [Unbeast](https://www.react.uni-saarland.de/tools/unbeast), [Wring](http://www.ist.tugraz.at/staff/bloem/wring.html),
  [structured Slugs](https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#structuredslugs), and [SlugsIn](https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#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.