Skip to content

Commit

Permalink
Merge pull request #74 from lkruger27/aalpy_lsharp_docstring
Browse files Browse the repository at this point in the history
Add AL# docstring and None option for state merging
  • Loading branch information
emuskardin authored Feb 3, 2025
2 parents 19212d0 + 07fa7cb commit 53309e8
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 17 deletions.
4 changes: 2 additions & 2 deletions Examples.py
Original file line number Diff line number Diff line change
Expand Up @@ -177,10 +177,10 @@ 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)
rebuilding=True, state_matching="Approximate", print_level=2)



Expand Down
29 changes: 20 additions & 9 deletions aalpy/learning_algs/adaptive/AdaptiveLSharp.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,15 @@


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.
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:
Expand All @@ -31,9 +33,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#. 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
Expand All @@ -57,9 +65,12 @@ 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 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)
Expand Down
21 changes: 16 additions & 5 deletions aalpy/learning_algs/adaptive/AdaptiveObservationTree.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -41,15 +41,19 @@ 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):
"""
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):
Expand Down Expand Up @@ -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):
Expand All @@ -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):
Expand Down
3 changes: 2 additions & 1 deletion aalpy/learning_algs/deterministic/LSharp.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit 53309e8

Please sign in to comment.