Skip to content

Commit d8bd4c9

Browse files
author
Felix Klein
committed
Syfco 1.0 Release
1 parent 00f4532 commit d8bd4c9

File tree

4 files changed

+81
-32
lines changed

4 files changed

+81
-32
lines changed

Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ profile: ${MAIN.hs}
3535
@mkdir -p ${BLDDIR}
3636
@ghc -prof -fprof-auto -idir1:src ${GHCFLAGS} ${MAIN} -odir ${BLDDIR} -hidir ${BLDDIR} -o ${NAME}
3737
@strip ${NAME}
38-
@echo -e '#!/bin/bash\n\n./syfco +RTS -p -RTS $${*}' > ${NAME}_profile
38+
@echo -e '#!/bin/bash\n\n./${NAME} +RTS -p -RTS $${*}' > ${NAME}_profile
3939
@chmod +x ${NAME}_profile
4040

4141
static:

README

Lines changed: 46 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
11
# Synthesis Format Conversion Tool
2-
# (Version 0.1.0.3)
2+
# (Version 1.0.0.0)
33

44
A tool for reading, manipulating and transforming synthesis
5-
specifications in TLSF (Temporal Logic Synthesis Format).
5+
specifications in TLSF [1].
66

77
## About this tool
88

9-
The tool interprets the high level constructs of TLSF (functions,
9+
The tool interprets the high level constructs of TLSF 1.1 (functions,
1010
sets, ...) and supports the transformation of the specification to
1111
Linear Temporal Logic (LTL) in different output formats. The tool has
1212
been designed to be modular with respect to the supported output
1313
formats and semantics. Furthermore, the tool allows to identify and
14-
manipulate parameters, targets and semantics of a specification on the
14+
manipulate parameters, targets and semantics of a specification on the
1515
fly. This is especially thought to be useful for comparative studies,
16-
as they are for example needed in the Synthesis Competition.
16+
as they are for example needed in the Synthesis Competition [2].
1717

1818
The main features of the tool are summarized as follows:
1919

@@ -22,7 +22,10 @@ The main features of the tool are summarized as follows:
2222
variable bindings occur (i.e., without the GLOBAL section).
2323

2424
* Transformation to other existing specification formats, like Basic
25-
TLSF, Promela LTL, PSL, Unbeast or Wring.
25+
TLSF, Promela LTL [3], PSL [4], Unbeast [5], Wring [6] or Slugs [7].
26+
27+
* Syntactical analysis of membership in GR(k) for any k (modulo
28+
boolean identities).
2629

2730
* On the fly adjustment of parameters, semantics or targets.
2831

@@ -44,11 +47,21 @@ Haskell Compiler (GHC).
4447

4548
Prerequisites:
4649

47-
* GHC (recommended version: >= 7.0.1, Haskell2010)
50+
* GHC [8] (recommended version: >= 7.0.1, Haskell2010 [9])
4851

49-
* parsec (recommended version: >= 3.1)
52+
* parsec [10] (recommended version: >= 3.1)
53+
54+
* array [11] (recommended version: >= 0.5)
55+
56+
* containers [12] (recommended version: >= 0.5)
57+
58+
* directory [13] (recommended version: >= 1.2)
5059

51-
Building the tool should be simple using cabal
60+
* mtl [14] (recommended version: >= 2.2)
61+
62+
* transformers [15] (recommended version: >= 0.4)
63+
64+
Building the tool should be simple using cabal [16]
5265

5366
cabal install
5467

@@ -57,8 +70,9 @@ or, if you work in a UNIX environment, simply by using
5770
make
5871

5972
However, if you encounter any problems, pleaseinform us via the
60-
project bug tracker
61-
(https://github.com/reactive-systems/syfco/issues).
73+
project bug tracker:
74+
75+
https://github.com/reactive-systems/syfco/issues
6276

6377
## Usage
6478

@@ -167,11 +181,31 @@ directory.
167181

168182
## Editor Support
169183

170-
If you use Emacs, you should try our emacs mode (tlsf-mode.el), which can
184+
If you use Emacs [17], you should try our emacs mode (tlsf-mode.el), which can
171185
be found in the /misc directory.
172186

173187
## Adding output formats
174188

175189
If you like to add a new output format, first consider
176190
/Writer/Formats/Example.hs, which contains the most common standard
177191
constructs and a short tutorial.
192+
193+
--------------------------------------------------
194+
195+
[1] https://arxiv.org/abs/1604.02284
196+
[2] http://www.syntcomp.org
197+
[3] http://spinroot.com/spin/Man/ltl.html
198+
[4] https://en.wikipedia.org/wiki/Property_Specification_Language
199+
[5] https://www.react.uni-saarland.de/tools/unbeast
200+
[6] http://www.ist.tugraz.at/staff/bloem/wring.html
201+
[7] https://github.com/VerifiableRobotics/slugs
202+
[8] https://www.haskell.org/ghc
203+
[9] https://wiki.haskell.org/Definition
204+
[10] https://hackage.haskell.org/package/parsec
205+
[11] https://hackage.haskell.org/package/array
206+
[12] https://hackage.haskell.org/package/containers
207+
[13] https://hackage.haskell.org/package/directory
208+
[14] https://hackage.haskell.org/package/mtl
209+
[15] https://hackage.haskell.org/package/transformers
210+
[16] https://www.haskell.org/cabal
211+
[17] https://www.gnu.org/software/emacs

README.md

Lines changed: 32 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,20 @@
1-
# Synthesis Format Conversion Tool<br/>(Version 0.1.0.3)
1+
# Synthesis Format Conversion Tool<br/>(Version 1.0.0.0)
22

33
A tool for reading, manipulating and transforming synthesis
4-
specifications in TLSF (Temporal Logic Synthesis Format).
4+
specifications in [TLSF](https://arxiv.org/abs/1604.02284).
55

66
## About this tool
77

8-
The tool interprets the high level constructs of TLSF (functions,
9-
sets, ...) and supports the transformation of the specification to
10-
Linear Temporal Logic (LTL) in different output formats. The tool has
11-
been designed to be modular with respect to the supported output
12-
formats and semantics. Furthermore, the tool allows to identify and
13-
manipulate parameters, targets and semantics of a specification on the
14-
fly. This is especially thought to be useful for comparative studies,
15-
as they are for example needed in the [Synthesis
16-
Competition](http://www.syntcomp.org/).
8+
The tool interprets the high level constructs of
9+
[TLSF 1.1](https://arxiv.org/abs/1604.02284)
10+
(functions, sets, ...) and supports the transformation of the
11+
specification to Linear Temporal Logic (LTL) in different output
12+
formats. The tool has been designed to be modular with respect to the
13+
supported output formats and semantics. Furthermore, the tool allows
14+
to identify and manipulate parameters, targets and semantics of a
15+
specification on the fly. This is especially thought to be useful for
16+
comparative studies, as they are for example needed in the [Synthesis
17+
Competition](http://www.syntcomp.org).
1718

1819
The main features of the tool are summarized as follows:
1920

@@ -24,8 +25,12 @@ The main features of the tool are summarized as follows:
2425
* Transformation to other existing specification formats, like Basic
2526
TLSF, [Promela LTL](http://spinroot.com/spin/Man/ltl.html),
2627
[PSL](https://en.wikipedia.org/wiki/Property_Specification_Language),
27-
[Unbeast](https://www.react.uni-saarland.de/tools/unbeast/) or
28-
[Wring](http://www.ist.tugraz.at/staff/bloem/wring.html).
28+
[Unbeast](https://www.react.uni-saarland.de/tools/unbeast),
29+
[Wring](http://www.ist.tugraz.at/staff/bloem/wring.html) or
30+
[Slugs](https://github.com/VerifiableRobotics/slugs).
31+
32+
* Syntactical analysis of membership in GR(k) for any k (modulo
33+
boolean identities).
2934

3035
* On the fly adjustment of parameters, semantics or targets.
3136

@@ -45,11 +50,21 @@ SyfCo is written in Haskell and can be compiled using the Glasgow Haskell Compil
4550

4651
Prerequisites:
4752

48-
* [GHC](https://www.haskell.org/ghc/) (recommended version: >= 7.0.1, [Haskell2010](https://wiki.haskell.org/Definition))
53+
* [GHC](https://www.haskell.org/ghc) (recommended version: >= 7.0.1, [Haskell2010](https://wiki.haskell.org/Definition))
4954

50-
* [parsec](https://hackage.haskell.org/package/parsec-3.1.0) (recommended version: >= 3.1)
55+
* [parsec](https://hackage.haskell.org/package/parsec) (recommended version: >= 3.1)
56+
57+
* [array](https://hackage.haskell.org/package/array) (recommended version: >= 0.5)
58+
59+
* [containers](https://hackage.haskell.org/package/containers) (recommended version: >= 0.5)
60+
61+
* [directory](https://hackage.haskell.org/package/directory) (recommended version: >= 1.2)
62+
63+
* [mtl](https://hackage.haskell.org/package/mtl) (recommended version: >= 2.2)
64+
65+
* [transformers](https://hackage.haskell.org/package/transformers) (recommended version: >= 0.4)
5166

52-
Building the tool should be simple using [cabal](https://www.haskell.org/cabal/)
67+
Building the tool should be simple using [cabal](https://www.haskell.org/cabal)
5368

5469
<code>cabal install</code>
5570

@@ -140,7 +155,7 @@ A number of synthesis benchmarks in TLSF can be found in the
140155

141156
## Editor Support
142157

143-
If you use [Emacs](https://www.gnu.org/software/emacs/), you should try our emacs mode (```tlsf-mode.el```),
158+
If you use [Emacs](https://www.gnu.org/software/emacs), you should try our emacs mode (```tlsf-mode.el```),
144159
which can be found in the ```/misc``` directory.
145160

146161
## Adding output formats

syfco.cabal

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
name: syfco
2-
version: 0.1.0.3
2+
version: 1.0.0.0
33
synopsis: A tool for reading, manipulating and transforming synthesis specifications.
44
description: Synthesis Format Conversion Tool
55
license: MIT
66
license-file: LICENSE
77
author: Felix Klein <[email protected]>
88
maintainer: Felix Klein <[email protected]>
9-
stability: alpha
9+
stability: stable
1010
category: SyntComp
1111
homepage: https://github.com/reactive-systems/syfco
1212
bug-reports: https://github.com/reactive-systems/syfco/issues

0 commit comments

Comments
 (0)