installed a linter and formatter for python

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()