Merge pull request #93 from taburg/rpni-mealy-fix

Fix regression in classic RPNI with Mealy machines

Author: Edi Muškardin

DotModels/SimpleABC/simple_abc_dfa.dot

@@ -0,0 +1,12 @@
+digraph simpleABCDfa {
+s0 [label="s0"];
+s1 [label="s1", shape=doublecircle];
+s0 -> s1 [label="a"];
+s0 -> s0 [label="b"];
+s0 -> s0 [label="c"];
+s1 -> s1 [label="a"];
+s1 -> s0 [label="b"];
+s1 -> s0 [label="c"];
+__start0 [shape=none, label=""];
+__start0 -> s0 [label=""];
+}

DotModels/SimpleABC/simple_abc_mealy.dot

@@ -0,0 +1,8 @@
+digraph simpleABCmealy{
+s0 [label="s0"];
+s0 -> s0 [label="a/1"];
+s0 -> s0 [label="b/2"];
+s0 -> s0 [label="c/3"];
+__start0 [shape=none, label=""];
+__start0 -> s0 [label=""];
+}

DotModels/SimpleABC/simple_abc_moore.dot

@@ -0,0 +1,21 @@
+digraph simpleABCmoore{
+s0 [label="s0|0", shape=record, style=rounded];
+s1 [label="s1|1", shape=record, style=rounded];
+s2 [label="s2|2", shape=record, style=rounded];
+s3 [label="s3|3", shape=record, style=rounded];
+s0 -> s1 [label="a"];
+s0 -> s2 [label="b"];
+s0 -> s3 [label="c"];
+s1 -> s1 [label="a"];
+s1 -> s2 [label="b"];
+s1 -> s3 [label="c"];
+s2 -> s1 [label="a"];
+s2 -> s2 [label="b"];
+s2 -> s3 [label="c"];
+s3 -> s1 [label="a"];
+s3 -> s2 [label="b"];
+s3 -> s3 [label="c"];
+__start0 [shape=none, label=""];
+__start0 -> s0 [label=""];
+}
+

aalpy/learning_algs/deterministic_passive/ClassicRPNI.py

@@ -12,7 +12,7 @@ def __init__(self, data, automaton_type, print_info=True):
 
         pta_construction_start = time.time()
         self.root_node = createPTA(data, automaton_type)
-        self.test_data = extract_unique_sequences(self.root_node)
+        self.test_data = extract_unique_sequences(self.root_node, automaton_type)
 
         if self.print_info:
             print(f'PTA Construction Time: {round(time.time() - pta_construction_start, 2)}')
@@ -27,7 +27,7 @@ def run_rpni(self):
             merged = False
 
             for red_state in red:
-                if not self._compatible_states(red_state, lex_min_blue):
+                if not red_state.compatible_outputs(lex_min_blue):
                     continue
                 merge_candidate = self._merge(red_state, lex_min_blue, copy_nodes=True)
                 if self._compatible(merge_candidate):
@@ -62,21 +62,6 @@ def _compatible(self, root_node):
                 return False
         return True
 
-    def _compatible_states(self, red_node, blue_node):
-        """
-        Only allow merging of states that have same output(s).
-        """
-        if self.automaton_type != 'mealy':
-            # None is compatible with everything
-            return red_node.output == blue_node.output or red_node.output is None or blue_node.output is None
-        else:
-            red_io = {i: o for i, o in red_node.children.keys()}
-            blue_io = {i: o for i, o in blue_node.children.keys()}
-            for common_i in set(red_io.keys()).intersection(blue_io.keys()):
-                if red_io[common_i] != blue_io[common_i]:
-                    return False
-        return True
-
     def _merge(self, red_node, lex_min_blue, copy_nodes=False):
         """
         Merge two states and return the root node of resulting model.
@@ -112,18 +97,12 @@ def _fold(self, red_node, blue_node):
                 red_node.children[i] = blue_node.children[i]
 
     def _fold_mealy(self, red_node, blue_node):
-        blue_io_map = {i: o for i, o in blue_node.children.keys()}
+        for i, o in blue_node.output.items():
+            red_node.output[i] = o
 
-        updated_keys = {}
-        for io, val in red_node.children.items():
-            o = blue_io_map[io[0]] if io[0] in blue_io_map.keys() else io[1]
-            updated_keys[(io[0], o)] = val
-
-        red_node.children = updated_keys
-
-        for io in blue_node.children.keys():
-            if io in red_node.children.keys():
-                self._fold_mealy(red_node.children[io], blue_node.children[io])
+        for i in blue_node.children.keys():
+            if i in red_node.children.keys():
+                self._fold_mealy(red_node.children[i], blue_node.children[i])
             else:
-                red_node.children[io] = blue_node.children[io]
+                red_node.children[i] = blue_node.children[i]
 

aalpy/learning_algs/deterministic_passive/rpni_helper_functions.py

@@ -34,6 +34,9 @@ def __hash__(self):
         return id(self)  # TODO This is a hack
 
     def compatible_outputs(self, other):
+        """
+        Only allow merging of states that have same output(s).
+        """
         # None is compatible with everything
         if self.type != 'mealy':
             return self.output == other.output or self.output is None or other.output is None
@@ -59,10 +62,9 @@ def check_sequence(root_node, seq, automaton_type):
     curr_node = root_node
     for i, o in seq:
         if automaton_type == 'mealy':
-            input_outputs = {i: o for i, o in curr_node.children.keys()}
-            if i[0] not in input_outputs.keys() or o is not None and input_outputs[i[0]] != o:
+            if i not in curr_node.output or o is not None and curr_node.output[i] != o:
                 return False
-            curr_node = curr_node.children[(i[0], input_outputs[i[0]])]
+            curr_node = curr_node.children[i]
         else:
             # For dfa and moore, check if outputs are the same, iff output in test data is concrete (not None)
             curr_node = curr_node.children[i]
@@ -98,7 +100,7 @@ def createPTA(data, automaton_type):
     return root_node
 
 
-def extract_unique_sequences(root_node):
+def extract_unique_sequences(root_node, automaton_type):
     def get_leaf_nodes(root):
         leaves = []
 
@@ -119,7 +121,10 @@ def _get_leaf_nodes(node):
         curr_node = root_node
         for i in node.prefix:
             curr_node = curr_node.children[i]
-            seq.append((i, curr_node.output))
+            if automaton_type == 'mealy':
+                seq.append((i, curr_node.output.get(i)))
+            else:
+                seq.append((i, curr_node.output))
         paths.append(seq)
 
     return paths

tests/test_deterministic_passive.py

@@ -0,0 +1,70 @@
+import unittest
+from itertools import product
+
+import aalpy
+from aalpy.automata import Dfa, MooreMachine, MealyMachine
+from aalpy.learning_algs import run_RPNI
+from aalpy.utils import load_automaton_from_file
+# from aalpy.utils.ModelChecking import bisimilar
+from aalpy.utils.ModelChecking import compare_automata
+
+correct_automata = {Dfa: load_automaton_from_file('../DotModels/SimpleABC/simple_abc_dfa.dot', automaton_type='dfa'),
+                    MooreMachine: load_automaton_from_file('../DotModels/SimpleABC/simple_abc_moore.dot', automaton_type='moore'),
+                    MealyMachine: load_automaton_from_file('../DotModels/SimpleABC/simple_abc_mealy.dot', automaton_type='mealy')}
+
+
+class DeterministicPassiveTest(unittest.TestCase):
+
+    def prove_equivalence(self, learned_automaton):
+
+        correct_automaton = correct_automata[learned_automaton.__class__]
+
+        # only work if correct automaton is already minimal
+        if len(learned_automaton.states) != len(correct_automaton.states):
+            print(len(learned_automaton.states), len(correct_automaton.states))
+            return False
+
+        return correct_automaton == learned_automaton  # bisimilar
+
+    def generate_data(self, ground_truth, depth=5):
+        data = []
+        if isinstance(ground_truth, aalpy.automata.Dfa) or isinstance(ground_truth, aalpy.automata.MooreMachine):
+            data.append(((), ground_truth.initial_state.output))
+    
+        alphabet = ground_truth.get_input_alphabet()
+        for level in range(1, depth + 1):
+            for seq in product(alphabet, repeat=level):
+                ground_truth.reset_to_initial()
+                outputs = ground_truth.execute_sequence(ground_truth.initial_state, seq)
+                data.append((seq, outputs[-1]))
+
+        return data
+
+    # TODO incomplete: skips input completeness options
+    def test_all_configuration_combinations(self):
+
+
+        automata_type = {Dfa: 'dfa', MooreMachine: 'moore', MealyMachine: 'mealy'}
+        algorithms = ['gsm', 'classic']
+
+        for automata in correct_automata:
+            correct_automaton = correct_automata[automata]
+            alphabet = correct_automaton.get_input_alphabet()
+            data = self.generate_data(correct_automaton, depth=3)
+            for algorithm in algorithms:
+                learned_model = run_RPNI(data,
+                                         automaton_type=automata_type[automata],
+                                         algorithm=algorithm,
+                                         print_info=False)
+
+                is_eq = self.prove_equivalence(learned_model)
+                if not is_eq:
+                    print("Learned:")
+                    print(learned_model)
+                    print(algorithm, automata_type[automata])
+                    cex = compare_automata(learned_model, correct_automaton)
+                    print(cex)
+                    assert False
+
+        assert True
+