More flags and optimisation

other/decompose_fsm.py

@@ -12,6 +12,8 @@ import argparse
 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('filename', help='path to .dot file')
 args = parser.parse_args()
 
@@ -82,7 +84,8 @@ def parse_dot_file(lines):
 
 with open(args.filename) as file:
   machine = parse_dot_file(file)
-  print(machine)
+  if args.verbose:
+    print(machine)
 
 
 ###################################
@@ -90,7 +93,7 @@ with open(args.filename) as file:
 
 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])
+  col_size = 1 + max([len(str(c)) for c in cs] + [len(cell(r, c)) for c in cs for r in rs])
 
   print(''.rjust(first_col_size), end='')
   for c in cs:
@@ -154,13 +157,14 @@ for rid in rids:
         # als xo R yo en yo R zo dan xo R zo
         cnf.append([-var_rel(rid, xo, yo), -var_rel(rid, yo, zo), var_rel(rid, xo, zo)])
 
-print('- transitivity (s)')
-for rid in rids:
-  for sx in machine.states:
-    for sy in machine.states:
-      for sz in machine.states:
-        # als sx R sy en sy R sz dan sx R sz
-        cnf.append([-var_state_rel(rid, sx, sy), -var_state_rel(rid, sy, sz), var_state_rel(rid, sx, sz)])
+if args.add_state_trans:
+  print('- transitivity (s)')
+  for rid in rids:
+    for sx in machine.states:
+      for sy in machine.states:
+        for sz in machine.states:
+          # als sx R sy en sy R sz dan sx R sz
+          cnf.append([-var_state_rel(rid, sx, sy), -var_state_rel(rid, sy, sz), var_state_rel(rid, sx, sz)])
 
 # Constraint zodat de relaties samen alle elementen kunnen onderscheiden.
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
@@ -233,23 +237,54 @@ with Solver(bootstrap_with=cnf) as solver:
     if l < 0: model[-l] = False
     else: model[l] = True
 
-  for rid in rids:
-    print(f'Relation {rid}:')
-    print_eqrel(lambda x, y: model[var_rel(rid, x, y)], os)
+  if args.verbose:
+    for rid in rids:
+      print(f'Relation {rid}:')
+      print_eqrel(lambda x, y: model[var_rel(rid, x, y)], os)
 
-  for rid in rids:
-    print(f'State relation {rid}:')
-    print_eqrel(lambda x, y: model[var_state_rel(rid, x, y)], machine.states)
+    for rid in rids:
+      print(f'State relation {rid}:')
+      print_eqrel(lambda x, y: model[var_state_rel(rid, x, y)], machine.states)
 
   # print equivalence classes
   count = 0
   for rid in rids:
-    print(f'component {rid}')
+    if args.verbose:
+      print(f'component {rid}')
     # Eerst verzamelen we de representanten
     for s in machine.states:
       if model[var_state_rep(rid, s)]:
-        print(f'- representative state {s}')
         count += 1
+        if args.verbose:
+          print(f'- representative state {s}')
 
-  # count moet gelijk zijn aan cost
+  # count moet gelijk zijn aan cost (of kleiner)
   print(f'total size = {count}')
+
+  projections = {}
+  for rid in rids:
+    local_outputs = machine.outputs.copy()
+    projections[rid] = {}
+    count = 0
+
+    while local_outputs:
+      repr = local_outputs.pop()
+      if repr in projections[rid]:
+        continue
+
+      projections[rid][repr] = f'cls_{rid}_{count}'
+      others = False
+
+      for o in local_outputs:
+        if model[var_rel(rid, o, repr)]:
+          others = True
+          projections[rid][o] = f'cls_{rid}_{count}'
+
+      if not others:
+        projections[rid][repr] = f'{repr}'
+
+      count += 1
+
+print('===============')
+print('Output mapping:')
+print_table(lambda o, rid: projections[rid][o], machine.outputs, rids)