genltl.test 4.07 KB
Newer Older
1
2
#!/bin/sh
# -*- coding: utf-8 -*-
3
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot 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 3 of the License, or
# (at your option) any later version.
#
# Spot 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, see <http://www.gnu.org/licenses/>.

. ./defs
set -e

24
25
26
27
28
29
30
31
# Make sure the name of each pattern is correctly output by %F.
opts=`genltl --help | sed -n '/=RANGE/{
s/^ *//
s/[=[].*/=1/p
}'`
res=`genltl $opts --format="--%F=%L"`
test "$opts" = "$res"

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
run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output
cat >expected <<EOF
dac-patterns:1 G!p0
!dac-patterns:1 !G!p0
dac-patterns:2 Fp0 -> (!p1 U p0)
!dac-patterns:2 !(Fp0 -> (!p1 U p0))
dac-patterns:3 G(p0 -> G!p1)
!dac-patterns:3 !G(p0 -> G!p1)
dac-patterns:4 G((p0 & !p1 & Fp1) -> (!p2 U p1))
!dac-patterns:4 !G((p0 & !p1 & Fp1) -> (!p2 U p1))
dac-patterns:5 G((p0 & !p1) -> (!p2 W p1))
!dac-patterns:5 !G((p0 & !p1) -> (!p2 W p1))
eh-patterns:1 p0 U (p1 & Gp2)
!eh-patterns:1 !(p0 U (p1 & Gp2))
eh-patterns:2 p0 U (p1 & X(p2 U p3))
!eh-patterns:2 !(p0 U (p1 & X(p2 U p3)))
eh-patterns:3 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
!eh-patterns:3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))))
eh-patterns:4 F(p0 & XGp1)
!eh-patterns:4 !F(p0 & XGp1)
eh-patterns:5 F(p0 & X(p1 & XFp2))
!eh-patterns:5 !F(p0 & X(p1 & XFp2))
EOF
diff expected output

genltl --dac=1..5 --eh=1..5 --neg --format="%L %f" >output
cat >expected <<EOF
1 !G!p0
2 !(Fp0 -> (!p1 U p0))
3 !G(p0 -> G!p1)
4 !G((p0 & !p1 & Fp1) -> (!p2 U p1))
5 !G((p0 & !p1) -> (!p2 W p1))
1 !(p0 U (p1 & Gp2))
2 !(p0 U (p1 & X(p2 U p3)))
3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))))
4 !F(p0 & XGp1)
5 !F(p0 & X(p1 & XFp2))
EOF
diff expected output

genltl --dac=1..5 --eh=1..5 --pos --format="%f" >output
cat >expected <<EOF
G!p0
Fp0 -> (!p1 U p0)
G(p0 -> G!p1)
G((p0 & !p1 & Fp1) -> (!p2 U p1))
G((p0 & !p1) -> (!p2 W p1))
p0 U (p1 & Gp2)
p0 U (p1 & X(p2 U p3))
p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
F(p0 & XGp1)
F(p0 & X(p1 & XFp2))
EOF
diff expected output

genltl --dac=1..5 --eh=1..5 >output2
diff output output2
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110


genltl --tv-f1=1:3 --tv-f2=1:3 --tv-g1=1:3 --tv-g2=1:3 --tv-uu=1:3 \
       --format=%F,%L,%f >output
cat >expected <<EOF
tv-f1,1,G(p -> q)
tv-f1,2,G(p -> (q | Xq))
tv-f1,3,G(p -> (q | Xq | XXq))
tv-f2,1,G(p -> q)
tv-f2,2,G(p -> (q | Xq))
tv-f2,3,G(p -> (q | X(q | Xq)))
tv-g1,1,G(p -> q)
tv-g1,2,G(p -> (q & Xq))
tv-g1,3,G(p -> (q & Xq & XXq))
tv-g2,1,G(p -> q)
tv-g2,2,G(p -> (q & Xq))
tv-g2,3,G(p -> (q & X(q & Xq)))
tv-uu,1,G(p1 -> (p1 U p2))
tv-uu,2,G(p1 -> (p1 U (p2 & (p2 U p3))))
tv-uu,3,G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U p4))))))
EOF
diff output expected
111

112

113
114
genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
       --format=%F=%L,%f |
115
116
117
118
119
120
121
122
    ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
cat >exp<<EOF
kv-psi=1,15
kv-psi=2,106
kr-nlogn=1,19
kr-nlogn=2,147
kr-n=1,12
kr-n=2,82
123
124
125
126
127
128
129
130
gxf-and=0,1
gxf-and=1,1
gxf-and=2,1
gxf-and=3,1
fxg-or=0,2
fxg-or=1,3
fxg-or=2,4
fxg-or=3,5
131
132
EOF
diff out exp
133
134
135
136

test $(genltl --kr-n2=4 | ltl2tgba --low --stats=%s) -ge 16
test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16
test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159

genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
       --format=%F=%L,%f |
    ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
cat >exp<<EOF
ms-example=0,1
ms-example=1,2
ms-example=2,4
ms-example=3,7
ms-example=4,12
ms-phi-r=0,2
ms-phi-r=1,16
ms-phi-r=2,25
ms-phi-s=0,5
ms-phi-s=1,7
ms-phi-s=2,1322
ms-phi-h=0,2
ms-phi-h=1,4
ms-phi-h=2,21
ms-phi-h=3,170
ms-phi-h=4,1816
EOF
diff out exp