-
Notifications
You must be signed in to change notification settings - Fork 2
/
README
104 lines (81 loc) · 3.38 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
1. ABOUT
The libltl2ba software is a modification of LTL2BA and incorporates the changes
from LTL2C. It aims at making the functionality of both available in form of a
library while maintaining compatibility with the original algorithms.
For bug-reports and/or questions about libltl2ba, please contact Franz Brauße:
LTL2C has been written by Jeremy Morse. It is based on LTL2BA version 1.1 and
adds output formats for dot and the ESBMC model checker.
LTL2BA has originally been written by Denis Oddoux and was modified by Paul
Gastin. It is based on the translation algorithm presented at CAV '01:
P.Gastin and D.Oddoux
"Fast LTL to Büchi Automata Translation"
in 13th International Conference on Computer Aided Verification, CAV 2001,
G. Berry, H. Comon, A. Finkel (Eds.)
Paris, France, July 18-22, 2001,
Proceedings - LNCS 2102, pp. 53-65
Part of the code included is issued from the SPIN software Version 3.4.1
The SPIN software is written by Gerard J. Holzmann, originally as part
of ``Design and Validation of Protocols,'' ISBN 0-13-539925-4,
1991, Prentice Hall, Englewood Cliffs, NJ, 07632
Here are the files that contain some code from Spin v3.4.1 :
cache.c (originally tl_cache.c)
lex.c ( tl_lex.c )
ltl2ba.h ( tl.h )
main.c ( tl_main.c )
mem.c. ( tl_mem.c )
parse.c ( tl_parse.c)
rewrt.c ( tl_rewrt.c)
2. COMPILING
unpack the archive:
> tar -xzf libltl2ba-2.0.tar.gz
> cd libltl2ba-2.0
compile the program
> make
3. EXECUTING
run the program
> ./ltl2ba -f 'formula'
The formula is an LTL formula, and may contain propositional symbols,
boolean operators, temporal operators, and parentheses. The syntax is a
backwards-compatible extension of the one used in the 'Spin' model-checker.
Propositonal Symbols:
true, false
any lowercase string
{C expression}
Boolean operators:
!, NOT (negation)
-> (implication)
<-> (equivalence)
&&, /\ (and)
||, \/ (or)
Temporal operators:
G, [] (always)
F, <> (eventually)
U (until)
V (release)
X (next)
Use spaces between any symbols. Unary operators bind stronger than binary ones.
Precedence (high to low) and associativity of binary operators is as follows:
U, V : right
&& : left
|| : left
<-> : none
-> : right
The result is a 'never' claim in Promela that can be given to the Spin model
checker to verify properties on a system.
run the command
> ./ltl2ba -h
to see the possible options for executing the program
4. LICENSE
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version. GNU GPL is included in this
distribution, in a file called 'LICENSE'
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA