Merge pull request #82 from lkruger27/dfa-moore

Add DFA and Moore functionality for L# and adaptive L#

Author: emuskardin

Examples.py

@@ -45,6 +45,29 @@ def angluin_seminal_example():
     assert learned_dfa == dfa
     return learned_dfa
 
+def angluin_seminal_example_lsharp():
+    """
+    Example automaton from Angluin's seminal paper.
+    :return: learned DFA
+    """
+    from aalpy.SULs import AutomatonSUL
+    from aalpy.oracles import RandomWalkEqOracle
+    from aalpy.learning_algs import run_Lstar, run_Lsharp
+    from aalpy.utils import get_Angluin_dfa
+
+    dfa = get_Angluin_dfa()
+
+    alphabet = dfa.get_input_alphabet()
+
+    sul = AutomatonSUL(dfa)
+    eq_oracle = RandomWalkEqOracle(alphabet, sul, 500)
+
+    learned_dfa = run_Lsharp(alphabet, sul, eq_oracle, automaton_type='dfa',
+                            extension_rule="SepSeq", separation_rule="ADS", max_learning_rounds=50, print_level=3)
+
+    assert learned_dfa == dfa
+    return learned_dfa
+
 
 def tomita_example(tomita_number=3):
     """
@@ -157,7 +180,7 @@ def bluetooth_Lsharp():
     # Extension rule options: {"Nothing", "SepSeq", "ADS"}
     # Separation rule options: {"SepSeq", "ADS"}
     learned_mealy = run_Lsharp(input_alphabet, sul_mealy, eq_oracle, automaton_type='mealy', extension_rule=None,
-                               separation_rule="SepSeq", max_learning_rounds=50, print_level=1)
+                               separation_rule="SepSeq", max_learning_rounds=50, print_level=3)
 
 
 def bluetooth_adaptive_Lsharp():
@@ -1300,4 +1323,4 @@ def ioa_compat_domain_knowledge(a: GsmNode, b: GsmNode):
     for name, score in scores.items():
         learned_model = run_GSM(traces, output_behavior="moore", transition_behavior="stochastic", score_calc=score,
                             compatibility_on_pta=True, compatibility_on_futures=True)
-        learned_model.visualize(name)
+        learned_model.visualize(name)

aalpy/base/SUL.py

@@ -59,7 +59,6 @@ def adaptive_query(self, word, ads):
 
             list of outputs, where the i-th output corresponds to the output of the system after the i-th input
         """
-
         self.pre()
 
         outputs_received = []
@@ -75,12 +74,14 @@ def adaptive_query(self, word, ads):
             next_input = ads.next_input(last_output)
             if next_input is None:
                 break
-
-            word.append(next_input)
-            output = self.step(next_input) 
-            outputs_received.append(output)
-            last_output = output
-            self.num_steps += 1
+            if next_input is tuple(): # Relevant for DFA/Moore
+                last_output = self.step(None)
+            else:
+                word.append(next_input)
+                output = self.step(next_input) 
+                outputs_received.append(output)
+                last_output = output
+                self.num_steps += 1
 
         self.num_queries += 1
         self.post()

aalpy/learning_algs/adaptive/AdaptiveLSharp.py

@@ -6,7 +6,7 @@
 from ...base.SUL import CacheSUL
 
 
-def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: Oracle, automaton_type='mealy',
+def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: Oracle, automaton_type,
                         extension_rule=None, separation_rule="SepSeq",
                         rebuilding=True, state_matching="Approximate",
                         samples=None, max_learning_rounds=None,
@@ -27,7 +27,7 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O
 
         eq_oracle: equivalence oracle
 
-        automaton_type: currently only 'mealy' is accepted
+        automaton_type: type of automaton to be learned. Either 'dfa', 'mealy' or 'moore'
 
         extension_rule: strategy used during the extension rule. Options: "Nothing" (default), "SepSeq" and "ADS".
 
@@ -61,7 +61,6 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O
         automaton of type automaton_type (dict containing all information about learning if 'return_data' is True)
 
     """
-    assert automaton_type == "mealy"
     assert extension_rule in {None, "SepSeq", "ADS"}
     assert separation_rule in {"SepSeq", "ADS"}
 
@@ -80,7 +79,7 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O
             for input_seq, output_seq in samples:
                 sul.cache.add_to_cache(input_seq, output_seq)
 
-    ob_tree = AdaptiveObservationTree(alphabet, sul, references,
+    ob_tree = AdaptiveObservationTree(alphabet, sul, references, automaton_type,
                                       extension_rule, separation_rule,
                                       rebuilding, state_matching)
     start_time = time.time()
@@ -100,7 +99,7 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O
             print(f'Hypothesis {learning_rounds}: {hypothesis.size} states.')
         if print_level == 3:
             print(hypothesis)
-            if state_matching != "None":
+            if ob_tree.state_matching:
                 ob_tree.state_matcher.print_match_table(ob_tree)
 
         # Pose Equivalence Query

aalpy/learning_algs/adaptive/AdaptiveObservationTree.py

@@ -3,17 +3,19 @@
 from aalpy.learning_algs.deterministic.Apartness import Apartness
 from aalpy.learning_algs.deterministic.ObservationTree import ObservationTree
 from aalpy.oracles.WpMethodEqOracle import state_characterization_set
+from aalpy.base import Automaton, SUL
+from aalpy.automata import Dfa, DfaState, MealyState, MealyMachine, MooreMachine, MooreState
 
 
 class AdaptiveObservationTree(ObservationTree):
-    def __init__(self, alphabet, sul, references, extension_rule, separation_rule, rebuilding=True, state_matching="Approximate"):
+    def __init__(self, alphabet, sul, references, automaton_type, extension_rule, separation_rule, rebuilding=True, state_matching="Approximate"):
         """
         Initialize the tree with a root node and the alphabet
         A temporary new basis is needed for the prioritized promotion rule
         The rebuild states counter counts the number of states found with rebuilding excluding the root
         The matching states counter counts the number of states found with match refinement and match separation (NOT prioritized separation)
         """
-        super().__init__(alphabet, sul, extension_rule, separation_rule)
+        super().__init__(alphabet, sul, automaton_type, extension_rule, separation_rule)
         self.references = references
         self.rebuild_states = 0
         self.matching_states = 0
@@ -28,6 +30,9 @@ def __init__(self, alphabet, sul, references, extension_rule, separation_rule, r
         self.prefixes_map = {}
         self.characterization_map = {}
         self.combined_model = self.get_combined_model()
+        if not self.combined_model:
+            self.state_matching = None
+            return
 
         # We keep track of a new basis to ensure maximal overlap between prefixes in the references and the new model
         self.new_basis = [self.root]
@@ -47,14 +52,22 @@ def __init__(self, alphabet, sul, references, extension_rule, separation_rule, r
 
     def build_hypothesis(self):
         """
-        Builds the hypothesis which will be sent to the SUL
+        Builds the hypothesis which will be sent to the SUL and checks consistency
         This is either done with or without matching rules
         """
-        if self.state_matching:
-            self.make_observation_tree_adequate_matching()
-        else:
-            super().make_observation_tree_adequate()
-        return self.construct_hypothesis()
+        while True:
+            if self.state_matching:
+                self.make_observation_tree_adequate_matching()
+            else:
+                super().make_observation_tree_adequate()
+            hypothesis = self.construct_hypothesis()
+            counter_example = Apartness.compute_witness_in_tree_and_hypothesis_states(self, self.root, hypothesis.initial_state)
+
+            if not counter_example:
+                return hypothesis
+
+            cex_outputs = self.get_observation(counter_example)
+            self.process_counter_example(hypothesis, counter_example, cex_outputs)
 
     def make_observation_tree_adequate_matching(self):
         """
@@ -111,7 +124,7 @@ def identify_frontier_with_matching(self, frontier_state):
         if not match:
             return
 
-        if match[0].output_fun[inp] != 'epsilon':
+        if inp in match[0].transitions:
             frontier_match = match[0].transitions[inp]
             identifiers = self.characterization_map[frontier_match]
             self.identify_frontier_with_identifiers(frontier_state, identifiers)
@@ -156,6 +169,31 @@ def match_refinement(self):
                 self.refine_matches_basis(basis_state, matches)
                 self.update_frontier_and_basis()
 
+    def find_distinguishing_seq_partial(self, model, state1, state2, alphabet):
+        """
+        A BFS to determine an input sequence that distinguishes two states in the automaton
+        Can handle partial models
+        """
+        visited = set()
+        to_explore = [(state1, state2, [])]
+        while to_explore:
+            (curr_s1, curr_s2, prefix) = to_explore.pop(0)
+            visited.add((curr_s1, curr_s2))
+            for i in alphabet:
+                if i in curr_s1.transitions and i in curr_s2.transitions:
+                    o1 = model.output_step(curr_s1, i)
+                    o2 = model.output_step(curr_s2, i)
+                    new_prefix = prefix + [i]
+                    if o1 != o2:
+                        return new_prefix
+                    else:
+                        next_s1 = curr_s1.transitions[i]
+                        next_s2 = curr_s2.transitions[i]
+                        if (next_s1, next_s2) not in visited:
+                            to_explore.append((next_s1, next_s2, new_prefix))
+
+        return None
+
     def refine_matches_basis(self, basis_state, matches):
         """ 
         Loops over the matched reference states and separates them using a separating sequence
@@ -172,7 +210,7 @@ def refine_matches_basis(self, basis_state, matches):
                 if ref_state_two not in current_matches:
                     continue
 
-                witness = self.combined_model.find_distinguishing_seq(
+                witness = self.find_distinguishing_seq_partial(self.combined_model,
                     ref_state_one, ref_state_two, self.alphabet)
                 if witness is None:
                     continue
@@ -217,7 +255,7 @@ def match_separation_frontier(self, matched_states, frontier_state, basis_candid
         parent_basis = frontier_state.parent
         inp = frontier_state.input_to_parent
         for match in self.state_matcher.best_match[parent_basis]:
-            if match.transitions[inp] in matched_states:
+            if (inp in match.transitions and match.transitions[inp] in matched_states) or (inp not in match.transitions):
                 continue
 
             frontier_match = match.transitions[inp]
@@ -367,11 +405,11 @@ def find_basis_frontier_pair(self, frontier_state, frontier_state_access):
                     reference.initial_state, basis_state_access)
                 state_two = reference.current_state
 
-                sep_seq = tuple(reference.find_distinguishing_seq(
-                    state_one, state_two, reference.get_input_alphabet()))
-                if sep_seq and (self.get_successor(frontier_state_access + sep_seq) is None or
-                                self.get_successor(basis_state_access + sep_seq) is None):
-                    return basis_state_access, frontier_state_access, sep_seq
+                sep_seq = self.find_distinguishing_seq_partial(reference,
+                    state_one, state_two, self.alphabet)
+                if sep_seq and (self.get_successor(frontier_state_access + tuple(sep_seq)) is None or
+                                self.get_successor(basis_state_access + tuple(sep_seq)) is None):
+                    return basis_state_access, frontier_state_access, tuple(sep_seq)
         return None
 
     def insert_observation_rebuilding(self, inputs, outputs):
@@ -402,22 +440,26 @@ def apart_from_all(self, frontier_state):
         return True
 
     # Functions related to finding the combined model
+    
     def add_ref_transitions_to_states(self, reference, reference_id):
         """ 
         Makes a copy of the states of a reference with a unique state id and only transitions with the new input alphabet
         """
-        states = [MealyState(f"s({reference_id},{ref_state})")
+        automaton_state = {'dfa': DfaState, 'mealy': MealyState, 'moore': MooreState}
+        states = [automaton_state[self.automaton_type](f"s({reference_id},{ref_state})")
                   for ref_state in range(0, len(reference.states))]
         for state_id in range(0, len(reference.states)):
-            states[state_id].output_fun = reference.states[state_id].output_fun
+            if self.automaton_type == 'mealy':
+                states[state_id].output_fun = reference.states[state_id].output_fun
+            elif self.automaton_type == 'dfa':
+                states[state_id].is_accepting = reference.states[state_id].is_accepting
+            else:
+                states[state_id].output = reference.states[state_id].output
             for inp in self.alphabet:
                 if inp in reference.get_input_alphabet():
                     old_index = reference.states.index(
                         reference.states[state_id].transitions[inp])
                     states[state_id].transitions[inp] = states[old_index]
-                else:
-                    states[state_id].transitions[inp] = states[state_id]
-                    states[state_id].output_fun[inp] = 'epsilon'
         return states
 
     def compute_prefix_map(self, reference, reference_id):
@@ -433,19 +475,18 @@ def compute_characterization_map(self, reference, states):
         """ 
         Computes the separating sequences of a reference model and stores them in a characterization map
         """
-
         for state, ref_state in zip(states, reference.states):
             all_sepseqs = state_characterization_set(reference, reference.get_input_alphabet(), ref_state)
             unique_sepseqs = list(dict.fromkeys(all_sepseqs))
             self.characterization_map[state] = unique_sepseqs
 
-
     def get_combined_model(self):
         """ 
         Builds a combined model from the reference models
         Compute the prefix and characterization maps used during construction of the combined model
-        The resulting mealy machine is made input complete by adding self-loops with output 'epsilon' for all undefined inputs
+        The resulting mealy machine may be partial
         """
+        automaton_class = {'dfa': Dfa, 'mealy': MealyMachine, 'moore': MooreMachine}
         all_states = []
         for reference_id in range(0, len(self.references)):
             reference = self.references[reference_id]
@@ -460,9 +501,11 @@ def get_combined_model(self):
             states = self.add_ref_transitions_to_states(reference, reference_id)
             all_states += states
 
-            self.compute_prefix_map(MealyMachine(states[0], states), reference_id)
+            self.compute_prefix_map(automaton_class[self.automaton_type](states[0], states), reference_id)
             self.compute_characterization_map(reference, states)
 
-        mm = MealyMachine(all_states[0], all_states)
-        mm.make_input_complete()
-        return mm
+        if all_states == []:
+            print(f"Warning: the references did not lead to any usable states, this could be due to empty models or no common inputs.")
+            return None
+        else:
+            return automaton_class[self.automaton_type](all_states[0], all_states)