Class: Ibex::Equiv

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/equiv.rb,
lib/ibex/equiv/machine.rb

Overview

Bounded language comparison over two immutable parser automata. rubocop:disable Metrics/ClassLength -- the three comparison strategies share one report and budget contract.

Defined Under Namespace

Classes: BudgetExceeded, Difference, Machine

Constant Summary collapse

CAVEAT =

@rbs! type tree_node_signature = [String, Array[String]] type tree_trace_entry = [String, Array[String], tree_node_signature?] type terminal_signature = [String, [Symbol, Integer]?] type production_signature = [String, Array[String], String?]

"Bounded search is not a proof of equivalence."
DEFAULT_MAX_ACTIONS =

: String

100_000
DEFAULT_MAX_STACK =

: Integer

10_000

Instance Method Summary collapse

Constructor Details

#initialize(left, right, sample_count: 100, seed: 0, max_tokens: 8, max_configurations: 50_000, max_actions: DEFAULT_MAX_ACTIONS, max_stack: DEFAULT_MAX_STACK, rule_map: {}) ⇒ Equiv

Returns a new instance of Equiv.

Raises:

  • (ArgumentError) 


46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
 
# File 'lib/ibex/equiv.rb', line 46

def initialize(left, right, sample_count: 100, seed: 0, max_tokens: 8, max_configurations: 50_000,
               max_actions: DEFAULT_MAX_ACTIONS, max_stack: DEFAULT_MAX_STACK, rule_map: {})
  budgets = {
    sample_count: sample_count, max_tokens: max_tokens, max_configurations: max_configurations,
    max_actions: max_actions, max_stack: max_stack
  }
  invalid = budgets.find { |_name, value| !value.positive? }
  raise ArgumentError, "#{invalid.fetch(0)} must be positive" if invalid

  @left = left
  @right = right
  @sample_count = sample_count
  @seed = seed
  @max_tokens = max_tokens
  @max_configurations = max_configurations
  @max_actions = max_actions
  @max_stack = max_stack
  @rule_map = rule_map.dup.freeze
  validate_rule_map!
  @left_machine = Machine.new(left, max_actions: max_actions, max_stack: max_stack)
  @right_machine = Machine.new(right, max_actions: max_actions, max_stack: max_stack)
end

Instance Method Details

#run ⇒ Object 



70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
 
# File 'lib/ibex/equiv.rb', line 70

def run
  verify_inputs!
  structural = structural_identity?
  tree_structural = tree_structural_identity?
  return successful_report(structural: true, samples: 0, configurations: 0) if structural && tree_structural

  samples = compare_samples
  configurations = search_product
  successful_report(structural: false, samples: samples, configurations: configurations)
rescue Machine::BudgetExceeded => e
  raise BudgetExceeded.new(
    result: "budget_exhausted", phase: "simulation", message: e.message,
    bounds: bounds, statement: CAVEAT
  )
rescue Ibex::Error => e
  raise if e.is_a?(Difference) || e.is_a?(BudgetExceeded)
  raise unless sample_budget_error?(e)

  raise BudgetExceeded.new(
    result: "budget_exhausted", phase: "sampling", message: e.message,
    bounds: bounds, statement: CAVEAT
  )
end