Skip to content

reactive-systems/syfco

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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:
fullinput file with applied transformations (default)
basichigh level format (without global section)
utf8human readable output using UTF8 symbols
wringWring input format
lilyLily input format
acaciaAcacia / Acacia+ input format
acacia-specsAcacia input format with spec units
ltlxbaLTL2BA / LTL3BA input format
ltlxba-finLTL2BA / LTL3BA input format (finite words)
ltlxba-decompLTL2BA / LTL3BA input format (decomposed)
ltlpure LTL formula
promelaPromela LTL
unbeastUnbeast input format
slugsstructured Slugs format [GR(1) only]
slugsinSlugsIn format [GR(1) only]
pslPSL Syntax
smvSMV file format
smv-decompSMV file format (decomposed)
bosyBosy input format
rabinizerRabinizer input format
-m, --mode output mode - possible values are:
prettypretty printing (as less parentheses as possible) (default)
fullyoutput fully parenthesized formulas
-q, --quote quote mode - possible values are:
noneidentifiers are not quoted (default)
doubleidentifiers 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.