From 353d191c0c6d62c65cbda62a1310911e06e6ee22 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 14 Jun 2024 14:00:25 +0200 Subject: [PATCH] installed a linter and formatter for python --- other/decompose_fsm_optimise.py | 36 +++++++++++++++++---------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/other/decompose_fsm_optimise.py b/other/decompose_fsm_optimise.py index 14d0a49..e63f860 100644 --- a/other/decompose_fsm_optimise.py +++ b/other/decompose_fsm_optimise.py @@ -1,7 +1,6 @@ from pysat.solvers import Solver from pysat.card import ITotalizer from pysat.formula import IDPool -from pysat.formula import CNF import signal import math @@ -13,14 +12,15 @@ import argparse keep_log = True + def main(): record_file = './results/log.txt' if keep_log else None - parser = argparse.ArgumentParser(description="Decomposes a FSM into smaller components by remapping its outputs. Uses a SAT solver.") + parser = argparse.ArgumentParser(description='Decomposes a FSM into smaller components by remapping its outputs. Uses a SAT solver.') parser.add_argument('-c', '--components', type=int, default=2, help='number of components') - parser.add_argument('-w', '--weak', default=False, action="store_true", help='look for weak decomposition') - parser.add_argument('--add-state-trans', default=False, action="store_true", help='adds state transitivity constraints') - parser.add_argument('-v', '--verbose', default=False, action="store_true", help='prints more info') + parser.add_argument('-w', '--weak', default=False, action='store_true', help='look for weak decomposition') + parser.add_argument('--add-state-trans', default=False, action='store_true', help='adds state transitivity constraints') + parser.add_argument('-v', '--verbose', default=False, action='store_true', help='prints more info') parser.add_argument('-t', '--timeout', type=int, default=None, help='timeout (in seconds)') parser.add_argument('filename', help='path to .dot file') args = parser.parse_args() @@ -36,7 +36,8 @@ def main(): print(f'Input FSM: {len(machine.states)} states, {len(machine.inputs)} inputs, and {len(machine.outputs)} outputs') - if args.timeout != None: + if args.timeout: + def timeout_handler(*_): with open(record_file, 'a') as file: last_two_comps = '/'.join(args.filename.split('/')[-2:]) @@ -71,6 +72,7 @@ class FSM: def output(self, s, a): return self.output_map[(s, a)] + def parse_dot_file(lines): def parse_transition(line): (l, _, r) = line.partition('->') @@ -126,6 +128,7 @@ def print_table(cell, rs, cs): print(cell(r, c).rjust(col_size), end='') print('') + def print_eqrel(rel, xs): print_table(lambda r, c: 'Y' if rel(r, c) else 'ยท', xs, xs) @@ -164,8 +167,8 @@ class Encoder: self.c = self.args.components self.N = len(self.machine.states) - self.os = list(machine.outputs) # outputs - self.rids = [i for i in range(self.c)] # components + self.os = list(machine.outputs) # outputs + self.rids = [i for i in range(self.c)] # components self.vpool = IDPool() self.solver = Solver() @@ -179,7 +182,7 @@ class Encoder: # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger def var_const(self, b): - return(self.vpool.id(('const', b))) + return self.vpool.id(('const', b)) # Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die # aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus @@ -236,7 +239,7 @@ class Encoder: # (Aka: the bijbehorende quotienten zijn joint-injective.) self.progress.reset('injectivity', guess=len(self.os) * (len(self.os) - 1) / 2) for xi, xo in enumerate(self.os): - for yo in self.os[xi+1:]: + for yo in self.os[xi + 1 :]: # Tenminste een rid moet een verschil maken self.add_clause([-self.var_rel(rid, xo, yo) for rid in self.rids]) self.progress.add() @@ -268,7 +271,7 @@ class Encoder: # Belangrijkste: een element is een representant, of equivalent met een # eerder element. We forceren hiermee dat de solver representanten moet # kiezen (voor aan de lijst). - self.add_clause([self.var_state_rep(rid, sx)] + [self.var_state_rel(rid, sx, sy) for sy in states[:ix]] ) + self.add_clause([self.var_state_rep(rid, sx)] + [self.var_state_rel(rid, sx, sy) for sy in states[:ix]]) for sy in states[:ix]: # rx en ry kunnen niet beide een representant zijn, tenzij ze @@ -281,7 +284,7 @@ class Encoder: # formule. We gaan een binaire zoek doen met incremental sat solving. self.rhs = None if self.args.weak: - self.lower_bound = int(math.floor((self.N-1)**(1/self.c))) + self.lower_bound = int(math.floor((self.N - 1) ** (1 / self.c))) self.upper_bound = int(self.N) print(f'weak size constraints {self.lower_bound} {self.upper_bound}') self.rhs = [] @@ -292,7 +295,7 @@ class Encoder: self.add_clauses(cnf_optim.cnf.clauses) self.rhs.append(cnf_optim.rhs) else: - self.lower_bound = int(math.floor(self.c * (self.N-1)**(1/self.c))) + self.lower_bound = int(math.floor(self.c * (self.N - 1) ** (1 / self.c))) self.upper_bound = int(self.N + self.c - 1) print(f'size constraints {self.lower_bound} {self.upper_bound}') with ITotalizer([self.var_state_rep(rid, sx) for rid in self.rids for sx in self.machine.states], ubound=self.upper_bound, top_id=self.vpool.top) as cnf_optim: @@ -334,8 +337,7 @@ class Encoder: m = self.solver.get_model() model = {} for l in m: - if l < 0: model[-l] = False - else: model[l] = True + model[abs(l)] = l > 0 if self.args.verbose: for rid in self.rids: @@ -359,7 +361,7 @@ class Encoder: counts.append(count) print(f'Reduced sizes = {counts} = {sum(counts)}') - if self.record_file != None: + if self.record_file: with open(self.record_file, 'a') as file: last_two_comps = '/'.join(self.args.filename.split('/')[-2:]) file.write(f'{last_two_comps}\t{self.N}\t{len(self.machine.inputs)}\t{len(self.machine.outputs)}\t{self.args.weak}\t{self.c}\t{sum(counts)}\t{sorted(counts, reverse=True)}\n') @@ -396,5 +398,5 @@ class Encoder: ################################### # Run script -if __name__ == "__main__": +if __name__ == '__main__': main()