Class: Lernen::Equiv::ExhaustiveSearchOracle

Inherits:
Oracle
  • Object
show all
Defined in:
lib/lernen/equiv/exhaustive_search_oracle.rb

Overview

ExhaustiveSearchOracle provides an implementation of equivalence query that finds a counterexample by using exhaustive search to ‘depth` products of input alphabet characters.

For example, with ‘alphabet = %w[0 1]` and `depth = 3`, this oracle queries the following 14 words for finding a counterexample.

“‘ruby 0, 1, 00, 01, 10, 11, 000, 001, 010, 011, 100, 101, 110, 111 “`

As the strategy, this oracle is extremingly slow and we do not recommend to use this oracle for non-testing purposes.

Instance Attribute Summary

Attributes inherited from Oracle

#sul

Instance Method Summary collapse

Methods inherited from Oracle

#+, #stats

Constructor Details

#initialize(alphabet, sul, depth: 5) ⇒ ExhaustiveSearchOracle

Returns a new instance of ExhaustiveSearchOracle.



32
33
34
35
36
37
 
# File 'lib/lernen/equiv/exhaustive_search_oracle.rb', line 32

def initialize(alphabet, sul, depth: 5)
  super(sul)

  @alphabet = alphabet
  @depth = depth
end

Instance Method Details

#find_cex(hypothesis) ⇒ Object 



40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
 
# File 'lib/lernen/equiv/exhaustive_search_oracle.rb', line 40

def find_cex(hypothesis)
  super

  @alphabet.product(*[@alphabet] * (@depth - 1)) do |word| # steep:ignore
    reset_internal(hypothesis)

    word.each_with_index do |input, n|
      hypothesis_output, sul_output = step_internal(hypothesis, input)

      if hypothesis_output != sul_output # steep:ignore
        @sul.shutdown
        return word[0..n]
      end
    end
  end

  nil
end