diff --git a/.ruff.toml b/.ruff.toml
new file mode 100644
index 0000000..e944eb1
--- /dev/null
+++ b/.ruff.toml
@@ -0,0 +1,8 @@
+indent-width = 2
+line-length = 320
+
+[format]
+quote-style = "single"
+
+[lint]
+ignore = ["E741"]
diff --git a/other/decompose_fsm.py b/other/decompose_fsm.py
index 4262e18..7b9a289 100644
--- a/other/decompose_fsm.py
+++ b/other/decompose_fsm.py
@@ -10,11 +10,11 @@ import argparse
 # Stap 1: pip3 install python-sat
 # Stap 2: python3 decompose_fsm.py -h
 
-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('-n', '--total-size', type=int, help='total number of states of the components')
-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('--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('filename', help='path to .dot file')
 args = parser.parse_args()
 
@@ -22,7 +22,7 @@ args = parser.parse_args()
 c = args.components
 total_size = args.total_size
 
-assert c >= 1           # c = 1 is zinloos, maar zou moeten werken
+assert c >= 1  # c = 1 is zinloos, maar zou moeten werken
 assert total_size >= c  # elk component heeft tenminste 1 state
 
 
@@ -46,6 +46,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('->')
@@ -83,6 +84,7 @@ def parse_dot_file(lines):
 
   return FSM(initial_state, states, inputs, outputs, transition_map, output_map)
 
+
 with open(args.filename) as file:
   machine = parse_dot_file(file)
   if args.verbose:
@@ -94,6 +96,7 @@ print(f'Initial size: {len(machine.states)}')
 ###################################
 # Utility functions
 
+
 def print_table(cell, rs, cs):
   first_col_size = max([len(str(r)) for r in rs])
   col_size = 1 + max([len(str(c)) for c in cs] + [len(cell(r, c)) for c in cs for r in rs])
@@ -109,6 +112,7 @@ def print_table(cell, rs, cs):
       print(cell(r, c).rjust(col_size), end='')
     print('')
 
+
 class Progress:
   def __init__(self, name, guess):
     self.reset(name, guess, show=False)
@@ -131,23 +135,27 @@ class Progress:
       print(f'{self.percentage}%', end='', flush=True)
       print('\r', end='')
 
+
 progress = Progress('', 1)
 
 ########################
 # Encodering naar logica
 print('Start encoding')
-os = list(machine.outputs)   # outputs
-rids = [i for i in range(c)] # components
+os = list(machine.outputs)  # outputs
+rids = [i for i in range(c)]  # components
 vpool = IDPool()
 cnf = CNF()
 
+
 # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
 def var_const(b):
-  return(vpool.id(('const', b)))
+  return vpool.id(('const', b))
+
 
 cnf.append([var_const(True)])
 cnf.append([-var_const(False)])
 
+
 # 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
 # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@@ -156,7 +164,8 @@ def var_rel(rid, o1, o2):
     return var_const(True)
 
   [so1, so2] = sorted([o1, o2])
-  return(vpool.id(('rel', rid, so1, so2)))
+  return vpool.id(('rel', rid, so1, so2))
+
 
 # De relatie op outputs geeft een relaties op states. Deze relatie moet ook een
 # bisimulatie zijn.
@@ -165,12 +174,14 @@ def var_state_rel(rid, s1, s2):
     return var_const(True)
 
   [ss1, ss2] = sorted([s1, s2])
-  return(vpool.id(('state_rel', rid, ss1, ss2)))
+  return vpool.id(('state_rel', rid, ss1, ss2))
+
 
 # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 state
 # als representant. Deze variabele geeft aan welk element.
 def var_state_rep(rid, s):
-  return(vpool.id(('state_rep', rid, s)))
+  return vpool.id(('state_rep', rid, s))
+
 
 # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
 # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@@ -197,7 +208,7 @@ if args.add_state_trans:
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
 progress.reset('injectivity', guess=len(os) * (len(os) - 1) / 2)
 for xi, xo in enumerate(os):
-  for yo in os[xi+1:]:
+  for yo in os[xi + 1 :]:
     # Tenminste een rid moet een verschil maken
     cnf.append([-var_rel(rid, xo, yo) for rid in rids])
     progress.add()
@@ -229,7 +240,7 @@ for rid in rids:
     # 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).
-    cnf.append([var_state_rep(rid, sx)] + [var_state_rel(rid, sx, sy) for sy in states[:ix]] )
+    cnf.append([var_state_rep(rid, sx)] + [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
@@ -244,6 +255,7 @@ print('size constraints')
 cnf_optim = CardEnc.atmost([var_state_rep(rid, sx) for rid in rids for sx in machine.states], total_size, vpool=vpool)
 cnf.extend(cnf_optim)
 
+
 def print_eqrel(rel, xs):
   print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs)
 
@@ -261,15 +273,14 @@ with Solver(bootstrap_with=cnf) as solver:
     print('unsat :-(')
     exit()
 
-  print(f'sat :-)')
+  print('sat :-)')
 
   # Even omzetten in een makkelijkere data structuur
   print('- get model')
   m = solver.get_model()
   model = {}
   for l in m:
-    if l < 0: model[-l] = False
-    else: model[l] = True
+    model[abs(l)] = l > 0
 
   if args.verbose:
     for rid in rids:
diff --git a/other/decompose_observation_table.py b/other/decompose_observation_table.py
index 9fa6d09..b8358da 100644
--- a/other/decompose_observation_table.py
+++ b/other/decompose_observation_table.py
@@ -11,18 +11,20 @@ from pysat.formula import CNF
 ###################################
 # Wat dingetjes over Mealy machines
 
+
 # Voorbeeld: 2n states, input-alfabet 'a' en 'b', outputs [0...n-1]
 def rick_koenders_machine(N):
-  transition_fun = {((n, False), 'a') : ((n+1) % N, False) for n in range(N)}
-  transition_fun |= {(((n+1) % N, True), 'a') : (n % N, True) for n in range(N)}
-  transition_fun |= {((n, b), 'b') : (n, not b) for b in [False, True] for n in range(N)}
-  output_fun = {((n, b), 'a') : n for b in [False, True] for n in range(N)}
-  output_fun |= {((n, b), 'b') : 0 for b in [False, True] for n in range(N)}
+  transition_fun = {((n, False), 'a'): ((n + 1) % N, False) for n in range(N)}
+  transition_fun |= {(((n + 1) % N, True), 'a'): (n % N, True) for n in range(N)}
+  transition_fun |= {((n, b), 'b'): (n, not b) for b in [False, True] for n in range(N)}
+  output_fun = {((n, b), 'a'): n for b in [False, True] for n in range(N)}
+  output_fun |= {((n, b), 'b'): 0 for b in [False, True] for n in range(N)}
   initial_state = (0, False)
   inputs = ['a', 'b']
   outputs = [n for n in range(N)]
   return {'transition_fun': transition_fun, 'output_fun': output_fun, 'initial_state': initial_state, 'inputs': inputs, 'outputs': outputs}
 
+
 def mealy_sem_q(machine, word, state):
   if len(word) == 0:
     return None
@@ -31,9 +33,11 @@ def mealy_sem_q(machine, word, state):
   else:
     return mealy_sem_q(machine, word[1:], machine['transition_fun'][(state, word[0])])
 
+
 def mealy_sem(machine, word):
   return mealy_sem_q(machine, word, machine['initial_state'])
 
+
 def print_table(cell, rs, cs):
   first_col_size = max([len(str(r)) for r in rs])
   col_size = 1 + max([len(str(c)) for c in cs])
@@ -52,7 +56,7 @@ def print_table(cell, rs, cs):
 
 ################
 # Voorbeeld data
-machine = rick_koenders_machine(4) # 8 states
+machine = rick_koenders_machine(4)  # 8 states
 
 # L* table: Niet noodzakelijk volledig, werkt ook met minder data, maar ik
 # weet niet wat voor garanties we dan kunnen geven. Het is sowieso maar de
@@ -60,7 +64,7 @@ machine = rick_koenders_machine(4) # 8 states
 rows = ['', 'a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'aab', 'aaab']
 cols = ['a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'ba', 'abab']
 
-print_table(lambda r, c: str(mealy_sem(machine, r+c)), rows, cols)
+print_table(lambda r, c: str(mealy_sem(machine, r + c)), rows, cols)
 
 # We zoeken 2 componenten met gezamelijke grootte 6 (minder dan 8)
 # als de de total_size te laag is => UNSAT => duurt lang
@@ -71,18 +75,21 @@ total_size = 6
 ########################
 # Encodering naar logica
 print('Start encoding')
-os = machine['outputs']      # outputs
-rids = [i for i in range(c)] # components
+os = machine['outputs']  # outputs
+rids = [i for i in range(c)]  # components
 vpool = IDPool()
 cnf = CNF()
 
+
 # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
 def var_const(b):
-  return(vpool.id(('const', b)))
+  return vpool.id(('const', b))
+
 
 cnf.append([var_const(True)])
 cnf.append([-var_const(False)])
 
+
 # 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
 # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@@ -91,7 +98,8 @@ def var_rel(rid, o1, o2):
     return var_const(True)
 
   [so1, so2] = sorted([o1, o2])
-  return(vpool.id(('rel', rid, so1, so2)))
+  return vpool.id(('rel', rid, so1, so2))
+
 
 # De relatie op outputs geeft een relaties op rijen. Deze zijn geindexeerd
 # met de woorden uit 'rows'.
@@ -100,12 +108,14 @@ def var_row_rel(rid, r1, r2):
     return var_const(True)
 
   [sr1, sr2] = sorted([r1, r2])
-  return(vpool.id(('row_rel', rid, sr1, sr2)))
+  return vpool.id(('row_rel', rid, sr1, sr2))
+
 
 # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 rij
 # als representant. Deze variabele geeft aan welk element.
 def var_row_rep(rid, r):
-  return(vpool.id(('row_rep', rid, r)))
+  return vpool.id(('row_rep', rid, r))
+
 
 # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
 # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@@ -130,7 +140,7 @@ for rid in rids:
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
 print('- injectivity (o)')
 for xi, xo in enumerate(os):
-  for yo in os[xi+1:]:
+  for yo in os[xi + 1 :]:
     # Tenminste een rid moet een verschil maken
     cnf.append([-var_rel(rid, xo, yo) for rid in rids])
 
@@ -147,7 +157,7 @@ for rid in rids:
       cnf.append([-var_rel(rid, ox, oy) for (ox, oy) in oss] + [var_row_rel(rid, rx, ry)])
 
       # rx ~ ry => oxi ~ oyi
-      for (ox, oy) in oss:
+      for ox, oy in oss:
         cnf.append([-var_row_rel(rid, rx, ry), var_rel(rid, ox, oy)])
 
 # De constraints die zorgen dat representanten ook echt representanten zijn.
@@ -157,7 +167,7 @@ for rid in rids:
     # 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).
-    cnf.append([var_row_rep(rid, rx)] + [var_row_rel(rid, rx, ry) for ry in rows[:ix]] )
+    cnf.append([var_row_rep(rid, rx)] + [var_row_rel(rid, rx, ry) for ry in rows[:ix]])
     for ry in rows[:ix]:
       # rx en ry kunnen niet beide een representant zijn, tenzij ze
       # niet gerelateerd zijn.
@@ -169,6 +179,7 @@ print('- representatives at most k')
 cnf_optim = CardEnc.atmost([var_row_rep(rid, rx) for rid in rids for rx in rows], total_size, vpool=vpool)
 cnf.extend(cnf_optim)
 
+
 def print_eqrel(rel, xs):
   print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs)
 
@@ -185,15 +196,14 @@ with Solver(bootstrap_with=cnf) as solver:
     print('unsat :-(')
     exit()
 
-  print(f'sat :-)')
+  print('sat :-)')
 
   # Even omzetten in een makkelijkere data structuur
   print('- get model')
   m = solver.get_model()
   model = {}
   for l in m:
-    if l < 0: model[-l] = False
-    else: model[l] = True
+    model[abs(l)] = l > 0
 
   for rid in rids:
     print(f'Relation {rid}:')
diff --git a/other/decompose_set.py b/other/decompose_set.py
index bbd1cf0..c1fd927 100644
--- a/other/decompose_set.py
+++ b/other/decompose_set.py
@@ -17,10 +17,10 @@ from pysat.formula import CNF
 # langzaam vb.:   n = 151, c = 4 en total_size = 15
 n = 151
 c = 4
-total_size = 15 # als deze te laag is => UNSAT => duurt lang
+total_size = 15  # als deze te laag is => UNSAT => duurt lang
 
-os = [i for i in range(n)] # outputs
-rids = [i for i in range(c)] # components
+os = [i for i in range(n)]  # outputs
+rids = [i for i in range(c)]  # components
 
 # Optimale decompositie met slechts verzamelingen. Zie ook A007600 (omkering
 # A000792) in de OEIS, dit groeit met ongeveer O(log(n)). Ik weet niet hoeveel
@@ -37,13 +37,16 @@ print('Start encoding')
 vpool = IDPool()
 cnf = CNF()
 
+
 # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
 def var_const(b):
-  return(vpool.id(('bool', b)))
+  return vpool.id(('bool', b))
+
 
 cnf.append([var_const(True)])
 cnf.append([-var_const(False)])
 
+
 # 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
 # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@@ -52,12 +55,14 @@ def var_rel(rid, o1, o2):
     return var_const(True)
 
   [so1, so2] = sorted([o1, o2])
-  return(vpool.id(('var_rel', rid, so1, so2)))
+  return vpool.id(('var_rel', rid, so1, so2))
+
 
 # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 element
 # als representant. Deze variabele geeft aan welk element.
 def var_rep(rid, o):
-  return(vpool.id(('var_rep', rid, o)))
+  return vpool.id(('var_rep', rid, o))
+
 
 # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
 # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@@ -74,7 +79,7 @@ for rid in rids:
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
 print('- injectivity')
 for xi, xo in enumerate(os):
-  for yo in os[xi+1:]:
+  for yo in os[xi + 1 :]:
     # Tenminste een rid moet een verschil maken
     cnf.append([-var_rel(rid, xo, yo) for rid in rids])
 
@@ -85,8 +90,8 @@ for rid in rids:
     # Belangrijkste: een element is een representant, of equivalent met een
     # later element. We forceren hiermee dat de solver representanten moet
     # kiezen (achter aan de lijst).
-    cnf.append([var_rep(rid, xo)] + [var_rel(rid, xo, yo) for yo in os[xi+1:]] )
-    for _, yo in enumerate(os[xi+1:], xi+1):
+    cnf.append([var_rep(rid, xo)] + [var_rel(rid, xo, yo) for yo in os[xi + 1 :]])
+    for _, yo in enumerate(os[xi + 1 :], xi + 1):
       # xo en yo kunnen niet beide een representant zijn, tenzij ze
       # niet gerelateerd zijn.
       cnf.append([-var_rep(rid, xo), -var_rep(rid, yo), -var_rel(rid, xo, yo)])
@@ -109,15 +114,14 @@ with Solver(bootstrap_with=cnf) as solver:
     print('unsat :-(')
     exit()
 
-  print(f'sat :-)')
+  print('sat :-)')
 
   # Even omzetten in een makkelijkere data structuur
   print('- get model')
   m = solver.get_model()
   model = {}
   for l in m:
-    if l < 0: model[-l] = False
-    else: model[l] = True
+    model[abs(l)] = l > 0
 
   # print equivalence classes
   count = 0
diff --git a/other/fsm-examples.py b/other/fsm-examples.py
index 92ba690..0fa0ce2 100644
--- a/other/fsm-examples.py
+++ b/other/fsm-examples.py
@@ -1,5 +1,6 @@
 import argparse
 
+
 class RKMachine:
   # Rick Koenders came up with this example in the case of N=3.
   # FSM will have 2*N states, but can be decomposed into N + 2 states.
@@ -10,12 +11,12 @@ class RKMachine:
     self.outputs = [n for n in range(N)]
     self.states = [(n, b) for b in [False, True] for n in range(N)]
 
-    self.transition_map = {((n, 0), 'a') : ((n+1) % N, 0) for n in range(N)}
-    self.transition_map |= {(((n+1) % N, 1), 'a') : (n % N, 1) for n in range(N)}
-    self.transition_map |= {((n, b), 'b') : (n, not b) for b in [False, True] for n in range(N)}
+    self.transition_map = {((n, 0), 'a'): ((n + 1) % N, 0) for n in range(N)}
+    self.transition_map |= {(((n + 1) % N, 1), 'a'): (n % N, 1) for n in range(N)}
+    self.transition_map |= {((n, b), 'b'): (n, not b) for b in [False, True] for n in range(N)}
 
-    self.output_map = {((n, b), 'a') : n for b in [False, True] for n in range(N)}
-    self.output_map |= {((n, b), 'b') : 0 for b in [False, True] for n in range(N)}
+    self.output_map = {((n, b), 'a'): n for b in [False, True] for n in range(N)}
+    self.output_map |= {((n, b), 'b'): 0 for b in [False, True] for n in range(N)}
 
   def state_to_string(self, s):
     (n, b) = s
@@ -27,6 +28,7 @@ class RKMachine:
   def output(self, s, a):
     return self.output_map[(s, a)]
 
+
 def fsm_to_dot(name, m):
   def transition_string(s, i, o, t):
     return f'{s} -> {t} [label="{i}/{o}"]'
@@ -44,6 +46,7 @@ def fsm_to_dot(name, m):
 
   return ret
 
+
 parser = argparse.ArgumentParser()
 parser.add_argument('machine', nargs='?', default='rk', choices=['rk'])
 parser.add_argument('-n', type=int, default=3, help='size parameter')
diff --git a/other/partitions.py b/other/partitions.py
index a8ae540..30ae466 100644
--- a/other/partitions.py
+++ b/other/partitions.py
@@ -4,21 +4,24 @@ from math import prod
 N = 99999
 C = 16
 
+
 # precondition k <= n
 def all_partitions_(n, k):
   if n == 0:
     return [[]]
 
   acc = []
-  for j in range(1, k+1):
-    ps = all_partitions_(n-j, min(n-j, j))
-    acc.extend([[j]+p for p in ps])
+  for j in range(1, k + 1):
+    ps = all_partitions_(n - j, min(n - j, j))
+    acc.extend([[j] + p for p in ps])
 
   return acc
 
+
 def all_partitions(n):
   return all_partitions_(n, n)
 
+
 def highest_product(n):
   ps = all_partitions(n)
 
@@ -37,20 +40,22 @@ def highest_product(n):
 
   return highest_prod
 
+
 def tabulate(upper):
   highest_n_per_c = {}
   table = {}
-  for s in range(1, upper+1):
+  for s in range(1, upper + 1):
     res = highest_product(s)
 
     for c, n in res.items():
-      for n2 in range(highest_n_per_c.get(c, 0)+1, min(n, N)+1):
+      for n2 in range(highest_n_per_c.get(c, 0) + 1, min(n, N) + 1):
         table[(n2, c)] = s
 
       highest_n_per_c[c] = n
 
   return {(n, c): s for (n, c), s in table.items() if s <= n}
 
+
 def trim_tab(tab):
   best_s = {}
   best_c = {}
@@ -65,6 +70,7 @@ def trim_tab(tab):
 
   return {(n, c): s for (n, c), s in tab.items() if c <= best_c[n] or s <= best_s[n]}
 
+
 def print_table(tab0):
   tab = trim_tab(tab0)
 
@@ -79,10 +85,10 @@ def print_table(tab0):
 
   prev_row = ''
 
-  for n in range(1, N+1):
+  for n in range(1, N + 1):
     best = None
     row = ''
-    for c in range(1, C+1):
+    for c in range(1, C + 1):
       if (n, c) in tab:
         row += ' ' + str(tab[(n, c)]).rjust(col_width[c])
         if not best or tab[(n, c)] < best[0]: