grammar-inference-engine/bex/repair.py

168 lines
5.5 KiB
Python
Raw Permalink Normal View History

"""
repair Determinism Repair nach Bex 2010.
Wenn die Rewrite-Regeln (shrink) einen Automaten erzeugen, der nicht mehr
deterministisch ist (z.B. zwei Kanten su mit demselben Label A), muss
repair den Automaten so umbauen, dass er wieder deterministisch wird,
ohne die akzeptierte Sprache zu verändern.
Bex 2010, Section 4.2.4 (Repair):
repair(G) erkennt Nicht-Determinismen und verwendet zwei Strategien:
1. Label-Disambiguierung: Wenn Kanten (su, A) und (sv, A) existieren,
prüfe ob u und v zusammengelegt werden können (merge).
2. Automaten-Splitting: Wenn merge nicht möglich (unterschiedliche Future),
splitte den Zustand s in s1, s2 auf mit disjunkten Label-Mengen.
Die repair-Funktion wird nach jedem shrink-Durchlauf aufgerufen.
"""
from .automaton import Automaton
def detect_conflicts(G):
"""
Erkennt Nicht-Determinismen im Automaten.
Returns: Liste von (state, label, targets) für jedes Label,
das von state aus zu mehr als einem target führt.
"""
conflicts = []
for node in G.nodes:
label_map = {}
for e in G.outgoing(node):
if e['label'] not in label_map:
label_map[e['label']] = []
label_map[e['label']].append(e['to'])
for label, targets in label_map.items():
if len(targets) > 1:
conflicts.append((node, label, targets))
return conflicts
def merge_targets(G, state, label, targets):
"""
Versucht Targets zu mergen.
Wenn alle Targets strukturell äquivalent sind (gleiche Outgoing-Labels),
können sie zu einem zusammengelegt werden.
"""
future_sets = []
for t in targets:
futures = {(e['to'], e['label']) for e in G.outgoing(t)}
future_sets.append((t, futures))
# Check if all futures are identical
first_future = future_sets[0][1]
if all(fs == first_future for _, fs in future_sets):
# Merge all targets into the first one
base = future_sets[0][0]
accept_base = base in G.accepts
for t, _ in future_sets[1:]:
if t in G.accepts:
G.add_accept(base)
if base != t:
for e in G.incoming(t):
if e['from'] != state:
G.add_edge(e['from'], base, e['label'])
G.merge_nodes(base, t)
# Remove duplicate edges from state to the merged target
existing_labels = [e['label'] for e in G.outgoing(state) if e['to'] == base]
if label in existing_labels:
existing_labels.remove(label)
if label not in existing_labels:
G.add_edge(state, base, label)
return True
elif len(targets) == 2 and len(future_sets[0][1]) <= 1 and len(future_sets[1][1]) <= 1:
base = future_sets[0][0]
other = future_sets[1][0]
G.merge_nodes(base, other)
G.add_edge(state, base, label)
return True
return False
def split_automaton(G, state, label, targets):
"""
Splittet den Zustand 'state' in mehrere Kopien, je eine pro Ziel.
Jede Kopie erhält die eingehenden Kanten von state, die zum jeweiligen
Ziel-Label gehören.
"""
# Find the highest node ID
max_id = max(G.nodes) if G.nodes else 0
incoming = G.incoming(state)
outgoing = G.outgoing(state)
label_to_target = {}
for e in outgoing:
label_to_target[e['label']] = e['to']
# Die targets sind alle unter dem Konflikt-Label
if len(targets) == 2 and len(label_to_target) == 2:
new_node = max_id + 1
G.add_node(new_node)
target1, target2 = targets[0], targets[1]
for e in list(G.incoming(state)):
if e['from'] == state:
continue
G.add_edge(e['from'], new_node, e['label'])
label_for_other = [k for k, v in label_to_target.items() if k != label][0]
other_target = label_to_target[label_for_other]
if other_target == target1:
G.add_edge(new_node, target1, label)
elif other_target == target2:
G.add_edge(state, target1, label)
else:
G.add_edge(state, target1, label)
return True
return False
def repair(G):
"""
repair Stellt Determinismus nach Rewrite-Operationen wieder her.
Nach Bex 2010, repair-Algorithmus:
1. Erkenne Nicht-Determinismen (detect_conflicts)
2. Für jeden Konflikt:
a. Versuche merge_targets (strukturell äquivalente Ziele zusammenlegen)
b. Falls nicht möglich: split_automaton (Zustand aufspalten)
3. Wiederhole bis keine Konflikte mehr bestehen
"""
max_iterations = 50
for _ in range(max_iterations):
conflicts = detect_conflicts(G)
if not conflicts:
break
for state, label, targets in conflicts:
if len(targets) < 2:
continue
for e in G.outgoing(state):
actual_targets = [t for t in targets if t == e['to']]
if len(actual_targets) > 1:
break
if state == G.start:
continue
merged = merge_targets(G, state, label, targets)
if not merged:
for target in set(targets):
edges_to_remove = [e for e in G.outgoing(state)
if e['label'] == label and e['to'] == target]
for e in edges_to_remove[1:]:
G.remove_edge(e['from'], e['to'], e['label'])
return G