Skip to content

Commit 5f0e708

Browse files
author
Edi Muškardin
authored
Merge pull request #79 from DES-Lab/gsm-dev
Resolve Minor GSM issues
2 parents b55f445 + fc31caf commit 5f0e708

File tree

8 files changed

+317
-114
lines changed

8 files changed

+317
-114
lines changed

DotModels/car_alarm.dot

Lines changed: 12 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -5,22 +5,18 @@ q3_locked_closed [label="A"];
55
q5_unlocked_closed [label="N"];
66
q6_unlocked_open [label="N"];
77
q7_locked_open [label="N"];
8-
q4_faulty [label="N"];
9-
q1_locked_closed -> q2_locked_open [label="d:1"];
10-
q1_locked_closed -> q5_unlocked_closed [label="l:1"];
11-
q2_locked_open -> q3_locked_closed [label="d:1"];
12-
q2_locked_open -> q6_unlocked_open [label="l:1"];
13-
q3_locked_closed -> q2_locked_open [label="d:1"];
14-
q3_locked_closed -> q5_unlocked_closed [label="l:1"];
15-
q5_unlocked_closed -> q6_unlocked_open [label="d:1"];
16-
q5_unlocked_closed -> q1_locked_closed [label="l:1"];
17-
q6_unlocked_open -> q5_unlocked_closed [label="d:1"];
18-
q6_unlocked_open -> q7_locked_open [label="l:1"];
19-
q7_locked_open -> q4_faulty [label="d:1"];
20-
q7_locked_open -> q6_unlocked_open [label="l:1"];
21-
q4_faulty -> q2_locked_open [label="d:0.9"];
22-
q4_faulty -> q7_locked_open [label="d:0.1"];
23-
q4_faulty -> q5_unlocked_closed [label="l:1"];
8+
q1_locked_closed -> q2_locked_open [label="d"];
9+
q1_locked_closed -> q5_unlocked_closed [label="l"];
10+
q2_locked_open -> q3_locked_closed [label="d"];
11+
q2_locked_open -> q6_unlocked_open [label="l"];
12+
q3_locked_closed -> q2_locked_open [label="d"];
13+
q3_locked_closed -> q5_unlocked_closed [label="l"];
14+
q5_unlocked_closed -> q6_unlocked_open [label="d"];
15+
q5_unlocked_closed -> q1_locked_closed [label="l"];
16+
q6_unlocked_open -> q5_unlocked_closed [label="d"];
17+
q6_unlocked_open -> q7_locked_open [label="l"];
18+
q7_locked_open -> q1_locked_closed [label="d"];
19+
q7_locked_open -> q6_unlocked_open [label="l"];
2420
__start0 [label="", shape=none];
2521
__start0 -> q1_locked_closed [label=""];
2622
}

aalpy/learning_algs/__init__.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,5 @@
1010
from .stochastic_passive.ActiveAleriga import run_active_Alergia
1111
from .deterministic_passive.RPNI import run_RPNI, run_PAPNI
1212
from .deterministic_passive.active_RPNI import run_active_RPNI
13-
from .general_passive.GeneralizedStateMerging import run_GSM
13+
from .general_passive.GeneralizedStateMerging import run_GSM
14+
from .general_passive.GsmAlgorithms import run_EDSM

aalpy/learning_algs/general_passive/GeneralizedStateMerging.py

Lines changed: 49 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
import functools
2-
from bisect import insort
3-
from typing import Dict, Tuple, Callable, List, Optional
42
from collections import deque
3+
from typing import Dict, Tuple, Callable, List, Optional
54

65
from aalpy.learning_algs.general_passive.Node import Node, OutputBehavior, TransitionBehavior, TransitionInfo, \
7-
OutputBehaviorRange, TransitionBehaviorRange, intersection_iterator
6+
OutputBehaviorRange, TransitionBehaviorRange, intersection_iterator, NodeOrders, unknown_output, detect_data_format
87
from aalpy.learning_algs.general_passive.ScoreFunctionsGSM import ScoreCalculation, hoeffding_compatibility
98

109

@@ -54,10 +53,10 @@ def __init__(self, *,
5453
depth_first=False):
5554

5655
if output_behavior not in OutputBehaviorRange:
57-
raise ValueError(f"invalid output behavior {output_behavior}")
56+
raise ValueError(f"invalid output behavior {output_behavior}. should be in {OutputBehaviorRange}")
5857
self.output_behavior: OutputBehavior = output_behavior
5958
if transition_behavior not in TransitionBehaviorRange:
60-
raise ValueError(f"invalid transition behavior {transition_behavior}")
59+
raise ValueError(f"invalid transition behavior {transition_behavior}. should be in {TransitionBehaviorRange}")
6160
self.transition_behavior: TransitionBehavior = transition_behavior
6261

6362
if score_calc is None:
@@ -70,8 +69,11 @@ def __init__(self, *,
7069
self.score_calc: ScoreCalculation = score_calc
7170

7271
if node_order is None:
73-
node_order = Node.__lt__
74-
self.node_order = functools.cmp_to_key(lambda a, b: -1 if node_order(a, b) else 1)
72+
node_order = NodeOrders.Default
73+
if node_order is NodeOrders.NoCompare or node_order is NodeOrders.Default:
74+
self.node_order = node_order
75+
else:
76+
self.node_order = functools.cmp_to_key(lambda a, b: -1 if node_order(a, b) else 1)
7577

7678
self.pta_preprocessing = pta_preprocessing or (lambda x: x)
7779
self.postprocessing = postprocessing or (lambda x: x)
@@ -91,15 +93,16 @@ def compute_local_compatibility(self, a: Node, b: Node):
9193

9294
# TODO: make more generic by adding the option to use a different algorithm than red blue
9395
# for selecting potential merge candidates. Maybe using inheritance with abstract `run`.
94-
def run(self, data, convert=True, instrumentation: Instrumentation = None):
96+
def run(self, data, convert=True, instrumentation: Instrumentation=None, data_format=None):
9597
if instrumentation is None:
9698
instrumentation = Instrumentation()
9799
instrumentation.reset(self)
98100

99-
if isinstance(data, Node):
100-
root = data
101-
else:
102-
root = Node.createPTA(data, self.output_behavior)
101+
if data_format is None:
102+
data_format = detect_data_format(data)
103+
if data_format == "examples" and self.transition_behavior != "deterministic":
104+
raise ValueError("learning from examples is not possible for nondeterministic systems")
105+
root = Node.createPTA(data, self.output_behavior, data_format)
103106

104107
root = self.pta_preprocessing(root)
105108
instrumentation.pta_construction_done(root)
@@ -128,7 +131,11 @@ def run(self, data, convert=True, instrumentation: Instrumentation = None):
128131
# no blue states left -> done
129132
if len(blue_states) == 0:
130133
break
131-
blue_states.sort(key=self.node_order)
134+
if self.node_order is not NodeOrders.NoCompare:
135+
blue_states.sort(key=self.node_order)
136+
# red states are always sorted using default order on original prefix
137+
if self.node_order is not NodeOrders.Default:
138+
red_states.sort(key=self.node_order)
132139

133140
# loop over blue states
134141
promotion = False
@@ -139,7 +146,6 @@ def run(self, data, convert=True, instrumentation: Instrumentation = None):
139146
# calculate partitions resulting from merges with red states if necessary
140147
current_candidates: Dict[Node, Partitioning] = dict()
141148
perfect_partitioning = None
142-
143149
red_state = None
144150
for red_state in red_states:
145151
partition = partition_candidates.get((red_state, blue_state))
@@ -149,16 +155,16 @@ def run(self, data, convert=True, instrumentation: Instrumentation = None):
149155
perfect_partitioning = partition
150156
break
151157
current_candidates[red_state] = partition
152-
153158
assert red_state is not None
159+
154160
# partition with perfect score found: don't consider anything else
155161
if perfect_partitioning:
156162
partition_candidates = {(red_state, blue_state): perfect_partitioning}
157163
break
158164

159165
# no merge candidates for this blue state -> promote
160166
if all(part.score is False for part in current_candidates.values()):
161-
insort(red_states, blue_state, key=self.node_order)
167+
red_states.append(blue_state)
162168
instrumentation.log_promote(blue_state)
163169
promotion = True
164170
break
@@ -176,10 +182,11 @@ def run(self, data, convert=True, instrumentation: Instrumentation = None):
176182
best_candidate = max(partition_candidates.values(), key=lambda part: part.score)
177183
for real_node, partition_node in best_candidate.red_mapping.items():
178184
real_node.transitions = partition_node.transitions
185+
real_node.prefix_access_pair = partition_node.prefix_access_pair
179186
for access_pair, t_info in real_node.transition_iterator():
180187
if t_info.target not in red_states:
181188
t_info.target.predecessor = real_node
182-
t_info.target.prefix_access_pair = access_pair # not sure whether this is actually required
189+
# t_info.target.prefix_access_pair = access_pair # not sure whether this is actually required
183190
instrumentation.log_merge(best_candidate)
184191
# FUTURE: optimizations for compatibility tests where merges can be orthogonal
185192
# FUTURE: caching for aggregating compatibility tests
@@ -247,9 +254,13 @@ def update_partition(red_node: Node, blue_node: Optional[Node]) -> Node:
247254
blue_in_sym, blue_out_sym = blue.prefix_access_pair
248255
blue_parent.transitions[blue_in_sym][blue_out_sym].target = red
249256

257+
partition = update_partition(red, None)
258+
if self.output_behavior == "moore":
259+
partition.resolve_unknown_prefix_output(blue_out_sym)
260+
261+
# loop over implied merges
250262
q: deque[Tuple[Node, Node]] = deque([(red, blue)])
251263
pop = q.pop if self.depth_first else q.popleft
252-
253264
while len(q) != 0:
254265
red, blue = pop()
255266
partition = update_partition(red, blue)
@@ -258,10 +269,25 @@ def update_partition(red_node: Node, blue_node: Optional[Node]) -> Node:
258269
if self.compute_local_compatibility(partition, blue) is False:
259270
return partitioning
260271

272+
# create implied merges for all common successors
261273
for in_sym, blue_transitions in blue.transitions.items():
262274
partition_transitions = partition.get_or_create_transitions(in_sym)
263275
for out_sym, blue_transition in blue_transitions.items():
264276
partition_transition = partition_transitions.get(out_sym)
277+
# handle unknown output
278+
if partition_transition is None:
279+
if out_sym is unknown_output and len(partition_transitions) != 0:
280+
assert len(partition_transitions) == 1
281+
partition_transition = list(partition_transitions.values())[0]
282+
if unknown_output in partition_transitions:
283+
assert len(partition_transitions) == 1
284+
partition_transition = partition_transitions.pop(unknown_output)
285+
partition_transitions[out_sym] = partition_transition
286+
# re-hook access pair
287+
succ_part = update_partition(partition_transition.target, None)
288+
if self.output_behavior == "moore" or succ_part.predecessor is red:
289+
succ_part.resolve_unknown_prefix_output(out_sym)
290+
# add pairs
265291
if partition_transition is not None:
266292
q.append((partition_transition.target, blue_transition.target))
267293
partition_transition.count += blue_transition.count
@@ -287,6 +313,7 @@ def run_GSM(data, *,
287313
depth_first=False,
288314
instrumentation=None,
289315
convert=True,
316+
data_format=None,
290317
):
291318
"""
292319
TODO
@@ -318,12 +345,14 @@ def run_GSM(data, *,
318345
319346
convert:
320347
348+
data_format:
349+
321350
322351
Returns:
323352
324353
325354
"""
326-
# instantiate the gsm
355+
# instantiate gsm
327356
gsm = GeneralizedStateMerging(
328357
output_behavior=output_behavior,
329358
transition_behavior=transition_behavior,
@@ -338,4 +367,4 @@ def run_GSM(data, *,
338367
)
339368

340369
# run the algorithm
341-
return gsm.run(data=data, instrumentation=instrumentation, convert=convert)
370+
return gsm.run(data=data, instrumentation=instrumentation, convert=convert, data_format=data_format)
Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
from typing import Dict, Union
2+
3+
from aalpy import DeterministicAutomaton
4+
from aalpy.learning_algs.general_passive.GeneralizedStateMerging import run_GSM
5+
from aalpy.learning_algs.general_passive.Instrumentation import ProgressReport
6+
from aalpy.learning_algs.general_passive.Node import Node
7+
from aalpy.learning_algs.general_passive.ScoreFunctionsGSM import ScoreCalculation
8+
from aalpy.utils.HelperFunctions import dfa_from_moore
9+
10+
11+
def run_EDSM(data, automaton_type, input_completeness=None, print_info=True) -> Union[DeterministicAutomaton, None]:
12+
"""
13+
Run Evidence Driven State Merging.
14+
15+
Args:
16+
data: sequence of input sequences and corresponding label. Eg. [[(i1,i2,i3, ...), label], ...]
17+
automaton_type: either 'dfa', 'mealy', 'moore'. Note that for 'mealy' machine learning, data has to be prefix-closed.
18+
input_completeness: either None, 'sink_state', or 'self_loop'. If None, learned model could be input incomplete,
19+
sink_state will lead all undefined inputs form some state to the sink state, whereas self_loop will simply create
20+
a self loop. In case of Mealy learning output of the added transition will be 'epsilon'.
21+
print_info: print learning progress and runtime information
22+
23+
Returns:
24+
25+
Model conforming to the data, or None if data is non-deterministic.
26+
27+
"""
28+
assert automaton_type in {'dfa', 'mealy', 'moore'}
29+
assert input_completeness in {None, 'self_loop', 'sink_state'}
30+
31+
def EDSM_score(part: Dict[Node, Node]):
32+
nr_partitions = len(set(part.values()))
33+
nr_merged = len(part)
34+
return nr_merged - nr_partitions
35+
36+
score = ScoreCalculation(score_function=EDSM_score)
37+
38+
internal_automaton_type = 'moore' if automaton_type != 'mealy' else automaton_type
39+
40+
learned_model = run_GSM(data, output_behavior=internal_automaton_type,
41+
transition_behavior="deterministic",
42+
score_calc=score, instrumentation=ProgressReport(2))
43+
44+
if automaton_type == 'dfa':
45+
learned_model = dfa_from_moore(learned_model)
46+
47+
if not learned_model.is_input_complete():
48+
if not input_completeness:
49+
if print_info:
50+
print('Warning: Learned Model is not input complete (inputs not defined for all states). '
51+
'Consider calling .make_input_complete()')
52+
else:
53+
if print_info:
54+
print(f'Learned model was not input complete. Adapting it with {input_completeness} transitions.')
55+
learned_model.make_input_complete(input_completeness)
56+
57+
return learned_model

aalpy/learning_algs/general_passive/Instrumentation.py

Lines changed: 2 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
import time
2-
from functools import wraps
32
from typing import Dict, Optional
43

54
from aalpy.learning_algs.general_passive.GeneralizedStateMerging import Instrumentation, Partitioning, \
@@ -8,19 +7,6 @@
87

98

109
class ProgressReport(Instrumentation):
11-
@staticmethod
12-
def min_lvl(lvl):
13-
def decorator(fn):
14-
@wraps(fn)
15-
def wrapper(this, *args, **kw):
16-
if this.lvl < lvl:
17-
return
18-
fn(this, *args, **kw)
19-
20-
return wrapper
21-
22-
return decorator
23-
2410
def __init__(self, lvl):
2511
super().__init__()
2612
self.lvl = lvl
@@ -45,10 +31,9 @@ def reset(self, gsm: GeneralizedStateMerging):
4531

4632
self.previous_time = time.time()
4733

48-
@min_lvl(1)
4934
def pta_construction_done(self, root):
5035
print(f'PTA Construction Time: {round(time.time() - self.previous_time, 2)}')
51-
if self.lvl != 1:
36+
if 1 < self.lvl:
5237
states = root.get_all_nodes()
5338
leafs = [state for state in states if len(state.transitions.keys()) == 0]
5439
depth = [state.get_prefix_length() for state in leafs]
@@ -60,24 +45,21 @@ def pta_construction_done(self, root):
6045
def print_status(self):
6146
reset_char = "\33[2K\r"
6247
print_str = reset_char + f'Current automaton size: {self.nr_red_states}'
63-
if self.lvl != 1 and not self.gsm.compatibility_on_futures:
48+
if 1 < self.lvl and not self.gsm.compatibility_on_futures:
6449
print_str += f' Merged: {self.nr_merged_states_total} Remaining: {self.pta_size - self.nr_red_states - self.nr_merged_states_total}'
6550
print(print_str, end="")
6651

67-
@min_lvl(1)
6852
def log_promote(self, node: Node):
6953
self.log.append(["promote", (node.get_prefix(),)])
7054
self.nr_red_states += 1
7155
self.print_status()
7256

73-
@min_lvl(1)
7457
def log_merge(self, part: Partitioning):
7558
self.log.append(["merge", (part.red.get_prefix(), part.blue.get_prefix())])
7659
self.nr_merged_states_total += len(part.full_mapping) - len(part.red_mapping)
7760
self.nr_merged_states += 1
7861
self.print_status()
7962

80-
@min_lvl(1)
8163
def learning_done(self, root, red_states):
8264
print(f'\nLearning Time: {round(time.time() - self.previous_time, 2)}')
8365
print(f'Learned {len(red_states)} state automaton via {self.nr_merged_states} merges.')

0 commit comments

Comments
 (0)