Improvement for parsing LTL grammer

Question

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[0], s[1]
    print(f'Unary operators: op = {op}, p = {p}')
    if op == '~':
        if p == True:
            return False
        elif p in trace[0][0]:
            return False
        else:
            return True
    elif op == 'X':
        if p == True:
            return True
        elif p in trace[0][1]:
            return True
        else:
            return False
    elif op == 'G':
        if p == True:
            return True
        for s in trace[0]:
            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[0]:
            if p in s:
                return True
        return False

def eval_binary(s, trace):
    p1, op, p2 = s[0], s[1], s[2]
    # 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[0][0]:
                return True
            else:
                return False
        if p2 == True:
            if p1 in trace[0][0]:
                return True
            else:
                return False
        if (p1 in trace[0][0]) and (p2 in trace[0][0]):
            return True
        else:
            return False

    elif op == '|':
        if (p1 == True) or (p2 == True):
            return True
        if (p1 in trace[0][0]) or (p2 in trace[0][0]):
            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[0][0]) or (p2 in trace[0][0]):
            return True
        else:
            return False
    elif op == 'U':
        for s in trace[0]:
            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[0], rho[1]))
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[0]
    if len(form) == 2:
        op = form[0]
        tree1 = form[1]
        return eval_unary([op, evaluate_form(tree1, trace)], trace)
    elif len(form) == 3:
        tree1 = evaluate_form(form[0], trace)
        op = form[1]
        tree2 = evaluate_form(form[2], 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?

Answer 1

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[0][0])
    return matches

def logical_next(pattern):
    def matches(trace):
        return pattern(trace[0][1])
    return matches

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

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

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

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


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

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

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

def until(left_hand, right_hand):
    def matches(trace):
        for s in trace[0]:
            if left_hand(s[0]):
                continue
        return right_hand(s[0])
    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[0][1]). Perhaps using a NamedTuple or something?