Skip to content

Commit

Permalink
Implement Counterexamples
Browse files Browse the repository at this point in the history
Implement Nonunifying Counterexamples.
See https://www.cs.cornell.edu/andru/papers/cupex/cupex.pdf

These examples are rendered for conflicts.

```
Shift Conflict:
0:  stmt                                                           "end of file"
    3:  expr                                         '?' stmt stmt
        6:  expr                            '+' expr
            6: expr '+' expr
                        6: expr  • '+' expr

Reduce Conflict:
0:  stmt                                                "end of file"
    3:  expr                              '?' stmt stmt
        6:  expr                 '+' expr
            6: expr '+' expr  •
```
  • Loading branch information
yui-knk committed Aug 16, 2023
1 parent 575fd0c commit 20e0b9d
Show file tree
Hide file tree
Showing 22 changed files with 1,241 additions and 22 deletions.
4 changes: 4 additions & 0 deletions doc/TODO.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,10 @@
* Reporting
* [ ] Bison style
* [ ] Wrap not selected reduce with "[]". See basic.output file generated by Bison.
* Counterexamples
* [x] Nonunifying Counterexamples
* [ ] Unifying Counterexamples
* [ ] Performance improvement using reverse_transitions and reverse_productions
* Error Tolerance
* [x] Corchuelo et al. algorithm with N = 1 (this means the next token when error is raised)
* [x] Add new decl for error token semantic value initialization (%error-token)
Expand Down
1 change: 1 addition & 0 deletions lib/lrama.rb
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
require "lrama/bitmap"
require "lrama/command"
require "lrama/context"
require "lrama/counterexamples"
require "lrama/digraph"
require "lrama/grammar"
require "lrama/lexer"
Expand Down
2 changes: 1 addition & 1 deletion lib/lrama/command.rb
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ def validate_report(report)
bison_list = %w[states itemsets lookaheads solved counterexamples cex all none]
others = %w[verbose]
list = bison_list + others
not_supported = %w[counterexamples cex none]
not_supported = %w[cex none]
h = { grammar: true }

report.each do |r|
Expand Down
285 changes: 285 additions & 0 deletions lib/lrama/counterexamples.rb
Original file line number Diff line number Diff line change
@@ -0,0 +1,285 @@
require "set"

require "lrama/counterexamples/derivation"
require "lrama/counterexamples/example"
require "lrama/counterexamples/path"
require "lrama/counterexamples/state_item"
require "lrama/counterexamples/triple"

module Lrama
# See: https://www.cs.cornell.edu/andru/papers/cupex/cupex.pdf
# 4. Constructing Nonunifying Counterexamples
class Counterexamples
attr_reader :transitions, :productions

def initialize(states)
@states = states
setup_transitions
setup_productions
end

def to_s
"#<Counterexamples>"
end
alias :inspect :to_s

def compute(conflict_state)
conflict_state.conflicts.flat_map do |conflict|
case conflict.type
when :shift_reduce
shift_reduce_example(conflict_state, conflict)
when :reduce_reduce
reduce_reduce_examples(conflict_state, conflict)
end
end.compact
end

private

def setup_transitions
# Hash [StateItem, Symbol] => StateItem
@transitions = {}
# Hash [StateItem, Symbol] => Set(StateItem)
@reverse_transitions = {}

@states.states.each do |src_state|
trans = {}

src_state.transitions.each do |shift, next_state|
trans[shift.next_sym] = next_state
end

src_state.items.each do |src_item|
next if src_item.end_of_rule?
sym = src_item.next_sym
dest_state = trans[sym]

dest_state.kernels.each do |dest_item|
next unless (src_item.rule == dest_item.rule) && (src_item.position + 1 == dest_item.position)
src_state_item = StateItem.new(src_state, src_item)
dest_state_item = StateItem.new(dest_state, dest_item)

@transitions[[src_state_item, sym]] = dest_state_item

key = [dest_state_item, sym]
@reverse_transitions[key] ||= Set.new
@reverse_transitions[key] << src_state_item
end
end
end
end

def setup_productions
# Hash [StateItem] => Set(Item)
@productions = {}
# Hash [State, Symbol] => Set(Item). Symbol is nterm
@reverse_productions = {}

@states.states.each do |state|
# LHS => Set(Item)
h = {}

state.closure.each do |item|
sym = item.lhs

h[sym] ||= Set.new
h[sym] << item
end

state.items.each do |item|
next if item.end_of_rule?
next if item.next_sym.term?

sym = item.next_sym
state_item = StateItem.new(state, item)
key = [state, sym]

@productions[state_item] = h[sym]

@reverse_productions[key] ||= Set.new
@reverse_productions[key] << item
end
end
end

def shift_reduce_example(conflict_state, conflict)
conflict_symbol = conflict.symbols.first
shift_conflict_item = conflict_state.items.find { |item| item.next_sym == conflict_symbol }
path2 = shortest_path(conflict_state, conflict.reduce.item, conflict_symbol)
path1 = find_shift_conflict_shortest_path(path2, conflict_state, shift_conflict_item)

Example.new(path1, path2, conflict, conflict_symbol, self)
end

def reduce_reduce_examples(conflict_state, conflict)
conflict_symbol = conflict.symbols.first
path1 = shortest_path(conflict_state, conflict.reduce1.item, conflict_symbol)
path2 = shortest_path(conflict_state, conflict.reduce2.item, conflict_symbol)

Example.new(path1, path2, conflict, conflict_symbol, self)
end

def find_shift_conflict_shortest_path(reduce_path, conflict_state, conflict_item)
state_items = find_shift_conflict_shortest_state_items(reduce_path, conflict_state, conflict_item)
build_paths_from_state_items(state_items)
end

def find_shift_conflict_shortest_state_items(reduce_path, conflict_state, conflict_item)
target_state_item = StateItem.new(conflict_state, conflict_item)
result = [target_state_item]
reversed_reduce_path = reduce_path.to_a.reverse
# Index for state_item
i = 0

while (path = reversed_reduce_path[i])
# Index for prev_state_item
j = i + 1
_j = j

while (prev_path = reversed_reduce_path[j])
if prev_path.production?
j += 1
else
break
end
end

state_item = path.to
prev_state_item = prev_path&.to

if target_state_item == state_item || target_state_item.item.start_item?
result.concat(reversed_reduce_path[_j..-1].map(&:to))
break
end

if target_state_item.item.beginning_of_rule?
queue = []
queue << [target_state_item]

# Find reverse production
while (sis = queue.shift)
si = sis.last

# Reach to start state
if si.item.start_item?
sis.shift
result.concat(sis)
target_state_item = si
break
end

if !si.item.beginning_of_rule?
key = [si, si.item.previous_sym]
@reverse_transitions[key].each do |prev_target_state_item|
next if prev_target_state_item.state != prev_state_item.state
sis.shift
result.concat(sis)
result << prev_target_state_item
target_state_item = prev_target_state_item
i = j
queue.clear
break
end
else
key = [si.state, si.item.lhs]
@reverse_productions[key].each do |item|
state_item = StateItem.new(si.state, item)
queue << (sis + [state_item])
end
end
end
else
# Find reverse transition
key = [target_state_item, target_state_item.item.previous_sym]
@reverse_transitions[key].each do |prev_target_state_item|
next if prev_target_state_item.state != prev_state_item.state
result << prev_target_state_item
target_state_item = prev_target_state_item
i = j
break
end
end
end

result.reverse
end

def build_paths_from_state_items(state_items)
paths = state_items.zip([nil] + state_items).map do |si, prev_si|
case
when prev_si.nil?
StartPath.new(si)
when si.item.beginning_of_rule?
ProductionPath.new(prev_si, si)
else
TransitionPath.new(prev_si, si)
end
end

paths
end

def shortest_path(conflict_state, conflict_reduce_item, conflict_term)
# queue: is an array of [Triple, [Path]]
queue = []
visited = {}
start_state = @states.states.first
raise "BUG: Start state should be just one kernel." if start_state.kernels.count != 1

start = Triple.new(start_state, start_state.kernels.first, Set.new([@states.eof_symbol]))

queue << [start, [StartPath.new(start.state_item)]]

while true
triple, paths = queue.shift

next if visited[triple]
visited[triple] = true

# Found
if triple.state == conflict_state && triple.item == conflict_reduce_item && triple.l.include?(conflict_term)
return paths
end

# transition
triple.state.transitions.each do |shift, next_state|
next unless triple.item.next_sym && triple.item.next_sym == shift.next_sym
next_state.kernels.each do |kernel|
next if kernel.rule != triple.item.rule
t = Triple.new(next_state, kernel, triple.l)
queue << [t, paths + [TransitionPath.new(triple.state_item, t.state_item)]]
end
end

# production step
triple.state.closure.each do |item|
next unless triple.item.next_sym && triple.item.next_sym == item.lhs
l = follow_l(triple.item, triple.l)
t = Triple.new(triple.state, item, l)
queue << [t, paths + [ProductionPath.new(triple.state_item, t.state_item)]]
end

break if queue.empty?
end

return nil
end

def follow_l(item, current_l)
# 1. follow_L (A -> X1 ... Xn-1 • Xn) = L
# 2. follow_L (A -> X1 ... Xk • Xk+1 Xk+2 ... Xn) = {Xk+2} if Xk+2 is a terminal
# 3. follow_L (A -> X1 ... Xk • Xk+1 Xk+2 ... Xn) = FIRST(Xk+2) if Xk+2 is a nonnullable nonterminal
# 4. follow_L (A -> X1 ... Xk • Xk+1 Xk+2 ... Xn) = FIRST(Xk+2) + follow_L (A -> X1 ... Xk+1 • Xk+2 ... Xn) if Xk+2 is a nullable nonterminal
case
when item.number_of_rest_symbols == 1
current_l
when item.next_next_sym.term?
Set.new([item.next_next_sym])
when !item.next_next_sym.nullable
item.next_next_sym.first_set
else
item.next_next_sym.first_set + follow_l(item.new_by_next_position, current_l)
end
end
end
end
63 changes: 63 additions & 0 deletions lib/lrama/counterexamples/derivation.rb
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
module Lrama
class Counterexamples
class Derivation
attr_reader :item, :left, :right
attr_writer :right

def initialize(item, left, right = nil)
@item = item
@left = left
@right = right
end

def to_s
"#<Derivation(#{item.display_name})>"
end
alias :inspect :to_s

def render_strings_for_report
result = []
_render_for_report(self, 0, result, 0)
result.map(&:rstrip)
end

def render_for_report
render_strings_for_report.join("\n")
end

private

def _render_for_report(derivation, offset, strings, index)
item = derivation.item
if strings[index]
strings[index] << " " * (offset - strings[index].length)
else
strings[index] = " " * offset
end
str = strings[index]
str << "#{item.rule_id}: #{item.symbols_before_dot.map(&:display_name).join(" ")} "

if derivation.left
len = str.length
str << "#{item.next_sym.display_name}"
length = _render_for_report(derivation.left, len, strings, index + 1)
# I want String#ljust!
str << " " * (length - str.length)
else
str << " • #{item.symbols_after_dot.map(&:display_name).join(" ")} "
return str.length
end

if derivation.right&.left
length = _render_for_report(derivation.right.left, str.length, strings, index + 1)
str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} "
str << " " * (length - str.length) if length > str.length
elsif item.next_next_sym
str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} "
end

return str.length
end
end
end
end
Loading

0 comments on commit 20e0b9d

Please sign in to comment.