Merge remote-tracking branch 'origin/master' into master

DES-Lab · Dec 13, 2023 · 5256263 · 5256263
2 parents f53cdfd + 9d07f5d
commit 5256263
Show file tree

Hide file tree

Showing 31 changed files with 165 additions and 322 deletions.
diff --git a/Benchmarking/Benchmark_ErrorStop.py b/Benchmarking/Benchmark_ErrorStop.py
@@ -3,7 +3,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWordEqOracle import UnseenOutputRandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values
@@ -83,7 +83,7 @@
                     original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
                     input_alphabet = original_mdp.get_input_alphabet()
 
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = UnseenOutputRandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)
@@ -96,7 +96,7 @@
                     del mdp_sul
                     del eq_oracle
                     random.seed(seeds[seed])
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = UnseenOutputRandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/CompleteStochasticBenchmarking.py b/Benchmarking/CompleteStochasticBenchmarking.py
@@ -3,7 +3,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values
@@ -59,7 +59,7 @@
                     original_mdp = model_dict[exp_name]
                     input_alphabet = original_mdp.get_input_alphabet()
 
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=16, reset_after_cex=True)
@@ -72,7 +72,7 @@
                     del mdp_sul
                     del eq_oracle
                     random.seed(seeds[seed])
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/StochasticAlgComparison.py b/Benchmarking/StochasticAlgComparison.py
@@ -4,7 +4,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar, run_Alergia
 from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values
@@ -32,7 +32,7 @@
     original_mdp = model_dict[exp_name]
     input_alphabet = original_mdp.get_input_alphabet()
 
-    mdp_sul = MdpSUL(original_mdp)
+    mdp_sul = AutomatonSUL(original_mdp)
 
     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=500, min_walk_len=5,
                                    max_walk_len=16, reset_after_cex=True)
@@ -46,7 +46,7 @@
     del mdp_sul
     del eq_oracle
 
-    mdp_sul = MdpSUL(original_mdp)
+    mdp_sul = AutomatonSUL(original_mdp)
 
     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                    max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/StochasticBenchmarkingWPrism.py b/Benchmarking/StochasticBenchmarkingWPrism.py
@@ -2,7 +2,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWalkEqOracle import RandomWalkEqOracle
 from aalpy.utils import load_automaton_from_file, get_correct_prop_values, get_properties_file
@@ -65,7 +65,7 @@
         original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
         input_alphabet = original_mdp.get_input_alphabet()
 
-        mdp_sul = MdpSUL(original_mdp)
+        mdp_sul = AutomatonSUL(original_mdp)
 
         eq_oracle = RandomWalkEqOracle(input_alphabet, mdp_sul, num_steps=n_resample * (1 / 0.25),
                                        reset_after_cex=True, reset_prob=0.25)

diff --git a/Benchmarking/StopWithErorrRate.py b/Benchmarking/StopWithErorrRate.py
@@ -6,7 +6,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar, run_Alergia
 from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values, model_check_properties
@@ -43,7 +43,7 @@
 #                 original_mdp = model_dict[exp_name]
 #                 input_alphabet = original_mdp.get_input_alphabet()
 #
-#                 mdp_sul = MdpSUL(original_mdp)
+#                 mdp_sul = AutomatonSUL(original_mdp)
 #
 #                 eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=500, min_walk_len=5,
 #                                                max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/benchmark.py b/Benchmarking/benchmark.py
@@ -1,7 +1,7 @@
 import os
 from statistics import mean
 
-from aalpy.SULs import DfaSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_Lstar
 from aalpy.oracles import StatePrefixEqOracle
 from aalpy.utils import load_automaton_from_file
@@ -13,7 +13,7 @@
 run_times = []
 
 # change on which folder to perform experiments
-exp, sul = dfa_2000_states_10_inputs, DfaSUL
+exp = dfa_2000_states_10_inputs
 
 benchmarks = os.listdir(exp)
 benchmarks = benchmarks[:10]
@@ -28,7 +28,7 @@
     automaton = load_automaton_from_file(f'{exp}/{b}', automaton_type='dfa')
     input_al = automaton.get_input_alphabet()
 
-    sul_dfa = sul(automaton)
+    sul_dfa = AutomatonSUL(automaton)
 
     state_origin_eq_oracle = StatePrefixEqOracle(input_al, sul_dfa, walks_per_state=5, walk_len=25)
 

diff --git a/Benchmarking/benchmark_alphabet_increase.py b/Benchmarking/benchmark_alphabet_increase.py
@@ -1,7 +1,7 @@
 from statistics import mean
 import csv
 
-from aalpy.SULs import DfaSUL, MealySUL, MooreSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_Lstar
 from aalpy.oracles import RandomWalkEqOracle
 from aalpy.utils import generate_random_dfa, generate_random_mealy_machine, generate_random_moore_machine
@@ -28,7 +28,7 @@
         alphabet = list(range(alph_size))
 
         dfa = generate_random_dfa(num_states, alphabet=alphabet, num_accepting_states=num_states // 2)
-        sul = DfaSUL(dfa)
+        sul = AutomatonSUL(dfa)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, sul, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, sul, num_steps=10000, reset_prob=0.09)
@@ -42,7 +42,7 @@
         del eq_oracle
 
         mealy = generate_random_mealy_machine(num_states, input_alphabet=alphabet, output_alphabet=alphabet)
-        sul_mealy = MealySUL(mealy)
+        sul_mealy = AutomatonSUL(mealy)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, sul_mealy, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, sul_mealy, num_steps=10000, reset_prob=0.09)
@@ -58,7 +58,7 @@
         del eq_oracle
 
         moore = generate_random_moore_machine(num_states, input_alphabet=alphabet, output_alphabet=alphabet)
-        moore_sul = MooreSUL(moore)
+        moore_sul = AutomatonSUL(moore)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, moore_sul, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, moore_sul, num_steps=10000, reset_prob=0.09)

diff --git a/Benchmarking/benchmark_size_increase.py b/Benchmarking/benchmark_size_increase.py
@@ -1,7 +1,7 @@
 from statistics import mean
 import csv
 
-from aalpy.SULs import DfaSUL, MealySUL, MooreSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_Lstar
 from aalpy.oracles import RandomWalkEqOracle
 from aalpy.utils import generate_random_dfa, generate_random_mealy_machine, generate_random_moore_machine
@@ -35,7 +35,7 @@
 
     for _ in range(repeat):
         dfa = generate_random_dfa(num_states, alphabet=alphabet, num_accepting_states=num_states // 2)
-        sul = DfaSUL(dfa)
+        sul = AutomatonSUL(dfa)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, sul, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, sul, num_steps=9000, reset_prob=0.09)
@@ -51,7 +51,7 @@
         del dfa
 
         mealy = generate_random_mealy_machine(num_states, input_alphabet=alphabet, output_alphabet=alphabet)
-        sul_mealy = MealySUL(mealy)
+        sul_mealy = AutomatonSUL(mealy)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, sul_mealy, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, sul_mealy, num_steps=9000, reset_prob=0.09)
@@ -68,7 +68,7 @@
         del eq_oracle
 
         moore = generate_random_moore_machine(num_states, input_alphabet=alphabet, output_alphabet=alphabet)
-        moore_sul = MooreSUL(moore)
+        moore_sul = AutomatonSUL(moore)
 
         # eq_oracle = StatePrefixEqOracle(alphabet, moore_sul, walks_per_state=5, walk_len=40)
         eq_oracle = RandomWalkEqOracle(alphabet, moore_sul, num_steps=9000, reset_prob=0.09)

diff --git a/Benchmarking/compare_lstar_and_kv.py b/Benchmarking/compare_lstar_and_kv.py
@@ -1,4 +1,4 @@
-from aalpy.SULs import DfaSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_Lstar, run_KV
 from aalpy.oracles import RandomWordEqOracle
 from aalpy.utils import generate_random_deterministic_automata
@@ -23,14 +23,14 @@
                     print(f'Type: {model_type}, size: {size}, # inputs: {i}, # accepting: {size//8}')
 
                 # Lstar
-                sul = DfaSUL(random_model)
+                sul = AutomatonSUL(random_model)
                 eq_oracle = RandomWordEqOracle(input_al, sul, num_walks=5000, min_walk_len=10, max_walk_len=40)
                 l_star_model, l_star_info = run_Lstar(input_al, sul, eq_oracle, model_type, print_level=0, return_data=True)
 
                 l_star_steps, l_star_queries = l_star_info['steps_learning'], l_star_info['queries_learning']
 
                 # KV
-                sul = DfaSUL(random_model)
+                sul = AutomatonSUL(random_model)
                 eq_oracle = RandomWordEqOracle(input_al, sul, num_walks=5000, min_walk_len=10, max_walk_len=40)
                 kv_model, kv_info = run_KV(input_al, sul, eq_oracle, model_type, print_level=0, return_data=True)
 

diff --git a/Benchmarking/evaluate_l_star_configurations.py b/Benchmarking/evaluate_l_star_configurations.py
@@ -3,7 +3,7 @@
 from random import seed
 from statistics import mean
 
-from aalpy.SULs import DfaSUL, MealySUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_Lstar
 from aalpy.oracles import StatePrefixEqOracle, RandomWMethodEqOracle, RandomWalkEqOracle, RandomWordEqOracle
 from aalpy.utils import generate_random_deterministic_automata
@@ -40,7 +40,7 @@
                         tc += 1
                         print(round(tc / num_exp * 100, 2))
                         # seed(tc)
-                        sul = MealySUL(test_model)
+                        sul = AutomatonSUL(test_model)
                         eq_oracle = RandomWordEqOracle(input_al, sul, num_walks=5000, min_walk_len=10, max_walk_len=40)
                         model, info = run_Lstar(input_al, sul, eq_oracle, 'dfa',
                                                 closing_strategy=closing_strategy,

diff --git a/Benchmarking/passive_mdp_vs_smm.py b/Benchmarking/passive_mdp_vs_smm.py
@@ -1,7 +1,7 @@
 import random
 
 import aalpy.paths
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.automata.StochasticMealyMachine import smm_to_mdp_conversion
 from aalpy.learning_algs import run_Alergia
 from aalpy.utils import load_automaton_from_file, get_correct_prop_values, get_properties_file
@@ -45,7 +45,7 @@ def deleteSampleFile(path="alergiaSamples.txt"):
     original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
     input_alphabet = original_mdp.get_input_alphabet()
 
-    mdp_sul = MdpSUL(original_mdp)
+    mdp_sul = AutomatonSUL(original_mdp)
 
     for _ in range(1):
 

diff --git a/Benchmarking/stochastic_benchmarking/Benchmark_ErrorStop.py b/Benchmarking/stochastic_benchmarking/Benchmark_ErrorStop.py
@@ -3,7 +3,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values
@@ -83,7 +83,7 @@
                     original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
                     input_alphabet = original_mdp.get_input_alphabet()
 
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)
@@ -96,7 +96,7 @@
                     del mdp_sul
                     del eq_oracle
                     random.seed(seeds[seed])
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/stochastic_benchmarking/CompleteStochasticBenchmarking.py b/Benchmarking/stochastic_benchmarking/CompleteStochasticBenchmarking.py
@@ -3,7 +3,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle
 from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values
@@ -60,7 +60,7 @@
                     original_mdp = model_dict[exp_name]
                     input_alphabet = original_mdp.get_input_alphabet()
 
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=16, reset_after_cex=True)
@@ -73,7 +73,7 @@
                     del mdp_sul
                     del eq_oracle
                     random.seed(seeds[seed])
-                    mdp_sul = MdpSUL(original_mdp)
+                    mdp_sul = AutomatonSUL(original_mdp)
 
                     eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5,
                                                                max_walk_len=15, reset_after_cex=True)

diff --git a/Benchmarking/stochastic_benchmarking/StochasticBenchmarkingWPrism.py b/Benchmarking/stochastic_benchmarking/StochasticBenchmarkingWPrism.py
@@ -2,7 +2,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles.RandomWalkEqOracle import RandomWalkEqOracle
 from aalpy.utils import load_automaton_from_file, get_correct_prop_values, get_properties_file
@@ -65,7 +65,7 @@
         original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
         input_alphabet = original_mdp.get_input_alphabet()
 
-        mdp_sul = MdpSUL(original_mdp)
+        mdp_sul = AutomatonSUL(original_mdp)
 
         eq_oracle = RandomWalkEqOracle(input_alphabet, mdp_sul, num_steps=n_resample * (1 / 0.25),
                                                    reset_after_cex=True, reset_prob=0.25)

diff --git a/Benchmarking/stochastic_benchmarking/passive_mdp_vs_smm.py b/Benchmarking/stochastic_benchmarking/passive_mdp_vs_smm.py
@@ -1,7 +1,7 @@
 import random
 import os
 import aalpy.paths
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.automata.StochasticMealyMachine import smm_to_mdp_conversion
 from aalpy.learning_algs import run_Alergia, run_JAlergia
 from aalpy.utils import load_automaton_from_file, get_correct_prop_values, get_properties_file, visualize_automaton
@@ -45,7 +45,7 @@ def deleteSampleFile(path="alergiaSamples.txt"):
     original_mdp = load_automaton_from_file(path_to_dir + file, automaton_type='mdp')
     input_alphabet = original_mdp.get_input_alphabet()
 
-    mdp_sul = MdpSUL(original_mdp)
+    mdp_sul = AutomatonSUL(original_mdp)
 
     for _ in range(1):
 

diff --git a/Benchmarking/stochastic_benchmarking/stochastic_benchmark_random_automata.py b/Benchmarking/stochastic_benchmarking/stochastic_benchmark_random_automata.py
@@ -1,6 +1,6 @@
 from itertools import product
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 from aalpy.oracles import RandomWordEqOracle
 from aalpy.utils import generate_random_mdp, generate_random_smm
@@ -14,7 +14,7 @@
 
 def learn(mdp, type):
     input_al = mdp.get_input_alphabet()
-    sul = MdpSUL(mdp)
+    sul = AutomatonSUL(mdp)
     eq_oracle = RandomWordEqOracle(input_al, sul, num_walks=1000, min_walk_len=4, max_walk_len=20)
     return run_stochastic_Lstar(input_al, sul, eq_oracle, automaton_type=type, cex_processing=None, print_level=0,
                                 return_data=True)

diff --git a/Benchmarking/stochastic_benchmarking/strategy_comp.py b/Benchmarking/stochastic_benchmarking/strategy_comp.py
@@ -4,7 +4,7 @@
 
 import aalpy.paths
 
-from aalpy.SULs import MdpSUL
+from aalpy.SULs import AutomatonSUL
 from aalpy.learning_algs import run_stochastic_Lstar
 
 from aalpy.oracles import RandomWordEqOracle
@@ -22,7 +22,7 @@
 
 def learn(strategy):
     input_al = mdp.get_input_alphabet()
-    sul = MdpSUL(mdp)
+    sul = AutomatonSUL(mdp)
     eq_oracle = RandomWordEqOracle(input_al, sul, num_walks=1000, min_walk_len=4, max_walk_len=20)
     model, data = run_stochastic_Lstar(input_al, sul, eq_oracle, automaton_type='smm', strategy=strategy,
                                        cex_processing=None, print_level=0, return_data=True)