forked from tfiedor/gaston
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME
112 lines (86 loc) · 3.87 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
**
* Gaston - Novel Decision Procedure for WS1S Logic
*
* Copyright (c) 2015 Tomas Fiedor <ifiedortom@fit.vutbr.cz>
**************************************************************
* About *
*********
Gaston is an implementation of backward decision procedure for WSkS logic
(weak second-order theory of k successors). The tool is using libvata a
highly optimised non-deterministic finite tree automata library that supports
semi-symbolic encoding using multi-terminal binary decision diagrams (MTBDDs) for
storing transition table of the automaton. Procedure generates state space on-the-fly
and prunes the states using the antichain-based approach. State space is represented
by downward and upward closed represenation of states. The tool computes the
representation of final states and test if initial states are included in final states
and thus (dis)prove validity.
* Prerequisities *
******************
Following packages are needed in order to compile and run Gaston on your system:
git (>= 1.6.0.0)
cmake (>= 2.8.2)
gcc (>= 4.8.0)
flex (>= 2.5.35)
bison (>= 2.7.1)
* Download *
************
In order to compile and work with our tool we highly recommend to clone the repository
to the local repository. You need to have the git version control system installed.
To download the library, run
$ git clone https://github.com/tfiedor/Gaston.git
* Compilation *
***************
In order to prepare the tool for compilation and commiting a background check for
prerequisite package issue the following command in the root directory of the tool:
$ cmake CMakeLists.txt
To further compile the source files to runable binary issue the following command:
$ make
* Input file syntax *
*********************
The following grammar describes supported subset of MONA syntax
for the specification of verified formulae. It uses the classical BNF-like
notation.
For full syntax for MONA tool consult the tool manual at http://www.brics.dk/mona/mona14.pdf.
program ::= (header;)? (declaration;)+
header ::= ws1s | ws2s
declaration ::= formula
| var0 (varname)+
| var1 (varname)+
| var2 (varname)+
| 'pred' varname (params)? = formula
| 'macro' varname (params)? = formula
formula ::= 'true' | 'false' | (formula)
| zero-order-var
| ~formula
| formula | formula
| formula & formula
| formula => formula
| formula <=> formula
| first-order-term = first-order-term
| first-order-term ~= first-order-term
| first-order-term < first-order-term
| first-order-term > first-order-term
| first-order-term <= first-order-term
| first-order-term >= first-order-term
| second-order-term = second-order-term
| second-order-term = { (int)+ }
| second-order-term ~= second-order-term
| second-order-term 'sub' second-order-term
| first-order-term 'in' second-order-term
| ex1 (varname)+ : formula
| all1 (varname)+ : formula
| ex2 (varname)+ : formula
| all2 (varname)+ : formula
first-order-term ::= varname | (first-order-term)
| int
| first-order-term + int
second-order-term ::= varname | (second-order-term)
| second-order-term + int
* Contact *
***********
If you have any questions, do not hesitate to contact the tool/method authors:
* Tomas Fiedor <ifiedortom@fit.vutbr.cz> (corresponding author of Gaston)
* Lukas Holik <holik@fit.vutbr.cz>
* Petr Janku <ijanku@fit.vutbr.cz> (optimizations of MONA wrapper)
* Ondrej Lengal <ilengal@fit.vutbr.cz> (corresponding author of VATA)
* Tomas Vojnar <vojnar@fit.vutbr.cz>