# Improvement for parsing LTL grammer

I'm new here. I wrote the following code to parse the linear temporal logic(LTL) formula and evaluate it with respect to a trace. But I'm totally not happy with my code because I think the complexity is very high and the "if else" condition in the two eval functions can be improved. The LTL grammar is as follows,

phi = True|a|~phi|phi1 & phi2|(phi1 | phi2)|phi1 U phi2|G phi|F phi|X phi|phi1->phi2|phi1<->phi2


I have the following code,

import pyparsing as pp

def eval_unary(s, trace):
op, p = s, s
print(f'Unary operators: op = {op}, p = {p}')
if op == '~':
if p == True:
return False
elif p in trace:
return False
else:
return True
elif op == 'X':
if p == True:
return True
elif p in trace:
return True
else:
return False
elif op == 'G':
if p == True:
return True
for s in trace:
if p not in s:
return False
return True
elif op == 'F':
if p == True:
return True
if p == False:
return True
for s in trace:
if p in s:
return True
return False

def eval_binary(s, trace):
p1, op, p2 = s, s, s
# print(f'Binary operators: op = {op}, p1 = {p1}, p2 = {p2}')
if op == '&':
if p1 == False or p2 == False:
return False
if p1 == True:
if p2 == True:
return True
elif p2 in trace:
return True
else:
return False
if p2 == True:
if p1 in trace:
return True
else:
return False
if (p1 in trace) and (p2 in trace):
return True
else:
return False

elif op == '|':
if (p1 == True) or (p2 == True):
return True
if (p1 in trace) or (p2 in trace):
return True
else:
return False
elif op == '->':
if (p1 == False) and (p2 == False):
return True
if (p1 == False) or (p2 == True):
return True
if (p1 not in trace) or (p2 in trace):
return True
else:
return False
elif op == 'U':
for s in trace:
if p2 in s:
return True
elif p1 == True:
continue
elif p1 in s:
continue
else:
return False
return False

# Building the formula for checking
atom = pp.Regex(r'[a-z]') | 'True'
binop = pp.Regex(r'[U&|]|(->)|(<->)')
unop = pp.Regex(r'[~XGF]')
# phi = (atom + binop + atom) | (unop + atom)
phi = pp.infixNotation(
atom, [
(unop, 1, pp.opAssoc.RIGHT),
(binop, 2, pp.opAssoc.LEFT)]
)
form = '(F (a & b))'

parsed_form = phi.parse_string(form)
updated_form = parsed_form.as_list()
# print(type(updated_form))
# print(f'length of tree: {len(updated_form)}')
print(f'parsed formula: {updated_form}')

# Making the trace
rho = [('a', 'b', 'ab', '', 'b', 'b', '', '', '', ''), (1, 21, 37, 43, 59, 65, 73, 83, 99, 100)]
rho2 = list(zip(rho, rho))
print(rho2)

# test = eval_unary(['X','b'], rho)
# test2 = eval_binary(['a','<->','b'], rho)
# print(test)
# print(test2)

def evaluate_form(form, trace):
if len(form) == 1:
form = form
if len(form) == 2:
op = form
tree1 = form
return eval_unary([op, evaluate_form(tree1, trace)], trace)
elif len(form) == 3:
tree1 = evaluate_form(form, trace)
op = form
tree2 = evaluate_form(form, trace)
return eval_binary([tree1, op, tree2], trace)
else:
return form

result = evaluate_form(updated_form, rho)
print(result)


Please give me some idea on how can I improve this code?

• Looks like you forgot the imports. What is pp? Aug 5 at 21:16
• I am using pyparsing library for parsing. And imported it as pp at the top. Check the first line of the code. Aug 5 at 21:20

I wasn't able to get your code running, I think perhaps we have different versions of pyparsing. I've given some ideas below but I don't know whether they would work as written. In general I think you need to break things down more, grammars are quite specific things, I'd expect to see lots of rules for the different operators and things that you're using, not just one big 'binary_op' rule.

That said, we can still split things up more post-parsing and get a lot of the same readability benefits, although there are a few things that would be more efficient if we handled them at the parser level.

I personally prefer using a more functional style when parsing, but YMMV.

from functools import singledispatch

@singledispatch
def symbol(symbol: str):
def matches(element):
return symbol in element
return matches

@symbol.register
def literal_bool(value: bool):
def matches(_):
return value
return matches

def logical_not(pattern):
def matches(trace):
return not pattern(trace)
return matches

def logical_next(pattern):
def matches(trace):
return pattern(trace)
return matches

def logical_global(pattern):
def matches(trace):
return all(pattern(symbol) for symbol in trace)
return matches

def logical_finally(pattern):
def matches(trace):
return any(pattern(symbol) for symbol in trace)
return matches

_unary_operators = {'~': logical_not, 'X': logical_next, 'G': logical_global, 'F': logical_finally}

def eval_unary(s, trace):
op, p = s, s
return _unary_operators[op](symbol(p))(trace)

def logical_and(left_hand, right_hand):
def matches(trace):
return left_hand(trace) and right_hand(trace)
return matches

def logical_or(left_hand, right_hand):
def matches(trace):
return left_hand(trace) or right_hand(trace)
return matches

def logical_imply(left_hand, right_hand):
def matches(trace):
return not (left_hand(trace) and not right_hand(trace))
return matches

def until(left_hand, right_hand):
def matches(trace):
for s in trace:
if left_hand(s):
continue
return right_hand(s)
return matches

_binary_ops = {'&': logical_and, '|': logical_or, '->': logical_imply, 'U': until}
def eval_binary(s, trace):
# print(f'Binary operators: op = {op}, p1 = {p1}, p2 = {p2}')
left, op, right = s
return _binary_ops[op](symbol(left), symbol(right))(trace)


You may also want to do something better with your trace to get rid of the magic numbers (e.g. trace). Perhaps using a NamedTuple or something?

• Thanks a lot. It is useful (cannot upvote due to low reputation). But I want to know does my code has more complexity than yours. I hope not. Aug 6 at 18:11