diff --git a/thys/Buchi_Complementation/code/analysis.py b/thys/Buchi_Complementation/code/analysis.py --- a/thys/Buchi_Complementation/code/analysis.py +++ b/thys/Buchi_Complementation/code/analysis.py @@ -1,45 +1,75 @@ #!/usr/bin/python -import sys, random, subprocess, time +import sys, random, subprocess, time, math def read(path): f = open(path, "r") text = f.read() f.close return text def write(path, text): f = open(path, "w") f.write(text) f.close() def stats(entries, finished): entry_count = "{}".format(len(entries)) finished_ratio = "{:.2f} \\%".format(100 * len(finished) / len(entries)) if entries else "N/A" finished_time = "{:.3f} s".format(sum(finished) / len(finished)) if finished else "N/A" return "{} & {} & {}".format(entry_count, finished_ratio, finished_time) def stats_entries(entries, label, predicate): entries = list(time for (state_count, result, time) in entries if predicate(state_count, result, time)) finished = list(float(time) for time in entries if time != "T") print("{} & {}\\\\".format(label, stats(entries, finished))) if sys.argv[1] == "states": entries = list(line.split() for line in read(sys.argv[2]).splitlines()) entries = list((int(state_count_1), int(state_count_2), result, time) for [state_count_1, state_count_2, result, time] in entries) non_timeout = list(time for (state_count_1, state_count_2, result, time) in entries if time != "T") print(all(result == "True" or time == "T" for (state_count_1, state_count_2, result, time) in entries)) print("completion rate: {}".format(len(non_timeout) / len(entries))) print("{} {}".format(sum(state_count_1 for (state_count_1, state_count_2, result, time) in entries) / len(entries), sum(state_count_2 for (state_count_1, state_count_2, result, time) in entries) / len(entries))) if sys.argv[1] == "complement": entries = list(line.split() for line in read(sys.argv[2]).splitlines()) entries = list(time for [state_count, time] in entries) non_timeout = list(float(time) for time in entries if time != "T") print(stats(entries, non_timeout)) if sys.argv[1] == "equivalence": - cutoff = 20 + segments = 4 + size = 5 entries = list(line.split() for line in read(sys.argv[2]).splitlines()) entries = list((max(int(state_count_1), int(state_count_2)), result, time) for [state_count_1, state_count_2, result, time] in entries) print(all(result == "True" or time == "T" for (state_count, result, time) in entries)) - for n in range(1, cutoff + 1): stats_entries(entries, n, lambda state_count, result, time: state_count == n) - stats_entries(entries, "> {}".format(cutoff), lambda state_count, result, time: state_count > cutoff) + for n in range(segments): stats_entries(entries, "$({}, {}]$".format(n * size, (n + 1) * size), lambda state_count, result, time: n * size < state_count and state_count <= (n + 1) * size) + stats_entries(entries, "$({}, \infty)$".format(segments * size), lambda state_count, result, time: segments * size < state_count) + print("\hline") stats_entries(entries, "total", lambda state_count, result, time: True) +if sys.argv[1] == "compare": + def read_block(blocks): + if blocks[0] == 'None': return (None, blocks[1:]) + return (int(blocks[0]), int(blocks[1]), float(blocks[2])), blocks[3:] + def parse(line): + blocks = line.replace(',', '').replace('(', '').replace(')', '').split() + state_count, blocks = int(blocks[0]), blocks[1:] + r1, blocks = read_block(blocks) + r2, blocks = read_block(blocks) + r3, blocks = read_block(blocks) + r4, blocks = read_block(blocks) + return r1, r2, r3, r4 + def stats(label, entries, finished, completed): + def round_(digits, value): return float(('%.' + str(digits) + 'g') % value) + def digits(digits, value): return round(value, digits -int(math.floor(math.log10(abs(value)))) - 1) + ratio = "{:.2f} \\%".format(100 * len(finished) / len(entries)) + time = "{:.3f} s".format(sum(time for _, _, time in completed) / len(completed)) + states = "{:g}".format(digits(4, sum(states for states, _, _ in completed) / len(completed))) + return "{} & {} & {} & {}\\\\".format(label, ratio, time, states) + entries = list(parse(line) for line in read(sys.argv[2]).splitlines()) + completed = list(entry for entry in entries if all(entry)) + print("finished by all: {} of {}".format(len(completed), len(entries))) + label = ["Spot (\\texttt{-{}-complement -{}-ba})", "\\textsc{Goal} (\\texttt{rank -tr})", "\\textsc{Goal} (\\texttt{rank -rd})", "Our Tool"] + for index in range(4): + block_entries = list(entry[index] for entry in entries) + block_finished = list(entry[index] for entry in entries if entry[index] is not None) + block_completed = list(entry[index] for entry in completed) + print(stats(label[index], block_entries, block_finished, block_completed)) diff --git a/thys/Buchi_Complementation/code/benchmark.py b/thys/Buchi_Complementation/code/benchmark.py --- a/thys/Buchi_Complementation/code/benchmark.py +++ b/thys/Buchi_Complementation/code/benchmark.py @@ -1,110 +1,121 @@ -#!/usr/bin/python +#!/usr/bin/python -u import sys, random, subprocess, time -owl = "/home/Projects/owl/build/distributions/owl-minimized-20.XX-development/bin/owl" - def read(path): - f = open(path, "r") - text = f.read() - f.close - return text + with open(path, "r") as f: return f.read() def write(path, text): - f = open(path, "w") - f.write(text) - f.close() + with open(path, "w") as f: f.write(text) + +def measure(action): + start = time.time() + result = action() + return result, time.time() - start def get_state_count(path): result = subprocess.run(["autfilt", path, "--stats=%s"], stdout = subprocess.PIPE, text = True) return int(result.stdout.strip()) +def get_transition_count(path): + result = subprocess.run(["autfilt", path, "--stats=%t"], stdout = subprocess.PIPE, text = True) + return int(result.stdout.strip()) def spot_generate_automaton(state_count, proposition_count): seed = random.randrange(0x10000) result = subprocess.run(["randaut", "--seed={}".format(seed), "--ba", "--states={}".format(state_count), str(proposition_count)], stdout = subprocess.PIPE, text = True) return result.stdout def spot_generate_formula(proposition_count): seed = random.randrange(0x10000) result = subprocess.run(["randltl", "--seed={}".format(seed), str(proposition_count)], stdout = subprocess.PIPE, text = True) return result.stdout.strip() def spot_simplify_automaton(path): result = subprocess.run(["autfilt", "--ba", "--small", path], stdout = subprocess.PIPE, text = True) return result.stdout def owl_simplify_automaton(path): result = subprocess.run(["owl", "-I", path, "---", "hoa", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout -def spot_to_buchi_automaton(path): - result = subprocess.run(["autfilt", "--ba", "--small", path], stdout = subprocess.PIPE, text = True, timeout = 60) - return result.stdout - def spot_formula_to_nba(formula): result = subprocess.run(["ltl2tgba", "--ba", formula], stdout = subprocess.PIPE, text = True) return result.stdout def owl_formula_to_nba(formula): result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2nba", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout def owl_formula_to_nba_opt(formula): result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2nba", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout def owl_formula_to_dra(formula): result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2dra", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout def owl_formula_to_dra_opt(formula): result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2dra", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout -def bc_complement(path1, path2): - subprocess.run(["./Autool", "complement_quick", path1, path2], timeout = 60) -def bc_equivalence(path1, path2): - result = subprocess.run(["./Autool", "equivalence", path1, path2], timeout = 60, stdout = subprocess.PIPE, text = True) - return result.stdout.strip() == "true" +def spot_complement(path_input, path_output): + try: _, time = measure(lambda: write(path_output, subprocess.run(["autfilt", "--complement", "--ba", path_input], timeout = 60, stdout = subprocess.PIPE, text = True).stdout)) + except subprocess.TimeoutExpired: return None + state_count = get_state_count(path_output) + transition_count = get_transition_count(path_output) + return state_count, transition_count, time -def complement(path_input, path_output): - start = time.time() - try: bc_complement(path_input, path_output) - except subprocess.TimeoutExpired: duration = "T" - else: duration = str(time.time() - start) - print("{} {}".format(get_state_count(path_input), duration)) +def goal_complement(path_input, path_output, tight): + try: _, time = measure(lambda: subprocess.run(["gc", "complement", "-m", "rank", "-tr" if tight else "-rd", "1", "-o", path_output, path_input], timeout = 60)) + except subprocess.TimeoutExpired: + subprocess.run(["killall", "java"]) + return None + state_count = int(subprocess.run(["gc", "stat", "-s", path_output], stdout = subprocess.PIPE, text = True).stdout.strip()) + transition_count = int(subprocess.run(["gc", "stat", "-t", path_output], stdout = subprocess.PIPE, text = True).stdout.strip()) + return state_count, transition_count, time + +def bc_complement(path_input, path_output): + try: _, time = measure(lambda: subprocess.run(["./Autool", "complement_quick", path_input, path_output], timeout = 60)) + except subprocess.TimeoutExpired: return None + complement = read(path_output).splitlines() + state_count = int(complement[0].split()[0]) + 1 + transition_count = len(complement) + return state_count, transition_count, time +def bc_equivalence(path1, path2): + try: result, time = measure(lambda: subprocess.run(["./Autool", "equivalence", path1, path2], timeout = 60, stdout = subprocess.PIPE, text = True)) + except subprocess.TimeoutExpired: return None + return result.stdout.strip() == "true", time + +def complement(path): + r1 = spot_complement(path, path + ".spot") + r2 = goal_complement(path, path + ".goaltr", True) + r3 = goal_complement(path, path + ".goalrd", False) + r4 = bc_complement(path, path + ".bc") + print("{} {} {} {} {}".format(get_state_count(path), r1, r2, r3, r4)) def equivalence(path_1, path_2): - start = time.time() - try: eq = bc_equivalence(path_1, path_2) - except subprocess.TimeoutExpired: eq = None; duration = "T" - else: duration = str(time.time() - start) - print("{} {} {} {}".format(get_state_count(path_1), get_state_count(path_2), eq, duration)) + r = bc_equivalence(path_1, path_2) + print("{} {} {}".format(get_state_count(path_1), get_state_count(path_2), r)) + if not r: return None + eq, _ = r return eq if sys.argv[1] == "complement_automaton": while True: write("a.hoa", spot_generate_automaton(20, 4)) - complement("a.hoa", "c.txt") + complement("a.hoa") if sys.argv[1] == "complement_formula": while True: - write("a.hoa", spot_formula_to_nba(spot_generate_formula(4))) - complement("a.hoa", "c.txt") + while True: + write("a.hoa", spot_formula_to_nba(spot_generate_formula(4))) + if get_state_count("a.hoa") == 10: break + complement("a.hoa") if sys.argv[1] == "equivalence_random": while True: write("a.hoa", spot_generate_automaton(100, 4)) write("b.hoa", spot_generate_automaton(100, 4)) equivalence("a.hoa", "b.hoa") if sys.argv[1] == "equivalence_simplify": while True: - write("a.hoa", spot_generate_automaton(10, 4)) + write("a.hoa", spot_generate_automaton(20, 4)) write("b.hoa", spot_simplify_automaton("a.hoa")) equivalence("a.hoa", "b.hoa") if sys.argv[1] == "equivalence_translate": while True: formula = spot_generate_formula(4) write("a.hoa", spot_formula_to_nba(formula)) write("b.hoa", owl_formula_to_dra_opt(formula)) write("c.hoa", spot_simplify_automaton("b.hoa")) if equivalence("a.hoa", "c.hoa") == False: print(formula) -if sys.argv[1] == "equivalence_translate_collection": - for formula in read(sys.argv[2]).splitlines(): - print(formula) - try: - write("a.hoa", spot_formula_to_nba(formula)) - write("b.hoa", owl_formula_to_dra_opt(formula)) - write("c.hoa", spot_to_buchi_automaton("b.hoa")) - equivalence("a.hoa", "c.hoa") - except subprocess.TimeoutExpired: print("T")