Class: Lernen::Equiv::Oracle

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

Overview

Oracle is an oracle for answering a equivalence query.

On running equivalence queries, this records the statistics information. We can obtain this information by ‘Oracle#stats`.

Note that this class is abstract. You should implement the following method:

  • ‘#find_cex(hypothesis)`

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(sul) ⇒ Oracle

: (System::SUL[In, Out] sul) -> void



25
26
27
28
29
30
31
32
 
# File 'lib/lernen/equiv/oracle.rb', line 25

def initialize(sul)
  @sul = sul

  @num_calls = 0
  @num_queries = 0
  @num_steps = 0
  @current_conf = nil
end

Instance Attribute Details

#sul ⇒ Object (readonly)

: System::SUL[In, Out]



34
35
36
 
# File 'lib/lernen/equiv/oracle.rb', line 34

def sul
  @sul
end

Instance Method Details

#+(other) ⇒ Object

Combines two oracles.

: (Oracle[In, Out] other) -> CombinedOracle[In, Out]



70
71
72
73
74
75
76
77
 
# File 'lib/lernen/equiv/oracle.rb', line 70

def +(other)
  oracles = []

  is_a?(CombinedOracle) ? oracles.concat(oracles) : oracles << self
  other.is_a?(CombinedOracle) ? oracles.concat(other.oracles) : oracles << other

  CombinedOracle.new(oracles)
end

#find_cex(hypothesis) ⇒ Object

Finds a conterexample against the given ‘hypothesis` automaton. If it is found, it returns the counterexample word, or it returns `nil` otherwise.

A counterexample means that it separates a sul and a hypothesis automaton on an output value, i.e., ‘hypothesis.run(cex).last != sul.query_last(cex)`. We also assume a counterexample is minimal; that is, there is no `n` (where `0 <= n < cex.size`) such that `hypothesis.run(cex)[0].last != sul.query_last(cex)`.

: [Conf] (Automaton::TransitionSystem[Conf, In, Out] hypothesis) -> (Array | nil)



47
48
49
50
 
# File 'lib/lernen/equiv/oracle.rb', line 47

def find_cex(hypothesis)
  @num_calls += 1
  nil
end

#stats ⇒ Object

Returns the statistics information as a ‘Hash` object.

The result hash contains the following values.

  • ‘num_calls`: The number of calls of `find_cex`.

  • ‘num_queries`: The number of queries.

  • ‘num_steps`: The total number of steps.

: () -> Hash[Symbol, Integer]



63
64
65
 
# File 'lib/lernen/equiv/oracle.rb', line 63

def stats
  { num_calls: @num_calls, num_queries: @num_queries, num_steps: @num_steps }
end