Repository navigation
Expand file tree
/
Copy pathlogic_checker.py
More file actions
360 lines (324 loc) · 17.2 KB
/
Copy pathlogic_checker.py
File metadata and controls
360 lines (324 loc) · 17.2 KB
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
# -*- coding: utf-8 -*-
import sys
from ltlf2dfa.parser.ltlf import LTLfParser, LTLfAnd, LTLfUntil, LTLfNot, LTLfAlways, LTLfAtomic, LTLfNext, LTLfOr, LTLfEventually, LTLfImplies, LTLfRelease
# 三个&的时候这个生成的是& a & b c
proof=''
proofcnt=0
printproof=False
len_cache={}
# switch_cnt = [0] * 100
# change1: f_wait 在当前状态之前已经要求检查的cache
# change2:
# 新增输出证明树，证明节点需要 (t时刻，(a,b)公式区间，1或0期望的满足性)
# 所以输入时增加输入当前公式起点位置a ，b可以计算得到（目前直接简单转成str算），期望值
# 返回值多一个证明节点
# 递归时，根据递归来的值是否与期望一样决定是否将 str(当前节点):子节点搞进去
def formula_len(f,cache):
# print('f',f)
if cache.get(f,-1)!=-1:
return cache[f]
if isinstance(f,str):
cache[f] = 1
return 1
else:
cnt=0
for i in f:
cnt+=formula_len(i,cache)
cache[f]=cnt
return cnt
# def get_switch_cnt():
# global switch_cnt
# return switch_cnt
def checkLTL(f, f_wait, t, trace, loop_start, vocab, c={}, v=False, formula_start=0, expect_val=1, proof_dic={}):
""" Checks satisfaction of a LTL formula on an execution trace
NOTES:
* This works by using the semantics of LTL and forward progression through recursion
* Note that this does NOT require using any off-the-shelf planner
ARGUMENTS:
f - an LTL formula (must be in TREE format using nested tuples
if you are using LTL dict, then use ltl['str_tree'])
t - time stamp where formula f is evaluated
trace - execution trace (a dict containing:
trace['name']: trace name (have to be unique if calling from a set of traces)
trace['trace']: execution trace (in propositions format)
trace['plan']: plan that generated the trace (unneeded)
vocab - vocabulary of propositions
c - cache for checking LTL on subtrees
v - verbosity
OUTPUT:
satisfaction - true/false indicating ltl satisfaction on the given trace
"""
# change
if t==len(trace['trace']):#循环
t=loop_start
global len_cache
# global switch_cnt
#当前的证明树节点
proof_node=(t,(formula_start,formula_start+formula_len(f,len_cache)-1),expect_val)
sub_node_list=[]
sub_node_mode='or' # 默认就or
if v:
print('\nCurrent t = ' + str(t))
print('Current f =', f)
# if printproof:
# print(proofcnt,':'+str(t)+':'+str(trace['trace'][t])+':'+str(f)+'\n')
###################################################
# Check if first operator is a proposition
if type(f) is str and f in vocab:
# proofcnt-=1
# switch_cnt[0]+=1
return (f in trace['trace'][t], proof_node)
#change: 现在公式里还有0，1
if type(f) is str and f=='0':
# switch_cnt[0] += 1
# proofcnt-=1
return (False, proof_node)
if type(f) is str and f=='1':
# switch_cnt[0] += 1
# proofcnt-=1
return (True, proof_node)
# Check if sub-tree info is available in the cache
key = (f, t, trace['name'])
if c is not None:
if key in c:
if v: print('Found subtree history')
# proofcnt-=1
return (c[key],proof_node)
# change 用这个避免无限递归
if key in f_wait:
f_wait[key]+=1
else:
f_wait[key]=1
# Check for standard logic operators
# 语义一样不需要改
f0case=0
if f[0] in ['not', '!']:
value,sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start+1, 1-expect_val, proof_dic)
value = not value
sub_node_list.append(sub_node)
f0case=1
elif f[0] in ['and', '&', '&&']:
sub_node_mode='and'
cnt=1
value = True
for i in range(1,len(f)):
value,sub_node=checkLTL(f[i], f_wait, t, trace, loop_start, vocab, c, v, formula_start+cnt, expect_val, proof_dic)
cnt+=formula_len(f[i],len_cache) #记下前面的公式占多长
sub_node_list.append(sub_node)
if value is False:
break
f0case=2
#
# value = all((checkLTL(f[i], f_wait, t, trace, loop_start, vocab, c, v) for i in range(1, len(f))))
elif f[0] in ['or', '||','|']:
cnt = 1
value = False
for i in range(1,len(f)):
value,sub_node=checkLTL(f[i], f_wait, t, trace, loop_start, vocab, c, v, formula_start+cnt, expect_val, proof_dic)
cnt+=formula_len(f[i],len_cache) #记下前面的公式占多长
sub_node_list.append(sub_node)
if value is True:
break
f0case=3
# value = any((checkLTL(f[i], f_wait, t, trace, loop_start, vocab, c, v) for i in range(1, len(f))))
elif f[0] in ['imp', '->']:
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start + 1, 1 - expect_val, proof_dic)
value = not value
sub_node_list.append(sub_node)
if value is False: # 一个为真就够了
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v, formula_start+1+formula_len(f[1],len_cache), proof_dic)
sub_node_list.append(sub_node)
# switch_cnt[4] += 1
# value = not (checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v)) or checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v)
# change:原来这里是到了最后一个时刻进入该分支，现在改为已经有同样的调用待返回时进入该递归
elif f_wait[key]>1: #这个已经待证明了 #这里面的都是证明到最后时刻了，所以只要
# Confirm what your interpretation for this should be.
if f[0] in ['G', 'F']:
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start+1, expect_val, proof_dic) # Confirm what your interpretation here should be
sub_node_list.append(sub_node)
f0case=5
if f[0]=='F':
f0case = 6
elif f[0] == 'U':
# 检查 p U q，到最后时刻q还不出现则肯定没出现了，所以只要检查q
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v, formula_start+1+formula_len(f[1],len_cache), expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case=7
elif f[0] == 'W': # weak-until
# p W q, q可以不出现，只要p一直成立
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start + 1, 1 - expect_val, proof_dic)
sub_node_list.append(sub_node)
if value is False: # 一个为真就够了
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1 + formula_len(f[1], len_cache), proof_dic)
sub_node_list.append(sub_node)
elif f[0] == 'R': # release (weak by default)
# p R q，q一直为真或者有个状态 p&q为真 所以也不用改
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1 + formula_len(f[1],len_cache), expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case=8
# value = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v)
elif f[0] == 'X':
value, sub_node = checkLTL(f[1], f_wait, t+1, trace, loop_start, vocab, c, v, formula_start + 1, expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case=9
# change:没有weak next
else:
# Does not exist in vocab, nor any of operators
print(f,t,vocab)
sys.exit('LTL check - something wrong')
else:
# Forward progression rules
if f[0] == 'X': # change:删去了N
# value = checkLTL(f[1], f_wait, t + 1, trace, loop_start, vocab, c, v)
value, sub_node = checkLTL(f[1], f_wait, t + 1, trace, loop_start, vocab, c, v, formula_start + 1,
expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case=10
elif f[0] == 'G':
sub_node_mode = 'and'
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start + 1,
expect_val, proof_dic)
sub_node_list.append(sub_node)
if value is True:
value, sub_node = checkLTL(f, f_wait, t + 1, trace, loop_start, vocab, c, v, formula_start, expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case = 11
elif f[0] == 'F':
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v, formula_start + 1,
expect_val, proof_dic)
sub_node_list.append(sub_node)
if value is False:
value, sub_node = checkLTL(f, f_wait, t + 1, trace, loop_start, vocab, c, v, formula_start, expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case = 12
# value = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v) or checkLTL(('F', f[1]), f_wait, t + 1, trace, loop_start, vocab, c, v)
elif f[0] == 'U' or f[0]=='W':
# Basically enforces f[1] has to occur for f[1] U f[2] to be valid.
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1 + formula_len(f[1],len_cache), expect_val, proof_dic)
sub_node_list.append(sub_node)
if value is False:
if expect_val == True: #期待为真的话，要两个都加入list
sub_node_list=[]
sub_node_mode='and'
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1, expect_val, proof_dic)
sub_node_list.append(sub_node)
if value is True:
value, sub_node = checkLTL(f, f_wait, t+1, trace, loop_start, vocab, c, v,
formula_start, expect_val, proof_dic)
if expect_val == False: #期待为假的话，只要一个
sub_node_list[-1]=sub_node
else:
sub_node_list.append(sub_node)
f0case = 13
# value = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v) or (
# checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v) and checkLTL(('U', f[1], f[2]), f_wait, t + 1, trace, loop_start, vocab,
# c, v))
# elif f[0] == 'W': # weak-until
# value = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v) or (
# checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v) and checkLTL(('W', f[1], f[2]), f_wait, t + 1, trace, loop_start, vocab, c,
# v))
elif f[0] == 'R': # release (weak by default)
sub_node_mode = 'and'
value, sub_node = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1 + formula_len(f[1],len_cache), expect_val, proof_dic)
sub_node_list.append(sub_node)
f0case = 14
if value == True:
if expect_val == False: #期待为假的话，前面那个就不需要了
sub_node_list=[]
sub_node_mode='or'
value, sub_node = checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v,
formula_start + 1, expect_val, proof_dic)
sub_node_list.append(sub_node)
if value == False:
value, sub_node = checkLTL(f, f_wait, t+1, trace, loop_start, vocab, c, v,
formula_start, expect_val, proof_dic)
if expect_val == True: #期待为真那前面false的就不用了
sub_node_list[-1]=sub_node
else:
sub_node_list.append(sub_node)
# value = checkLTL(f[2], f_wait, t, trace, loop_start, vocab, c, v) and (
# checkLTL(f[1], f_wait, t, trace, loop_start, vocab, c, v) or checkLTL(('R', f[1], f[2]), f_wait, t + 1, trace, loop_start, vocab, c, v))
else:
# Does not exist in vocab, nor any of operators
print(f, t, vocab)
sys.exit('LTL check - something wrong')
if v: print('Returned: ' + str(value))
if expect_val == value:#这个需求跟实际一样，说明子节点肯定也满足了需要，可以作为证明树
if expect_val == False: #需求为假而且是and关系，那肯定是最后一个False
if sub_node_mode == 'and':
sub_node_list = sub_node_list[-1:]
if expect_val == True:
if sub_node_mode == 'or':
sub_node_list = sub_node_list[-1:]
cof=len(sub_node_list)
# switch_cnt[cof*15-15+f0case]+=1
# if f[0] == 'U':
# print('pre-curnode:', proof_node, sub_node_list)
if proof_dic.get(proof_node,-1)!=-1:
a=set(sub_node_list)
a=a.union(proof_dic[proof_node])
proof_dic[proof_node]=a
else:
proof_dic[proof_node]=set(sub_node_list)
if proof_node in proof_dic[proof_node]:
proof_dic[proof_node].remove(proof_node)
# if f[0] == 'U':
# print('after-curnode:', proof_node, proof_dic[proof_node])
# Save result
if c is not None and type(c) is dict:
key = (f, t, trace['name'])
c[key] = value # append
if printproof:
print('state:'+str(t) + ':' + str(trace['trace'][t]) + ', sub formula:' + str(f) + 'is '+ str(value))
# proofcnt -= 1
return (value,proof_node)
# 将输入的原始ltl公式转换成前缀元组
def preorder_turple(f):
if isinstance(f, LTLfAtomic):
return f.s.replace('true', '1').replace('false', '0')
if isinstance(f, LTLfAnd) or isinstance(f, LTLfUntil) or isinstance(f, LTLfOr) or isinstance(f, LTLfRelease) or isinstance(f, LTLfImplies):
# if len(f.formulas)>2:
# nf=deepcopy(f)
# nf.formulas=nf.formulas[1:]
# return (f.operator_symbol,preorder_turple(f.formulas[0]),preorder_turple(nf))
return tuple([f.operator_symbol.replace('R', 'W')]+[preorder_turple(f.formulas[i]) for i in range(len(f.formulas))])
if isinstance(f, LTLfNot) or isinstance(f, LTLfNext) or isinstance(f, LTLfAlways) or isinstance(f, LTLfEventually):
return (f.operator_symbol,preorder_turple(f.f))
def ltl2turple(ltl: str):
# print('ltl',ltl)
parser = LTLfParser()
formula = parser(ltl)
return preorder_turple(formula)
def list_to_nested_tuple(input_list):
if isinstance(input_list, list):
return tuple(list_to_nested_tuple(item) for item in input_list)
else:
return input_list
def check(ltl,trace,vocab):
'''
ltl必须是二叉树元组（op，左子树，右子树），子树如果是原子命题是字符串，否则为二叉树元组。
'''
t,loop_start=trace
trace={'name':'t','trace':t}
# formula=ltl2turple(ltl)
# formula =list_to_nested_tuple(ltl)
formula = ltl
if printproof:
print('formula',formula)
# print(ltl2prefix(ltl))
print('trace',t)
print('loop_start',loop_start)
proof_dic={}
value,root_node=checkLTL(formula, {}, 0, trace, loop_start, vocab, {}, False, 0, 1, proof_dic)
return value
if __name__ == '__main__':
ltl='((!(F((!(p24)) | (F(X(F((p21) & (F(!(F(G(p42)))))))))))) | (G((p9) | (X(p56))))) & (F((X(!(p96))) | (G(F(!(X(G(F(p79))))))))) & (F(G((X(X((X((F((!(p17)) U ((X(p13)) | ((X(p91)) & (!(G(p89))))))) & (G((!((p95) & ((p37) | (F(p77))))) U ((p93) & (!(F(p83)))))) & (!(((X(p93)) U ((p76) | ((p9) & (p33)))) | ((F(p5)) U (p60)) | (!((p83) & ((p31) U (p71)))))))) U ((F(G((!((p53) & (p92))) U (!(p71))))) U (G(F(!(G((X((X(p77)) U (X(X(p53))))) U ((p52) | (p67))))))))))) & (X(G((p82) U (p77)))))))'
trace=([['p76', 'p71', 'p21', 'p9', 'p13', 'p95', 'p53', 'p42', 'p92'], ['p71', 'p9', 'p13', 'p52', 'p89', 'p42', 'p77'], ['p76', 'p96', 'p82', 'p13', 'p89', 'p95', 'p93', 'p42'], ['p96', 'p71', 'p9', 'p52', 'p56', 'p89', 'p42', 'p77'], ['p76', 'p96', 'p82', 'p13', 'p89', 'p95', 'p93', 'p42']],2)
vocab={'p24': 109, 'p21': 30, 'p42': 112, 'p9': 31, 'p56': 71, 'p96': 17, 'p79': 96, 'p17': 90, 'p13': 45, 'p91': 35, 'p89': 81, 'p95': 84, 'p37': 98, 'p77': 123, 'p93': 111, 'p83': 63, 'p76': 6, 'p33': 77, 'p5': 43, 'p60': 69, 'p31': 125, 'p71': 22, 'p53': 92, 'p92': 127, 'p52': 59, 'p67': 91, 'p82': 39}
value=check(ltl2turple(ltl),trace,vocab.keys())
print('value',value)