Movatterモバイル変換


[0]ホーム

URL:


Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

Sign up
Appearance settings

Commit828579b

Browse files
authored
Merge pull request#97 from DES-Lab/k_way_oracle_bounds
K way oracle bounds
2 parents7945a1c +9e8d601 commit828579b

File tree

6 files changed

+81
-40
lines changed

6 files changed

+81
-40
lines changed

‎aalpy/automata/Dfa.py‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,8 @@ def compute_output_seq(self, state, sequence):
5353

5454
defexecute_sequence(self,origin_state,seq):
5555
ifnotseq:
56-
returnorigin_state.output
56+
self.current_state=origin_state
57+
returnself.current_state.output
5758
returnsuper(Dfa,self).execute_sequence(origin_state,seq)
5859

5960

‎aalpy/automata/MooreMachine.py‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,8 @@ def compute_output_seq(self, state, sequence):
5050

5151
defexecute_sequence(self,origin_state,seq):
5252
ifnotseq:
53-
returnorigin_state.output
53+
self.current_state=origin_state
54+
returnself.current_state.output
5455
returnsuper(MooreMachine,self).execute_sequence(origin_state,seq)
5556

5657
defto_state_setup(self):

‎aalpy/learning_algs/adaptive/AdaptiveObservationTree.py‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -398,11 +398,10 @@ def find_basis_frontier_pair(self, frontier_state, frontier_state_access):
398398
iffrontier_stateandApartness.compute_witness(basis_state,frontier_state,self)isnotNone:
399399
continue
400400

401-
reference.execute_sequence(
402-
reference.initial_state,frontier_state_access)
401+
reference.execute_sequence(reference.initial_state,frontier_state_access)
403402
state_one=reference.current_state
404-
reference.execute_sequence(
405-
reference.initial_state,basis_state_access)
403+
404+
reference.execute_sequence(reference.initial_state,basis_state_access)
406405
state_two=reference.current_state
407406

408407
sep_seq=self.find_distinguishing_seq_partial(reference,

‎aalpy/learning_algs/deterministic/ClassificationTree.py‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -367,7 +367,6 @@ def process_counterexample(self, cex: tuple, hypothesis, cex_processing_fun):
367367
u=cex[:len(cex)-len(v)-1]
368368
assert (*u,a,*v)==cex
369369

370-
hypothesis.reset_to_initial()
371370
hypothesis.execute_sequence(hypothesis.initial_state,u)
372371
u_state=hypothesis.current_state
373372

‎aalpy/oracles/KWayStateCoverageEqOracle.py‎

Lines changed: 29 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -10,20 +10,22 @@ class KWayStateCoverageEqOracle(Oracle):
1010
random walk at the end.
1111
"""
1212

13-
def__init__(self,alphabet:list,sul:SUL,k=2,random_walk_len=20,method='permutations'):
13+
def__init__(self,alphabet:list,sul:SUL,k=2,random_walk_len=20,
14+
method='permutations',
15+
num_test_lower_bound=None,
16+
num_test_upper_bound=None):
1417
"""
1518
1619
Args:
1720
1821
alphabet: input alphabet
19-
2022
sul: system under learning
21-
2223
k: k value used for k-wise combinations/permutations of states
23-
2424
random_walk_len: length of random walk performed at the end of each combination/permutation
25-
2625
method: either 'combinations' or 'permutations'
26+
num_test_lower_bound= either None or number a minimum number of test-cases to be performed in each testing round
27+
num_test_upper_bound= either None or number a maximum number of test-cases to be performed in each testing round
28+
2729
"""
2830
super().__init__(alphabet,sul)
2931
assertk>1andmethodin ['combinations','permutations']
@@ -32,39 +34,24 @@ def __init__(self, alphabet: list, sul: SUL, k=2, random_walk_len=20, method='pe
3234
self.fun=combinationsifmethod=='combinations'elsepermutations
3335
self.random_walk_len=random_walk_len
3436

35-
deffind_cex(self,hypothesis):
36-
37-
iflen(hypothesis.states)==1:
38-
for_inrange(self.random_walk_len):
39-
path=choices(self.alphabet,k=self.random_walk_len)
40-
hypothesis.reset_to_initial()
41-
self.sul.post()
42-
self.sul.pre()
43-
fori,pinenumerate(path):
44-
out_sul=self.sul.step(p)
45-
out_hyp=hypothesis.step(p)
46-
self.num_steps+=1
37+
self.num_test_lower_bound=num_test_lower_bound
38+
self.num_test_upper_bound=num_test_upper_bound
4739

48-
ifout_sul!=out_hyp:
49-
self.sul.post()
50-
returnpath[:i+1]
40+
deffind_cex(self,hypothesis):
5141

52-
states=hypothesis.states
53-
shuffle(states)
42+
shuffle(hypothesis.states)
5443

44+
test_cases= []
5545
forcombinself.fun(hypothesis.states,self.k):
5646
prefixes=frozenset([c.prefixforcincomb])
5747
ifprefixesinself.cache:
5848
continue
59-
else:
60-
self.cache.add(prefixes)
49+
self.cache.add(prefixes)
6150

6251
index=0
6352
path=comb[0].prefix
64-
65-
# in case of non-strongly connected automata test case might not be possible as a path between 2 states
66-
# might not exist
6753
possible_test_case=True
54+
6855
whileindex<len(comb)-1:
6956
path_between_states=hypothesis.get_shortest_path(comb[index],comb[index+1])
7057
index+=1
@@ -79,9 +66,23 @@ def find_cex(self, hypothesis):
7966
continue
8067

8168
path+=tuple(choices(self.alphabet,k=self.random_walk_len))
69+
test_cases.append(path)
8270

83-
self.reset_hyp_and_sul(hypothesis)
71+
# lower bound (also accounts for single state hypothesis when a lower bound is not defined)
72+
lower_bound=self.num_test_lower_bound
73+
iflen(hypothesis.states)==1andlower_boundisNone:
74+
lower_bound=50
8475

76+
whilelower_boundisnotNoneandlen(test_cases)<lower_bound:
77+
path=tuple(choices(self.alphabet,k=self.random_walk_len))
78+
test_cases.append(path)
79+
80+
# upper bound
81+
ifself.num_test_upper_boundisnotNone:
82+
test_cases=test_cases[:self.num_test_upper_bound]
83+
84+
forpathintest_cases:
85+
self.reset_hyp_and_sul(hypothesis)
8586
fori,pinenumerate(path):
8687
out_sul=self.sul.step(p)
8788
out_hyp=hypothesis.step(p)

‎aalpy/oracles/KWayTransitionCoverageEqOracle.py‎

Lines changed: 45 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,10 @@ def __init__(self, alphabet: list, sul: SUL, k: int = 2, method='random',
2020
max_path_len:int=50,
2121
max_number_of_steps:int=0,
2222
optimize:str='steps',
23-
random_walk_len=10):
23+
random_walk_len=10,
24+
num_test_lower_bound=None,
25+
num_test_upper_bound=None,
26+
):
2427
"""
2528
Args:
2629
@@ -33,6 +36,8 @@ def __init__(self, alphabet: list, sul: SUL, k: int = 2, method='random',
3336
max_number_of_steps: maximum number of steps that will be executed on the SUL (0 = no limit)
3437
optimize: minimize either the number of 'steps' or 'queries' that are executed
3538
random_walk_len: the number of steps that are added by 'prefix' generated paths
39+
num_test_lower_bound= either None or number a minimum number of test-cases to be performed in each testing round
40+
num_test_upper_bound= either None or number a maximum number of test-cases to be performed in each testing round
3641
3742
"""
3843
super().__init__(alphabet,sul)
@@ -48,26 +53,62 @@ def __init__(self, alphabet: list, sul: SUL, k: int = 2, method='random',
4853
self.optimize=optimize
4954
self.random_walk_len=random_walk_len
5055

56+
# to account for cases where number of test-cases generated by the oracle is either too big or too small
57+
# num_test_lower_bound does not affect k-way transition coverage, but limiting the upper bound might as not all
58+
# tests will be executed
59+
self.num_test_lower_bound=num_test_lower_bound
60+
self.num_test_upper_bound=num_test_upper_bound
61+
5162
self.cached_paths=list()
5263

5364
deffind_cex(self,hypothesis:Automaton):
5465
ifself.method=='random':
5566
paths=self.generate_random_paths(hypothesis)+self.cached_paths
5667
self.cached_paths=self.greedy_set_cover(hypothesis,paths)
5768

58-
print('Num TC',len(self.cached_paths))
59-
forpathinself.cached_paths:
69+
# to account for lower bound
70+
additional_test_cases= []
71+
num_executed_tcs=0
72+
ifself.num_test_lower_boundisnotNone:
73+
whilelen(self.cached_paths)+len(additional_test_cases)<self.num_test_lower_bound:
74+
random_length=randint(self.k,self.max_path_len)
75+
steps=tuple(choices(self.alphabet,k=random_length))
76+
additional_test_cases.append(self.create_path(hypothesis,steps))
77+
78+
forpathinlist(self.cached_paths+additional_test_cases):
79+
ifself.num_test_upper_boundisnotNoneandnum_executed_tcs>=self.num_test_upper_bound:
80+
break
81+
6082
counter_example=self.check_path(hypothesis,path.steps)
83+
num_executed_tcs+=1
6184

6285
ifcounter_exampleisnotNone:
6386
returncounter_example
6487

6588
elifself.method=='prefix':
89+
generated_paths= []
90+
# generate tcs with prefix coverage
6691
forstepsinself.generate_prefix_steps(hypothesis):
67-
counter_example=self.check_path(hypothesis,steps)
92+
generated_paths.append(self.create_path(hypothesis,steps))
93+
94+
ifself.num_test_lower_boundisnotNoneandlen(generated_paths)>=self.num_test_lower_bound:
95+
break
6896

97+
# add random paths if needed
98+
whileself.num_test_lower_boundisnotNoneandlen(generated_paths)<self.num_test_lower_bound:
99+
random_length=randint(self.k,self.max_path_len)
100+
steps=tuple(choices(self.alphabet,k=random_length))
101+
generated_paths.append(self.create_path(hypothesis,steps))
102+
103+
# limit upper bound
104+
ifself.num_test_upper_boundisnotNone:
105+
generated_paths=generated_paths[:self.num_test_upper_bound]
106+
107+
forpathingenerated_paths:
108+
counter_example=self.check_path(hypothesis,path.steps)
69109
ifcounter_exampleisnotNone:
70110
returncounter_example
111+
71112
returnNone
72113

73114
defgreedy_set_cover(self,hypothesis:Automaton,paths:list):
@@ -90,7 +131,6 @@ def greedy_set_cover(self, hypothesis: Automaton, paths: list):
90131
paths= [self.create_path(hypothesis,steps)forstepsinself.generate_prefix_steps(hypothesis)]
91132

92133
ifself.max_number_of_steps!=0andstep_count>self.max_number_of_steps:
93-
print("stop")
94134
break
95135

96136
returnresult

0 commit comments

Comments
 (0)

[8]ページ先頭

©2009-2025 Movatter.jp