forked from yzh89/MITL2Timed
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
114 lines (87 loc) · 4.15 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
MITL2Timed - transforms a MITL formula to a timed automaton based on LTL2BA. Forked from
https://github.com/slivingston/ltl2gba.
Modified by Yuchen Zhou, University of Maryland, USA.
Copyright (c) 2015 Yuchen Zhou
Available at https://github.com/yzh89/MITL2ta
1. LICENSE OF LTL2BA
LTL2BA - Version 1.0 - October 2001
Written by Denis Oddoux, LIAFA, France
Copyright (c) 2001 Denis Oddoux
LTL2BA - Version 1.1 - August 2007
Modified by Paul Gastin, LSV, France
Copyright (c) 2007 Paul Gastin
Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba
Modified by Scott C. Livingston, Caltech, USA.
Copyright (c) 2013 Scott C. Livingston
Available at https://github.com/slivingston/ltl2gba.
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
The LTL2BA software was written by Denis Oddoux and 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
Send bug-reports and/or questions to Paul Gastin
http://www.lsv.ens-cachan.fr/~gastin
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)
trans.c ( tl_trans.c)
2. Changes for MITL2Timed
Main changes is the addition of file timed.c to create the timed automata based on MITL.
parse.c and trans.c is modified according to parse the input and generate the output correctly.
Additional python scripts are generated alone the way to create UPPAAL models for model checking.
3. COMPILING
compile the program
> make
4. EXECUTING (for MITL2Timed)
run the program
> ./mitl2ta -f "formula"
The formula is an MITL formula, and may contain propositional symbols,
boolean operators, temporal operators, and parentheses.
The syntax used is the one used in the 'Spin' model-checker
Propositonal Symbols:
true, false
any lowercase string
Boolean operators:
! (negation)
-> (implication)
<-> (equivalence)
&& (and)
|| (or)
Temporal operators:
[] (always)
<> (eventually)
U (until)
V (release)
X (next)
<>_[l,r] (eventually with interval l to r)
[]_[l,r] (always with interval l to r)
Use spaces between any symbols.
5. Map information is hard coded at current stage.
The robot can move up or down and right or left if there is any. It can
be easily extends to larger grid.
pos0 pos1:b
pos2:a pos3