Class: Bparity::Formal::ExhaustiveRunner

Inherits:
Object
  • Object
show all
Defined in:
lib/bparity/formal/bounded.rb

Constant Summary collapse

DEFAULT_MAX_CASES = 
100_000
DEFAULT_TIMEBOX = 
300

Instance Method Summary collapse

Constructor Details

#initialize(new_callable:, domains:, size:, depth:, assumptions:, old_callable: nil, contracts: [], preconditions: [], max_cases: DEFAULT_MAX_CASES, timebox: DEFAULT_TIMEBOX, comparator: Verification::Comparator.new(mode: :strict), new_error_mapper: nil) ⇒ ExhaustiveRunner

Returns a new instance of ExhaustiveRunner.

Raises:



207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
 
# File 'lib/bparity/formal/bounded.rb', line 207

def initialize(new_callable:, domains:, size:, depth:, assumptions:, old_callable: nil,
               contracts: [], preconditions: [], max_cases: DEFAULT_MAX_CASES,
               timebox: DEFAULT_TIMEBOX, comparator: Verification::Comparator.new(mode: :strict),
               new_error_mapper: nil)
  @old_callable = old_callable
  @new_callable = new_callable
  @domains = domains
  @size = size
  @depth = depth
  @assumptions = assumptions
  @max_cases = max_cases
  @timebox = timebox
  @comparator = comparator
  @new_error_mapper = new_error_mapper
  @contracts = contracts
  @preconditions = preconditions
  @checker = ContractChecker.new
  return unless @old_callable.nil? && @contracts.empty?

  raise ConfigurationError,
        "F2 needs a runnable legacy implementation or declared postconditions/invariants."
end

Instance Method Details

#run ⇒ Object 



230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
 
# File 'lib/bparity/formal/bounded.rb', line 230

def run
  started = Process.clock_gettime(Process::CLOCK_MONOTONIC)
  count = 0
  visited = filtered = 0
  counterexample = nil
  fallback = @domains.any? { |domain| domain.respond_to?(:truncated) && domain.truncated } ||
             total_cases > @max_cases
  inputs = fallback ? pairwise_inputs : exhaustive_inputs
  timed_out = false
  inputs.first(@max_cases).each do |input|
    if Process.clock_gettime(Process::CLOCK_MONOTONIC) - started >= @timebox
      timed_out = true
      break
    end
    visited += 1
    unless admissible?(input)
      filtered += 1
      next
    end
    count += 1
    counterexample = compare(input)
    break if counterexample
  end
  complete = !fallback && !timed_out && visited == total_cases && count.positive?
  result(count, complete, counterexample, fallback ? count : 0, filtered)
end