Added dot parser for python to the sat solver

other/decompose_fsm.py

@@ -12,6 +12,7 @@ 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('filename', help='path to .dot file')
 args = parser.parse_args()
 
 # als de de total_size te laag is => UNSAT => duurt lang
@@ -23,19 +24,69 @@ assert total_size >= c  # elk component heeft tenminste 1 state
 
 
 ###################################
-# Wat dingetjes over Mealy machines
+# .dot file parser (heuristic)
+class FSM:
+  def __init__(self, initial_state, states, inputs, outputs, transition_map, output_map):
+    self.initial_state = initial_state
+    self.states = states
+    self.inputs = inputs
+    self.outputs = outputs
+    self.transition_map = transition_map
+    self.output_map = output_map
 
-# Voorbeeld: 2n states, input-alfabet 'a' en 'b', outputs [0...n-1]
-def rick_koenders_machine(N):
-  transition_fun = {((n, 0), 'a') : ((n+1) % N, 0) for n in range(N)}
-  transition_fun |= {(((n+1) % N, 1), 'a') : (n % N, 1) for n in range(N)}
-  transition_fun |= {((n, b), 'b') : (n, not b) for b in [0, 1] for n in range(N)}
-  output_fun = {((n, b), 'a') : n for b in [0, 1] for n in range(N)}
-  output_fun |= {((n, b), 'b') : 0 for b in [0, 1] for n in range(N)}
-  initial_state = (0, 0)
-  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 __str__(self):
+    return f'FSM({self.initial_state}, {self.states}, {self.inputs}, {self.outputs}, {self.transition_map}, {self.output_map})'
+
+  def transition(self, s, a):
+    return self.transition_map[(s, a)]
+
+  def output(self, s, a):
+    return self.output_map[(s, a)]
+
+def parse_dot_file(lines):
+  def parse_transition(line):
+    (l, _, r) = line.partition('->')
+    s = l.strip()
+
+    (l, _, r) = r.partition('[label="')
+    t = l.strip()
+
+    (l, _, _) = r.partition('"]')
+    (i, _, o) = l.partition('/')
+
+    return (s, i, o, t)
+
+  initial_state = None
+  states, inputs, outputs = set(), set(), set()
+  transition_map, output_map = {}, {}
+
+  for line in lines:
+    (s, i, o, t) = parse_transition(line)
+    if s and i and o and t:
+      states.add(s)
+      inputs.add(i)
+      outputs.add(o)
+      states.add(t)
+
+      transition_map[(s, i)] = t
+      output_map[(s, i)] = o
+
+      if not initial_state:
+        initial_state = s
+
+  assert initial_state in states
+  assert len(transition_map) == len(states) * len(inputs)
+  assert len(output_map) == len(states) * len(inputs)
+
+  return FSM(initial_state, states, inputs, outputs, transition_map, output_map)
+
+with open(args.filename) as file:
+  machine = parse_dot_file(file)
+  print(machine)
+
+
+###################################
+# Utility function
 
 def print_table(cell, rs, cs):
   first_col_size = max([len(str(r)) for r in rs])
@@ -53,17 +104,10 @@ def print_table(cell, rs, cs):
     print('')
 
 
-################
-# Voorbeeld data
-N = 8
-machine = rick_koenders_machine(N)
-states = [(n, b) for n in range(N) for b in [0, 1]]
-
-
 ########################
 # Encodering naar logica
 print('Start encoding')
-os = machine['outputs']      # outputs
+os = list(machine.outputs)   # outputs
 rids = [i for i in range(c)] # components
 vpool = IDPool()
 cnf = CNF()
@@ -112,9 +156,9 @@ for rid in rids:
 
 print('- transitivity (s)')
 for rid in rids:
-  for sx in states:
-    for sy in states:
-      for sz in states:
+  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)])
 
@@ -130,21 +174,22 @@ for xi, xo in enumerate(os):
 # Momenteel hebben we niet de inverse implicatie, is misschien ook niet nodig?
 print('- bisimulation modulo rel')
 for rid in rids:
-  for sx in states:
-    for sy in states:
-      for i in machine['inputs']:
+  for sx in machine.states:
+    for sy in machine.states:
+      for i in machine.inputs:
         # sx ~ sy => output(sx, i) ~ output(sy, i)
-        ox = machine['output_fun'][(sx, i)]
-        oy = machine['output_fun'][(sy, i)]
+        ox = machine.output(sx, i)
+        oy = machine.output(sy, i)
         cnf.append([-var_state_rel(rid, sx, sy), var_rel(rid, ox, oy)])
 
         # sx ~ sy => delta(sx, i) ~ delta(sy, i)
-        tx = machine['transition_fun'][(sx, i)]
-        ty = machine['transition_fun'][(sy, i)]
+        tx = machine.transition(sx, i)
+        ty = machine.transition(sy, i)
         cnf.append([-var_state_rel(rid, sx, sy), var_state_rel(rid, tx, ty)])
 
 # De constraints die zorgen dat representanten ook echt representanten zijn.
 print('- representatives')
+states = list(machine.states)
 for rid in rids:
   for ix, sx in enumerate(states):
     # Belangrijkste: een element is een representant, of equivalent met een
@@ -159,7 +204,7 @@ for rid in rids:
 # 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')
-cnf_optim = CardEnc.atmost([var_state_rep(rid, sx) for rid in rids for sx in states], total_size, vpool=vpool)
+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):
@@ -194,14 +239,14 @@ with Solver(bootstrap_with=cnf) as solver:
 
   for rid in rids:
     print(f'State relation {rid}:')
-    print_eqrel(lambda x, y: model[var_state_rel(rid, x, y)], states)
+    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}')
     # Eerst verzamelen we de representanten
-    for s in states:
+    for s in machine.states:
       if model[var_state_rep(rid, s)]:
         print(f'- representative state {s}')
         count += 1

other/fsm-examples.py

@@ -0,0 +1,53 @@
+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.
+  # For N <= 2, the machine is NOT minimal, i.e., there are equivalent states.
+  def __init__(self, N):
+    self.initial_state = (0, False)
+    self.inputs = ['a', 'b']
+    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.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
+    return f's{n}Dn' if b else f's{n}Up'
+
+  def transition(self, s, a):
+    return self.transition_map[(s, a)]
+
+  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}"]'
+
+  ret = f'digraph {name} {{\n'
+  for s in m.states:
+    for a in m.inputs:
+      t = m.transition(s, a)
+      o = m.output(s, a)
+      ret += '  '
+      ret += transition_string(m.state_to_string(s), a, o, m.state_to_string(t))
+      ret += '\n'
+
+  ret += '}\n'
+
+  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')
+args = parser.parse_args()
+
+if args.machine == 'rk':
+  print(fsm_to_dot(f'RKMachine_{args.n}', RKMachine(args.n)))