Merge remote-tracking branch 'origin/master'

Author: emuskardin

aalpy/learning_algs/general_passive/GeneralizedStateMerging.py

@@ -35,7 +35,7 @@ def log_promote(self, node: GsmNode):
     def log_merge(self, part: Partitioning):
         pass
 
-    def learning_done(self, root: GsmNode, red_states: List[GsmNode]):
+    def learning_done(self, root: GsmNode):
         pass
 
 
@@ -192,7 +192,7 @@ def run(self, data, convert=True, instrumentation: Instrumentation=None, data_fo
             # FUTURE: caching for aggregating compatibility tests
             partition_candidates.clear()
 
-        instrumentation.learning_done(root, red_states)
+        instrumentation.learning_done(root)
 
         root = self.postprocessing(root)
         if convert:

aalpy/learning_algs/general_passive/GsmNode.py

@@ -64,8 +64,6 @@ def detect_data_format(data, check_consistency=False, guess=False):
     # - "traces": [[o, o, ...], ...]
 
     if isinstance(data, GsmNode):
-        if not data.is_tree():
-            raise ValueError("provided automaton is not a tree")
         return "tree"
 
     accepted_types = (Tuple, List)
@@ -432,6 +430,8 @@ def createPTA(data, output_behavior, data_format=None) -> 'GsmNode':
             raise ValueError(f"invalid data format {data_format}. should be in {DataFormatRange}")
 
         if data_format == "tree":
+            if not data.is_tree():
+                raise ValueError("provided automaton is not a tree")
             return data
         root_node = GsmNode((None, unknown_output), None)
         if data_format == "labeled_sequences":

aalpy/learning_algs/general_passive/Instrumentation.py

@@ -1,4 +1,4 @@
-import time
+from time import perf_counter
 from typing import Dict, Optional
 
 from aalpy.learning_algs.general_passive.GeneralizedStateMerging import Instrumentation, Partitioning, \
@@ -29,18 +29,18 @@ def reset(self, gsm: GeneralizedStateMerging):
         self.nr_merged_states = 0
         self.nr_red_states = 0
 
-        self.previous_time = time.time()
+        self.previous_time = perf_counter()
 
     def pta_construction_done(self, root):
-        print(f'PTA Construction Time: {round(time.time() - self.previous_time, 2)}')
+        print(f'PTA Construction Time: {round(perf_counter() - self.previous_time, 2)} s')
         if 1 < self.lvl:
             states = root.get_all_nodes()
             leafs = [state for state in states if len(state.transitions.keys()) == 0]
             depth = [state.get_prefix_length() for state in leafs]
             self.pta_size = len(states)
             print(f'PTA has {len(states)} states leading to {len(leafs)} leafs')
             print(f'min / avg / max depth : {min(depth)} / {sum(depth) / len(depth)} / {max(depth)}')
-        self.previous_time = time.time()
+        self.previous_time = perf_counter()
 
     def print_status(self):
         reset_char = "\33[2K\r"
@@ -60,9 +60,9 @@ def log_merge(self, part: Partitioning):
         self.nr_merged_states += 1
         self.print_status()
 
-    def learning_done(self, root, red_states):
-        print(f'\nLearning Time: {round(time.time() - self.previous_time, 2)}')
-        print(f'Learned {len(red_states)} state automaton via {self.nr_merged_states} merges.')
+    def learning_done(self, root: GsmNode):
+        print(f'\nLearning Time: {round(perf_counter() - self.previous_time, 2)} s')
+        print(f'Learned {self.nr_red_states} state automaton via {self.nr_merged_states} merges.')
         if 2 < self.lvl:
             root.visualize("model", self.gsm.output_behavior)
 

aalpy/oracles/StatePrefixEqOracle.py

@@ -12,7 +12,7 @@ class StatePrefixEqOracle(Oracle):
     rand_walk_len exactly walk_per_state times during learning. Therefore excessive testing of initial states is
     avoided.
     """
-    def __init__(self, alphabet: list, sul: SUL, walks_per_state=10, walk_len=12, depth_first=False):
+    def __init__(self, alphabet: list, sul: SUL, walks_per_state=10, walk_len=12, max_tests=None, depth_first=True):
         """
         Args:
 
@@ -24,18 +24,20 @@ def __init__(self, alphabet: list, sul: SUL, walks_per_state=10, walk_len=12, de
 
             walk_len:length of random walk
 
-            depth_first:first explore newest states
+            max_tests:number of maximum tests. If set to None, this parameter will be ignored.
+
+            depth_first:first explore the newest states
         """
 
         super().__init__(alphabet, sul)
         self.walks_per_state = walks_per_state
         self.steps_per_walk = walk_len
         self.depth_first = depth_first
+        self.max_tests = max_tests
 
         self.freq_dict = dict()
 
     def find_cex(self, hypothesis):
-
         states_to_cover = []
         for state in hypothesis.states:
             if state.prefix is None:
@@ -57,6 +59,9 @@ def find_cex(self, hypothesis):
 
             self.reset_hyp_and_sul(hypothesis)
 
+            if self.max_tests and self.num_queries == self.max_tests:
+                return None
+
             prefix = state.prefix
             for p in prefix:
                 hypothesis.step(p)