The syfco package

[ Tags: library, mit, program, syntcomp ] [ Propose Tags ]

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

[Skip to Readme]


Dependencies array (==0.5.*), base (>=4.7 && <4.10), containers (==0.5.*), convertible (>=1.1), directory (>=1.2 && <1.4), mtl (==2.2.*), parsec (==3.1.*), transformers (>=0.4 && <0.6) [details]
License MIT
Author Felix Klein <>
Maintainer Felix Klein <>
Category SyntComp
Home page
Bug tracker
Source repo head: git clone
Uploaded Mon Jul 3 14:29:06 UTC 2017 by kleinreact
Distributions NixOS:
Executables syfco
Downloads 203 total (7 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-07-03 [all 1 reports]
Hackage Matrix CI




Maintainer's Corner

For package maintainers and hackage trustees

Readme for syfco-

[back to package description]

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.