Hackage :: [Package]

syfco: Synthesis Format Conversion Tool / Library

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

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

[Skip to Readme]

Modules

[Index]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 1.1.0.0
Dependencies array (>=0.5 && <0.6), base (>=4.7 && <4.10), containers (>=0.5 && <0.6), convertible (>=1.1), directory (>=1.2 && <1.4), mtl (>=2.2 && <2.3), parsec (>=3.1 && <3.2), transformers (>=0.4 && <0.6) [details]
License MIT
Author Felix Klein <klein@react.uni-saarland.de>
Maintainer Felix Klein <klein@react.uni-saarland.de>
Category SyntComp
Home page https://github.com/reactive-systems/syfco
Bug tracker https://github.com/reactive-systems/syfco/issues
Source repo head: git clone https://github.com/reactive-systems/syfco
Uploaded by kleinreact at 2017-07-03T14:29:06Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables syfco
Downloads 869 total (4 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-07-03 [all 1 reports]

Readme for syfco-1.1.0.0

[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.