forked from reactive-systems/syfco
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
249 lines (189 loc) · 10.4 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
# Synthesis Format Conversion Tool
# (Version 1.2.1.2)
A tool for reading, manipulating and transforming synthesis
specifications in TLSF [0].
## About this tool
The tool interprets the high level constructs of TLSF 1.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 [2].
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 [3], PSL [4], Unbeast [5], Wring [6],
structured Slugs [7], and SlugsIn [8].
* 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 [9] or stack [10] (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 [11] 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:
https://github.com/reactive-systems/syfco/issues
## Usage
syfco [OPTIONS]... <file>
### File Operations:
-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 [default] : input file with applied transformations
* 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 [default] : pretty printing (as less parentheses as
possible)
* fully : output fully parenthesized formulas
-q, --quote : quote mode - possible values are:
* none [default] : identifiers are not quoted
* 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:
-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):
-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):
-gr, --generalized-reactivity : check whether the input is in the Generalized
Reactivity fragment
### Extract Information (and exit):
-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 [12], 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.
--------------------------------------------------
[0] https://arxiv.org/abs/1604.02284
[1] https://arxiv.org/abs/1604.02284
[2] http://www.syntcomp.org
[3] http://spinroot.com/spin/Man/ltl.html
[4] https://en.wikipedia.org/wiki/Property_Specification_Language
[5] https://www.react.uni-saarland.de/tools/unbeast
[6] http://www.ist.tugraz.at/staff/bloem/wring.html
[7] https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#structuredslugs
[8] https://github.com/VerifiableRobotics/slugs/blob/master/doc/input_formats.md#slugsin
[9] https://www.haskell.org/cabal
[10] https://docs.haskellstack.org/en/stable/README/
[11] https://www.fpcomplete.com/blog/2015/06/why-is-stack-not-cabal
[12] https://www.gnu.org/software/emacs