Wrapper to enhance a program to translate from LTL formulae to Büchi automata

Question

The following is a script that is supposed to act as a wrapper for ltl2ba, a program which transforms LTL formulas into Buchi Automatons encoded in the Promela language. The wrapper adds a limited set of functionalities to the original program. I tested it on my local linux machine and it works.

Now, in addition to the fact that i did not test this tool for other operating systems, I am also concerned that the hard-coded decoding of binary text into utf-8 might be a too strong assumption, even though ltl2ba seems to use this character-set.

Since I consider myself a novice python developer, I decided to share the code here in order learn how experienced programmers would do things differently and how far I am from consolidated best practices with respect to two particular points:

• handling output of independent system application
• portability over other operating systems, which right now is likely absent

Criticism about any other violated best-practice, which is not 'split into several files' (I would like to keep things as simple as possible.), or conventions is also accepted. And yes, I did not comment any function or class yet.

This code and updates are available at: gltl2ba.

#!/usr/bin/env python3

from graphviz.dot import Digraph
from subprocess import Popen, PIPE
import re, argparse, sys, __main__

#
## draw graph of Buchi Automaton
#

class Graph:
    def __init__(self):
        self.dot = Digraph()

    def title(self, str):
        self.dot.graph_attr.update(label=str)

    def node(self, name, label, accepting=False):
        num_peripheries = '2' if accepting else '1'
        self.dot.node(name, label, shape='circle', peripheries=num_peripheries)

    def edge(self, src, dst, label):
        self.dot.edge(src, dst, label)

    def show(self):
        self.dot.render(view=True)

    def save_render(self, path, on_screen):
        self.dot.render(path, view=on_screen)

    def save_dot(self, path):
        self.dot.save(path)

    def __str__(self):
        return str(self.dot)

#
## parser for ltl2ba output
#

class ltl2baParser:
    prog_title  = re.compile('never\s+{\s+/\* (.*) \*/')
    prog_node   = re.compile('(.*)_(.*):')
    prog_ignore = re.compile('(?:\s+[do|if])|(?:\s+[od|fi];)|(?:})|(?:)')
    prog_edge   = re.compile('\s+:: (.*) -> goto (.*)')

    @staticmethod
    def parse(ltl2ba_output, ignore_title = True):
        graph = Graph()
        src_node = None
        for line in ltl2ba_output.decode('utf-8').split('\n'):
            if ltl2baParser.is_title(line):
                title = ltl2baParser.get_title(line)
                if not ignore_title:
                    graph.title(title)
            elif ltl2baParser.is_node(line):
                name, label, accepting = ltl2baParser.get_node(line)
                graph.node(name, label, accepting)
                src_node = name
            elif ltl2baParser.is_edge(line):
                dst_node, label = ltl2baParser.get_edge(line)
                assert(src_node is not None)
                graph.edge(src_node, dst_node, label)
            elif ltl2baParser.is_ignore(line):
                pass
            else:
                raise ValueError("{}: invalid input:\n{}".format(__class__.__name__, line))

        return graph

    @staticmethod
    def is_title(line):
        return ltl2baParser.prog_title.match(line) is not None

    @staticmethod
    def get_title(line):
        assert(ltl2baParser.is_title(line))
        return ltl2baParser.prog_title.search(line).group(1)

    @staticmethod
    def is_node(line):
        return ltl2baParser.prog_node.match(line) is not None

    @staticmethod
    def get_node(line):
        assert(ltl2baParser.is_node(line))
        prefix, label = ltl2baParser.prog_node.search(line).groups()
        return (prefix + "_" + label, label, True if prefix == "accept" else False)

    @staticmethod
    def is_edge(line):
        return ltl2baParser.prog_edge.match(line) is not None

    @staticmethod
    def get_edge(line):
        assert(ltl2baParser.is_edge(line))
        label, dst_node = ltl2baParser.prog_edge.search(line).groups()
        return (dst_node, label)

    @staticmethod
    def is_ignore(line):
        return ltl2baParser.prog_ignore.match(line) is not None


#
## main
#

def gltl2ba ():
    args = parse_args()

    ltl = get_ltl_formula(args.file, args.formula)

    (output, err, exit_code) = run_ltl2ba(args, ltl)

    if exit_code != 1:

        print(output.decode('utf-8'))

        if args.graph or args.output_graph is not None \
                or args.dot or args.output_dot is not None:

            prog = re.compile(b"[\s\S\w\W]*(never\s*{[\s\S\w\W]*})[\s\S\w\W]*")
            match = prog.search(output)
            assert(match is not None)

            graph = ltl2baParser.parse(match.group(1))

            if args.output_graph is not None:
                graph.save_render(args.output_graph.name, args.graph)
                args.output_graph.close()
            elif args.graph:
                graph.show()

            if args.output_dot is not None:
                graph.save_dot(args.output_dot.name)
                args.output_dot.close()
            if args.dot:
                print(graph)

    else:
        eprint("{}: ltl2ba error:".format(__main__.__file__))
        eprint(output.decode('utf-8'))
        quit(exit_code)

    return

def parse_args():
    parser = argparse.ArgumentParser()
    group = parser.add_mutually_exclusive_group(required=True)
    group.add_argument("-f", "--formula", help="translate LTL into never claim", type=str)
    group.add_argument("-F", "--file", help="like -f, but with the LTL formula stored in a 1-line file", type=argparse.FileType('r'))
    parser.add_argument("-d", help="display automata (D)escription at each step", action='store_true')
    parser.add_argument("-s", help="computing time and automata sizes (S)tatistics", action='store_true')
    parser.add_argument("-l", help="disable (L)ogic formula simplification", action='store_true')
    parser.add_argument("-p", help="disable a-(P)osteriori simplification", action='store_true')
    parser.add_argument("-o", help="disable (O)n-the-fly simplification", action='store_true')
    parser.add_argument("-c", help="disable strongly (C)onnected components simplification", action='store_true')
    parser.add_argument("-a", help="disable trick in (A)ccepting conditions", action='store_true')
    parser.add_argument("-g", "--graph", help="display buchi automaton graph", action='store_true')
    parser.add_argument("-G", "--output-graph", help="save buchi automaton graph in pdf file", type=argparse.FileType('w'))
    parser.add_argument("-t", "--dot", help="print buchi automaton graph in DOT notation", action='store_true')
    parser.add_argument("-T", "--output-dot", help="save buchi automaton graph in DOT file", type=argparse.FileType('w'))
    return parser.parse_args()

def get_ltl_formula(file, formula):
    assert(file is not None or formula is not None)
    if (file is not None):
        try:
            with open(file, 'r') as fd:
                ltl = fd.read()
        except Exception as e:
            eprint("{}: {}".format(__main__.__file__, str(e)))
            quit(1)
    else:
        ltl = formula
    ltl = re.sub('\s+', ' ', ltl)
    if len(ltl) == 0 or ltl == ' ' :
        eprint("{}: empty ltl formula.".format(__main__.__file__))
        quit(1)
    return ltl

def run_ltl2ba(args, ltl):
    ltl2ba_args = ["ltl2ba", "-f", ltl]
    if args.d:
        ltl2ba_args.append("-d")
    if args.s:
        ltl2ba_args.append("-s")
    if args.l:
        ltl2ba_args.append("-l")
    if args.p:
        ltl2ba_args.append("-p")
    if args.o:
        ltl2ba_args.append("-o")
    if args.c:
        ltl2ba_args.append("-c")
    if args.a:
        ltl2ba_args.append("-a")

    try:
        process = Popen(ltl2ba_args, stdout=PIPE)
        (output, err) = process.communicate()
        exit_code = process.wait()
    except FileNotFoundError as e:
        eprint("{}: ltl2ba not found.\n".format(__main__.__file__))
        eprint("Please download ltl2ba from\n")
        eprint("\thttp://www.lsv.fr/~gastin/ltl2ba/ltl2ba-1.2b1.tar.gz\n")
        eprint("compile the sources and add the binary to your $PATH, e.g.\n")
        eprint("\t~$ export PATH=$PATH:path-to-ltlb2ba-dir\n")
        quit(1)

    return output, err, exit_code

def eprint(*args, **kwargs):
    print(*args, file=sys.stderr, **kwargs)

###
###
###

if (__name__ == '__main__'):
    gltl2ba()

---

The ltl2ba tool has the following output for a simple ltl formula:

~$ ltl2ba -f "[] <> (q0 -> <> q1)"
never { /* [] <> (q0 -> <> q1) */
accept_init:
    if
    :: (q1) || (!q0) -> goto accept_init
    :: (1) -> goto T0_S2
    :: (1) -> goto T1_S1
    fi;
T0_S2:
    if
    :: (1) -> goto T0_S2
    :: (q1) -> goto accept_init
    fi;
T1_S1:
    if
    :: (q1) || (!q0) -> goto accept_init
    :: (1) -> goto accept_S2
    :: (1) -> goto T1_S1
    fi;
accept_S2:
    if
    :: (1) -> goto T0_S2
    :: (q1) -> goto accept_init
    fi;
}

The wrapper simply allows to display/save the Buchi Automaton as a PDF (with -g/-G file_name) or in DOT format (with -t, -T file_name). All the rest remains equal with the ltl2ba tool.

~$ export PATH=$PATH:path_to_ltl2ba
~$ ./gltl2ba.py -f "[] <> (q0 -> <> q1)" -g -t
never { /* [] <> (q0 -> <> q1) */
accept_init:
    if
    :: (q1) || (!q0) -> goto accept_init
    :: (1) -> goto T0_S2
    :: (1) -> goto T1_S1
    fi;
T0_S2:
    if
    :: (1) -> goto T0_S2
    :: (q1) -> goto accept_init
    fi;
T1_S1:
    if
    :: (q1) || (!q0) -> goto accept_init
    :: (1) -> goto accept_S2
    :: (1) -> goto T1_S1
    fi;
accept_S2:
    if
    :: (1) -> goto T0_S2
    :: (q1) -> goto accept_init
    fi;
}

digraph {
    accept_init [label=init peripheries=2 shape=circle]
    accept_init -> accept_init [label="(q1) || (!q0)"]
    accept_init -> T0_S2 [label="(1)"]
    accept_init -> T1_S1 [label="(1)"]
    T0_S2 [label=S2 peripheries=1 shape=circle]
    T0_S2 -> T0_S2 [label="(1)"]
    T0_S2 -> accept_init [label="(q1)"]
    T1_S1 [label=S1 peripheries=1 shape=circle]
    T1_S1 -> accept_init [label="(q1) || (!q0)"]
    T1_S1 -> accept_S2 [label="(1)"]
    T1_S1 -> T1_S1 [label="(1)"]
    accept_S2 [label=S2 peripheries=2 shape=circle]
    accept_S2 -> T0_S2 [label="(1)"]
    accept_S2 -> accept_init [label="(q1)"]
}

since option -g is used, it also displays the following graph:

Answer 1

I'll raise a few nits, but (aside from asserts) there's nothing major.

PEP8 asks you to break this:

import re, argparse, sys, __main__

into four lines. Flake8 is your friend. Also, PEP8 wants a capital "L" in class ltl2baParser:.

It's easy to accidentally put nested loops into a regex when you don't need to. Nested backtracking can make matching more expensive than you'd like. In the expression re.compile('(.*)_(.*):') you consume the whole string, then notice $ is not followed by _, so you backtrack one, nope, string doesn't end with underscore, backtrack another, another, keep going. If matching the first underscore and the first colon is acceptable, perhaps because each occurs just once, then '^([^_]*)_([^:]*):' would be a fair way to code it, though typically + is more appropriate than *. If they occur more than just once, then consider using non-greedy: '^(.*?)_(.*?):' On the topic of nesting, deeply nested loops like ^(.*):(.*):(.*):$ are especially horrible.

The @staticmethod annotations are very nice. A class with only static methods is maybe a little weird, feels more like a module than a class, but hardly the end of the world. Keeping prog_title and its three friends in a nice tidy namespace is certainly useful.

You don't want parentheses in assert(src_node is not None), cf SO assert w/ parens. Same pattern in get_node, get_edge, get_ltl_formula, and assert(match is not None).

In gltl2ba() the if args.graph ... expression, with backslash, is perfectly nice, but PEP8 weakly prefers paren over backslash: if (args.graph ... [next line] ... output_dot is not None):. It's just a minor stylistic thing.

Consider re-assigning decoded output immediately after calling run_ltl2ba().

The prog regex (\s\S\w\W) is not obvious to me -- I would appreciate a comment and/or a sample text line you hope to match. The usual assert idiom would be simply assert match, or more informatively, assert match, output, since the group(1) dereference is redundant with assert match, you're guaranteed to raise an error either way.

There are two calls for closing the output graph, which is fine, it just makes me wonder if there's a way to get a with clause to close upon leaving scope.

In get_ltl_formula(), please drop parens in if (file is not None):. Testing if file: would suffice. If you dropped the generic fatal Exception handler, the end result would be much the same.

In run_ltl2ba(), there's an opportunity to run a loop over 'dslpoca'.split(''), if desired.

I saw no glaring portability issues. Not sure if calling quit() works the same on Windows. The other usual gotchas would be CRLF issues (so r'x$' matches 'x\n' but not 'x\r\n'), or needing open with 'wb' for write binary, but nothing leapt off the page.

Overall, the program appears to be in fairly good shape!