adds progress when constructing the formula

other/decompose_fsm.py

@@ -3,6 +3,7 @@ from pysat.card import CardEnc
 from pysat.formula import IDPool
 from pysat.formula import CNF
 
+import math
 import argparse
 
 ### Gebruik:
@@ -91,7 +92,7 @@ print(f'Initial size: {len(machine.states)}')
 
 
 ###################################
-# Utility function
+# Utility functions
 
 def print_table(cell, rs, cs):
   first_col_size = max([len(str(r)) for r in rs])
@@ -108,6 +109,29 @@ 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)
+
+  def reset(self, name, guess, show=True):
+    self.name = name
+    self.guess = math.ceil(guess)
+    self.count = 0
+    self.percentage = None
+
+    if show:
+      print(name)
+
+  def add(self, n=1):
+    self.count += n
+    percentage = math.floor(100 * self.count / self.guess)
+
+    if percentage != self.percentage:
+      self.percentage = percentage
+      print(f'{self.percentage}%', end='', flush=True)
+      print('\r', end='')
+
+progress = Progress('', 1)
 
 ########################
 # Encodering naar logica
@@ -150,35 +174,37 @@ def var_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.
-# Dit stukje van het encoderen duurt het langst.
-print('- transitivity (o)')
+progress.reset('transitivity (o)', guess=len(rids) * len(os) ** 3)
 for rid in rids:
   for xo in os:
     for yo in os:
       for zo in os:
         # 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)])
+        progress.add()
 
 if args.add_state_trans:
-  print('- transitivity (s)')
+  progress.reset('transitivity (s)', guess=len(rids) * len(machine.states) ** 3)
   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)])
+          progress.add()
 
 # Constraint zodat de relaties samen alle elementen kunnen onderscheiden.
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
-print('- injectivity (o)')
+progress.reset('injectivity', guess=len(os) * (len(os) - 1) / 2)
 for xi, xo in enumerate(os):
   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()
 
 # sx ~ sy => for each input: (1) outputs equivalent AND (2) successors related
 # Momenteel hebben we niet de inverse implicatie, is misschien ook niet nodig?
-print('- bisimulation modulo rel')
+progress.reset('bisimulation modulo rel', guess=len(rids) * len(machine.states) * len(machine.states) * len(machine.inputs))
 for rid in rids:
   for sx in machine.states:
     for sy in machine.states:
@@ -193,23 +219,28 @@ for rid in rids:
         ty = machine.transition(sy, i)
         cnf.append([-var_state_rel(rid, sx, sy), var_state_rel(rid, tx, ty)])
 
+        progress.add()
+
 # De constraints die zorgen dat representanten ook echt representanten zijn.
-print('- representatives')
 states = list(machine.states)
+progress.reset('representatives', guess=len(rids) * len(states))
 for rid in rids:
   for ix, sx in enumerate(states):
     # 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]] )
+
     for sy in states[:ix]:
       # rx en ry kunnen niet beide een representant zijn, tenzij ze
       # niet gerelateerd zijn.
       cnf.append([-var_state_rep(rid, sx), -var_state_rep(rid, sy), -var_state_rel(rid, sx, sy)])
 
+    progress.add()
+
 # Tot slot willen we weinig representanten. Dit doen we met een "atmost"
 # formule. Idealiter zoeken we naar de total_size, maar die staat nu vast.
-print('- representatives at most k')
+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)