inductive-invariant-dependency-graph.py

import subprocess

f = open('paxos_epr.ivy')
source = f.read().split('\n')
f.close()

conjecture_line_numbers = []
all_lines = []

for i, line in enumerate(source):
    all_lines.append(line)
    if line.startswith('conjecture'):
        conjecture_line_numbers.append(i)


def does_it_work(p): # p is a list of integers representing line numbers to comment out
    filename = 'test-' + '-'.join(map(str, list(p))) + '.ivy'
    with open(filename, 'w') as f:
        for i, line in enumerate(all_lines):
            if i in p:
                f.write('#' + line + '\n')
            else:
                f.write(line + '\n')
    try:
        subprocess.check_output(['ivy_check', filename])
        return (True, [])
    except subprocess.CalledProcessError as e:
        err_lines = e.output.split('\n')
        err_lines = [l for l in err_lines if 'FAIL' in l]
        err_lines = [int(l.split(' line ')[1].split(':')[0]) - 1 for l in err_lines]
        return (False, err_lines)

print 'digraph G {'
for i in conjecture_line_numbers:
    works, edges = does_it_work([i])
    print i, '[label="' + all_lines[i][11:30] + '..."];';
    for e in edges:
        print e, '->', i, ';'
print '}'