Download The LTL Checker Plugins a (reference) manual

Contents
1 Introduction
2 Use
2.1
2.2
2.3
2.4
2.5
2.6
2.7
2.8
2.9
3
of the LTL Checker Plugins
Introduction . . . . . . . . . . . . . . . . .
Importing LTL Template Files . . . . . .
Using the stand alone LTL Parser . . . .
Starting the Default LTL Checker Plugin
Starting The LTL Checker Plugin . . . . .
Using the Template GUI . . . . . . . . . .
Viewing the Results . . . . . . . . . . . .
Exporting the Results . . . . . . . . . . .
Reusing the results . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4
4
5
7
8
9
10
13
14
14
3 LTL Language
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . .
3.2 The Environment in which the Language operates
3.2.1 A running Example . . . . . . . . . . . . .
3.3 Definitions and Comments . . . . . . . . . . . . . .
3.3.1 Comments . . . . . . . . . . . . . . . . . . .
3.3.2 Attribute Definitions . . . . . . . . . . . . .
3.3.3 Renaming of defined Attributes . . . . . . .
3.3.4 Formula Definitions . . . . . . . . . . . . .
3.4 Formula calls . . . . . . . . . . . . . . . . . . . . .
3.5 Comparisons . . . . . . . . . . . . . . . . . . . . .
3.5.1 Standard comparisons . . . . . . . . . . . .
3.5.2 The string type operators and literals . . .
3.5.3 The set type operators and literals . . . . .
3.5.4 The date type literals . . . . . . . . . . . .
3.5.5 The number type literals and expressions .
3.5.6 Examples . . . . . . . . . . . . . . . . . . .
3.5.7 Parse errors . . . . . . . . . . . . . . . . . .
3.6 Propositional Logic . . . . . . . . . . . . . . . . . .
3.6.1 Not . . . . . . . . . . . . . . . . . . . . . .
3.6.2 And . . . . . . . . . . . . . . . . . . . . . .
3.6.3 Or . . . . . . . . . . . . . . . . . . . . . . .
3.6.4 Implication . . . . . . . . . . . . . . . . . .
3.6.5 Bi-implication . . . . . . . . . . . . . . . . .
3.6.6 Examples . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
17
17
17
19
19
19
20
23
24
26
28
29
30
31
31
31
31
32
33
33
34
34
34
35
35
1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.