A tool for reading, manipulating and transforming synthesis specifications in TLSF.
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.
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.
syfco [OPTIONS]...
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:
|
||||||||||||||||||||||||||||||||||||||
-m, --mode |
output mode - possible values are:
|
||||||||||||||||||||||||||||||||||||||
-q, --quote |
quote mode - possible values are:
|
||||||||||||||||||||||||||||||||||||||
-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 |
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 |
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 inwardsG (a && b) => (G a) && (G b) |
-pfi, --push-finally-inwards |
push finally operators inwardsF (a || b) => (F a) || (F b) |
-pxi, --push-next-inwards |
push next operators inwardsX (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 operatorsa W b => (a U b) || (G a) |
-nr, --no-release |
replace release operatorsa R b => b W (a && b) |
-nf, --no-finally |
replace finally operatorsF a => true U a |
-ng, --no-globally |
replace global operatorsG a => false R a |
-nd, --no-derived |
same as: -nw -nf -ng |
Command | Description |
---|---|
-gr, --generalized-reactivity |
check whether the input is in the Generalized Reactivity fragment |
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 |
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
A number of synthesis benchmarks in TLSF can be found in the
/examples
directory.
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
If you use Emacs, you should try our emacs mode (tlsf-mode.el
),
which can be found in the /misc
directory.
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.