1# -*- mode: python; coding: utf-8 -*-
2# Copyright (C) 2009-2012, 2014-2017, 2019, 2021 Laboratoire de Recherche et
3# Développement de l'Epita (LRDE).
4# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5# département Systèmes Répartis Coopératifs (SRC), Université Pierre
6# et Marie Curie.
7#
8# This file is part of Spot, a model checking library.
9#
10# Spot is free software; you can redistribute it and/or modify it
11# under the terms of the GNU General Public License as published by
12# the Free Software Foundation; either version 3 of the License, or
13# (at your option) any later version.
14#
15# Spot is distributed in the hope that it will be useful, but WITHOUT
16# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
18# License for more details.
19#
20# You should have received a copy of the GNU General Public License
21# along with this program.  If not, see <http://www.gnu.org/licenses/>.
22
23import sys
24import spot
25
26e = spot.default_environment.instance()
27
28l = [('GFa', False),
29     ('a U (((b)) xor c)', False),
30     ('!(FFx <=> Fx)', True),
31     ('a \\/ a \\/ b \\/ a \\/ a', False)]
32
33
34for str1, isl in l:
35    pf = spot.parse_infix_psl(str1, e, False)
36    if pf.format_errors(spot.get_cout()):
37        sys.exit(1)
38    str2 = str(pf.f)
39    del pf
40    # Try to reparse the stringified formula
41    pf = spot.parse_infix_psl(str2, e)
42    if pf.format_errors(spot.get_cout()):
43        sys.exit(1)
44    assert isl == pf.f.is_leaf()
45    del pf
46
47assert spot.formula('a').is_leaf()
48assert spot.formula('0').is_leaf()
49
50for str1 in ['a * b', 'a xor b', 'a <-> b']:
51    pf = spot.parse_infix_boolean(str1, e, False)
52    if pf.format_errors(spot.get_cout()):
53        sys.exit(1)
54    str2 = str(pf.f)
55    del pf
56    # Try to reparse the stringified formula
57    pf = spot.parse_infix_boolean(str2, e)
58    if pf.format_errors(spot.get_cout()):
59        sys.exit(1)
60    del pf
61
62for (x, op) in [('a* <-> b*', "`<->'"),
63                ('a* -> b', "`->'"),
64                ('a ^ b*', "`^'"),
65                ('!(b*)', "`!'"),
66                ('a*[=2]', "[=...]"),
67                ('a*[->2]', "[->...]")]:
68    f5 = spot.parse_infix_sere(x)
69    assert f5.errors
70    ostr = spot.ostringstream()
71    f5.format_errors(ostr)
72    err = ostr.str()
73    assert "not a Boolean expression" in err
74    assert op in err
75    assert "SERE" in err
76    del f5
77
78f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]')
79assert not f6.errors
80del f6
81
82f6 = spot.parse_infix_sere('-')
83assert f6.errors
84del f6
85
86for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
87                 ('{foo[->', 'missing closing bracket for goto operator'),
88                 ('{foo[->3..1]}', "reversed range"),
89                 ('{foo[*bug]}', "treating this star block as [*]"),
90                 ('{foo[*bug', "missing closing bracket for star"),
91                 ('{foo[*3..1]}', "reversed range"),
92                 ('{[*3..1]}', "reversed range"),
93                 ('{foo[:*bug]}', "treating this fusion-star block as [:*]"),
94                 ('{foo[:*3..1]}', "reversed range"),
95                 ('{foo[:*bug', "missing closing bracket for fusion-star"),
96                 ('{foo[=bug]}', "treating this equal block as [=]"),
97                 ('{foo[=bug', "missing closing bracket for equal operator"),
98                 ('{foo[=3..1]}', "reversed range"),
99                 ('{()}', "treating this brace block as false"),
100                 ('{(a b)}', "treating this parenthetical block as false"),
101                 ('{(a*}', "missing closing parenthesis"),
102                 ('{(a*&)}', "missing right operand for "
103                  + "\"non-length-matching and operator\""),
104                 ('{(a*&&)}', "missing right operand for "
105                  + "\"length-matching and operator\""),
106                 ('{(a*|)}', "missing right operand for \"or operator\""),
107                 ('{a*;}', "missing right operand for \"concat operator\""),
108                 ('{a*::b}', "missing right operand for \"fusion operator\""),
109                 ('{a* xor }', "missing right operand for \"xor operator\""),
110                 ('{a* -> }', "missing right operand for "
111                  + "\"implication operator\""),
112                 ('{a <-> <-> b }',
113                  "missing right operand for \"equivalent operator\""),
114                 ('{a;b b}', "ignoring this"),
115                 ('{*', "missing closing brace"),
116                 ('{(a', "missing closing parenthesis"),
117                 ('{* a',
118                  "ignoring trailing garbage and missing closing brace"),
119                 ('F(a b)', "ignoring this"),
120                 ('F(-)', "treating this parenthetical block as false"),
121                 ('F(', "missing closing parenthesis"),
122                 ('F(a b', "ignoring trailing garbage and "
123                  + "missing closing parenthesis"),
124                 ('F(-', "missing closing parenthesis"),
125                 ('F(-', "parenthetical block as false"),
126                 ('a&', "missing right operand for \"and operator\""),
127                 ('a*', "missing right operand for \"and operator\""),
128                 ('a|', "missing right operand for \"or operator\""),
129                 ('a^', "missing right operand for \"xor operator\""),
130                 ('a->', "missing right operand for \"implication operator\""),
131                 ('a<->', "missing right operand for \"equivalent operator\""),
132                 ('!', "missing right operand for \"not operator\""),
133                 ('a W', "missing right operand for \"weak until operator\""),
134                 ('a U', "missing right operand for \"until operator\""),
135                 ('a R', "missing right operand for \"release operator\""),
136                 ('a M', "missing right operand for "
137                  + "\"strong release operator\""),
138                 ('{a}[]->', "missing right operand for "
139                  + "\"universal overlapping concat operator\""),
140                 ('{a}[]=>', "missing right operand for "
141                  + "\"universal non-overlapping concat operator\""),
142                 ('{a}<>->', "missing right operand for "
143                  + "\"existential overlapping concat operator\""),
144                 ('{a}<>=>', "missing right operand for "
145                  + "\"existential non-overlapping concat operator\""),
146                 ('(X)', "missing right operand for \"next operator\""),
147                 ('("X)', "unclosed string"),
148                 ('("X)', "missing closing parenthesis"),
149                 ('{"X', "unclosed string"),
150                 ('{"X}', "missing closing brace"),
151                 ]:
152    f7 = spot.parse_infix_psl(x)
153    assert f7.errors
154    ostr = spot.ostringstream()
155    f7.format_errors(ostr)
156    err = ostr.str()
157    print(err)
158    assert msg in err
159    del f7
160
161for (x, msg) in [('a&', "missing right operand for \"and operator\""),
162                 ('a*', "missing right operand for \"and operator\""),
163                 ('a|', "missing right operand for \"or operator\""),
164                 ('a^', "missing right operand for \"xor operator\""),
165                 ('a->', "missing right operand for \"implication operator\""),
166                 ('a<->', "missing right operand for \"equivalent operator\""),
167                 ('(-', "parenthetical block as false"),
168                 ('(-', "missing closing parenthesis"),
169                 ('(-)', "treating this parenthetical block as false"),
170                 ('(a', "missing closing parenthesis"),
171                 ('(a b)', "ignoring this"),
172                 ('(a b', "ignoring trailing garbage and "
173                  + "missing closing parenthesis"),
174                 ('!', "missing right operand for \"not operator\""),
175                 ]:
176    f8 = spot.parse_infix_boolean(x)
177    assert f8.errors
178    ostr = spot.ostringstream()
179    f8.format_errors(ostr)
180    err = ostr.str()
181    print(err)
182    assert msg in err
183    del f8
184
185for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
186                 ('a<->', "missing right operand for \"equivalent operator\""),
187                 ('(aa', "missing closing parenthesis"),
188                 ('("aa', "missing closing parenthesis"),
189                 ('"(aa', "unclosed string"),
190                 ('{aa', "missing closing brace"),
191                 ]:
192    f9 = spot.parse_infix_psl(x, spot.default_environment.instance(),
193                              False, True)
194    assert f9.errors
195    ostr = spot.ostringstream()
196    f9.format_errors(ostr)
197    err = ostr.str()
198    print(err)
199    assert msg in err
200    del f9
201
202# force GC before fnode_instances_check(), unless it's CPython
203from platform import python_implementation
204if python_implementation() != 'CPython':
205    import gc
206    gc.collect()
207
208assert spot.fnode_instances_check()
209
210f = spot.formula_F(2, 4, spot.formula_ap("a"))
211assert f == spot.formula("XX(a | X(a | X(a)))")
212f = spot.formula_G(2, 4, spot.formula_ap("a"))
213assert f == spot.formula("XX(a & X(a & X(a)))")
214f = spot.formula_X(2, spot.formula_ap("a"))
215assert f == spot.formula("XX(a)")
216f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a"))
217assert f == spot.formula("XXG(a)")
218f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a"))
219assert f == spot.formula("XXF(a)")
220