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