Class: Ibex::Verify::ActionCorrespondence

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/verify/action_correspondence.rb

Overview

Compares resolved ACTION/GOTO behavior over all paired viable prefixes.

Defined Under Namespace

Classes: Difference, Result

Instance Method Summary collapse

Constructor Details

#initialize(canonical, target, max_pairs: nil) ⇒ ActionCorrespondence

Returns a new instance of ActionCorrespondence.



47
48
49
50
51
# File 'lib/ibex/verify/action_correspondence.rb', line 47

def initialize(canonical, target, max_pairs: nil)
  @canonical = canonical
  @target = target
  @max_pairs = max_pairs || [canonical.states.length * 8, 1].max
end

Instance Method Details

#verifyObject



54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
# File 'lib/ibex/verify/action_correspondence.rb', line 54

def verify
  queue = @canonical.entry_states.map do |name, canonical_state|
    [canonical_state, @target.entry_states[name]]
  end
  seen = {}
  differences = []
  truncated = false
  until queue.empty?
    canonical_id, target_id = queue.shift
    key = [canonical_id, target_id]
    next if seen[key]

    if seen.length >= @max_pairs
      truncated = true
      break
    end
    seen[key] = true
    canonical_state = @canonical.states[canonical_id]
    target_state = @target.states[target_id]
    unless canonical_state && target_state
      differences << Difference.new(
        kind: :state, canonical_state: canonical_id, target_state: target_id,
        symbol: nil, canonical: canonical_state, target: target_state
      )
      next
    end
    compare_terminals(canonical_id, target_id, canonical_state, target_state, differences, queue)
    compare_gotos(canonical_id, target_id, canonical_state, target_state, differences, queue)
  end
  Result.new(differences: differences.freeze, explored: seen.length, truncated: truncated)
end