README.md

Synthesis Format Conversion Tool
(Version 1.2.1.2)

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.

Installation

SyfCo is written in Haskell and can be compiled using the Glasgow Haskell Compiler (GHC). To install the tool you can either use cabal or stack (recommended). For more information about the purpose of these tools and why you should prefer using stack instead of cabal, we recommend reading this blog post by Mathieu Boespflug.

To install the tool with stack use:

stack install

Stack then automatically fetches the right compiler version and required dependencies. After that it builds and installs the package into you local stack path. If you instead prefer to build only, use stack build.

If you insist to use cabal instead, we recommend at least to use a sandbox. Initialize the sandbox and configure the project via

cabal sandbox init && cabal configure

Then use cabal build or cabal install to build or install the tool.

Note that (independent of the chosen build method) building the tool will only create the final executable in a hidden sub-folder, which might get cumbersome for development or testing local changes. Hence, for this purpose, you may prefer to use make. The makefile determines the chosen build method, rebuilds the package, and copies the final syfco executable to the root directory of the project.

If you still encounter any problems, please inform us via the project bug tracker.

Usage

syfco [OPTIONS]...

File Operations:

Command	Description
-o, --output	path of the output file (results are printed to STDOUT if not set)
-r, --read-config	read parameters from the given configuration file (may overwrite prior arguments)
-w, --write-config	write the current configuration to the given path (includes later arguments)
-f, --format	output format - possible values are: full input file with applied transformations (default) basic high level format (without global section) utf8 human readable output using UTF8 symbols wring Wring input format lily Lily input format acacia Acacia / Acacia+ input format acacia-specs Acacia input format with spec units ltlxba LTL2BA / LTL3BA input format ltlxba-decomp LTL2BA / LTL3BA input format (decomposed) ltl pure LTL formula promela Promela LTL unbeast Unbeast input format slugs structured Slugs format [GR(1) only] slugsin SlugsIn format [GR(1) only] psl PSL Syntax smv SMV file format smv-decomp SMV file format (decomposed) bosy Bosy input format rabinizer Rabinizer input format
-m, --mode	output mode - possible values are: pretty pretty printing (as less parentheses as possible) (default) fully output fully parenthesized formulas
-q, --quote	quote mode - possible values are: none identifiers are not quoted (default) double identifiers are quoted using "
-pf, --part-file	create a partitioning (.part) file
-bd, --bus-delimiter	delimiter used to print indexed bus signals (default: _)
-ps, --prime-symbol	symbol/string denoting primes in signals (default: ')
-as, --at-symbol	symbol/string denoting @-symbols in signals (default: @)
-in, --stdin	read the input file from STDIN

File Modifications:

Command	Description
-os, --overwrite-semantics	overwrite the semantics of the file
-ot, --overwrite-target	overwrite the target of the file
-op, --overwrite-parameter	overwrite a parameter of the file

Formula Transformations (disabled by default):

Command	Description
-s0, --weak-simplify	simple simplifications (removal of true/false in boolean connectives, redundant temporal operators, etc.)
-s1, --strong-simplify	advanced simplifications (includes: -s0 -nnf -nw -nr -pgo -pfo -pxo)
-nnf, --negation-normal-form	convert the resulting LTL formula into negation normal form
-pgi, --push-globally-inwards	push global operators inwards G (a && b) => (G a) && (G b)
-pfi, --push-finally-inwards	push finally operators inwards F (a || b) => (F a) || (F b)
-pxi, --push-next-inwards	push next operators inwards X (a && b) => (X a) && (X b) X (a || b) => (X a) || (X b)
-pgo, --pull-globally-outwards	pull global operators outwards (G a) && (G b) => G (a && b)
-pfo, --pull-finally-outwards	pull finally operators outwards (F a) || (F b) => F (a || b)
-pxo, --pull-next-outwards	pull next operators outwards (X a) && (X b) => X (a && b) (X a) || (X b) => X (a || b)
-nw, --no-weak-until	replace weak until operators a W b => (a U b) || (G a)
-nr, --no-release	replace release operators a R b => b W (a && b)
-nf, --no-finally	replace finally operators F a => true U a
-ng, --no-globally	replace global operators G a => false R a
-nd, --no-derived	same as: -nw -nf -ng

Check Specification Type (and exit):

Command	Description
-gr, --generalized-reactivity	check whether the input is in the Generalized Reactivity fragment

Extract Information (and exit):

Command	Description
-c, --check	check that input conforms to TLSF
-t, --print-title	output the title of the input file
-d, --print-description	output the description of the input file
-s, --print-semantics	output the semantics of the input file
-g, --print-target	output the target of the input file
-a, --print-tags	output the target of the input file
-p, --print-parameters	output the parameters of the input file
-i, --print-info	output all data of the info section
-ins, --print-input-signals	output the input signals of the specification
-outs, --print-output-signals	output the output signals of the specification
-v, --version	output version information
-h, --help	display this help

Sample Usage:

syfco -o converted -f promela -m fully -nnf -nd file.tlsf
syfco -f psl -op n=3 -os Strict,Mealy -o converted file.tlsf
syfco -o converted -in
syfco -t file.tlsf

Examples

A number of synthesis benchmarks in TLSF can be found in the /examples directory.

Syfco Library

Syfco is also provided as a Haskell library. In fact, the syfco executable is nothing different than a fancy command line interface to this library. If you are interested in using the interface, we recommend to build and check the interface documentation, which is generated by:

make haddock

Editor Support

If you use Emacs, you should try our emacs mode (tlsf-mode.el), which can be found in the /misc directory.

Adding output formats

If you like to add a new output format, first consider /Writer/Formats/Example.hs, which contains the most common standard constructs and a short tutorial.