From 8cedca387a603a3b661421a0fa18e7ec6cd6b1d3 Mon Sep 17 00:00:00 2001 From: lkruger27 Date: Mon, 3 Feb 2025 10:24:53 +0100 Subject: [PATCH 1/4] Updated docstrings and None feature for state matching. --- Examples.py | 5 ++++- .../learning_algs/adaptive/AdaptiveLSharp.py | 20 +++++++++++------- .../adaptive/AdaptiveObservationTree.py | 21 ++++++++++++++----- 3 files changed, 33 insertions(+), 13 deletions(-) diff --git a/Examples.py b/Examples.py index 6d75a9807b..57bb974796 100644 --- a/Examples.py +++ b/Examples.py @@ -177,7 +177,7 @@ def bluetooth_adaptive_Lsharp(): eq_oracle = WpMethodEqOracle(input_alphabet, sul_mealy, len(target.states)) # Rebuilding options: {True, False} - # State Matching options: {"None", "Total", "Approximate"} + # State Matching options: {None, "Total", "Approximate"} learned_mealy = run_adaptive_Lsharp(input_alphabet, sul_mealy, [reference1, reference2, reference3], eq_oracle, automaton_type='mealy', extension_rule='SepSeq', separation_rule="ADS", rebuilding=True, state_matching="Approximate",print_level=2) @@ -1160,3 +1160,6 @@ def passive_vpa_learning_on_all_benchmark_models(): assert False, 'Papni Learned Model not consistent with data.' print('PAPNI model conforms to data.') + +# bluetooth_Lsharp() +bluetooth_adaptive_Lsharp() diff --git a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py index 339531aa3e..5111b80e3a 100644 --- a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py +++ b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py @@ -7,10 +7,10 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: Oracle, automaton_type='mealy', - extension_rule=None, separation_rule="SepSeq", - rebuilding=True, state_matching="Approximate", - samples=None, max_learning_rounds=None, - cache_and_non_det_check=True, return_data=False, print_level=2): + extension_rule=None, separation_rule="SepSeq", + rebuilding=True, state_matching="Approximate", + samples=None, max_learning_rounds=None, + cache_and_non_det_check=True, return_data=False, print_level=2): """ Executes the Adaptive L# algorithm (prefix-tree based automaton learning) which can use reference models to kickstart the learning process. @@ -31,9 +31,15 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O separation_rule: strategy used during the extension rule. Options: "SepSeq" (default) and "ADS". - rebuilding: default value: True + rebuilding: procedure that poses output queries to rebuild the observation tree based on prefixes and separating sequences from the reference(s). + Only executes at the start of adaptive L#. For more information see: https://arxiv.org/abs/2406.19714. default value: True. - state_matching: either "Approximate" or "Total" + state_matching: if not None, the learner maintains a matching relation between basis states (in the observation tree) and reference model states. + This matching relation is used in three rules added on top of L# to either identify a frontier state faster or isolate it when the matching indicates + that the frontier state corresponds to a reference model state not yet present in the basis. default value: "Approximate". + - Two states match according to "total matching" if all output over the defined and shared alphabet are exactly the same. + - Two states match according to "approximate matching" if they have the highest ratio of equivalent outputs to defined outputs over the shared alphabet. + - None can be used if only the rebuilding procedure is needed. samples: input output traces provided to the learning algorithm. They are added to cache and could reduce total interaction with the system. Syntax: list of [(input_sequence, output_sequence)] or None @@ -57,7 +63,7 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O assert extension_rule in {None, "SepSeq", "ADS"} assert separation_rule in {"SepSeq", "ADS"} - assert state_matching in {"Total", "Approximate"} + assert state_matching in {None, "Total", "Approximate"} assert references is not None, 'List of reference models is empty. Use L*, KV, L#, or provide models.' if cache_and_non_det_check or samples is not None: diff --git a/aalpy/learning_algs/adaptive/AdaptiveObservationTree.py b/aalpy/learning_algs/adaptive/AdaptiveObservationTree.py index 494298e49b..90d806a4c7 100644 --- a/aalpy/learning_algs/adaptive/AdaptiveObservationTree.py +++ b/aalpy/learning_algs/adaptive/AdaptiveObservationTree.py @@ -19,7 +19,7 @@ def __init__(self, alphabet, sul, references, extension_rule, separation_rule, r self.matching_states = 0 if not references: - self.state_matching = "None" + self.state_matching = None print(f"Warning: no references given, normal L# is executed.") return @@ -41,7 +41,8 @@ def __init__(self, alphabet, sul, references, extension_rule, separation_rule, r elif self.state_matching == "Approximate": self.state_matcher = ApproximateStateMatching(self.alphabet, self.combined_model) - self.state_matcher.initialize_matching(self) + if self.state_matching: + self.state_matcher.initialize_matching(self) def build_hypothesis(self): @@ -49,7 +50,10 @@ def build_hypothesis(self): Builds the hypothesis which will be sent to the SUL This is either done with or without matching rules """ - self.make_observation_tree_adequate_matching() + if self.state_matching: + self.make_observation_tree_adequate_matching() + else: + super().make_observation_tree_adequate() return self.construct_hypothesis() def make_observation_tree_adequate_matching(self): @@ -244,7 +248,8 @@ def promote_frontier_state(self): new_basis = iso_frontier_state self.basis.append(new_basis) self.frontier_to_basis_dict.pop(new_basis) - self.state_matcher.update_matching_basis(new_basis, self) + if self.state_matching: + self.state_matcher.update_matching_basis(new_basis, self) for frontier_state, new_basis_list in self.frontier_to_basis_dict.items(): if not Apartness.states_are_apart(new_basis, frontier_state, self): @@ -259,7 +264,13 @@ def insert_observation(self, inputs, outputs): if len(inputs) != len(outputs): raise ValueError("Inputs and outputs must have the same length.") - self.extend_node_and_update_matching(inputs, outputs) + if self.state_matching: + self.extend_node_and_update_matching(inputs, outputs) + else: + current_node = self.root + for input_val, output_val in zip(inputs, outputs): + current_node = current_node.extend_and_get( + input_val, output_val) def extend_node_and_update_matching(self, inputs, outputs): From 909511908543ed38bf422fddaf3434872b704a4a Mon Sep 17 00:00:00 2001 From: lkruger27 Date: Mon, 3 Feb 2025 10:32:05 +0100 Subject: [PATCH 2/4] Added exception when adaptive L# is called with rebuilding False and state matching None --- aalpy/learning_algs/adaptive/AdaptiveLSharp.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py index 5111b80e3a..5ee2735c6f 100644 --- a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py +++ b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py @@ -66,6 +66,9 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O assert state_matching in {None, "Total", "Approximate"} assert references is not None, 'List of reference models is empty. Use L*, KV, L#, or provide models.' + if not rebuilding and not state_matching: + raise Exception(f"Use L# instead of Adaptive L# if rebuilding is set to False and state matching to None.") + if cache_and_non_det_check or samples is not None: # Wrap the sul in the CacheSUL, so that all steps/queries are cached sul = CacheSUL(sul) From 686972a8bb618e2fc3af2c066b1041c78b43a687 Mon Sep 17 00:00:00 2001 From: lkruger27 Date: Mon, 3 Feb 2025 10:47:32 +0100 Subject: [PATCH 3/4] added introductory text to the L# and AL# algorithms. --- aalpy/learning_algs/adaptive/AdaptiveLSharp.py | 8 +++++--- aalpy/learning_algs/deterministic/LSharp.py | 3 ++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py index 5ee2735c6f..a9dd8ae358 100644 --- a/aalpy/learning_algs/adaptive/AdaptiveLSharp.py +++ b/aalpy/learning_algs/adaptive/AdaptiveLSharp.py @@ -12,8 +12,10 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O samples=None, max_learning_rounds=None, cache_and_non_det_check=True, return_data=False, print_level=2): """ - Executes the Adaptive L# algorithm (prefix-tree based automaton learning) - which can use reference models to kickstart the learning process. + Based on ''State Matching and Multiple References in Adaptive Active Automata Learning'' from Kruger, Junges and Rot. + The algorithm learns a Mealy machine using a set of references. These references are used by two procedures + 1) Rebuilding which kickstarts the learning process using the references and 2) State Matching which matches the + basis states and references states to find new basis states faster. Args: @@ -32,7 +34,7 @@ def run_adaptive_Lsharp(alphabet: list, sul: SUL, references: list, eq_oracle: O separation_rule: strategy used during the extension rule. Options: "SepSeq" (default) and "ADS". rebuilding: procedure that poses output queries to rebuild the observation tree based on prefixes and separating sequences from the reference(s). - Only executes at the start of adaptive L#. For more information see: https://arxiv.org/abs/2406.19714. default value: True. + Only executes at the start of adaptive L#. default value: True. state_matching: if not None, the learner maintains a matching relation between basis states (in the observation tree) and reference model states. This matching relation is used in three rules added on top of L# to either identify a frontier state faster or isolate it when the matching indicates diff --git a/aalpy/learning_algs/deterministic/LSharp.py b/aalpy/learning_algs/deterministic/LSharp.py index 6d2f5d5c87..cc32d8fcd9 100644 --- a/aalpy/learning_algs/deterministic/LSharp.py +++ b/aalpy/learning_algs/deterministic/LSharp.py @@ -10,7 +10,8 @@ def run_Lsharp(alphabet: list, sul: SUL, eq_oracle: Oracle, automaton_type, extension_rule='SepSeq', separation_rule="ADS", samples=None, max_learning_rounds=None, cache_and_non_det_check=True, return_data=False, print_level=2): """ - Executes the L# algorithm (prefix-tree based automaton learning). + Based on ''A New Approach for Active Automata Learning Based on Apartness'' from Vaandrager, Garhewal, Rot and Wissmann. + The algorithm learns a Mealy machine using apartness and an observation tree. Args: From 07fa7cbd8b00feca47f2385d377d1eda7340a984 Mon Sep 17 00:00:00 2001 From: lkruger27 Date: Mon, 3 Feb 2025 10:51:39 +0100 Subject: [PATCH 4/4] remove function call in Examples --- Examples.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Examples.py b/Examples.py index 57bb974796..82d86ce548 100644 --- a/Examples.py +++ b/Examples.py @@ -180,7 +180,7 @@ def bluetooth_adaptive_Lsharp(): # State Matching options: {None, "Total", "Approximate"} learned_mealy = run_adaptive_Lsharp(input_alphabet, sul_mealy, [reference1, reference2, reference3], eq_oracle, automaton_type='mealy', extension_rule='SepSeq', separation_rule="ADS", - rebuilding=True, state_matching="Approximate",print_level=2) + rebuilding=True, state_matching="Approximate", print_level=2) @@ -1160,6 +1160,3 @@ def passive_vpa_learning_on_all_benchmark_models(): assert False, 'Papni Learned Model not consistent with data.' print('PAPNI model conforms to data.') - -# bluetooth_Lsharp() -bluetooth_adaptive_Lsharp()